nat.bend
bend-mathlib@0.2.0.0 · 1,751 lines · 0 definitions
1# bend-mathlib/nat.bend: Nat arithmetic (add, mul, sub, min, max, pow) and order (le, lt, ge, gt).
2import Base
3
4# Zero is a right identity for addition: x + 0 = x.
5law add_zero:
6 for x: Nat
7 {Nat.add(x, 0n) == x : Nat}
8
9def add_zero(x):
10 match x:
11 case 0n:
12 {==}
13 case 1n+p:
14 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
15 {==}
16
17# Zero is a left identity for addition: 0 + x = x.
18law zero_add:
19 for -x: Nat
20 {Nat.add(0n, x) == x : Nat}
21
22def zero_add(x):
23 {==}
24
25# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
26law add_succ:
27 for n: Nat
28 for -m: Nat
29 {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
30
31def add_succ(n, m):
32 match n:
33 case 0n:
34 {==}
35 case 1n+p:
36 %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
37 {==}
38
39# Adding a successor on the left: (n + 1) + m = (n + m) + 1.
40law succ_add:
41 for -n: Nat
42 for -m: Nat
43 {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}
44
45def succ_add(n, m):
46 {==}
47
48# Addition is commutative: n + m = m + n.
49law add_comm:
50 for n: Nat
51 for m: Nat
52 {Nat.add(n, m) == Nat.add(m, n) : Nat}
53
54def add_comm(n, m):
55 match n m:
56 case 0n 0n:
57 {==}
58 case 0n 1n+q:
59 %add_zero(q) : {1n+_ == 1n+Nat.add(q, 0n) : Nat}
60 {==}
61 case 1n+p 0n:
62 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
63 {==}
64 case 1n++p 1n++q:
65 %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}
66 %Equal.sym(Nat, Nat.add(q, 1n+p), 1n+Nat.add(q, p), add_succ(q, p)) : {2n+Nat.add(p, q) == 1n+_ : Nat}
67 %add_comm(p, q) : {2n+Nat.add(p, q) == 2n+_ : Nat}
68 {==}
69
70# Addition is associative: (a + b) + c = a + (b + c).
71law add_assoc:
72 for a: Nat
73 for -b: Nat
74 for -c: Nat
75 {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
76
77def add_assoc(a, b, c):
78 match a:
79 case 0n:
80 {==}
81 case 1n+p:
82 %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
83 {==}
84
85# Left commutativity of addition: a + (b + c) = b + (a + c).
86law add_left_comm:
87 for a: Nat
88 for b: Nat
89 for -c: Nat
90 {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
91
92def add_left_comm(a, b, c):
93 match a:
94 case 0n:
95 {==}
96 case 1n+p:
97 +b = b
98 %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}
99 %add_left_comm(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
100 {==}
101
102# Right commutativity of addition: (a + b) + c = (a + c) + b.
103law add_right_comm:
104 for a: Nat
105 for b: Nat
106 for c: Nat
107 {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
108
109def add_right_comm(a, b, c):
110 match a:
111 case 0n:
112 add_comm(b, c)
113 case 1n+p:
114 %add_right_comm(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
115 {==}
116
117# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).
118law add_add_add_comm:
119 for a: Nat
120 for b: Nat
121 for c: Nat
122 for -d: Nat
123 {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
124
125def add_add_add_comm(a, b, c, d):
126 match a:
127 case 0n:
128 add_left_comm(b, c, d)
129 case 1n+p:
130 %add_add_add_comm(p, b, c, d) : {1n+Nat.add(Nat.add(p, b), Nat.add(c, d)) == 1n+_ : Nat}
131 {==}
132
133def internal_pred(n: Nat) -> Nat:
134 match n:
135 case 0n:
136 0n
137 case 1n+p:
138 p
139
140# The successor function is injective: a + 1 = b + 1 implies a = b.
141law succ_inj:
142 for -a: Nat
143 for -b: Nat
144 for e: {1n+a == 1n+b : Nat}
145 {a == b : Nat}
146
147def succ_inj(a, b, e):
148 %e : {a == internal_pred(_) : Nat}
149 {==}
150
151def internal_zero_ne_succ(-n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
152 %e : Bool.pick(Type, Nat.is_eq(_, 0n), Unit, Empty)
153 Unit{}
154
155# Zero is not a successor.
156law zero_ne_succ:
157 for -n: Nat
158 {0n != 1n+n : Nat}
159
160def zero_ne_succ(n):
161 e => internal_zero_ne_succ(n, e)
162
163def internal_succ_ne_zero(-n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
164 %e : Bool.pick(Type, Nat.is_eq(_, 0n), Empty, Unit)
165 Unit{}
166
167# A successor is not zero.
168law succ_ne_zero:
169 for -n: Nat
170 {1n+n != 0n : Nat}
171
172def succ_ne_zero(n):
173 e => internal_succ_ne_zero(n, e)
174
175# Addition cancels on the left: a + b = a + c implies b = c.
176law add_left_cancel:
177 for a: Nat
178 for -b: Nat
179 for -c: Nat
180 for e: {Nat.add(a, b) == Nat.add(a, c) : Nat}
181 {b == c : Nat}
182
183def add_left_cancel(a, b, c, e):
184 match a:
185 case 0n:
186 e
187 case 1n+p:
188 add_left_cancel(p, b, c, succ_inj(Nat.add(p, b), Nat.add(p, c), e))
189
190# Addition cancels on the right: a + b = c + b implies a = c.
191law add_right_cancel:
192 for a: Nat
193 for b: Nat
194 for c: Nat
195 for e: {Nat.add(a, b) == Nat.add(c, b) : Nat}
196 {a == c : Nat}
197
198def add_right_cancel(a, b, c, e):
199 +b = b
200 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))))
201
202# Zero absorbs multiplication on the right: x * 0 = 0.
203law mul_zero:
204 for x: Nat
205 {Nat.mul(x, 0n) == 0n : Nat}
206
207def mul_zero(x):
208 match x:
209 case 0n:
210 {==}
211 case 1n+p:
212 mul_zero(p)
213
214# Zero absorbs multiplication on the left: 0 * x = 0.
215law zero_mul:
216 for -x: Nat
217 {Nat.mul(0n, x) == 0n : Nat}
218
219def zero_mul(x):
220 {==}
221
222# One is a right identity for multiplication: x * 1 = x.
223law mul_one:
224 for x: Nat
225 {Nat.mul(x, 1n) == x : Nat}
226
227def mul_one(x):
228 match x:
229 case 0n:
230 {==}
231 case 1n+p:
232 %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
233 {==}
234
235# One is a left identity for multiplication: 1 * x = x.
236law one_mul:
237 for x: Nat
238 {Nat.mul(1n, x) == x : Nat}
239
240def one_mul(x):
241 add_zero(x)
242
243# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
244law mul_succ:
245 for n: Nat
246 for m: Nat
247 {Nat.mul(n, 1n+m) == Nat.add(Nat.mul(n, m), n) : Nat}
248
249def mul_succ(n, m):
250 match n:
251 case 0n:
252 {==}
253 case 1n++p:
254 +m = m
255 %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}
256 %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}
257 %mul_succ(p, m) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+Nat.add(m, _) : Nat}
258 {==}
259
260# Multiplying by a successor on the left: (n + 1) * m = n * m + m.
261law succ_mul:
262 for n: Nat
263 for m: Nat
264 {Nat.mul(1n+n, m) == Nat.add(Nat.mul(n, m), m) : Nat}
265
266def succ_mul(n, m):
267 +m = m
268 add_comm(m, Nat.mul(n, m))
269
270# Multiplication is commutative: n * m = m * n.
271law mul_comm:
272 for n: Nat
273 for m: Nat
274 {Nat.mul(n, m) == Nat.mul(m, n) : Nat}
275
276def mul_comm(n, m):
277 match n:
278 case 0n:
279 %mul_zero(m) : {_ == Nat.mul(m, 0n) : Nat}
280 {==}
281 case 1n++p:
282 +m = m
283 %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}
284 %mul_comm(p, m) : {Nat.add(m, Nat.mul(p, m)) == Nat.add(_, m) : Nat}
285 add_comm(m, Nat.mul(p, m))
286
287# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
288law add_mul:
289 for a: Nat
290 for -b: Nat
291 for c: Nat
292 {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
293
294def add_mul(a, b, c):
295 match a:
296 case 0n:
297 {==}
298 case 1n+p:
299 +c = c
300 %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}
301 %add_mul(p, b, c) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == Nat.add(c, _) : Nat}
302 {==}
303
304# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
305law mul_add:
306 for a: Nat
307 for b: Nat
308 for c: Nat
309 {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
310
311def mul_add(a, b, c):
312 match a:
313 case 0n:
314 {==}
315 case 1n++p:
316 +b = b
317 +c = c
318 %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}
319 add_add_add_comm(b, c, Nat.mul(p, b), Nat.mul(p, c))
320
321# Multiplication is associative: (a * b) * c = a * (b * c).
322law mul_assoc:
323 for a: Nat
324 for b: Nat
325 for c: Nat
326 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
327
328def mul_assoc(a, b, c):
329 match a:
330 case 0n:
331 {==}
332 case 1n+p:
333 +b = b
334 +c = c
335 %mul_assoc(p, b, c) : {Nat.mul(Nat.add(b, Nat.mul(p, b)), c) == Nat.add(Nat.mul(b, c), _) : Nat}
336 add_mul(b, Nat.mul(p, b), c)
337
338# The order a <= b on naturals, as a reusable proposition.
339def le(a: Nat, b: Nat) -> Data:
340 {Nat.is_le(a, b) == True{} : Bool}
341
342# The strict order a < b on naturals, as a reusable proposition.
343def lt(a: Nat, b: Nat) -> Data:
344 {Nat.is_lt(a, b) == True{} : Bool}
345
346# The order a >= b on naturals, as a reusable proposition.
347def ge(a: Nat, b: Nat) -> Data:
348 {Nat.is_ge(a, b) == True{} : Bool}
349
350# The strict order a > b on naturals, as a reusable proposition.
351def gt(a: Nat, b: Nat) -> Data:
352 {Nat.is_gt(a, b) == True{} : Bool}
353
354def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
355 %e : Bool.pick(Type, _, Empty, Unit)
356 Unit{}
357
358# Every natural is at most itself: a <= a.
359law le_refl:
360 for a: Nat
361 le(a, a)
362
363def le_refl(a):
364 match a:
365 case 0n:
366 {==}
367 case 1n+p:
368 le_refl(p)
369
370# Zero is at most every natural: 0 <= b.
371law zero_le:
372 for b: Nat
373 le(0n, b)
374
375def zero_le(b):
376 match b:
377 case 0n:
378 {==}
379 case 1n+p:
380 {==}
381
382# Every natural is at most its successor: n <= n + 1.
383law le_succ:
384 for n: Nat
385 le(n, 1n+n)
386
387def le_succ(n):
388 match n:
389 case 0n:
390 {==}
391 case 1n+p:
392 le_succ(p)
393
394# Adding on the right never decreases a natural: n <= n + k.
395law le_add_right:
396 for n: Nat
397 for k: Nat
398 le(n, Nat.add(n, k))
399
400def le_add_right(n, k):
401 match n:
402 case 0n:
403 zero_le(k)
404 case 1n+p:
405 le_add_right(p, k)
406
407# The order is transitive: a <= b and b <= c imply a <= c.
408law le_trans:
409 for a: Nat
410 for b: Nat
411 for c: Nat
412 for ab: le(a, b)
413 for bc: le(b, c)
414 le(a, c)
415
416def le_trans(a, b, c, ab, bc):
417 match a b c:
418 case 0n _ 0n:
419 {==}
420 case 0n _ 1n+r:
421 {==}
422 case 1n+p 0n _:
423 Empty.absurd(le(1n+p, c), internal_false_ne_true(ab))
424 case 1n+p 1n+q 0n:
425 Empty.absurd(le(1n+p, 0n), internal_false_ne_true(bc))
426 case 1n+p 1n+q 1n+r:
427 le_trans(p, q, r, ab, bc)
428
429# The order is antisymmetric: a <= b and b <= a imply a = b.
430law le_antisymm:
431 for a: Nat
432 for b: Nat
433 for ab: le(a, b)
434 for ba: le(b, a)
435 {a == b : Nat}
436
437def le_antisymm(a, b, ab, ba):
438 match a b:
439 case 0n 0n:
440 {==}
441 case 0n 1n+q:
442 Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(ba))
443 case 1n+p 0n:
444 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(ab))
445 case 1n+p 1n+q:
446 %le_antisymm(p, q, ab, ba) : {1n+p == 1n+_ : Nat}
447 {==}
448
449# The order is total: a <= b or b <= a.
450law le_total:
451 for a: Nat
452 for b: Nat
453 Or(le(a, b), le(b, a))
454
455def le_total(a, b):
456 match a b:
457 case 0n 0n:
458 Inl{{==}}
459 case 0n 1n+q:
460 Inl{{==}}
461 case 1n+p 0n:
462 Inr{{==}}
463 case 1n+p 1n+q:
464 le_total(p, q)
465
466# The order is total, as a reusable sum: a <= b or b <= a.
467law le_total_d:
468 for a: Nat
469 for b: Nat
470 Either<&2, &2, le(a, b), le(b, a)>
471
472def le_total_d(a, b):
473 match a b:
474 case 0n 0n:
475 Inl{{==}}
476 case 0n 1n+q:
477 Inl{{==}}
478 case 1n+p 0n:
479 Inr{{==}}
480 case 1n+p 1n+q:
481 le_total_d(p, q)
482
483# No natural is less than itself.
484law lt_irrefl:
485 for a: Nat
486 lt(a, a) -> Empty
487
488def lt_irrefl(a):
489 match a:
490 case 0n:
491 h => internal_false_ne_true(h)
492 case 1n+p:
493 lt_irrefl(p)
494
495# The strict order is transitive: a < b and b < c imply a < c.
496law lt_trans:
497 for a: Nat
498 for b: Nat
499 for c: Nat
500 for ab: lt(a, b)
501 for bc: lt(b, c)
502 lt(a, c)
503
504def lt_trans(a, b, c, ab, bc):
505 match a b c:
506 case 0n 0n _:
507 Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
508 case 0n 1n+q 0n:
509 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
510 case 0n 1n+q 1n+r:
511 {==}
512 case 1n+p 0n _:
513 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
514 case 1n+p 1n+q 0n:
515 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
516 case 1n+p 1n+q 1n+r:
517 lt_trans(p, q, r, ab, bc)
518
519# A strict inequality implies the weak one: a < b implies a <= b.
520law le_of_lt:
521 for a: Nat
522 for b: Nat
523 for h: lt(a, b)
524 le(a, b)
525
526def le_of_lt(a, b, h):
527 match a b:
528 case 0n 0n:
529 {==}
530 case 0n 1n+q:
531 {==}
532 case 1n+p 0n:
533 Empty.absurd(le(1n+p, 0n), internal_false_ne_true(h))
534 case 1n+p 1n+q:
535 le_of_lt(p, q, h)
536
537# Flipping a >= b gives b <= a.
538law le_of_ge:
539 for a: Nat
540 for b: Nat
541 for h: ge(a, b)
542 le(b, a)
543
544def le_of_ge(a, b, h):
545 match a b:
546 case 0n 0n:
547 {==}
548 case 0n 1n+q:
549 Empty.absurd(le(1n+q, 0n), internal_false_ne_true(h))
550 case 1n+p 0n:
551 {==}
552 case 1n+p 1n+q:
553 le_of_ge(p, q, h)
554
555# Flipping b <= a gives a >= b.
556law ge_of_le:
557 for a: Nat
558 for b: Nat
559 for h: le(b, a)
560 ge(a, b)
561
562def ge_of_le(a, b, h):
563 match a b:
564 case 0n 0n:
565 {==}
566 case 0n 1n+q:
567 Empty.absurd(ge(0n, 1n+q), internal_false_ne_true(h))
568 case 1n+p 0n:
569 {==}
570 case 1n+p 1n+q:
571 ge_of_le(p, q, h)
572
573# Flipping a > b gives b < a.
574law lt_of_gt:
575 for a: Nat
576 for b: Nat
577 for h: gt(a, b)
578 lt(b, a)
579
580def lt_of_gt(a, b, h):
581 match a b:
582 case 0n 0n:
583 Empty.absurd(lt(0n, 0n), internal_false_ne_true(h))
584 case 0n 1n+q:
585 Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(h))
586 case 1n+p 0n:
587 {==}
588 case 1n+p 1n+q:
589 lt_of_gt(p, q, h)
590
591# Flipping b < a gives a > b.
592law gt_of_lt:
593 for a: Nat
594 for b: Nat
595 for h: lt(b, a)
596 gt(a, b)
597
598def gt_of_lt(a, b, h):
599 match a b:
600 case 0n 0n:
601 Empty.absurd(gt(0n, 0n), internal_false_ne_true(h))
602 case 0n 1n+q:
603 Empty.absurd(gt(0n, 1n+q), internal_false_ne_true(h))
604 case 1n+p 0n:
605 {==}
606 case 1n+p 1n+q:
607 gt_of_lt(p, q, h)
608
609# Subtracting zero changes nothing: n - 0 = n.
610law sub_zero:
611 for n: Nat
612 {Nat.sub(n, 0n) == n : Nat}
613
614def sub_zero(n):
615 match n:
616 case 0n:
617 {==}
618 case 1n+p:
619 {==}
620
621# Truncated subtraction from zero is zero: 0 - n = 0.
622law zero_sub:
623 for n: Nat
624 {Nat.sub(0n, n) == 0n : Nat}
625
626def zero_sub(n):
627 match n:
628 case 0n:
629 {==}
630 case 1n+p:
631 {==}
632
633# A natural minus itself is zero: n - n = 0.
634law sub_self:
635 for n: Nat
636 {Nat.sub(n, n) == 0n : Nat}
637
638def sub_self(n):
639 match n:
640 case 0n:
641 {==}
642 case 1n+p:
643 sub_self(p)
644
645# Subtracting successors: (n + 1) - (m + 1) = n - m.
646law succ_sub_succ:
647 for -n: Nat
648 for -m: Nat
649 {Nat.sub(1n+n, 1n+m) == Nat.sub(n, m) : Nat}
650
651def succ_sub_succ(n, m):
652 {==}
653
654# Adding then subtracting m cancels: (n + m) - m = n.
655law add_sub_cancel:
656 for n: Nat
657 for m: Nat
658 {Nat.sub(Nat.add(n, m), m) == n : Nat}
659
660def add_sub_cancel(n, m):
661 match m:
662 case 0n:
663 +n = n
664 %Equal.sym(Nat, Nat.add(n, 0n), n, add_zero(n)) : {Nat.sub(_, 0n) == n : Nat}
665 sub_zero(n)
666 case 1n++q:
667 +n = n
668 %Equal.sym(Nat, Nat.add(n, 1n+q), 1n+Nat.add(n, q), add_succ(n, q)) : {Nat.sub(_, 1n+q) == n : Nat}
669 add_sub_cancel(n, q)
670
671# Adding then subtracting n cancels: (n + m) - n = m.
672law add_sub_cancel_left:
673 for n: Nat
674 for m: Nat
675 {Nat.sub(Nat.add(n, m), n) == m : Nat}
676
677def add_sub_cancel_left(n, m):
678 match n:
679 case 0n:
680 sub_zero(m)
681 case 1n+p:
682 add_sub_cancel_left(p, m)
683
684# If m <= n, subtracting and adding m back gives n: (n - m) + m = n.
685law sub_add_cancel:
686 for n: Nat
687 for m: Nat
688 for h: le(m, n)
689 {Nat.add(Nat.sub(n, m), m) == n : Nat}
690
691def sub_add_cancel(n, m, h):
692 match n m:
693 case 0n 0n:
694 {==}
695 case 0n 1n+q:
696 Empty.absurd({1n+q == 0n : Nat}, internal_false_ne_true(h))
697 case 1n++p 0n:
698 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
699 {==}
700 case 1n++p 1n++q:
701 %Equal.sym(Nat, Nat.add(Nat.sub(p, q), 1n+q), 1n+Nat.add(Nat.sub(p, q), q), add_succ(Nat.sub(p, q), q)) : {_ == 1n+p : Nat}
702 %Equal.sym(Nat, Nat.add(Nat.sub(p, q), q), p, sub_add_cancel(p, q, h)) : {1n+_ == 1n+p : Nat}
703 {==}
704
705# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k).
706law sub_sub:
707 for n: Nat
708 for m: Nat
709 for k: Nat
710 {Nat.sub(Nat.sub(n, m), k) == Nat.sub(n, Nat.add(m, k)) : Nat}
711
712def sub_sub(n, m, k):
713 match n m:
714 case 0n 0n:
715 {==}
716 case 0n 1n+q:
717 zero_sub(k)
718 case 1n+p 0n:
719 {==}
720 case 1n+p 1n+q:
721 sub_sub(p, q, k)
722
723# Truncated subtraction never increases: n - m <= n.
724law sub_le:
725 for n: Nat
726 for m: Nat
727 le(Nat.sub(n, m), n)
728
729def sub_le(n, m):
730 match n m:
731 case 0n 0n:
732 {==}
733 case 0n 1n+q:
734 {==}
735 case 1n+p 0n:
736 le_refl(1n+p)
737 case 1n++p 1n++q:
738 le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), le_succ(p))
739
740# Minimum is commutative.
741law min_comm:
742 for a: Nat
743 for b: Nat
744 {Nat.min(a, b) == Nat.min(b, a) : Nat}
745
746def min_comm(a, b):
747 match a b:
748 case 0n 0n:
749 {==}
750 case 0n 1n+q:
751 {==}
752 case 1n+p 0n:
753 {==}
754 case 1n++p 1n++q:
755 %min_comm(p, q) : {1n+Nat.min(p, q) == 1n+_ : Nat}
756 {==}
757
758# Maximum is commutative.
759law max_comm:
760 for a: Nat
761 for b: Nat
762 {Nat.max(a, b) == Nat.max(b, a) : Nat}
763
764def max_comm(a, b):
765 match a b:
766 case 0n 0n:
767 {==}
768 case 0n 1n+q:
769 {==}
770 case 1n+p 0n:
771 {==}
772 case 1n++p 1n++q:
773 %max_comm(p, q) : {1n+Nat.max(p, q) == 1n+_ : Nat}
774 {==}
775
776# The minimum of a natural and itself is itself.
777law min_self:
778 for a: Nat
779 {Nat.min(a, a) == a : Nat}
780
781def min_self(a):
782 match a:
783 case 0n:
784 {==}
785 case 1n++p:
786 %min_self(p) : {1n+Nat.min(p, p) == 1n+_ : Nat}
787 {==}
788
789# The maximum of a natural and itself is itself.
790law max_self:
791 for a: Nat
792 {Nat.max(a, a) == a : Nat}
793
794def max_self(a):
795 match a:
796 case 0n:
797 {==}
798 case 1n++p:
799 %max_self(p) : {1n+Nat.max(p, p) == 1n+_ : Nat}
800 {==}
801
802# The minimum with zero is zero: min(a, 0) = 0.
803law min_zero:
804 for a: Nat
805 {Nat.min(a, 0n) == 0n : Nat}
806
807def min_zero(a):
808 match a:
809 case 0n:
810 {==}
811 case 1n+p:
812 {==}
813
814# The minimum with zero is zero: min(0, a) = 0.
815law zero_min:
816 for a: Nat
817 {Nat.min(0n, a) == 0n : Nat}
818
819def zero_min(a):
820 match a:
821 case 0n:
822 {==}
823 case 1n+p:
824 {==}
825
826# Zero is an identity for maximum: max(a, 0) = a.
827law max_zero:
828 for a: Nat
829 {Nat.max(a, 0n) == a : Nat}
830
831def max_zero(a):
832 match a:
833 case 0n:
834 {==}
835 case 1n+p:
836 {==}
837
838# Zero is an identity for maximum: max(0, a) = a.
839law zero_max:
840 for a: Nat
841 {Nat.max(0n, a) == a : Nat}
842
843def zero_max(a):
844 match a:
845 case 0n:
846 {==}
847 case 1n+p:
848 {==}
849
850# Minimum is associative.
851law min_assoc:
852 for a: Nat
853 for b: Nat
854 for c: Nat
855 {Nat.min(Nat.min(a, b), c) == Nat.min(a, Nat.min(b, c)) : Nat}
856
857def min_assoc(a, b, c):
858 match a b c:
859 case 0n _ _:
860 {==}
861 case 1n+p 0n _:
862 {==}
863 case 1n+p 1n+q 0n:
864 {==}
865 case 1n++p 1n++q 1n++r:
866 %min_assoc(p, q, r) : {1n+Nat.min(Nat.min(p, q), r) == 1n+_ : Nat}
867 {==}
868
869# Maximum is associative.
870law max_assoc:
871 for a: Nat
872 for b: Nat
873 for c: Nat
874 {Nat.max(Nat.max(a, b), c) == Nat.max(a, Nat.max(b, c)) : Nat}
875
876def max_assoc(a, b, c):
877 match a b c:
878 case 0n _ _:
879 {==}
880 case 1n+p 0n _:
881 {==}
882 case 1n+p 1n+q 0n:
883 {==}
884 case 1n++p 1n++q 1n++r:
885 %max_assoc(p, q, r) : {1n+Nat.max(Nat.max(p, q), r) == 1n+_ : Nat}
886 {==}
887
888# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
889law min_add_max:
890 for a: Nat
891 for b: Nat
892 {Nat.add(Nat.min(a, b), Nat.max(a, b)) == Nat.add(a, b) : Nat}
893
894def min_add_max(a, b):
895 match a b:
896 case 0n 0n:
897 {==}
898 case 0n 1n+q:
899 {==}
900 case 1n++p 0n:
901 %add_zero(p) : {1n+_ == 1n+Nat.add(p, 0n) : Nat}
902 {==}
903 case 1n++p 1n++q:
904 %Equal.sym(Nat, Nat.add(Nat.min(p, q), 1n+Nat.max(p, q)), 1n+Nat.add(Nat.min(p, q), Nat.max(p, q)), add_succ(Nat.min(p, q), Nat.max(p, q))) : {1n+_ == 1n+Nat.add(p, 1n+q) : Nat}
905 %Equal.sym(Nat, Nat.add(p, 1n+q), 1n+Nat.add(p, q), add_succ(p, q)) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 1n+_ : Nat}
906 %min_add_max(p, q) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 2n+_ : Nat}
907 {==}
908
909# The minimum is at most its left argument.
910law min_le_left:
911 for a: Nat
912 for b: Nat
913 le(Nat.min(a, b), a)
914
915def min_le_left(a, b):
916 match a b:
917 case 0n 0n:
918 {==}
919 case 0n 1n+q:
920 {==}
921 case 1n+p 0n:
922 {==}
923 case 1n+p 1n+q:
924 min_le_left(p, q)
925
926# The minimum is at most its right argument.
927law min_le_right:
928 for a: Nat
929 for b: Nat
930 le(Nat.min(a, b), b)
931
932def min_le_right(a, b):
933 match a b:
934 case 0n 0n:
935 {==}
936 case 0n 1n+q:
937 {==}
938 case 1n+p 0n:
939 {==}
940 case 1n+p 1n+q:
941 min_le_right(p, q)
942
943# The left argument is at most the maximum.
944law le_max_left:
945 for a: Nat
946 for b: Nat
947 le(a, Nat.max(a, b))
948
949def le_max_left(a, b):
950 match a b:
951 case 0n 0n:
952 {==}
953 case 0n 1n+q:
954 {==}
955 case 1n+p 0n:
956 le_refl(1n+p)
957 case 1n+p 1n+q:
958 le_max_left(p, q)
959
960# The right argument is at most the maximum.
961law le_max_right:
962 for a: Nat
963 for b: Nat
964 le(b, Nat.max(a, b))
965
966def le_max_right(a, b):
967 match a b:
968 case 0n 0n:
969 {==}
970 case 0n 1n+q:
971 le_refl(1n+q)
972 case 1n+p 0n:
973 {==}
974 case 1n+p 1n+q:
975 le_max_right(p, q)
976
977# Any natural to the power zero is one.
978law pow_zero:
979 for -a: Nat
980 {Nat.pow(a, 0n) == 1n : Nat}
981
982def pow_zero(a):
983 {==}
984
985# A power with a successor exponent: a^(n+1) = a * a^n.
986law pow_succ:
987 for -a: Nat
988 for -n: Nat
989 {Nat.pow(a, 1n+n) == Nat.mul(a, Nat.pow(a, n)) : Nat}
990
991def pow_succ(a, n):
992 {==}
993
994# Any natural to the power one is itself.
995law pow_one:
996 for a: Nat
997 {Nat.pow(a, 1n) == a : Nat}
998
999def pow_one(a):
1000 mul_one(a)
1001
1002# One to any power is one.
1003law one_pow:
1004 for n: Nat
1005 {Nat.pow(1n, n) == 1n : Nat}
1006
1007def one_pow(n):
1008 match n:
1009 case 0n:
1010 {==}
1011 case 1n++p:
1012 %Equal.sym(Nat, Nat.mul(1n, Nat.pow(1n, p)), Nat.pow(1n, p), one_mul(Nat.pow(1n, p))) : {_ == 1n : Nat}
1013 one_pow(p)
1014
1015# Exponents add under multiplication: a^(m+n) = a^m * a^n.
1016law pow_add:
1017 for a: Nat
1018 for m: Nat
1019 for n: Nat
1020 {Nat.pow(a, Nat.add(m, n)) == Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) : Nat}
1021
1022def pow_add(a, m, n):
1023 match m:
1024 case 0n:
1025 +a = a
1026 +n = n
1027 %Equal.sym(Nat, Nat.mul(1n, Nat.pow(a, n)), Nat.pow(a, n), one_mul(Nat.pow(a, n))) : {Nat.pow(a, n) == _ : Nat}
1028 {==}
1029 case 1n++p:
1030 +a = a
1031 +n = n
1032 %Equal.sym(Nat, Nat.pow(a, Nat.add(p, n)), Nat.mul(Nat.pow(a, p), Nat.pow(a, n)), pow_add(a, p, n)) : {Nat.mul(a, _) == Nat.mul(Nat.mul(a, Nat.pow(a, p)), Nat.pow(a, n)) : Nat}
1033 Equal.sym(Nat, Nat.mul(Nat.mul(a, Nat.pow(a, p)), Nat.pow(a, n)), Nat.mul(a, Nat.mul(Nat.pow(a, p), Nat.pow(a, n))), mul_assoc(a, Nat.pow(a, p), Nat.pow(a, n)))
1034
1035# Doubling is adding a natural to itself.
1036law double_eq_add:
1037 for n: Nat
1038 {Nat.double(n) == Nat.add(n, n) : Nat}
1039
1040def double_eq_add(n):
1041 match n:
1042 case 0n:
1043 {==}
1044 case 1n++p:
1045 %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
1046 %double_eq_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
1047 {==}
1048
1049# Every natural tests equal to itself.
1050law is_eq_refl:
1051 for n: Nat
1052 {Nat.is_eq(n, n) == True{} : Bool}
1053
1054def is_eq_refl(n):
1055 match n:
1056 case 0n:
1057 {==}
1058 case 1n+p:
1059 is_eq_refl(p)
1060
1061# The equality test is symmetric.
1062law is_eq_comm:
1063 for a: Nat
1064 for b: Nat
1065 {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1066
1067def is_eq_comm(a, b):
1068 match a b:
1069 case 0n 0n:
1070 {==}
1071 case 0n 1n+q:
1072 {==}
1073 case 1n+p 0n:
1074 {==}
1075 case 1n++p 1n++q:
1076 %is_eq_comm(p, q) : {Nat.is_eq(p, q) == _ : Bool}
1077 {==}
1078
1079# If the equality test says true, the naturals are equal.
1080law eq_of_is_eq:
1081 for a: Nat
1082 for b: Nat
1083 for h: {Nat.is_eq(a, b) == True{} : Bool}
1084 {a == b : Nat}
1085
1086def eq_of_is_eq(a, b, h):
1087 match a b:
1088 case 0n 0n:
1089 {==}
1090 case 0n 1n+q:
1091 Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(h))
1092 case 1n+p 0n:
1093 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1094 case 1n++p 1n++q:
1095 %eq_of_is_eq(p, q, h) : {1n+p == 1n+_ : Nat}
1096 {==}
1097
1098# A >= b tests the same as b <= a.
1099law is_ge_eq_is_le:
1100 for a: Nat
1101 for b: Nat
1102 {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}
1103
1104def is_ge_eq_is_le(a, b):
1105 match a b:
1106 case 0n 0n:
1107 {==}
1108 case 0n 1n+q:
1109 {==}
1110 case 1n+p 0n:
1111 {==}
1112 case 1n++p 1n++q:
1113 %is_ge_eq_is_le(p, q) : {Nat.is_ge(p, q) == _ : Bool}
1114 {==}
1115
1116# A > b tests the same as b < a.
1117law is_gt_eq_is_lt:
1118 for a: Nat
1119 for b: Nat
1120 {Nat.is_gt(a, b) == Nat.is_lt(b, a) : Bool}
1121
1122def is_gt_eq_is_lt(a, b):
1123 match a b:
1124 case 0n 0n:
1125 {==}
1126 case 0n 1n+q:
1127 {==}
1128 case 1n+p 0n:
1129 {==}
1130 case 1n++p 1n++q:
1131 %is_gt_eq_is_lt(p, q) : {Nat.is_gt(p, q) == _ : Bool}
1132 {==}
1133
1134# A < b tests the same as a + 1 <= b.
1135law is_lt_eq_succ_le:
1136 for a: Nat
1137 for b: Nat
1138 {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}
1139
1140def is_lt_eq_succ_le(a, b):
1141 match a b:
1142 case 0n 0n:
1143 {==}
1144 case 0n 1n+q:
1145 match q:
1146 case 0n:
1147 {==}
1148 case 1n+r:
1149 {==}
1150 case 1n+p 0n:
1151 {==}
1152 case 1n+p 1n+q:
1153 is_lt_eq_succ_le(p, q)
1154
1155# Not (a <= b) tests the same as b < a.
1156law not_is_le:
1157 for a: Nat
1158 for b: Nat
1159 {Bool.not(Nat.is_le(a, b)) == Nat.is_lt(b, a) : Bool}
1160
1161def not_is_le(a, b):
1162 match a b:
1163 case 0n 0n:
1164 {==}
1165 case 0n 1n+q:
1166 {==}
1167 case 1n+p 0n:
1168 {==}
1169 case 1n+p 1n+q:
1170 not_is_le(p, q)
1171
1172# Not (a < b) tests the same as b <= a.
1173law not_is_lt:
1174 for a: Nat
1175 for b: Nat
1176 {Bool.not(Nat.is_lt(a, b)) == Nat.is_le(b, a) : Bool}
1177
1178def not_is_lt(a, b):
1179 match a b:
1180 case 0n 0n:
1181 {==}
1182 case 0n 1n+q:
1183 {==}
1184 case 1n+p 0n:
1185 {==}
1186 case 1n+p 1n+q:
1187 not_is_lt(p, q)
1188
1189# Every natural is less than its successor: n < n + 1.
1190law lt_succ_self:
1191 for n: Nat
1192 lt(n, 1n+n)
1193
1194def lt_succ_self(n):
1195 match n:
1196 case 0n:
1197 {==}
1198 case 1n+p:
1199 lt_succ_self(p)
1200
1201# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1202law succ_le_succ:
1203 for -a: Nat
1204 for -b: Nat
1205 for h: le(a, b)
1206 le(1n+a, 1n+b)
1207
1208def succ_le_succ(a, b, h):
1209 h
1210
1211# The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
1212law le_of_succ_le_succ:
1213 for -a: Nat
1214 for -b: Nat
1215 for h: le(1n+a, 1n+b)
1216 le(a, b)
1217
1218def le_of_succ_le_succ(a, b, h):
1219 h
1220
1221# A < b and b <= c imply a < c.
1222law lt_of_lt_of_le:
1223 for a: Nat
1224 for b: Nat
1225 for c: Nat
1226 for ab: lt(a, b)
1227 for bc: le(b, c)
1228 lt(a, c)
1229
1230def lt_of_lt_of_le(a, b, c, ab, bc):
1231 match a b c:
1232 case 0n 0n _:
1233 Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
1234 case 0n 1n+q 0n:
1235 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1236 case 0n 1n+q 1n+r:
1237 {==}
1238 case 1n+p 0n _:
1239 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1240 case 1n+p 1n+q 0n:
1241 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1242 case 1n+p 1n+q 1n+r:
1243 lt_of_lt_of_le(p, q, r, ab, bc)
1244
1245# A <= b and b < c imply a < c.
1246law lt_of_le_of_lt:
1247 for a: Nat
1248 for b: Nat
1249 for c: Nat
1250 for ab: le(a, b)
1251 for bc: lt(b, c)
1252 lt(a, c)
1253
1254def lt_of_le_of_lt(a, b, c, ab, bc):
1255 match a b c:
1256 case 0n 0n 0n:
1257 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1258 case 0n 1n+q 0n:
1259 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1260 case 0n _ 1n+r:
1261 {==}
1262 case 1n+p 0n _:
1263 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1264 case 1n+p 1n+q 0n:
1265 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1266 case 1n+p 1n+q 1n+r:
1267 lt_of_le_of_lt(p, q, r, ab, bc)
1268
1269# Adding on the left preserves the order: a <= b implies k + a <= k + b.
1270law add_le_add_left:
1271 for -a: Nat
1272 for -b: Nat
1273 for k: Nat
1274 for h: le(a, b)
1275 le(Nat.add(k, a), Nat.add(k, b))
1276
1277def add_le_add_left(a, b, k, h):
1278 match k:
1279 case 0n:
1280 h
1281 case 1n+p:
1282 add_le_add_left(a, b, p, h)
1283
1284# The only natural at most zero is zero.
1285law le_zero_eq:
1286 for n: Nat
1287 for h: le(n, 0n)
1288 {n == 0n : Nat}
1289
1290def le_zero_eq(n, h):
1291 match n:
1292 case 0n:
1293 {==}
1294 case 1n+p:
1295 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1296
1297# No natural is less than zero.
1298law lt_zero:
1299 for n: Nat
1300 lt(n, 0n) -> Empty
1301
1302def lt_zero(n):
1303 match n:
1304 case 0n:
1305 h => internal_false_ne_true(h)
1306 case 1n+p:
1307 h => internal_false_ne_true(h)
1308
1309# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
1310
1311# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
1312law add_zero_sym:
1313 for x: Nat
1314 {x == Nat.add(x, 0n) : Nat}
1315
1316def add_zero_sym(x):
1317 Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
1318
1319# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
1320law zero_add_sym:
1321 for -x: Nat
1322 {x == Nat.add(0n, x) : Nat}
1323
1324def zero_add_sym(x):
1325 Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
1326
1327# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
1328law add_succ_sym:
1329 for n: Nat
1330 for -m: Nat
1331 {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
1332
1333def add_succ_sym(n, m):
1334 Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
1335
1336# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
1337law succ_add_sym:
1338 for -n: Nat
1339 for -m: Nat
1340 {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
1341
1342def succ_add_sym(n, m):
1343 Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
1344
1345# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
1346law add_comm_sym:
1347 for n: Nat
1348 for m: Nat
1349 {Nat.add(m, n) == Nat.add(n, m) : Nat}
1350
1351def add_comm_sym(n, m):
1352 Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
1353
1354# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
1355law add_assoc_sym:
1356 for a: Nat
1357 for -b: Nat
1358 for -c: Nat
1359 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
1360
1361def add_assoc_sym(a, b, c):
1362 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
1363
1364# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
1365law add_left_comm_sym:
1366 for a: Nat
1367 for b: Nat
1368 for -c: Nat
1369 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
1370
1371def add_left_comm_sym(a, b, c):
1372 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
1373
1374# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
1375law add_right_comm_sym:
1376 for a: Nat
1377 for b: Nat
1378 for c: Nat
1379 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
1380
1381def add_right_comm_sym(a, b, c):
1382 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
1383
1384# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
1385law add_add_add_comm_sym:
1386 for a: Nat
1387 for b: Nat
1388 for c: Nat
1389 for -d: Nat
1390 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
1391
1392def add_add_add_comm_sym(a, b, c, d):
1393 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))
1394
1395# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
1396law mul_zero_sym:
1397 for x: Nat
1398 {0n == Nat.mul(x, 0n) : Nat}
1399
1400def mul_zero_sym(x):
1401 Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
1402
1403# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
1404law zero_mul_sym:
1405 for -x: Nat
1406 {0n == Nat.mul(0n, x) : Nat}
1407
1408def zero_mul_sym(x):
1409 Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
1410
1411# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
1412law mul_one_sym:
1413 for x: Nat
1414 {x == Nat.mul(x, 1n) : Nat}
1415
1416def mul_one_sym(x):
1417 Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
1418
1419# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
1420law one_mul_sym:
1421 for x: Nat
1422 {x == Nat.mul(1n, x) : Nat}
1423
1424def one_mul_sym(x):
1425 Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
1426
1427# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
1428law mul_succ_sym:
1429 for n: Nat
1430 for m: Nat
1431 {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
1432
1433def mul_succ_sym(n, m):
1434 Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
1435
1436# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
1437law succ_mul_sym:
1438 for n: Nat
1439 for m: Nat
1440 {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
1441
1442def succ_mul_sym(n, m):
1443 Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
1444
1445# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
1446law mul_comm_sym:
1447 for n: Nat
1448 for m: Nat
1449 {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
1450
1451def mul_comm_sym(n, m):
1452 Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
1453
1454# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
1455law add_mul_sym:
1456 for a: Nat
1457 for -b: Nat
1458 for c: Nat
1459 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
1460
1461def add_mul_sym(a, b, c):
1462 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))
1463
1464# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
1465law mul_add_sym:
1466 for a: Nat
1467 for b: Nat
1468 for c: Nat
1469 {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
1470
1471def mul_add_sym(a, b, c):
1472 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))
1473
1474# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
1475law mul_assoc_sym:
1476 for a: Nat
1477 for b: Nat
1478 for c: Nat
1479 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
1480
1481def mul_assoc_sym(a, b, c):
1482 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
1483
1484# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
1485law sub_zero_sym:
1486 for n: Nat
1487 {n == Nat.sub(n, 0n) : Nat}
1488
1489def sub_zero_sym(n):
1490 Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
1491
1492# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
1493law zero_sub_sym:
1494 for n: Nat
1495 {0n == Nat.sub(0n, n) : Nat}
1496
1497def zero_sub_sym(n):
1498 Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
1499
1500# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
1501law sub_self_sym:
1502 for n: Nat
1503 {0n == Nat.sub(n, n) : Nat}
1504
1505def sub_self_sym(n):
1506 Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
1507
1508# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
1509law succ_sub_succ_sym:
1510 for -n: Nat
1511 for -m: Nat
1512 {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
1513
1514def succ_sub_succ_sym(n, m):
1515 Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
1516
1517# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
1518law add_sub_cancel_sym:
1519 for n: Nat
1520 for m: Nat
1521 {n == Nat.sub(Nat.add(n, m), m) : Nat}
1522
1523def add_sub_cancel_sym(n, m):
1524 Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
1525
1526# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
1527law add_sub_cancel_left_sym:
1528 for n: Nat
1529 for m: Nat
1530 {m == Nat.sub(Nat.add(n, m), n) : Nat}
1531
1532def add_sub_cancel_left_sym(n, m):
1533 Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
1534
1535# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
1536law sub_sub_sym:
1537 for n: Nat
1538 for m: Nat
1539 for k: Nat
1540 {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
1541
1542def sub_sub_sym(n, m, k):
1543 Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
1544
1545# Minimum is commutative, reversed to rewrite toward the simple side.
1546law min_comm_sym:
1547 for a: Nat
1548 for b: Nat
1549 {Nat.min(b, a) == Nat.min(a, b) : Nat}
1550
1551def min_comm_sym(a, b):
1552 Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
1553
1554# Maximum is commutative, reversed to rewrite toward the simple side.
1555law max_comm_sym:
1556 for a: Nat
1557 for b: Nat
1558 {Nat.max(b, a) == Nat.max(a, b) : Nat}
1559
1560def max_comm_sym(a, b):
1561 Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
1562
1563# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
1564law min_self_sym:
1565 for a: Nat
1566 {a == Nat.min(a, a) : Nat}
1567
1568def min_self_sym(a):
1569 Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
1570
1571# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
1572law max_self_sym:
1573 for a: Nat
1574 {a == Nat.max(a, a) : Nat}
1575
1576def max_self_sym(a):
1577 Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
1578
1579# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
1580law min_zero_sym:
1581 for a: Nat
1582 {0n == Nat.min(a, 0n) : Nat}
1583
1584def min_zero_sym(a):
1585 Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
1586
1587# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
1588law zero_min_sym:
1589 for a: Nat
1590 {0n == Nat.min(0n, a) : Nat}
1591
1592def zero_min_sym(a):
1593 Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
1594
1595# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
1596law max_zero_sym:
1597 for a: Nat
1598 {a == Nat.max(a, 0n) : Nat}
1599
1600def max_zero_sym(a):
1601 Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
1602
1603# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
1604law zero_max_sym:
1605 for a: Nat
1606 {a == Nat.max(0n, a) : Nat}
1607
1608def zero_max_sym(a):
1609 Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
1610
1611# Minimum is associative, reversed to rewrite toward the simple side.
1612law min_assoc_sym:
1613 for a: Nat
1614 for b: Nat
1615 for c: Nat
1616 {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
1617
1618def min_assoc_sym(a, b, c):
1619 Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
1620
1621# Maximum is associative, reversed to rewrite toward the simple side.
1622law max_assoc_sym:
1623 for a: Nat
1624 for b: Nat
1625 for c: Nat
1626 {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
1627
1628def max_assoc_sym(a, b, c):
1629 Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
1630
1631# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
1632law min_add_max_sym:
1633 for a: Nat
1634 for b: Nat
1635 {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
1636
1637def min_add_max_sym(a, b):
1638 Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
1639
1640# Any natural to the power zero is one, reversed to rewrite toward the simple side.
1641law pow_zero_sym:
1642 for -a: Nat
1643 {1n == Nat.pow(a, 0n) : Nat}
1644
1645def pow_zero_sym(a):
1646 Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
1647
1648# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
1649law pow_succ_sym:
1650 for -a: Nat
1651 for -n: Nat
1652 {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
1653
1654def pow_succ_sym(a, n):
1655 Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
1656
1657# Any natural to the power one is itself, reversed to rewrite toward the simple side.
1658law pow_one_sym:
1659 for a: Nat
1660 {a == Nat.pow(a, 1n) : Nat}
1661
1662def pow_one_sym(a):
1663 Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
1664
1665# One to any power is one, reversed to rewrite toward the simple side.
1666law one_pow_sym:
1667 for n: Nat
1668 {1n == Nat.pow(1n, n) : Nat}
1669
1670def one_pow_sym(n):
1671 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
1672
1673# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
1674law pow_add_sym:
1675 for a: Nat
1676 for m: Nat
1677 for n: Nat
1678 {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
1679
1680def pow_add_sym(a, m, n):
1681 Equal.sym(Nat, Nat.pow(a, Nat.add(m, n)), Nat.mul(Nat.pow(a, m), Nat.pow(a, n)), pow_add(a, m, n))
1682
1683# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
1684law double_eq_add_sym:
1685 for n: Nat
1686 {Nat.add(n, n) == Nat.double(n) : Nat}
1687
1688def double_eq_add_sym(n):
1689 Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
1690
1691# Every natural tests equal to itself, reversed to rewrite toward the simple side.
1692law is_eq_refl_sym:
1693 for n: Nat
1694 {True{} == Nat.is_eq(n, n) : Bool}
1695
1696def is_eq_refl_sym(n):
1697 Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
1698
1699# The equality test is symmetric, reversed to rewrite toward the simple side.
1700law is_eq_comm_sym:
1701 for a: Nat
1702 for b: Nat
1703 {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
1704
1705def is_eq_comm_sym(a, b):
1706 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
1707
1708# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
1709law is_ge_eq_is_le_sym:
1710 for a: Nat
1711 for b: Nat
1712 {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
1713
1714def is_ge_eq_is_le_sym(a, b):
1715 Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
1716
1717# A > b tests the same as b < a, reversed to rewrite toward the simple side.
1718law is_gt_eq_is_lt_sym:
1719 for a: Nat
1720 for b: Nat
1721 {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
1722
1723def is_gt_eq_is_lt_sym(a, b):
1724 Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
1725
1726# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
1727law is_lt_eq_succ_le_sym:
1728 for a: Nat
1729 for b: Nat
1730 {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
1731
1732def is_lt_eq_succ_le_sym(a, b):
1733 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
1734
1735# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
1736law not_is_le_sym:
1737 for a: Nat
1738 for b: Nat
1739 {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
1740
1741def not_is_le_sym(a, b):
1742 Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
1743
1744# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
1745law not_is_lt_sym:
1746 for a: Nat
1747 for b: Nat
1748 {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
1749
1750def not_is_lt_sym(a, b):
1751 Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))