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.2.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	
15	import 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.
19	def 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	
27	law 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.
33	def 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	
41	law 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)
47	def 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	
55	law 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
61	def 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	
71	law 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
78	def 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	
86	law mul_zero:
87	  for a: Nat
88	  {Nat.mul(a, 0n) == 0n : Nat}
89	
90	# a * 0 == 0
91	def 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.)
100	def 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	
109	law 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
115	def 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	
124	law 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
130	def 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	
140	law 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
147	def 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	
156	law 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.
165	def 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	
173	law add4:
174	  for +a: Nat
175	  for +b: Nat
176	  for +c: Nat
177	  for +d: Nat
178	  {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
179	
180	# (a + b) + (c + d) == (a + c) + (b + d)
181	# Regroup to a + (b + (c + d)), swap b and c in the middle (add_swap), and regroup back.
182	def add4(a, b, c, d):
183	  Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)),
184	    Equal.sym(Nat, Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(Nat.add(a, b), Nat.add(c, d)), add_assoc(a, b, Nat.add(c, d))),
185	    Equal.trans(Nat, Nat.add(a, Nat.add(b, Nat.add(c, d))), Nat.add(a, Nat.add(c, Nat.add(b, d))), Nat.add(Nat.add(a, c), Nat.add(b, d)),
186	      Equal.cong(Nat, Nat, s => Nat.add(a, s), Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), add_swap(b, c, d)),
187	      add_assoc(a, c, Nat.add(b, d))))
188	
189	law mul_dist_l:
190	  for +k: Nat
191	  for +a: Nat
192	  for +b: Nat
193	  {Nat.mul(k, Nat.add(a, b)) == Nat.add(Nat.mul(k, a), Nat.mul(k, b)) : Nat}
194	
195	# k * (a + b) == k * a + k * b
196	# Turn k * (a + b) into (a + b) * k (mul_comm), split it with mul_dist, and turn each product back around.
197	def mul_dist_l(k, a, b):
198	  Equal.trans(Nat, Nat.mul(k, Nat.add(a, b)), Nat.mul(Nat.add(a, b), k), Nat.add(Nat.mul(k, a), Nat.mul(k, b)),
199	    mul_comm(k, Nat.add(a, b)),
200	    Equal.trans(Nat, Nat.mul(Nat.add(a, b), k), Nat.add(Nat.mul(a, k), Nat.mul(b, k)), Nat.add(Nat.mul(k, a), Nat.mul(k, b)),
201	      Equal.sym(Nat, Nat.add(Nat.mul(a, k), Nat.mul(b, k)), Nat.mul(Nat.add(a, b), k), mul_dist(a, b, k)),
202	      Equal.trans(Nat, Nat.add(Nat.mul(a, k), Nat.mul(b, k)), Nat.add(Nat.mul(k, a), Nat.mul(b, k)), Nat.add(Nat.mul(k, a), Nat.mul(k, b)),
203	        Equal.cong(Nat, Nat, s => Nat.add(s, Nat.mul(b, k)), Nat.mul(a, k), Nat.mul(k, a), mul_comm(a, k)),
204	        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(k, a), s), Nat.mul(b, k), Nat.mul(k, b), mul_comm(b, k)))))
205	
206	law mul_one_l:
207	  for +a: Nat
208	  {Nat.mul(1n, a) == a : Nat}
209	
210	# 1 * a == a
211	# 1 * a computes to a + 0, and we already proved that a + 0 == a.
212	def mul_one_l(a):
213	  add_zero(a)
214	
215	law mul_one_r:
216	  for +a: Nat
217	  {Nat.mul(a, 1n) == a : Nat}
218	
219	# a * 1 == a
220	def mul_one_r(a):
221	  match a:
222	    case 0n:
223	      {==}
224	    case 1n++p:
225	      %mul_one_r(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
226	      {==}
227	
228	law append_nil:
229	  for -A: Data
230	  for  xs: List<&2, A>
231	  {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}
232	
233	# xs ++ [] == xs
234	def append_nil(A, xs):
235	  match xs:
236	    case Nil{}:
237	      {==}
238	    case Con{h, t}:
239	      %append_nil(A, t) : {Con{h, List.append(&2, A, t, Nil{})} == Con{h, _} : List<&2, A>}
240	      {==}
241	
242	law append_assoc:
243	  for -A: Data
244	  for  xs: List<&2, A>
245	  for  ys: List<&2, A>
246	  for  zs: List<&2, A>
247	  {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>}
248	
249	# (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
250	def append_assoc(A, xs, ys, zs):
251	  match xs:
252	    case Nil{}:
253	      {==}
254	    case Con{h, t}:
255	      %append_assoc(A, t, ys, zs) : {Con{h, List.append(&2, A, List.append(&2, A, t, ys), zs)} == Con{h, _} : List<&2, A>}
256	      {==}
257	
258	law length_append:
259	  for -A: Data
260	  for  xs: List<&2, A>
261	  for  ys: List<&2, A>
262	  {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}
263	
264	# length (xs ++ ys) == length xs + length ys
265	def length_append(A, xs, ys):
266	  match xs:
267	    case Nil{}:
268	      {==}
269	    case Con{h, t}:
270	      %length_append(A, t, ys) : {1n+List.length(&2, A, List.append(&2, A, t, ys)) == 1n+_ : Nat}
271	      {==}
272	
273	law product_append:
274	  for +xs: List<&2, Nat>
275	  for +ys: List<&2, Nat>
276	  {product(List.append(&2, Nat, xs, ys)) == Nat.mul(product(xs), product(ys)) : Nat}
277	
278	# product (xs ++ ys) == product xs * product ys
279	# Nil: product ys == 1 * product ys (by the mul_one_l law, read backwards).
280	# Con: product(h :: t ++ ys) = h * product(t ++ ys); the hypothesis replaces that with
281	# h * (product t * product ys), and mul_assoc closes it.
282	def product_append(xs, ys):
283	  match xs:
284	    case Nil{}:
285	      Equal.sym(Nat, Nat.mul(1n, product(ys)), product(ys), mul_one_l(product(ys)))
286	    case Con{+h, +t}:
287	      %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}
288	      mul_assoc(h, product(t), product(ys))