1	# bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.
2	import Base
3	import ./nat.bend as MNat
4	import ./bool.bend as MBool
5	import ./list.bend as MList
6	
7	# Four-way reassociation from associativity alone.
8	law op_assoc4:
9	  for ~A: Data
10	  for ~op: A -> A -> A
11	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
12	  for +a: A
13	  for +b: A
14	  for +c: A
15	  for +d: A
16	  {op(op(op(a, b), c), d) == op(a, op(b, op(c, d))) : A}
17	
18	def op_assoc4(A, op, assoc, a, b, c, d):
19	  %assoc(a, b, op(c, d)) : {op(op(op(a, b), c), d) == _ : A}
20	  assoc(op(a, b), c, d)
21	
22	# Left commutation from associativity and commutativity.
23	law op_left_comm:
24	  for ~A: Data
25	  for ~op: A -> A -> A
26	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
27	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
28	  for +a: A
29	  for +b: A
30	  for +c: A
31	  {op(a, op(b, c)) == op(b, op(a, c)) : A}
32	
33	def op_left_comm(A, op, assoc, comm, a, b, c):
34	  %assoc(a, b, c) : {_ == op(b, op(a, c)) : A}
35	  %Equal.sym(A, op(a, b), op(b, a), comm(a, b)) : {op(_, c) == op(b, op(a, c)) : A}
36	  assoc(b, a, c)
37	
38	# Right commutation from associativity and commutativity.
39	law op_right_comm:
40	  for ~A: Data
41	  for ~op: A -> A -> A
42	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
43	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
44	  for +a: A
45	  for +b: A
46	  for +c: A
47	  {op(op(a, b), c) == op(op(a, c), b) : A}
48	
49	def op_right_comm(A, op, assoc, comm, a, b, c):
50	  %Equal.sym(A, op(op(a, b), c), op(a, op(b, c)), assoc(a, b, c)) : {_ == op(op(a, c), b) : A}
51	  %Equal.sym(A, op(op(a, c), b), op(a, op(c, b)), assoc(a, c, b)) : {op(a, op(b, c)) == _ : A}
52	  %Equal.sym(A, op(c, b), op(b, c), comm(c, b)) : {op(a, op(b, c)) == op(a, _) : A}
53	  {==}
54	
55	# Middle-four interchange from associativity and commutativity.
56	law op_four:
57	  for ~A: Data
58	  for ~op: A -> A -> A
59	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
60	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
61	  for +a: A
62	  for +b: A
63	  for +c: A
64	  for +d: A
65	  {op(op(a, b), op(c, d)) == op(op(a, c), op(b, d)) : A}
66	
67	def op_four(A, op, assoc, comm, a, b, c, d):
68	  %Equal.sym(A, op(op(a, b), op(c, d)), op(a, op(b, op(c, d))), assoc(a, b, op(c, d))) : {_ == op(op(a, c), op(b, d)) : A}
69	  %Equal.sym(A, op(op(a, c), op(b, d)), op(a, op(c, op(b, d))), assoc(a, c, op(b, d))) : {op(a, op(b, op(c, d))) == _ : A}
70	  %op_left_comm(A, op, assoc, comm, b, c, d) : {op(a, op(b, op(c, d))) == op(a, _) : A}
71	  {==}
72	
73	# Three-way commutation from commutativity alone.
74	law op_comm3:
75	  for ~A: Data
76	  for ~op: A -> A -> A
77	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
78	  for +a: A
79	  for +b: A
80	  for +c: A
81	  {op(op(a, b), c) == op(c, op(b, a)) : A}
82	
83	def op_comm3(A, op, comm, a, b, c):
84	  %Equal.sym(A, op(op(a, b), c), op(c, op(a, b)), comm(op(a, b), c)) : {_ == op(c, op(b, a)) : A}
85	  %Equal.sym(A, op(b, a), op(a, b), comm(b, a)) : {op(c, op(a, b)) == op(c, _) : A}
86	  {==}
87	
88	def internal_nat_add_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}:
89	  MNat.add_assoc(x, y, z)
90	
91	def internal_nat_add_comm(x: Nat, y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
92	  MNat.add_comm(x, y)
93	
94	def internal_nat_zero_add(x: Nat) -> {Nat.add(0n, x) == x : Nat}:
95	  MNat.zero_add(x)
96	
97	def internal_nat_mul(x: Nat, y: Nat) -> Nat:
98	  Nat.mul(x, y)
99	
100	def internal_nat_mul_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}:
101	  MNat.mul_assoc(x, y, z)
102	
103	def internal_nat_mul_comm(x: Nat, y: Nat) -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}:
104	  MNat.mul_comm(x, y)
105	
106	def internal_bool_and_assoc(x: Bool, y: Bool, z: Bool) -> {Bool.and(Bool.and(x, y), z) == Bool.and(x, Bool.and(y, z)) : Bool}:
107	  MBool.and_assoc(x, y, z)
108	
109	def internal_bool_and_comm(x: Bool, y: Bool) -> {Bool.and(x, y) == Bool.and(y, x) : Bool}:
110	  MBool.and_comm(x, y)
111	
112	def internal_bool_or_assoc(x: Bool, y: Bool, z: Bool) -> {Bool.or(Bool.or(x, y), z) == Bool.or(x, Bool.or(y, z)) : Bool}:
113	  MBool.or_assoc(x, y, z)
114	
115	def internal_bool_or_comm(x: Bool, y: Bool) -> {Bool.or(x, y) == Bool.or(y, x) : Bool}:
116	  MBool.or_comm(x, y)
117	
118	def internal_list_nat_append_assoc(x: List<&2, Nat>, y: List<&2, Nat>, z: List<&2, Nat>) -> {List.append(&2, Nat, List.append(&2, Nat, x, y), z) == List.append(&2, Nat, x, List.append(&2, Nat, y, z)) : List<&2, Nat>}:
119	  MList.append_assoc(&2, Nat, x, y, z)
120	
121	# Nat addition is left-commutative (the same statement as MNat.add_left_comm).
122	law nat_add_left_comm:
123	  for +a: Nat
124	  for +b: Nat
125	  for +c: Nat
126	  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
127	
128	def nat_add_left_comm(a, b, c):
129	  op_left_comm(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c)
130	
131	# Nat addition is right-commutative (the same statement as MNat.add_right_comm).
132	law nat_add_right_comm:
133	  for +a: Nat
134	  for +b: Nat
135	  for +c: Nat
136	  {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
137	
138	def nat_add_right_comm(a, b, c):
139	  op_right_comm(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c)
140	
141	# Nat addition's middle-four interchange (the same statement as MNat.add_add_add_comm).
142	law nat_add_four:
143	  for +a: Nat
144	  for +b: Nat
145	  for +c: Nat
146	  for +d: Nat
147	  {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
148	
149	def nat_add_four(a, b, c, d):
150	  op_four(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c, d)
151	
152	# Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm).
153	law nat_mul_left_comm:
154	  for +a: Nat
155	  for +b: Nat
156	  for +c: Nat
157	  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
158	
159	def nat_mul_left_comm(a, b, c):
160	  op_left_comm(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c)
161	
162	# Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm).
163	law nat_mul_right_comm:
164	  for +a: Nat
165	  for +b: Nat
166	  for +c: Nat
167	  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
168	
169	def nat_mul_right_comm(a, b, c):
170	  op_right_comm(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c)
171	
172	# Nat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm).
173	law nat_mul_four:
174	  for +a: Nat
175	  for +b: Nat
176	  for +c: Nat
177	  for +d: Nat
178	  {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
179	
180	def nat_mul_four(a, b, c, d):
181	  op_four(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c, d)
182	
183	# Bool and is left-commutative.
184	law bool_and_left_comm:
185	  for +a: Bool
186	  for +b: Bool
187	  for +c: Bool
188	  {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}
189	
190	def bool_and_left_comm(a, b, c):
191	  op_left_comm(~Bool, ~Bool.and, ~internal_bool_and_assoc, ~internal_bool_and_comm, a, b, c)
192	
193	# Bool and is right-commutative.
194	law bool_and_right_comm:
195	  for +a: Bool
196	  for +b: Bool
197	  for +c: Bool
198	  {Bool.and(Bool.and(a, b), c) == Bool.and(Bool.and(a, c), b) : Bool}
199	
200	def bool_and_right_comm(a, b, c):
201	  op_right_comm(~Bool, ~Bool.and, ~internal_bool_and_assoc, ~internal_bool_and_comm, a, b, c)
202	
203	# Bool or is left-commutative.
204	law bool_or_left_comm:
205	  for +a: Bool
206	  for +b: Bool
207	  for +c: Bool
208	  {Bool.or(a, Bool.or(b, c)) == Bool.or(b, Bool.or(a, c)) : Bool}
209	
210	def bool_or_left_comm(a, b, c):
211	  op_left_comm(~Bool, ~Bool.or, ~internal_bool_or_assoc, ~internal_bool_or_comm, a, b, c)
212	
213	# Bool or is right-commutative.
214	law bool_or_right_comm:
215	  for +a: Bool
216	  for +b: Bool
217	  for +c: Bool
218	  {Bool.or(Bool.or(a, b), c) == Bool.or(Bool.or(a, c), b) : Bool}
219	
220	def bool_or_right_comm(a, b, c):
221	  op_right_comm(~Bool, ~Bool.or, ~internal_bool_or_assoc, ~internal_bool_or_comm, a, b, c)
222	
223	# Four-way reassociation for List append over Nat.
224	law list_nat_append_assoc4:
225	  for +a: List<&2, Nat>
226	  for +b: List<&2, Nat>
227	  for +c: List<&2, Nat>
228	  for +d: List<&2, Nat>
229	  {List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) == List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) : List<&2, Nat>}
230	
231	def list_nat_append_assoc4(a, b, c, d):
232	  op_assoc4(~List<&2, Nat>, ~List.append(&2, Nat), ~internal_list_nat_append_assoc, a, b, c, d)
233	
234	def internal_foldl_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, ~z: B, ~id: @x: B -> {op(z, x) == x : B}, +xs: List<&2, B>, +acc: B) -> {List.foldl(&2, B, B, op, xs, acc) == op(acc, List.foldr(&2, B, B, op, xs, z)) : B}:
235	  match xs:
236	    case Nil{}:
237	      Equal.sym(B, op(acc, z), acc, Equal.trans(B, op(acc, z), op(z, acc), acc, comm(acc, z), id(acc)))
238	    case +h <> +t:
239	      %Equal.sym(B, List.foldl(&2, B, B, op, t, op(acc, h)), op(op(acc, h), List.foldr(&2, B, B, op, t, z)), internal_foldl_foldr(~B, ~op, ~assoc, ~comm, ~z, ~id, t, op(acc, h))) : {_ == op(acc, op(h, List.foldr(&2, B, B, op, t, z))) : B}
240	      assoc(acc, h, List.foldr(&2, B, B, op, t, z))
241	
242	# Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity).
243	law foldl_op_eq_foldr_op:
244	  for ~B: Data
245	  for ~op: B -> B -> B
246	  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
247	  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
248	  for ~z: B
249	  for ~id: @x: B -> {op(z, x) == x : B}
250	  for +xs: List<&2, B>
251	  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}
252	
253	def foldl_op_eq_foldr_op(B, op, assoc, comm, z, id, xs):
254	  %Equal.sym(B, List.foldl(&2, B, B, op, xs, z), op(z, List.foldr(&2, B, B, op, xs, z)), internal_foldl_foldr(~B, ~op, ~assoc, ~comm, ~z, ~id, xs, z)) : {_ == List.foldr(&2, B, B, op, xs, z) : B}
255	  id(List.foldr(&2, B, B, op, xs, z))
256	
257	# A Nat call: --verdict takes a ~ constant's model from a call of its law (PLAN F38).
258	def internal_nat_foldl_op_eq_foldr_op(+xs: List<&2, Nat>) -> {List.foldl(&2, Nat, Nat, Nat.add, xs, 0n) == List.foldr(&2, Nat, Nat, Nat.add, xs, 0n) : Nat}:
259	  foldl_op_eq_foldr_op(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, ~0n, ~internal_nat_zero_add, xs)
260	
261	def internal_foldl_assoc(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, +xs: List<&2, B>, +a: B, +b: B) -> {List.foldl(&2, B, B, op, xs, op(a, b)) == op(a, List.foldl(&2, B, B, op, xs, b)) : B}:
262	  match xs:
263	    case Nil{}:
264	      {==}
265	    case +h <> +t:
266	      %Equal.sym(B, op(op(a, b), h), op(a, op(b, h)), assoc(a, b, h)) : {List.foldl(&2, B, B, op, t, _) == op(a, List.foldl(&2, B, B, op, t, op(b, h))) : B}
267	      internal_foldl_assoc(~B, ~op, ~assoc, t, a, op(b, h))
268	
269	def internal_foldl_eq_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, +z: B, +xs: List<&2, B>) -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}:
270	  match xs:
271	    case Nil{}:
272	      {==}
273	    case +h <> +t:
274	      %comm(h, z) : {List.foldl(&2, B, B, op, t, _) == op(h, List.foldr(&2, B, B, op, t, z)) : B}
275	      %Equal.sym(B, List.foldl(&2, B, B, op, t, op(h, z)), op(h, List.foldl(&2, B, B, op, t, z)), internal_foldl_assoc(~B, ~op, ~assoc, t, h, z)) : {_ == op(h, List.foldr(&2, B, B, op, t, z)) : B}
276	      %internal_foldl_eq_foldr(~B, ~op, ~assoc, ~comm, z, t) : {op(h, List.foldl(&2, B, B, op, t, z)) == op(h, _) : B}
277	      {==}
278	
279	# Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr).
280	law foldl_eq_foldr:
281	  for ~B: Data
282	  for ~op: B -> B -> B
283	  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
284	  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
285	  for +z: B
286	  for +xs: List<&2, B>
287	  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}
288	
289	def foldl_eq_foldr(B, op, assoc, comm, z, xs):
290	  internal_foldl_eq_foldr(~B, ~op, ~assoc, ~comm, z, xs)
291	
292	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
293	
294	# Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.
295	law op_assoc4_sym:
296	  for ~A: Data
297	  for ~op: A -> A -> A
298	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
299	  for +a: A
300	  for +b: A
301	  for +c: A
302	  for +d: A
303	  {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}
304	
305	def op_assoc4_sym(A, op, assoc, a, b, c, d):
306	  Equal.sym(A, op(op(op(a, b), c), d), op(a, op(b, op(c, d))), op_assoc4(~A, ~op, ~assoc, a, b, c, d))
307	
308	# Left commutation from associativity and commutativity, reversed to rewrite toward the simple side.
309	law op_left_comm_sym:
310	  for ~A: Data
311	  for ~op: A -> A -> A
312	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
313	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
314	  for +a: A
315	  for +b: A
316	  for +c: A
317	  {op(b, op(a, c)) == op(a, op(b, c)) : A}
318	
319	def op_left_comm_sym(A, op, assoc, comm, a, b, c):
320	  Equal.sym(A, op(a, op(b, c)), op(b, op(a, c)), op_left_comm(~A, ~op, ~assoc, ~comm, a, b, c))
321	
322	# Right commutation from associativity and commutativity, reversed to rewrite toward the simple side.
323	law op_right_comm_sym:
324	  for ~A: Data
325	  for ~op: A -> A -> A
326	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
327	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
328	  for +a: A
329	  for +b: A
330	  for +c: A
331	  {op(op(a, c), b) == op(op(a, b), c) : A}
332	
333	def op_right_comm_sym(A, op, assoc, comm, a, b, c):
334	  Equal.sym(A, op(op(a, b), c), op(op(a, c), b), op_right_comm(~A, ~op, ~assoc, ~comm, a, b, c))
335	
336	# Middle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.
337	law op_four_sym:
338	  for ~A: Data
339	  for ~op: A -> A -> A
340	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
341	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
342	  for +a: A
343	  for +b: A
344	  for +c: A
345	  for +d: A
346	  {op(op(a, c), op(b, d)) == op(op(a, b), op(c, d)) : A}
347	
348	def op_four_sym(A, op, assoc, comm, a, b, c, d):
349	  Equal.sym(A, op(op(a, b), op(c, d)), op(op(a, c), op(b, d)), op_four(~A, ~op, ~assoc, ~comm, a, b, c, d))
350	
351	# Three-way commutation from commutativity alone, reversed to rewrite toward the simple side.
352	law op_comm3_sym:
353	  for ~A: Data
354	  for ~op: A -> A -> A
355	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
356	  for +a: A
357	  for +b: A
358	  for +c: A
359	  {op(c, op(b, a)) == op(op(a, b), c) : A}
360	
361	def op_comm3_sym(A, op, comm, a, b, c):
362	  Equal.sym(A, op(op(a, b), c), op(c, op(b, a)), op_comm3(~A, ~op, ~comm, a, b, c))
363	
364	# Nat addition is left-commutative (the same statement as MNat.add_left_comm), reversed to rewrite toward the simple side.
365	law nat_add_left_comm_sym:
366	  for +a: Nat
367	  for +b: Nat
368	  for +c: Nat
369	  {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
370	
371	def nat_add_left_comm_sym(a, b, c):
372	  Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), nat_add_left_comm(a, b, c))
373	
374	# Nat addition is right-commutative (the same statement as MNat.add_right_comm), reversed to rewrite toward the simple side.
375	law nat_add_right_comm_sym:
376	  for +a: Nat
377	  for +b: Nat
378	  for +c: Nat
379	  {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
380	
381	def nat_add_right_comm_sym(a, b, c):
382	  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), nat_add_right_comm(a, b, c))
383	
384	# Nat addition's middle-four interchange (the same statement as MNat.add_add_add_comm), reversed to rewrite toward the simple side.
385	law nat_add_four_sym:
386	  for +a: Nat
387	  for +b: Nat
388	  for +c: Nat
389	  for +d: Nat
390	  {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
391	
392	def nat_add_four_sym(a, b, c, d):
393	  Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), nat_add_four(a, b, c, d))
394	
395	# Nat multiplication is left-commutative (the same statement as MNat.mul_left_comm), reversed to rewrite toward the simple side.
396	law nat_mul_left_comm_sym:
397	  for +a: Nat
398	  for +b: Nat
399	  for +c: Nat
400	  {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
401	
402	def nat_mul_left_comm_sym(a, b, c):
403	  Equal.sym(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)), nat_mul_left_comm(a, b, c))
404	
405	# Nat multiplication is right-commutative (the same statement as MNat.mul_right_comm), reversed to rewrite toward the simple side.
406	law nat_mul_right_comm_sym:
407	  for +a: Nat
408	  for +b: Nat
409	  for +c: Nat
410	  {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
411	
412	def nat_mul_right_comm_sym(a, b, c):
413	  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(Nat.mul(a, c), b), nat_mul_right_comm(a, b, c))
414	
415	# Nat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm), reversed to rewrite toward the simple side.
416	law nat_mul_four_sym:
417	  for +a: Nat
418	  for +b: Nat
419	  for +c: Nat
420	  for +d: Nat
421	  {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
422	
423	def nat_mul_four_sym(a, b, c, d):
424	  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), Nat.mul(c, d)), Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), nat_mul_four(a, b, c, d))
425	
426	# Bool and is left-commutative, reversed to rewrite toward the simple side.
427	law bool_and_left_comm_sym:
428	  for +a: Bool
429	  for +b: Bool
430	  for +c: Bool
431	  {Bool.and(b, Bool.and(a, c)) == Bool.and(a, Bool.and(b, c)) : Bool}
432	
433	def bool_and_left_comm_sym(a, b, c):
434	  Equal.sym(Bool, Bool.and(a, Bool.and(b, c)), Bool.and(b, Bool.and(a, c)), bool_and_left_comm(a, b, c))
435	
436	# Bool and is right-commutative, reversed to rewrite toward the simple side.
437	law bool_and_right_comm_sym:
438	  for +a: Bool
439	  for +b: Bool
440	  for +c: Bool
441	  {Bool.and(Bool.and(a, c), b) == Bool.and(Bool.and(a, b), c) : Bool}
442	
443	def bool_and_right_comm_sym(a, b, c):
444	  Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(Bool.and(a, c), b), bool_and_right_comm(a, b, c))
445	
446	# Bool or is left-commutative, reversed to rewrite toward the simple side.
447	law bool_or_left_comm_sym:
448	  for +a: Bool
449	  for +b: Bool
450	  for +c: Bool
451	  {Bool.or(b, Bool.or(a, c)) == Bool.or(a, Bool.or(b, c)) : Bool}
452	
453	def bool_or_left_comm_sym(a, b, c):
454	  Equal.sym(Bool, Bool.or(a, Bool.or(b, c)), Bool.or(b, Bool.or(a, c)), bool_or_left_comm(a, b, c))
455	
456	# Bool or is right-commutative, reversed to rewrite toward the simple side.
457	law bool_or_right_comm_sym:
458	  for +a: Bool
459	  for +b: Bool
460	  for +c: Bool
461	  {Bool.or(Bool.or(a, c), b) == Bool.or(Bool.or(a, b), c) : Bool}
462	
463	def bool_or_right_comm_sym(a, b, c):
464	  Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(Bool.or(a, c), b), bool_or_right_comm(a, b, c))
465	
466	# Four-way reassociation for List append over Nat, reversed to rewrite toward the simple side.
467	law list_nat_append_assoc4_sym:
468	  for +a: List<&2, Nat>
469	  for +b: List<&2, Nat>
470	  for +c: List<&2, Nat>
471	  for +d: List<&2, Nat>
472	  {List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) == List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) : List<&2, Nat>}
473	
474	def list_nat_append_assoc4_sym(a, b, c, d):
475	  Equal.sym(List<&2, Nat>, List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d), List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))), list_nat_append_assoc4(a, b, c, d))
476	
477	# Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity), reversed to rewrite toward the simple side.
478	law foldl_op_eq_foldr_op_sym:
479	  for ~B: Data
480	  for ~op: B -> B -> B
481	  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
482	  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
483	  for ~z: B
484	  for ~id: @x: B -> {op(z, x) == x : B}
485	  for +xs: List<&2, B>
486	  {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}
487	
488	def foldl_op_eq_foldr_op_sym(B, op, assoc, comm, z, id, xs):
489	  Equal.sym(B, List.foldl(&2, B, B, op, xs, z), List.foldr(&2, B, B, op, xs, z), foldl_op_eq_foldr_op(~B, ~op, ~assoc, ~comm, ~z, ~id, xs))
490	
491	# Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr), reversed to rewrite toward the simple side.
492	law foldl_eq_foldr_sym:
493	  for ~B: Data
494	  for ~op: B -> B -> B
495	  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
496	  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
497	  for +z: B
498	  for +xs: List<&2, B>
499	  {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}
500	
501	def foldl_eq_foldr_sym(B, op, assoc, comm, z, xs):
502	  Equal.sym(B, List.foldl(&2, B, B, op, xs, z), List.foldr(&2, B, B, op, xs, z), foldl_eq_foldr(~B, ~op, ~assoc, ~comm, z, xs))
503	
504	# Calls of the twins, as the calls above the generated section make of their laws (PLAN F38).
505	def internal_nat_foldl_op_eq_foldr_op_sym(+xs: List<&2, Nat>) -> {List.foldr(&2, Nat, Nat, Nat.add, xs, 0n) == List.foldl(&2, Nat, Nat, Nat.add, xs, 0n) : Nat}:
506	  foldl_op_eq_foldr_op_sym(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, ~0n, ~internal_nat_zero_add, xs)