src/shape/unique_proofs.bend
bendtorch-core@0.1.0.0 · 141 lines · 15 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
4import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
5
6def pred(value: Nat) -> Nat:
7 match value:
8 case 0n:
9 0n
10 case 1n+p:
11 p
12
13def positive(value: Nat) -> Data:
14 match value:
15 case 0n:
16 Empty
17 case 1n+p:
18 Unit
19
20def succ_injective(-a: Nat, -b: Nat, equal: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
21 Equal.cong(Nat, Nat, pred, 1n+a, 1n+b, equal)
22
23def cancel_right(+a: Nat, +b: Nat, +c: Nat, equal: {Nat.add(a, c) == Nat.add(b, c) : Nat}) -> {a == b : Nat}:
24 match c:
25 case 0n:
26 Equal.trans(Nat, a, Nat.add(a, 0n), b, Equal.sym(Nat, Nat.add(a, 0n), a, Broadcast.add_zero(a)), Equal.trans(Nat, Nat.add(a, 0n), Nat.add(b, 0n), b, equal, Broadcast.add_zero(b)))
27 case 1n+p:
28 cancel_right(a, b, p, succ_injective(Nat.add(a, p), Nat.add(b, p), Equal.trans(Nat, 1n+Nat.add(a, p), Nat.add(a, 1n+p), 1n+Nat.add(b, p), Broadcast.add_succ(a, p), Equal.trans(Nat, Nat.add(a, 1n+p), Nat.add(b, 1n+p), 1n+Nat.add(b, p), equal, Equal.sym(Nat, 1n+Nat.add(b, p), Nat.add(b, 1n+p), Broadcast.add_succ(b, p))))))
29
30def absorb(+a: Nat, +c: Nat, equal: {Nat.add(a, c) == c : Nat}) -> {Nat.add(a, 0n) == 0n : Nat}:
31 match c:
32 case 0n:
33 equal
34 case 1n+p:
35 absorb(a, p, succ_injective(Nat.add(a, p), p, Equal.trans(Nat, 1n+Nat.add(a, p), Nat.add(a, 1n+p), 1n+p, Broadcast.add_succ(a, p), equal)))
36
37def succ_zero(-value: Nat, equal: {1n+value == 0n : Nat}) -> Empty:
38 %equal : positive(_)
39 Unit{}
40
41def sum_zero(+a: Nat, -b: Nat, equal: {Nat.add(a, b) == 0n : Nat}) -> {a == 0n : Nat}:
42 match a:
43 case 0n:
44 {==}
45 case 1n+p:
46 Empty.absurd({1n+p == 0n : Nat}, succ_zero(Nat.add(p, b), equal))
47
48def balance(+left_padding: Nat, +right_padding: Nat, +left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +aligned: Shape.Aligned(Shape.pad(left_padding, left), Shape.pad(right_padding, right), output)) -> {Nat.add(left_padding, List.length(&2, Nat, left)) == Nat.add(right_padding, List.length(&2, Nat, right)) : Nat}:
49 Equal.trans(Nat, Nat.add(left_padding, List.length(&2, Nat, left)), List.length(&2, Nat, Shape.pad(left_padding, left)), Nat.add(right_padding, List.length(&2, Nat, right)), Broadcast.pad_length(left_padding, left), Equal.trans(Nat, List.length(&2, Nat, Shape.pad(left_padding, left)), List.length(&2, Nat, output), Nat.add(right_padding, List.length(&2, Nat, right)), Broadcast.aligned_length_left(Shape.pad(left_padding, left), Shape.pad(right_padding, right), output, aligned), Equal.trans(Nat, List.length(&2, Nat, output), List.length(&2, Nat, Shape.pad(right_padding, right)), Nat.add(right_padding, List.length(&2, Nat, right)), Equal.sym(Nat, List.length(&2, Nat, Shape.pad(right_padding, right)), List.length(&2, Nat, output), Broadcast.aligned_length_right(Shape.pad(left_padding, left), Shape.pad(right_padding, right), output, aligned)), Equal.sym(Nat, Nat.add(right_padding, List.length(&2, Nat, right)), List.length(&2, Nat, Shape.pad(right_padding, right)), Broadcast.pad_length(right_padding, right)))))
50
51def crossed(+zero_left: Nat, +right_a: Nat, +left_b: Nat, +zero_right: Nat, +left_rank: Nat, +right_rank: Nat, +zero_a: {0n == zero_left : Nat}, zero_b: {0n == zero_right : Nat}, first: {Nat.add(zero_left, left_rank) == Nat.add(right_a, right_rank) : Nat}, second: {Nat.add(left_b, left_rank) == Nat.add(zero_right, right_rank) : Nat}) -> {zero_left == left_b : Nat}:
52 +left_rank_eq = Equal.trans(Nat, left_rank, Nat.add(zero_left, left_rank), Nat.add(right_a, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, left_rank), 0n, zero_left, zero_a), first)
53 +second_eq = Equal.trans(Nat, Nat.add(left_b, left_rank), Nat.add(zero_right, right_rank), right_rank, second, Equal.sym(Nat, right_rank, Nat.add(zero_right, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, right_rank), 0n, zero_right, zero_b)))
54 +nested = Equal.trans(Nat, Nat.add(left_b, Nat.add(right_a, right_rank)), Nat.add(left_b, left_rank), right_rank, Equal.sym(Nat, Nat.add(left_b, left_rank), Nat.add(left_b, Nat.add(right_a, right_rank)), Equal.cong(Nat, Nat, value => Nat.add(left_b, value), left_rank, Nat.add(right_a, right_rank), left_rank_eq)), second_eq)
55 +flat = Equal.trans(Nat, Nat.add(Nat.add(left_b, right_a), right_rank), Nat.add(left_b, Nat.add(right_a, right_rank)), right_rank, Equal.sym(Nat, Nat.add(left_b, Nat.add(right_a, right_rank)), Nat.add(Nat.add(left_b, right_a), right_rank), Index.add_assoc(left_b, right_a, right_rank)), nested)
56 +sum = Equal.trans(Nat, Nat.add(left_b, right_a), Nat.add(Nat.add(left_b, right_a), 0n), 0n, Equal.sym(Nat, Nat.add(Nat.add(left_b, right_a), 0n), Nat.add(left_b, right_a), Broadcast.add_zero(Nat.add(left_b, right_a))), absorb(Nat.add(left_b, right_a), right_rank, flat))
57 Equal.trans(Nat, zero_left, 0n, left_b, Equal.sym(Nat, 0n, zero_left, zero_a), Equal.sym(Nat, left_b, 0n, sum_zero(left_b, right_a, sum)))
58
59def unpadded(+left_padding: Nat, +right_padding: Nat, +left_rank: Nat, +right_rank: Nat, zero: {0n == right_padding : Nat}, balanced: {Nat.add(left_padding, left_rank) == Nat.add(right_padding, right_rank) : Nat}) -> {Nat.add(left_padding, left_rank) == right_rank : Nat}:
60 Equal.trans(Nat, Nat.add(left_padding, left_rank), Nat.add(right_padding, right_rank), right_rank, balanced, Equal.sym(Nat, right_rank, Nat.add(right_padding, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, right_rank), 0n, right_padding, zero)))
61
62def left_padding_equal(+lp1: Nat, +rp1: Nat, +lp2: Nat, +rp2: Nat, +left_rank: Nat, +right_rank: Nat, +m1: Shape.PadMinimal<lp1, rp1>, +m2: Shape.PadMinimal<lp2, rp2>, +first: {Nat.add(lp1, left_rank) == Nat.add(rp1, right_rank) : Nat}, +second: {Nat.add(lp2, left_rank) == Nat.add(rp2, right_rank) : Nat}) -> {lp1 == lp2 : Nat}:
63 match m1 m2:
64 case Shape.PLeftZero{z1} Shape.PLeftZero{z2}:
65 Equal.trans(Nat, lp1, 0n, lp2, Equal.sym(Nat, 0n, lp1, z1), z2)
66 case Shape.PRightZero{z1} Shape.PRightZero{z2}:
67 cancel_right(lp1, lp2, left_rank, Equal.trans(Nat, Nat.add(lp1, left_rank), right_rank, Nat.add(lp2, left_rank), unpadded(lp1, rp1, left_rank, right_rank, z1, first), Equal.sym(Nat, Nat.add(lp2, left_rank), right_rank, unpadded(lp2, rp2, left_rank, right_rank, z2, second))))
68 case Shape.PLeftZero{z1} Shape.PRightZero{z2}:
69 crossed(lp1, rp1, lp2, rp2, left_rank, right_rank, z1, z2, first, second)
70 case Shape.PRightZero{z1} Shape.PLeftZero{z2}:
71 Equal.sym(Nat, lp2, lp1, crossed(lp2, rp2, lp1, rp1, left_rank, right_rank, z2, z1, second, first))
72
73def axis_unique(-left: Nat, -right: Nat, -output: Nat, -other: Nat, +first: Shape.Axis<left, right, output>, +second: Shape.Axis<left, right, other>) -> {output == other : Nat}:
74 match first second:
75 case Shape.AxisEqual{l1, r1} Shape.AxisEqual{l2, r2}:
76 Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
77 case Shape.AxisEqual{l1, r1} Shape.AxisLeftOne{o2, r2}:
78 Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
79 case Shape.AxisEqual{l1, r1} Shape.AxisRightOne{l2, o2}:
80 Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
81 case Shape.AxisLeftOne{o1, r1} Shape.AxisEqual{l2, r2}:
82 Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
83 case Shape.AxisLeftOne{o1, r1} Shape.AxisLeftOne{o2, r2}:
84 Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
85 case Shape.AxisLeftOne{o1, r1} Shape.AxisRightOne{l2, o2}:
86 Equal.trans(Nat, output, 1n, other, Equal.trans(Nat, output, right, 1n, r1, Equal.sym(Nat, 1n, right, o2)), Equal.trans(Nat, 1n, left, other, o1, Equal.sym(Nat, other, left, l2)))
87 case Shape.AxisRightOne{l1, o1} Shape.AxisEqual{l2, r2}:
88 Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
89 case Shape.AxisRightOne{l1, o1} Shape.AxisLeftOne{o2, r2}:
90 Equal.trans(Nat, output, 1n, other, Equal.trans(Nat, output, left, 1n, l1, Equal.sym(Nat, 1n, left, o2)), Equal.trans(Nat, 1n, right, other, o1, Equal.sym(Nat, other, right, r2)))
91 case Shape.AxisRightOne{l1, o1} Shape.AxisRightOne{l2, o2}:
92 Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
93
94def aligned_unique(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +other: List<&2, Nat>, +first: Shape.Aligned(left, right, output), +second: Shape.Aligned(left, right, other)) -> {output == other : List<&2, Nat>}:
95 match left right output:
96 case Nil{} Nil{} Nil{}:
97 match other:
98 case Nil{}:
99 {==}
100 case oh <> ot:
101 match second:
102 case +lh <> +lt +rh <> +rt +oh <> +ot:
103 match other:
104 case Nil{}:
105 match second:
106 case +qh <> +qt:
107 Shape.AStep{+a1, +t1} = first
108 Shape.AStep{+a2, +t2} = second
109 %axis_unique(lh, rh, oh, qh, a1, a2) : {oh <> ot == _ <> qt : List<&2, Nat>}
110 %aligned_unique(lt, rt, ot, qt, t1, t2) : {oh <> ot == oh <> _ : List<&2, Nat>}
111 {==}
112 case Nil{} Nil{} oh <> ot:
113 match first:
114 case Nil{} rh <> rt Nil{}:
115 match first:
116 case lh <> lt Nil{} Nil{}:
117 match first:
118 case Nil{} rh <> rt oh <> ot:
119 match first:
120 case lh <> lt Nil{} oh <> ot:
121 match first:
122 case lh <> lt rh <> rt Nil{}:
123 match first:
124
125def retype(+lp1: Nat, +lp2: Nat, +rp1: Nat, +rp2: Nat, -left: List<&2, Nat>, -right: List<&2, Nat>, -other: List<&2, Nat>, same_left: {lp1 == lp2 : Nat}, same_right: {rp1 == rp2 : Nat}, aligned: Shape.Aligned(Shape.pad(lp2, left), Shape.pad(rp2, right), other)) -> Shape.Aligned(Shape.pad(lp1, left), Shape.pad(rp1, right), other):
126 %Equal.sym(Nat, lp1, lp2, same_left) : Shape.Aligned(Shape.pad(_, left), Shape.pad(rp1, right), other)
127 %Equal.sym(Nat, rp1, rp2, same_right) : Shape.Aligned(Shape.pad(lp2, left), Shape.pad(_, right), other)
128 aligned
129
130def broadcast_unique(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +other: List<&2, Nat>, +first: Shape.Broadcast<left, right, output>, +second: Shape.Broadcast<left, right, other>) -> {output == other : List<&2, Nat>}:
131 match first:
132 case Shape.BAlign{+lp1, +rp1, +m1, +a1}:
133 match second:
134 case Shape.BAlign{+lp2, +rp2, +m2, +a2}:
135 +left_rank = List.length(&2, Nat, left)
136 +right_rank = List.length(&2, Nat, right)
137 +e1 = balance(lp1, rp1, left, right, output, a1)
138 +e2 = balance(lp2, rp2, left, right, other, a2)
139 +same_left = left_padding_equal(lp1, rp1, lp2, rp2, left_rank, right_rank, m1, m2, e1, e2)
140 +same_right = cancel_right(rp1, rp2, right_rank, Equal.trans(Nat, Nat.add(rp1, right_rank), Nat.add(lp1, left_rank), Nat.add(rp2, right_rank), Equal.sym(Nat, Nat.add(lp1, left_rank), Nat.add(rp1, right_rank), e1), Equal.trans(Nat, Nat.add(lp1, left_rank), Nat.add(lp2, left_rank), Nat.add(rp2, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, left_rank), lp1, lp2, same_left), e2)))
141 aligned_unique(Shape.pad(lp1, left), Shape.pad(rp1, right), output, other, a1, retype(lp1, lp2, rp1, rp2, left, right, other, same_left, same_right, a2))