main.bend
bend-ml-nat-lemmas@0.1.1.0 · 255 lines · 0 definitions
1# bend-ml-nat-lemmas: Nat and List lemmas, proved, that Bend's Base does not have.
2#
3# import bend-ml-nat-lemmas@0.1.1.0/main.bend as NL
4# NL.add_comm(a, b) NL.mul_assoc(a, b, c) NL.product_append(xs, ys) ...
5#
6# Each `law` states a fact; the `def` right below it is the proof, checked by the kernel.
7# How to read a proof: it is a function whose TYPE is the statement.
8# - `match` does case analysis (the number is 0, or it is 1 + p).
9# - A call to the function itself is the induction hypothesis ("I already know
10# it holds for p, so I prove it for 1 + p").
11# - `%e : P` rewrites the goal using the equality `e`.
12# - `{==}` closes the goal when both sides already compute to the same thing.
13# A parameter carries `+` when the proof uses it more than once.
14
15import Base
16
17# Product of the elements of a list of Nat; the empty list is 1.
18# It is the "number of elements" of a tensor whose shape is the list.
19def product(xs: List<&2, Nat>) -> Nat:
20 match xs:
21 case Nil{}:
22 1n
23 case Con{h, t}:
24 Nat.mul(h, product(t))
25
26
27law add_zero:
28 for a: Nat
29 {Nat.add(a, 0n) == a : Nat}
30
31# a + 0 == a
32# Case 0: 0 + 0 computes to 0. Step: uses the hypothesis for p.
33def add_zero(a):
34 match a:
35 case 0n:
36 {==}
37 case 1n+p:
38 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
39 {==}
40
41law add_succ:
42 for a: Nat
43 for -b: Nat
44 {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}
45
46# 1 + (a + b) == a + (1 + b)
47def add_succ(a, b):
48 match a:
49 case 0n:
50 {==}
51 case 1n+p:
52 %add_succ(p, b) : {2n+Nat.add(p, b) == 1n+_ : Nat}
53 {==}
54
55law add_comm:
56 for a: Nat
57 for +b: Nat
58 {Nat.add(a, b) == Nat.add(b, a) : Nat}
59
60# a + b == b + a
61def add_comm(a, b):
62 match a:
63 case 0n:
64 %add_zero(b) : {_ == Nat.add(b, 0n) : Nat}
65 {==}
66 case 1n+p:
67 %add_succ(b, p) : {1n+Nat.add(p, b) == _ : Nat}
68 %add_comm(p, b) : {1n+Nat.add(p, b) == 1n+_ : Nat}
69 {==}
70
71law add_assoc:
72 for a: Nat
73 for -b: Nat
74 for -c: Nat
75 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
76
77# a + (b + c) == (a + b) + c
78def add_assoc(a, b, c):
79 match a:
80 case 0n:
81 {==}
82 case 1n+p:
83 %add_assoc(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
84 {==}
85
86law mul_zero:
87 for a: Nat
88 {Nat.mul(a, 0n) == 0n : Nat}
89
90# a * 0 == 0
91def mul_zero(a):
92 match a:
93 case 0n:
94 {==}
95 case 1n+p:
96 mul_zero(p)
97
98# x + (y + z) == y + (x + z): swaps the middle terms of a triple sum.
99# (Auxiliary lemma; not a published law.)
100def add_swap(x: Nat, +y: Nat, +z: Nat) -> {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}:
101 match x:
102 case 0n:
103 {==}
104 case 1n+q:
105 %add_succ(y, Nat.add(q, z)) : {1n+Nat.add(q, Nat.add(y, z)) == _ : Nat}
106 %add_swap(q, y, z) : {1n+Nat.add(q, Nat.add(y, z)) == 1n+_ : Nat}
107 {==}
108
109law mul_succ:
110 for +a: Nat
111 for +b: Nat
112 {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}
113
114# a * (1 + b) == a + a * b
115def mul_succ(a, b):
116 match a:
117 case 0n:
118 {==}
119 case 1n++p:
120 %Equal.sym(Nat, Nat.mul(p, 1n+b), Nat.add(p, Nat.mul(p, b)), mul_succ(p, b)) : {1n+Nat.add(b, _) == 1n+Nat.add(p, Nat.add(b, Nat.mul(p, b))) : Nat}
121 %add_swap(b, p, Nat.mul(p, b)) : {1n+Nat.add(b, Nat.add(p, Nat.mul(p, b))) == 1n+_ : Nat}
122 {==}
123
124law mul_comm:
125 for +a: Nat
126 for +b: Nat
127 {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
128
129# a * b == b * a
130def mul_comm(a, b):
131 match a:
132 case 0n:
133 %mul_zero(b) : {_ == Nat.mul(b, 0n) : Nat}
134 {==}
135 case 1n++p:
136 %Equal.sym(Nat, Nat.mul(b, 1n+p), Nat.add(b, Nat.mul(b, p)), mul_succ(b, p)) : {Nat.add(b, Nat.mul(p, b)) == _ : Nat}
137 %mul_comm(p, b) : {Nat.add(b, Nat.mul(p, b)) == Nat.add(b, _) : Nat}
138 {==}
139
140law mul_dist:
141 for a: Nat
142 for -b: Nat
143 for +c: Nat
144 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
145
146# a * c + b * c == (a + b) * c
147def mul_dist(a, b, c):
148 match a:
149 case 0n:
150 {==}
151 case 1n+p:
152 %mul_dist(p, b, c) : {Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)) == Nat.add(c, _) : Nat}
153 %add_assoc(c, Nat.mul(p, c), Nat.mul(b, c)) : {_ == Nat.add(c, Nat.add(Nat.mul(p, c), Nat.mul(b, c))) : Nat}
154 {==}
155
156law mul_assoc:
157 for +a: Nat
158 for +b: Nat
159 for +c: Nat
160 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
161
162# a * (b * c) == (a * b) * c
163# Step: (1+p)*(b*c) = b*c + p*(b*c). The hypothesis says p*(b*c) == (p*b)*c, and
164# distributivity says b*c + (p*b)*c == (b + p*b)*c, which is the right-hand side.
165def mul_assoc(a, b, c):
166 match a:
167 case 0n:
168 {==}
169 case 1n++p:
170 %Equal.sym(Nat, Nat.mul(p, Nat.mul(b, c)), Nat.mul(Nat.mul(p, b), c), mul_assoc(p, b, c)) : {Nat.add(Nat.mul(b, c), _) == Nat.mul(Nat.add(b, Nat.mul(p, b)), c) : Nat}
171 mul_dist(b, Nat.mul(p, b), c)
172
173law mul_one_l:
174 for +a: Nat
175 {Nat.mul(1n, a) == a : Nat}
176
177# 1 * a == a
178# 1 * a computes to a + 0, and we already proved that a + 0 == a.
179def mul_one_l(a):
180 add_zero(a)
181
182law mul_one_r:
183 for +a: Nat
184 {Nat.mul(a, 1n) == a : Nat}
185
186# a * 1 == a
187def mul_one_r(a):
188 match a:
189 case 0n:
190 {==}
191 case 1n++p:
192 %mul_one_r(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
193 {==}
194
195law append_nil:
196 for -A: Data
197 for xs: List<&2, A>
198 {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}
199
200# xs ++ [] == xs
201def append_nil(A, xs):
202 match xs:
203 case Nil{}:
204 {==}
205 case Con{h, t}:
206 %append_nil(A, t) : {Con{h, List.append(&2, A, t, Nil{})} == Con{h, _} : List<&2, A>}
207 {==}
208
209law append_assoc:
210 for -A: Data
211 for xs: List<&2, A>
212 for ys: List<&2, A>
213 for zs: List<&2, A>
214 {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}
215
216# (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
217def append_assoc(A, xs, ys, zs):
218 match xs:
219 case Nil{}:
220 {==}
221 case Con{h, t}:
222 %append_assoc(A, t, ys, zs) : {Con{h, List.append(&2, A, List.append(&2, A, t, ys), zs)} == Con{h, _} : List<&2, A>}
223 {==}
224
225law length_append:
226 for -A: Data
227 for xs: List<&2, A>
228 for ys: List<&2, A>
229 {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}
230
231# length (xs ++ ys) == length xs + length ys
232def length_append(A, xs, ys):
233 match xs:
234 case Nil{}:
235 {==}
236 case Con{h, t}:
237 %length_append(A, t, ys) : {1n+List.length(&2, A, List.append(&2, A, t, ys)) == 1n+_ : Nat}
238 {==}
239
240law product_append:
241 for +xs: List<&2, Nat>
242 for +ys: List<&2, Nat>
243 {product(List.append(&2, Nat, xs, ys)) == Nat.mul(product(xs), product(ys)) : Nat}
244
245# product (xs ++ ys) == product xs * product ys
246# Nil: product ys == 1 * product ys (by the mul_one_l law, read backwards).
247# Con: product(h :: t ++ ys) = h * product(t ++ ys); the hypothesis replaces that with
248# h * (product t * product ys), and mul_assoc closes it.
249def product_append(xs, ys):
250 match xs:
251 case Nil{}:
252 Equal.sym(Nat, Nat.mul(1n, product(ys)), product(ys), mul_one_l(product(ys)))
253 case Con{+h, +t}:
254 %Equal.sym(Nat, product(List.append(&2, Nat, t, ys)), Nat.mul(product(t), product(ys)), product_append(t, ys)) : {Nat.mul(h, _) == Nat.mul(Nat.mul(h, product(t)), product(ys)) : Nat}
255 mul_assoc(h, product(t), product(ys))