src/shape/nat_proofs.bend
bendtorch-core@0.1.0.0 · 160 lines · 18 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 contradiction(-value: Bool, yes: {True{} == value : Bool}, no: {False{} == value : Bool}) -> Empty:
7 Shape.clash(Equal.trans(Bool, True{}, value, False{}, yes, Equal.sym(Bool, False{}, value, no)))
8
9def le_true(+a: Nat, +b: Nat, bound: Shape.LE(a, b)) -> {True{} == Nat.is_le(a, b) : Bool}:
10 match a b:
11 case 0n 0n:
12 {==}
13 case 0n 1n+q:
14 {==}
15 case 1n+p 0n:
16 match bound:
17 case 1n+p 1n+q:
18 le_true(p, q, bound)
19
20def lt_true(+a: Nat, +b: Nat, bound: Shape.LT(a, b)) -> {True{} == Nat.is_lt(a, b) : Bool}:
21 match a b:
22 case 0n 0n:
23 match bound:
24 case 0n 1n+q:
25 {==}
26 case 1n+p 0n:
27 match bound:
28 case 1n+p 1n+q:
29 lt_true(p, q, bound)
30
31def le_add_left(+a: Nat, -x: Nat, +c: Nat, bound: Shape.LE(Nat.add(a, x), c)) -> Shape.LE(a, c):
32 match a c:
33 case 0n c:
34 Unit{}
35 case 1n+p 0n:
36 match bound:
37 case 1n+p 1n+q:
38 le_add_left(p, x, q, bound)
39
40def le_rewrite(-a: Nat, -b: Nat, -c: Nat, equal: {b == a : Nat}, bound: Shape.LE(b, c)) -> Shape.LE(a, c):
41 %equal : Shape.LE(_, c)
42 bound
43
44def add_swap(+a: Nat, +b: Nat, -c: Nat) -> {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}:
45 match a:
46 case 0n:
47 {==}
48 case 1n+p:
49 %Equal.sym(Nat, Nat.add(p, Nat.add(b, c)), Nat.add(b, Nat.add(p, c)), add_swap(p, b, c)) : {1n+_ == Nat.add(b, 1n+Nat.add(p, c)) : Nat}
50 Broadcast.add_succ(b, Nat.add(p, c))
51
52def mul_succ_right(+a: Nat, +q: Nat) -> {Nat.mul(a, 1n+q) == Nat.add(a, Nat.mul(a, q)) : Nat}:
53 match a:
54 case 0n:
55 {==}
56 case 1n+p:
57 %Equal.sym(Nat, Nat.mul(p, 1n+q), Nat.add(p, Nat.mul(p, q)), mul_succ_right(p, q)) : {1n+Nat.add(q, _) == 1n+Nat.add(p, Nat.add(q, Nat.mul(p, q))) : Nat}
58 %add_swap(q, p, Nat.mul(p, q)) : {1n+Nat.add(q, Nat.add(p, Nat.mul(p, q))) == 1n+_ : Nat}
59 {==}
60
61def mul_zero_right(+a: Nat) -> {Nat.mul(a, 0n) == 0n : Nat}:
62 match a:
63 case 0n:
64 {==}
65 case 1n+p:
66 mul_zero_right(p)
67
68def mul_one_right(+a: Nat) -> {Nat.mul(a, 1n) == a : Nat}:
69 match a:
70 case 0n:
71 {==}
72 case 1n+p:
73 Equal.cong(Nat, Nat, value => 1n+value, Nat.mul(p, 1n), p, mul_one_right(p))
74
75def mul_comm(+a: Nat, +b: Nat) -> {Nat.mul(a, b) == Nat.mul(b, a) : Nat}:
76 match a:
77 case 0n:
78 Equal.sym(Nat, Nat.mul(b, 0n), 0n, mul_zero_right(b))
79 case 1n+p:
80 %Equal.sym(Nat, Nat.mul(b, 1n+p), Nat.add(b, Nat.mul(b, p)), mul_succ_right(b, p)) : {Nat.add(b, Nat.mul(p, b)) == _ : Nat}
81 Equal.cong(Nat, Nat, value => Nat.add(b, value), Nat.mul(p, b), Nat.mul(b, p), mul_comm(p, b))
82
83def mul_add_right(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}:
84 match a:
85 case 0n:
86 {==}
87 case 1n+p:
88 %Equal.sym(Nat, Nat.mul(Nat.add(p, b), c), Nat.add(Nat.mul(p, c), Nat.mul(b, c)), mul_add_right(p, b, c)) : {Nat.add(c, _) == Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)) : Nat}
89 Index.add_assoc(c, Nat.mul(p, c), Nat.mul(b, c))
90
91def mul_assoc(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}:
92 match a:
93 case 0n:
94 {==}
95 case 1n+p:
96 %Equal.sym(Nat, Nat.mul(Nat.add(b, Nat.mul(p, b)), c), Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p, b), c)), mul_add_right(b, Nat.mul(p, b), c)) : {_ == Nat.mul(1n+p, Nat.mul(b, c)) : Nat}
97 %Equal.sym(Nat, Nat.mul(Nat.mul(p, b), c), Nat.mul(p, Nat.mul(b, c)), mul_assoc(p, b, c)) : {Nat.add(Nat.mul(b, c), _) == Nat.mul(1n+p, Nat.mul(b, c)) : Nat}
98 {==}
99
100def lt_zero(+a: Nat, bound: Shape.LT(a, 0n)) -> Empty:
101 match a:
102 case 0n:
103 match bound:
104 case 1n+p:
105 match bound:
106
107def lt_le(+a: Nat, +b: Nat, bound: Shape.LT(a, 1n+b)) -> Shape.LE(a, b):
108 match a b:
109 case 0n b:
110 Unit{}
111 case 1n+p 0n:
112 Empty.absurd(Empty, lt_zero(p, bound))
113 case 1n+p 1n+q:
114 lt_le(p, q, bound)
115
116def drain(+k: Nat, -n: Nat, -m: Nat, -d: Nat, +r: Nat) -> {Nat.divmod.go(Nat.add(k, n), Nat.add(k, m), d, r) == Nat.divmod.go(n, m, d, Nat.add(k, r)) : Nat & Nat}:
117 match k:
118 case 0n:
119 {==}
120 case 1n+j:
121 %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(j, n), Nat.add(j, m), d, 1n+r), Nat.divmod.go(n, m, d, Nat.add(j, 1n+r)), drain(j, n, m, d, 1n+r)) : {_ == Nat.divmod.go(n, m, d, 1n+Nat.add(j, r)) : Nat & Nat}
122 %Broadcast.add_succ(j, r) : {Nat.divmod.go(n, m, d, _) == Nat.divmod.go(n, m, d, 1n+Nat.add(j, r)) : Nat & Nat}
123 {==}
124
125def remainder(+r: Nat, +m: Nat, -d: Nat, +a: Nat, bound: Shape.LE(r, m)) -> {Nat.divmod.go(r, m, d, a) == (d, Nat.add(r, a)) : Nat & Nat}:
126 match r m:
127 case 0n m:
128 {==}
129 case 1n+p 0n:
130 match bound:
131 case 1n+p 1n+q:
132 %Equal.sym(Nat & Nat, Nat.divmod.go(p, q, d, 1n+a), (d, Nat.add(p, 1n+a)), remainder(p, q, d, 1n+a, bound)) : {_ == (d, 1n+Nat.add(p, a)) : Nat & Nat}
133 %Broadcast.add_succ(p, a) : {(d, _) == (d, 1n+Nat.add(p, a)) : Nat & Nat}
134 {==}
135
136def periods(+q: Nat, +b: Nat, +r: Nat, +d: Nat, bound: Shape.LE(r, b)) -> {Nat.divmod.go(Nat.add(Nat.mul(q, 1n+b), r), b, d, 0n) == (Nat.add(q, d), r) : Nat & Nat}:
137 match q:
138 case 0n:
139 %Equal.sym(Nat & Nat, Nat.divmod.go(r, b, d, 0n), (d, Nat.add(r, 0n)), remainder(r, b, d, 0n, bound)) : {_ == (d, r) : Nat & Nat}
140 %Equal.sym(Nat, Nat.add(r, 0n), r, Broadcast.add_zero(r)) : {(d, _) == (d, r) : Nat & Nat}
141 {==}
142 case 1n+p:
143 +rest = Nat.add(Nat.mul(p, 1n+b), r)
144 %Index.add_assoc(b, Nat.mul(p, 1n+b), r) : {Nat.divmod.go(1n+_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
145 %Equal.sym(Nat, 1n+Nat.add(b, rest), Nat.add(b, 1n+rest), Broadcast.add_succ(b, rest)) : {Nat.divmod.go(_, b, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
146 %Broadcast.add_zero(b) : {Nat.divmod.go(Nat.add(b, 1n+rest), _, d, 0n) == (1n+Nat.add(p, d), r) : Nat & Nat}
147 %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(b, 1n+rest), Nat.add(b, 0n), d, 0n), Nat.divmod.go(1n+rest, 0n, d, Nat.add(b, 0n)), drain(b, 1n+rest, 0n, d, 0n)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
148 %Equal.sym(Nat, Nat.add(b, 0n), b, Broadcast.add_zero(b)) : {Nat.divmod.go(1n+rest, 0n, d, _) == (1n+Nat.add(p, d), r) : Nat & Nat}
149 %Equal.sym(Nat & Nat, Nat.divmod.go(rest, b, 1n+d, 0n), (Nat.add(p, 1n+d), r), periods(p, b, r, 1n+d, bound)) : {_ == (1n+Nat.add(p, d), r) : Nat & Nat}
150 %Broadcast.add_succ(p, d) : {(_, r) == (1n+Nat.add(p, d), r) : Nat & Nat}
151 {==}
152
153def divmod_exact(+q: Nat, +b: Nat, +r: Nat, bound: Shape.LT(r, b)) -> {(q, r) == Nat.divmod(Nat.add(Nat.mul(q, b), r), b) : Nat & Nat}:
154 match b:
155 case 0n:
156 Empty.absurd({(q, r) == Nat.divmod(Nat.add(Nat.mul(q, 0n), r), 0n) : Nat & Nat}, lt_zero(r, bound))
157 case 1n+p:
158 %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(Nat.mul(q, 1n+p), r), p, 0n, 0n), (Nat.add(q, 0n), r), periods(q, p, r, 0n, lt_le(r, p, bound))) : {(q, r) == _ : Nat & Nat}
159 %Equal.sym(Nat, Nat.add(q, 0n), q, Broadcast.add_zero(q)) : {(q, r) == (_, r) : Nat & Nat}
160 {==}