algebra.bend
bend-mathlib@0.7.5.0 · 506 lines · 0 definitions
1# bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.
2import Base
3import bend-mathlib@0.7.5.0/nat.bend as MNat
4import bend-mathlib@0.7.5.0/bool.bend as MBool
5import bend-mathlib@0.7.5.0/list.bend as MList
6
7# Four-way reassociation from associativity alone.
8law 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
18def 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.
23law 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
33def 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.
39law 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
49def 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.
56law 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
67def 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.
74law 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
83def 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
88def 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
91def internal_nat_add_comm(x: Nat, y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
92 MNat.add_comm(x, y)
93
94def internal_nat_zero_add(x: Nat) -> {Nat.add(0n, x) == x : Nat}:
95 MNat.zero_add(x)
96
97def internal_nat_mul(x: Nat, y: Nat) -> Nat:
98 Nat.mul(x, y)
99
100def 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
103def internal_nat_mul_comm(x: Nat, y: Nat) -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}:
104 MNat.mul_comm(x, y)
105
106def 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
109def internal_bool_and_comm(x: Bool, y: Bool) -> {Bool.and(x, y) == Bool.and(y, x) : Bool}:
110 MBool.and_comm(x, y)
111
112def 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
115def internal_bool_or_comm(x: Bool, y: Bool) -> {Bool.or(x, y) == Bool.or(y, x) : Bool}:
116 MBool.or_comm(x, y)
117
118def 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).
122law 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
128def 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).
132law 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
138def 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).
142law 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
149def 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).
153law 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
159def 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).
163law 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
169def 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).
173law 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
180def 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.
184law 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
190def 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.
194law 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
200def 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.
204law 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
210def 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.
214law 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
220def 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.
224law 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
231def 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
234def 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).
243law 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
253def 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).
258def 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
261def 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
269def 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).
280law 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
289def 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.
295law 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
305def 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.
309law 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
319def 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.
323law 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
333def 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.
337law 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
348def 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.
352law 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
361def 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.
365law 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
371def 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.
375law 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
381def 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.
385law 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
392def 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.
396law 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
402def 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.
406law 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
412def 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.
416law 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
423def 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.
427law 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
433def 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.
437law 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
443def 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.
447law 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
453def 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.
457law 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
463def 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.
467law 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
474def 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.
478law 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
488def 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.
492law 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
501def 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).
505def 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)