nat.bend
bend-mathlib@0.1.0.1 · 781 lines · 0 definitions
1import Base
2
3# Zero is a right identity for addition: x + 0 = x.
4law add_zero:
5 for x: Nat
6 {Nat.add(x, 0n) == x : Nat}
7
8def add_zero(x):
9 match x:
10 case 0n:
11 {==}
12 case 1n+p:
13 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
14 {==}
15
16# Zero is a left identity for addition: 0 + x = x.
17law zero_add:
18 for -x: Nat
19 {Nat.add(0n, x) == x : Nat}
20
21def zero_add(x):
22 {==}
23
24# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
25law add_succ:
26 for n: Nat
27 for -m: Nat
28 {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
29
30def add_succ(n, m):
31 match n:
32 case 0n:
33 {==}
34 case 1n+p:
35 %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
36 {==}
37
38# Adding a successor on the left: (n + 1) + m = (n + m) + 1.
39law succ_add:
40 for -n: Nat
41 for -m: Nat
42 {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}
43
44def succ_add(n, m):
45 {==}
46
47# Addition is commutative: n + m = m + n.
48law add_comm:
49 for n: Nat
50 for m: Nat
51 {Nat.add(n, m) == Nat.add(m, n) : Nat}
52
53def add_comm(n, m):
54 match n m:
55 case 0n 0n:
56 {==}
57 case 0n 1n+q:
58 %add_zero(q) : {1n+_ == 1n+Nat.add(q, 0n) : Nat}
59 {==}
60 case 1n+p 0n:
61 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
62 {==}
63 case 1n++p 1n++q:
64 %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), add_succ(p, q)) : {1n+_ == 1n+Nat.add(q, 1n+p) : Nat}
65 %Equal.sym(Nat, Nat.add(q, 1n+p), 1n+Nat.add(q, p), add_succ(q, p)) : {2n+Nat.add(p, q) == 1n+_ : Nat}
66 %add_comm(p, q) : {2n+Nat.add(p, q) == 2n+_ : Nat}
67 {==}
68
69# Addition is associative: (a + b) + c = a + (b + c).
70law add_assoc:
71 for a: Nat
72 for -b: Nat
73 for -c: Nat
74 {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
75
76def add_assoc(a, b, c):
77 match a:
78 case 0n:
79 {==}
80 case 1n+p:
81 %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
82 {==}
83
84# Left commutativity of addition: a + (b + c) = b + (a + c).
85law add_left_comm:
86 for a: Nat
87 for b: Nat
88 for -c: Nat
89 {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
90
91def add_left_comm(a, b, c):
92 match a:
93 case 0n:
94 {==}
95 case 1n+p:
96 +b = b
97 %Equal.sym(Nat, Nat.add(b, 1n+Nat.add(p, c)), 1n+Nat.add(b, Nat.add(p, c)), add_succ(b, Nat.add(p, c))) : {1n+Nat.add(p, Nat.add(b, c)) == _ : Nat}
98 %add_left_comm(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
99 {==}
100
101# Right commutativity of addition: (a + b) + c = (a + c) + b.
102law add_right_comm:
103 for a: Nat
104 for b: Nat
105 for c: Nat
106 {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
107
108def add_right_comm(a, b, c):
109 match a:
110 case 0n:
111 add_comm(b, c)
112 case 1n+p:
113 %add_right_comm(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
114 {==}
115
116# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).
117law add_add_add_comm:
118 for a: Nat
119 for b: Nat
120 for c: Nat
121 for -d: Nat
122 {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
123
124def add_add_add_comm(a, b, c, d):
125 match a:
126 case 0n:
127 add_left_comm(b, c, d)
128 case 1n+p:
129 %add_add_add_comm(p, b, c, d) : {1n+Nat.add(Nat.add(p, b), Nat.add(c, d)) == 1n+_ : Nat}
130 {==}
131
132def internal_pred(n: Nat) -> Nat:
133 match n:
134 case 0n:
135 0n
136 case 1n+p:
137 p
138
139# The successor function is injective: a + 1 = b + 1 implies a = b.
140law succ_inj:
141 for -a: Nat
142 for -b: Nat
143 for e: {1n+a == 1n+b : Nat}
144 {a == b : Nat}
145
146def succ_inj(a, b, e):
147 %e : {a == internal_pred(_) : Nat}
148 {==}
149
150def internal_zero_ne_succ(-n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
151 %e : Bool.pick(Type, Nat.is_eq(_, 0n), Unit, Empty)
152 Unit{}
153
154# Zero is not a successor.
155law zero_ne_succ:
156 for -n: Nat
157 {0n != 1n+n : Nat}
158
159def zero_ne_succ(n):
160 e => internal_zero_ne_succ(n, e)
161
162def internal_succ_ne_zero(-n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
163 %e : Bool.pick(Type, Nat.is_eq(_, 0n), Empty, Unit)
164 Unit{}
165
166# A successor is not zero.
167law succ_ne_zero:
168 for -n: Nat
169 {1n+n != 0n : Nat}
170
171def succ_ne_zero(n):
172 e => internal_succ_ne_zero(n, e)
173
174# Addition cancels on the left: a + b = a + c implies b = c.
175law add_left_cancel:
176 for a: Nat
177 for -b: Nat
178 for -c: Nat
179 for e: {Nat.add(a, b) == Nat.add(a, c) : Nat}
180 {b == c : Nat}
181
182def add_left_cancel(a, b, c, e):
183 match a:
184 case 0n:
185 e
186 case 1n+p:
187 add_left_cancel(p, b, c, succ_inj(Nat.add(p, b), Nat.add(p, c), e))
188
189# Addition cancels on the right: a + b = c + b implies a = c.
190law add_right_cancel:
191 for a: Nat
192 for b: Nat
193 for c: Nat
194 for e: {Nat.add(a, b) == Nat.add(c, b) : Nat}
195 {a == c : Nat}
196
197def add_right_cancel(a, b, c, e):
198 +b = b
199 add_left_cancel(b, a, c, Equal.trans(Nat, Nat.add(b, a), Nat.add(a, b), Nat.add(b, c), add_comm(b, a), Equal.trans(Nat, Nat.add(a, b), Nat.add(c, b), Nat.add(b, c), e, add_comm(c, b))))
200
201# Zero absorbs multiplication on the right: x * 0 = 0.
202law mul_zero:
203 for x: Nat
204 {Nat.mul(x, 0n) == 0n : Nat}
205
206def mul_zero(x):
207 match x:
208 case 0n:
209 {==}
210 case 1n+p:
211 mul_zero(p)
212
213# Zero absorbs multiplication on the left: 0 * x = 0.
214law zero_mul:
215 for -x: Nat
216 {Nat.mul(0n, x) == 0n : Nat}
217
218def zero_mul(x):
219 {==}
220
221# One is a right identity for multiplication: x * 1 = x.
222law mul_one:
223 for x: Nat
224 {Nat.mul(x, 1n) == x : Nat}
225
226def mul_one(x):
227 match x:
228 case 0n:
229 {==}
230 case 1n+p:
231 %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
232 {==}
233
234# One is a left identity for multiplication: 1 * x = x.
235law one_mul:
236 for x: Nat
237 {Nat.mul(1n, x) == x : Nat}
238
239def one_mul(x):
240 add_zero(x)
241
242# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
243law mul_succ:
244 for n: Nat
245 for m: Nat
246 {Nat.mul(n, 1n+m) == Nat.add(Nat.mul(n, m), n) : Nat}
247
248def mul_succ(n, m):
249 match n:
250 case 0n:
251 {==}
252 case 1n++p:
253 +m = m
254 %Equal.sym(Nat, Nat.add(Nat.add(m, Nat.mul(p, m)), 1n+p), 1n+Nat.add(Nat.add(m, Nat.mul(p, m)), p), add_succ(Nat.add(m, Nat.mul(p, m)), p)) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == _ : Nat}
255 %Equal.sym(Nat, Nat.add(Nat.add(m, Nat.mul(p, m)), p), Nat.add(m, Nat.add(Nat.mul(p, m), p)), add_assoc(m, Nat.mul(p, m), p)) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+_ : Nat}
256 %mul_succ(p, m) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+Nat.add(m, _) : Nat}
257 {==}
258
259# Multiplying by a successor on the left: (n + 1) * m = n * m + m.
260law succ_mul:
261 for n: Nat
262 for m: Nat
263 {Nat.mul(1n+n, m) == Nat.add(Nat.mul(n, m), m) : Nat}
264
265def succ_mul(n, m):
266 +m = m
267 add_comm(m, Nat.mul(n, m))
268
269# Multiplication is commutative: n * m = m * n.
270law mul_comm:
271 for n: Nat
272 for m: Nat
273 {Nat.mul(n, m) == Nat.mul(m, n) : Nat}
274
275def mul_comm(n, m):
276 match n:
277 case 0n:
278 %mul_zero(m) : {_ == Nat.mul(m, 0n) : Nat}
279 {==}
280 case 1n++p:
281 +m = m
282 %Equal.sym(Nat, Nat.mul(m, 1n+p), Nat.add(Nat.mul(m, p), m), mul_succ(m, p)) : {Nat.add(m, Nat.mul(p, m)) == _ : Nat}
283 %mul_comm(p, m) : {Nat.add(m, Nat.mul(p, m)) == Nat.add(_, m) : Nat}
284 add_comm(m, Nat.mul(p, m))
285
286# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
287law add_mul:
288 for a: Nat
289 for -b: Nat
290 for c: Nat
291 {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
292
293def add_mul(a, b, c):
294 match a:
295 case 0n:
296 {==}
297 case 1n+p:
298 +c = c
299 %Equal.sym(Nat, Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)), Nat.add(c, Nat.add(Nat.mul(p, c), Nat.mul(b, c))), add_assoc(c, Nat.mul(p, c), Nat.mul(b, c))) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == _ : Nat}
300 %add_mul(p, b, c) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == Nat.add(c, _) : Nat}
301 {==}
302
303# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
304law mul_add:
305 for a: Nat
306 for b: Nat
307 for c: Nat
308 {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
309
310def mul_add(a, b, c):
311 match a:
312 case 0n:
313 {==}
314 case 1n++p:
315 +b = b
316 +c = c
317 %Equal.sym(Nat, Nat.mul(p, Nat.add(b, c)), Nat.add(Nat.mul(p, b), Nat.mul(p, c)), mul_add(p, b, c)) : {Nat.add(Nat.add(b, c), _) == Nat.add(Nat.add(b, Nat.mul(p, b)), Nat.add(c, Nat.mul(p, c))) : Nat}
318 add_add_add_comm(b, c, Nat.mul(p, b), Nat.mul(p, c))
319
320# Multiplication is associative: (a * b) * c = a * (b * c).
321law mul_assoc:
322 for a: Nat
323 for b: Nat
324 for c: Nat
325 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
326
327def mul_assoc(a, b, c):
328 match a:
329 case 0n:
330 {==}
331 case 1n+p:
332 +b = b
333 +c = c
334 %mul_assoc(p, b, c) : {Nat.mul(Nat.add(b, Nat.mul(p, b)), c) == Nat.add(Nat.mul(b, c), _) : Nat}
335 add_mul(b, Nat.mul(p, b), c)
336
337# The order a <= b on naturals, as a reusable proposition.
338def le(a: Nat, b: Nat) -> Data:
339 {Nat.is_le(a, b) == True{} : Bool}
340
341# The strict order a < b on naturals, as a reusable proposition.
342def lt(a: Nat, b: Nat) -> Data:
343 {Nat.is_lt(a, b) == True{} : Bool}
344
345# The order a >= b on naturals, as a reusable proposition.
346def ge(a: Nat, b: Nat) -> Data:
347 {Nat.is_ge(a, b) == True{} : Bool}
348
349# The strict order a > b on naturals, as a reusable proposition.
350def gt(a: Nat, b: Nat) -> Data:
351 {Nat.is_gt(a, b) == True{} : Bool}
352
353def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
354 %e : Bool.pick(Type, _, Empty, Unit)
355 Unit{}
356
357# Every natural is at most itself: a <= a.
358law le_refl:
359 for a: Nat
360 le(a, a)
361
362def le_refl(a):
363 match a:
364 case 0n:
365 {==}
366 case 1n+p:
367 le_refl(p)
368
369# Zero is at most every natural: 0 <= b.
370law zero_le:
371 for b: Nat
372 le(0n, b)
373
374def zero_le(b):
375 match b:
376 case 0n:
377 {==}
378 case 1n+p:
379 {==}
380
381# Every natural is at most its successor: n <= n + 1.
382law le_succ:
383 for n: Nat
384 le(n, 1n+n)
385
386def le_succ(n):
387 match n:
388 case 0n:
389 {==}
390 case 1n+p:
391 le_succ(p)
392
393# Adding on the right never decreases a natural: n <= n + k.
394law le_add_right:
395 for n: Nat
396 for k: Nat
397 le(n, Nat.add(n, k))
398
399def le_add_right(n, k):
400 match n:
401 case 0n:
402 zero_le(k)
403 case 1n+p:
404 le_add_right(p, k)
405
406# The order is transitive: a <= b and b <= c imply a <= c.
407law le_trans:
408 for a: Nat
409 for b: Nat
410 for c: Nat
411 for ab: le(a, b)
412 for bc: le(b, c)
413 le(a, c)
414
415def le_trans(a, b, c, ab, bc):
416 match a b c:
417 case 0n _ 0n:
418 {==}
419 case 0n _ 1n+r:
420 {==}
421 case 1n+p 0n _:
422 Empty.absurd(le(1n+p, c), internal_false_ne_true(ab))
423 case 1n+p 1n+q 0n:
424 Empty.absurd(le(1n+p, 0n), internal_false_ne_true(bc))
425 case 1n+p 1n+q 1n+r:
426 le_trans(p, q, r, ab, bc)
427
428# The order is antisymmetric: a <= b and b <= a imply a = b.
429law le_antisymm:
430 for a: Nat
431 for b: Nat
432 for ab: le(a, b)
433 for ba: le(b, a)
434 {a == b : Nat}
435
436def le_antisymm(a, b, ab, ba):
437 match a b:
438 case 0n 0n:
439 {==}
440 case 0n 1n+q:
441 Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(ba))
442 case 1n+p 0n:
443 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(ab))
444 case 1n+p 1n+q:
445 %le_antisymm(p, q, ab, ba) : {1n+p == 1n+_ : Nat}
446 {==}
447
448# The order is total: a <= b or b <= a.
449law le_total:
450 for a: Nat
451 for b: Nat
452 Or(le(a, b), le(b, a))
453
454def le_total(a, b):
455 match a b:
456 case 0n 0n:
457 Inl{{==}}
458 case 0n 1n+q:
459 Inl{{==}}
460 case 1n+p 0n:
461 Inr{{==}}
462 case 1n+p 1n+q:
463 le_total(p, q)
464
465# The order is total, as a reusable sum: a <= b or b <= a.
466law le_total_d:
467 for a: Nat
468 for b: Nat
469 Either<&2, &2, le(a, b), le(b, a)>
470
471def le_total_d(a, b):
472 match a b:
473 case 0n 0n:
474 Inl{{==}}
475 case 0n 1n+q:
476 Inl{{==}}
477 case 1n+p 0n:
478 Inr{{==}}
479 case 1n+p 1n+q:
480 le_total_d(p, q)
481
482# No natural is less than itself.
483law lt_irrefl:
484 for a: Nat
485 lt(a, a) -> Empty
486
487def lt_irrefl(a):
488 match a:
489 case 0n:
490 h => internal_false_ne_true(h)
491 case 1n+p:
492 lt_irrefl(p)
493
494# The strict order is transitive: a < b and b < c imply a < c.
495law lt_trans:
496 for a: Nat
497 for b: Nat
498 for c: Nat
499 for ab: lt(a, b)
500 for bc: lt(b, c)
501 lt(a, c)
502
503def lt_trans(a, b, c, ab, bc):
504 match a b c:
505 case 0n 0n _:
506 Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
507 case 0n 1n+q 0n:
508 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
509 case 0n 1n+q 1n+r:
510 {==}
511 case 1n+p 0n _:
512 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
513 case 1n+p 1n+q 0n:
514 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
515 case 1n+p 1n+q 1n+r:
516 lt_trans(p, q, r, ab, bc)
517
518# A strict inequality implies the weak one: a < b implies a <= b.
519law le_of_lt:
520 for a: Nat
521 for b: Nat
522 for h: lt(a, b)
523 le(a, b)
524
525def le_of_lt(a, b, h):
526 match a b:
527 case 0n 0n:
528 {==}
529 case 0n 1n+q:
530 {==}
531 case 1n+p 0n:
532 Empty.absurd(le(1n+p, 0n), internal_false_ne_true(h))
533 case 1n+p 1n+q:
534 le_of_lt(p, q, h)
535
536# Flipping a >= b gives b <= a.
537law le_of_ge:
538 for a: Nat
539 for b: Nat
540 for h: ge(a, b)
541 le(b, a)
542
543def le_of_ge(a, b, h):
544 match a b:
545 case 0n 0n:
546 {==}
547 case 0n 1n+q:
548 Empty.absurd(le(1n+q, 0n), internal_false_ne_true(h))
549 case 1n+p 0n:
550 {==}
551 case 1n+p 1n+q:
552 le_of_ge(p, q, h)
553
554# Flipping b <= a gives a >= b.
555law ge_of_le:
556 for a: Nat
557 for b: Nat
558 for h: le(b, a)
559 ge(a, b)
560
561def ge_of_le(a, b, h):
562 match a b:
563 case 0n 0n:
564 {==}
565 case 0n 1n+q:
566 Empty.absurd(ge(0n, 1n+q), internal_false_ne_true(h))
567 case 1n+p 0n:
568 {==}
569 case 1n+p 1n+q:
570 ge_of_le(p, q, h)
571
572# Flipping a > b gives b < a.
573law lt_of_gt:
574 for a: Nat
575 for b: Nat
576 for h: gt(a, b)
577 lt(b, a)
578
579def lt_of_gt(a, b, h):
580 match a b:
581 case 0n 0n:
582 Empty.absurd(lt(0n, 0n), internal_false_ne_true(h))
583 case 0n 1n+q:
584 Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(h))
585 case 1n+p 0n:
586 {==}
587 case 1n+p 1n+q:
588 lt_of_gt(p, q, h)
589
590# Flipping b < a gives a > b.
591law gt_of_lt:
592 for a: Nat
593 for b: Nat
594 for h: lt(b, a)
595 gt(a, b)
596
597def gt_of_lt(a, b, h):
598 match a b:
599 case 0n 0n:
600 Empty.absurd(gt(0n, 0n), internal_false_ne_true(h))
601 case 0n 1n+q:
602 Empty.absurd(gt(0n, 1n+q), internal_false_ne_true(h))
603 case 1n+p 0n:
604 {==}
605 case 1n+p 1n+q:
606 gt_of_lt(p, q, h)
607
608# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
609
610# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
611law add_zero_sym:
612 for x: Nat
613 {x == Nat.add(x, 0n) : Nat}
614
615def add_zero_sym(x):
616 Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
617
618# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
619law zero_add_sym:
620 for -x: Nat
621 {x == Nat.add(0n, x) : Nat}
622
623def zero_add_sym(x):
624 Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
625
626# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
627law add_succ_sym:
628 for n: Nat
629 for -m: Nat
630 {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
631
632def add_succ_sym(n, m):
633 Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
634
635# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
636law succ_add_sym:
637 for -n: Nat
638 for -m: Nat
639 {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
640
641def succ_add_sym(n, m):
642 Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
643
644# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
645law add_comm_sym:
646 for n: Nat
647 for m: Nat
648 {Nat.add(m, n) == Nat.add(n, m) : Nat}
649
650def add_comm_sym(n, m):
651 Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
652
653# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
654law add_assoc_sym:
655 for a: Nat
656 for -b: Nat
657 for -c: Nat
658 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
659
660def add_assoc_sym(a, b, c):
661 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
662
663# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
664law add_left_comm_sym:
665 for a: Nat
666 for b: Nat
667 for -c: Nat
668 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
669
670def add_left_comm_sym(a, b, c):
671 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
672
673# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
674law add_right_comm_sym:
675 for a: Nat
676 for b: Nat
677 for c: Nat
678 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
679
680def add_right_comm_sym(a, b, c):
681 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
682
683# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
684law add_add_add_comm_sym:
685 for a: Nat
686 for b: Nat
687 for c: Nat
688 for -d: Nat
689 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
690
691def add_add_add_comm_sym(a, b, c, d):
692 Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), add_add_add_comm(a, b, c, d))
693
694# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
695law mul_zero_sym:
696 for x: Nat
697 {0n == Nat.mul(x, 0n) : Nat}
698
699def mul_zero_sym(x):
700 Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
701
702# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
703law zero_mul_sym:
704 for -x: Nat
705 {0n == Nat.mul(0n, x) : Nat}
706
707def zero_mul_sym(x):
708 Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
709
710# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
711law mul_one_sym:
712 for x: Nat
713 {x == Nat.mul(x, 1n) : Nat}
714
715def mul_one_sym(x):
716 Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
717
718# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
719law one_mul_sym:
720 for x: Nat
721 {x == Nat.mul(1n, x) : Nat}
722
723def one_mul_sym(x):
724 Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
725
726# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
727law mul_succ_sym:
728 for n: Nat
729 for m: Nat
730 {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
731
732def mul_succ_sym(n, m):
733 Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
734
735# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
736law succ_mul_sym:
737 for n: Nat
738 for m: Nat
739 {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
740
741def succ_mul_sym(n, m):
742 Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
743
744# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
745law mul_comm_sym:
746 for n: Nat
747 for m: Nat
748 {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
749
750def mul_comm_sym(n, m):
751 Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
752
753# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
754law add_mul_sym:
755 for a: Nat
756 for -b: Nat
757 for c: Nat
758 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
759
760def add_mul_sym(a, b, c):
761 Equal.sym(Nat, Nat.mul(Nat.add(a, b), c), Nat.add(Nat.mul(a, c), Nat.mul(b, c)), add_mul(a, b, c))
762
763# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
764law mul_add_sym:
765 for a: Nat
766 for b: Nat
767 for c: Nat
768 {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
769
770def mul_add_sym(a, b, c):
771 Equal.sym(Nat, Nat.mul(a, Nat.add(b, c)), Nat.add(Nat.mul(a, b), Nat.mul(a, c)), mul_add(a, b, c))
772
773# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
774law mul_assoc_sym:
775 for a: Nat
776 for b: Nat
777 for c: Nat
778 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
779
780def mul_assoc_sym(a, b, c):
781 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))