algebra.bend
bend-mathlib@0.4.0.0 · 451 lines · 0 definitions
1# bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.
2import Base
3import bend-mathlib@0.4.0.0/nat.bend as MNat
4import bend-mathlib@0.4.0.0/bool.bend as MBool
5import bend-mathlib@0.4.0.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_mul(x: Nat, y: Nat) -> Nat:
95 Nat.mul(x, y)
96
97def 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}:
98 MNat.mul_assoc(x, y, z)
99
100def internal_nat_mul_comm(x: Nat, y: Nat) -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}:
101 MNat.mul_comm(x, y)
102
103def 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}:
104 MBool.and_assoc(x, y, z)
105
106def internal_bool_and_comm(x: Bool, y: Bool) -> {Bool.and(x, y) == Bool.and(y, x) : Bool}:
107 MBool.and_comm(x, y)
108
109def 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}:
110 MBool.or_assoc(x, y, z)
111
112def internal_bool_or_comm(x: Bool, y: Bool) -> {Bool.or(x, y) == Bool.or(y, x) : Bool}:
113 MBool.or_comm(x, y)
114
115def 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>}:
116 MList.append_assoc(&2, Nat, x, y, z)
117
118# Nat addition is left-commutative.
119law nat_add_left_comm:
120 for +a: Nat
121 for +b: Nat
122 for +c: Nat
123 {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
124
125def nat_add_left_comm(a, b, c):
126 op_left_comm(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c)
127
128# Nat addition is right-commutative.
129law nat_add_right_comm:
130 for +a: Nat
131 for +b: Nat
132 for +c: Nat
133 {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
134
135def nat_add_right_comm(a, b, c):
136 op_right_comm(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c)
137
138# Nat addition's middle-four interchange.
139law nat_add_four:
140 for +a: Nat
141 for +b: Nat
142 for +c: Nat
143 for +d: Nat
144 {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
145
146def nat_add_four(a, b, c, d):
147 op_four(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c, d)
148
149# Nat multiplication is left-commutative.
150law nat_mul_left_comm:
151 for +a: Nat
152 for +b: Nat
153 for +c: Nat
154 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
155
156def nat_mul_left_comm(a, b, c):
157 op_left_comm(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c)
158
159# Nat multiplication is right-commutative.
160law nat_mul_right_comm:
161 for +a: Nat
162 for +b: Nat
163 for +c: Nat
164 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
165
166def nat_mul_right_comm(a, b, c):
167 op_right_comm(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c)
168
169# Nat multiplication's middle-four interchange.
170law nat_mul_four:
171 for +a: Nat
172 for +b: Nat
173 for +c: Nat
174 for +d: Nat
175 {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
176
177def nat_mul_four(a, b, c, d):
178 op_four(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c, d)
179
180# Bool and is left-commutative.
181law bool_and_left_comm:
182 for +a: Bool
183 for +b: Bool
184 for +c: Bool
185 {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}
186
187def bool_and_left_comm(a, b, c):
188 op_left_comm(~Bool, ~Bool.and, ~internal_bool_and_assoc, ~internal_bool_and_comm, a, b, c)
189
190# Bool and is right-commutative.
191law bool_and_right_comm:
192 for +a: Bool
193 for +b: Bool
194 for +c: Bool
195 {Bool.and(Bool.and(a, b), c) == Bool.and(Bool.and(a, c), b) : Bool}
196
197def bool_and_right_comm(a, b, c):
198 op_right_comm(~Bool, ~Bool.and, ~internal_bool_and_assoc, ~internal_bool_and_comm, a, b, c)
199
200# Bool or is left-commutative.
201law bool_or_left_comm:
202 for +a: Bool
203 for +b: Bool
204 for +c: Bool
205 {Bool.or(a, Bool.or(b, c)) == Bool.or(b, Bool.or(a, c)) : Bool}
206
207def bool_or_left_comm(a, b, c):
208 op_left_comm(~Bool, ~Bool.or, ~internal_bool_or_assoc, ~internal_bool_or_comm, a, b, c)
209
210# Bool or is right-commutative.
211law bool_or_right_comm:
212 for +a: Bool
213 for +b: Bool
214 for +c: Bool
215 {Bool.or(Bool.or(a, b), c) == Bool.or(Bool.or(a, c), b) : Bool}
216
217def bool_or_right_comm(a, b, c):
218 op_right_comm(~Bool, ~Bool.or, ~internal_bool_or_assoc, ~internal_bool_or_comm, a, b, c)
219
220# Four-way reassociation for List append over Nat.
221law list_nat_append_assoc4:
222 for +a: List<&2, Nat>
223 for +b: List<&2, Nat>
224 for +c: List<&2, Nat>
225 for +d: List<&2, Nat>
226 {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>}
227
228def list_nat_append_assoc4(a, b, c, d):
229 op_assoc4(~List<&2, Nat>, ~List.append(&2, Nat), ~internal_list_nat_append_assoc, a, b, c, d)
230
231# Folding left equals folding right for an associative, commutative operation with a left identity.
232law foldl_op_eq_foldr_op:
233 for ~B: Data
234 for ~op: B -> B -> B
235 for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
236 for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
237 for ~z: B
238 for ~id: @x: B -> {op(z, x) == x : B}
239 for +xs: List<&2, B>
240 {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}
241
242def 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}:
243 match xs:
244 case Nil{}:
245 Equal.sym(B, op(acc, z), acc, Equal.trans(B, op(acc, z), op(z, acc), acc, comm(acc, z), id(acc)))
246 case +h <> +t:
247 %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}
248 assoc(acc, h, List.foldr(&2, B, B, op, t, z))
249
250def foldl_op_eq_foldr_op(B, op, assoc, comm, z, id, xs):
251 %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}
252 id(List.foldr(&2, B, B, op, xs, z))
253
254# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
255
256# Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.
257law op_assoc4_sym:
258 for ~A: Data
259 for ~op: A -> A -> A
260 for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
261 for +a: A
262 for +b: A
263 for +c: A
264 for +d: A
265 {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}
266
267def op_assoc4_sym(A, op, assoc, a, b, c, d):
268 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))
269
270# Left commutation from associativity and commutativity, reversed to rewrite toward the simple side.
271law op_left_comm_sym:
272 for ~A: Data
273 for ~op: A -> A -> A
274 for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
275 for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
276 for +a: A
277 for +b: A
278 for +c: A
279 {op(b, op(a, c)) == op(a, op(b, c)) : A}
280
281def op_left_comm_sym(A, op, assoc, comm, a, b, c):
282 Equal.sym(A, op(a, op(b, c)), op(b, op(a, c)), op_left_comm(~A, ~op, ~assoc, ~comm, a, b, c))
283
284# Right commutation from associativity and commutativity, reversed to rewrite toward the simple side.
285law op_right_comm_sym:
286 for ~A: Data
287 for ~op: A -> A -> A
288 for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
289 for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
290 for +a: A
291 for +b: A
292 for +c: A
293 {op(op(a, c), b) == op(op(a, b), c) : A}
294
295def op_right_comm_sym(A, op, assoc, comm, a, b, c):
296 Equal.sym(A, op(op(a, b), c), op(op(a, c), b), op_right_comm(~A, ~op, ~assoc, ~comm, a, b, c))
297
298# Middle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.
299law op_four_sym:
300 for ~A: Data
301 for ~op: A -> A -> A
302 for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
303 for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
304 for +a: A
305 for +b: A
306 for +c: A
307 for +d: A
308 {op(op(a, c), op(b, d)) == op(op(a, b), op(c, d)) : A}
309
310def op_four_sym(A, op, assoc, comm, a, b, c, d):
311 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))
312
313# Three-way commutation from commutativity alone, reversed to rewrite toward the simple side.
314law op_comm3_sym:
315 for ~A: Data
316 for ~op: A -> A -> A
317 for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
318 for +a: A
319 for +b: A
320 for +c: A
321 {op(c, op(b, a)) == op(op(a, b), c) : A}
322
323def op_comm3_sym(A, op, comm, a, b, c):
324 Equal.sym(A, op(op(a, b), c), op(c, op(b, a)), op_comm3(~A, ~op, ~comm, a, b, c))
325
326# Nat addition is left-commutative, reversed to rewrite toward the simple side.
327law nat_add_left_comm_sym:
328 for +a: Nat
329 for +b: Nat
330 for +c: Nat
331 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
332
333def nat_add_left_comm_sym(a, b, c):
334 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), nat_add_left_comm(a, b, c))
335
336# Nat addition is right-commutative, reversed to rewrite toward the simple side.
337law nat_add_right_comm_sym:
338 for +a: Nat
339 for +b: Nat
340 for +c: Nat
341 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
342
343def nat_add_right_comm_sym(a, b, c):
344 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), nat_add_right_comm(a, b, c))
345
346# Nat addition's middle-four interchange, reversed to rewrite toward the simple side.
347law nat_add_four_sym:
348 for +a: Nat
349 for +b: Nat
350 for +c: Nat
351 for +d: Nat
352 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
353
354def nat_add_four_sym(a, b, c, d):
355 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))
356
357# Nat multiplication is left-commutative, reversed to rewrite toward the simple side.
358law nat_mul_left_comm_sym:
359 for +a: Nat
360 for +b: Nat
361 for +c: Nat
362 {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
363
364def nat_mul_left_comm_sym(a, b, c):
365 Equal.sym(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)), nat_mul_left_comm(a, b, c))
366
367# Nat multiplication is right-commutative, reversed to rewrite toward the simple side.
368law nat_mul_right_comm_sym:
369 for +a: Nat
370 for +b: Nat
371 for +c: Nat
372 {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
373
374def nat_mul_right_comm_sym(a, b, c):
375 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(Nat.mul(a, c), b), nat_mul_right_comm(a, b, c))
376
377# Nat multiplication's middle-four interchange, reversed to rewrite toward the simple side.
378law nat_mul_four_sym:
379 for +a: Nat
380 for +b: Nat
381 for +c: Nat
382 for +d: Nat
383 {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
384
385def nat_mul_four_sym(a, b, c, d):
386 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))
387
388# Bool and is left-commutative, reversed to rewrite toward the simple side.
389law bool_and_left_comm_sym:
390 for +a: Bool
391 for +b: Bool
392 for +c: Bool
393 {Bool.and(b, Bool.and(a, c)) == Bool.and(a, Bool.and(b, c)) : Bool}
394
395def bool_and_left_comm_sym(a, b, c):
396 Equal.sym(Bool, Bool.and(a, Bool.and(b, c)), Bool.and(b, Bool.and(a, c)), bool_and_left_comm(a, b, c))
397
398# Bool and is right-commutative, reversed to rewrite toward the simple side.
399law bool_and_right_comm_sym:
400 for +a: Bool
401 for +b: Bool
402 for +c: Bool
403 {Bool.and(Bool.and(a, c), b) == Bool.and(Bool.and(a, b), c) : Bool}
404
405def bool_and_right_comm_sym(a, b, c):
406 Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(Bool.and(a, c), b), bool_and_right_comm(a, b, c))
407
408# Bool or is left-commutative, reversed to rewrite toward the simple side.
409law bool_or_left_comm_sym:
410 for +a: Bool
411 for +b: Bool
412 for +c: Bool
413 {Bool.or(b, Bool.or(a, c)) == Bool.or(a, Bool.or(b, c)) : Bool}
414
415def bool_or_left_comm_sym(a, b, c):
416 Equal.sym(Bool, Bool.or(a, Bool.or(b, c)), Bool.or(b, Bool.or(a, c)), bool_or_left_comm(a, b, c))
417
418# Bool or is right-commutative, reversed to rewrite toward the simple side.
419law bool_or_right_comm_sym:
420 for +a: Bool
421 for +b: Bool
422 for +c: Bool
423 {Bool.or(Bool.or(a, c), b) == Bool.or(Bool.or(a, b), c) : Bool}
424
425def bool_or_right_comm_sym(a, b, c):
426 Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(Bool.or(a, c), b), bool_or_right_comm(a, b, c))
427
428# Four-way reassociation for List append over Nat, reversed to rewrite toward the simple side.
429law list_nat_append_assoc4_sym:
430 for +a: List<&2, Nat>
431 for +b: List<&2, Nat>
432 for +c: List<&2, Nat>
433 for +d: List<&2, Nat>
434 {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>}
435
436def list_nat_append_assoc4_sym(a, b, c, d):
437 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))
438
439# Folding left equals folding right for an associative, commutative operation with a left identity, reversed to rewrite toward the simple side.
440law foldl_op_eq_foldr_op_sym:
441 for ~B: Data
442 for ~op: B -> B -> B
443 for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
444 for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
445 for ~z: B
446 for ~id: @x: B -> {op(z, x) == x : B}
447 for +xs: List<&2, B>
448 {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}
449
450def foldl_op_eq_foldr_op_sym(B, op, assoc, comm, z, id, xs):
451 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))