nat.bend
bend-mathlib@0.5.0.0 · 2,367 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
740def internal_div_true_ne_false(h: {True{} == False{} : Bool}) -> Empty:
741 internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h))
742
743def internal_div_add_zero_r(a: Nat) -> {a == Nat.add(a, 0n) : Nat}:
744 Equal.sym(Nat, Nat.add(a, 0n), a, add_zero(a))
745
746def internal_div_le_refl(a: Nat) -> {True{} == Nat.is_le(a, a) : Bool}:
747 Equal.sym(Bool, Nat.is_le(a, a), True{}, le_refl(a))
748
749def internal_div_zero_le(x: Nat) -> {True{} == Nat.is_le(0n, x) : Bool}:
750 Equal.sym(Bool, Nat.is_le(0n, x), True{}, zero_le(x))
751
752def internal_div_block_start(-bp: Nat, +r: Nat, h: {bp == Nat.add(r, 0n) : Nat}) -> {bp == r : Nat}:
753 %add_zero(r) : {bp == _ : Nat}
754 h
755
756def internal_div_block_step(-bp: Nat, r: Nat, -mp: Nat, h: {bp == Nat.add(r, 1n+mp) : Nat}) -> {bp == 1n+Nat.add(r, mp) : Nat}:
757 %add_succ(r, mp) : {bp == _ : Nat}
758 h
759
760def internal_div_go_eq(n: Nat, m: Nat, +bp: Nat, +d: Nat, +r: Nat, +h: {bp == Nat.add(r, m) : Nat}) -> {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r))) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}:
761 match n m:
762 case 0n _:
763 {==}
764 case 1n++np 0n:
765 %add_succ(np, Nat.add(Nat.mul(d, 1n+bp), r)) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == _ : Nat}
766 %add_comm(r, Nat.mul(d, 1n+bp)) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == Nat.add(np, 1n+_) : Nat}
767 %internal_div_block_start(bp, r, h) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == Nat.add(np, 1n+Nat.add(_, Nat.mul(d, 1n+bp))) : Nat}
768 %add_zero(Nat.add(bp, Nat.mul(d, 1n+bp))) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))) == Nat.add(np, 1n+_) : Nat}
769 internal_div_go_eq(np, r, bp, 1n+d, 0n, internal_div_block_start(bp, r, h))
770 case 1n++np 1n++mp:
771 %add_succ(np, Nat.add(Nat.mul(d, 1n+bp), r)) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))) == _ : Nat}
772 %add_succ(Nat.mul(d, 1n+bp), r) : {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))) == Nat.add(np, _) : Nat}
773 internal_div_go_eq(np, mp, bp, d, 1n+r, internal_div_block_step(bp, r, mp, h))
774
775# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a.
776law div_mod_eq:
777 for +a: Nat
778 for +b: Nat
779 {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == a : Nat}
780
781def div_mod_eq(a, b):
782 %add_zero(a) : {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == _ : Nat}
783 internal_div_go_eq(a, b, b, 0n, 0n, {==})
784
785def internal_div_wit_succ(+ap: Nat, +bq: Nat, w: &k:Nat -> {Nat.add(ap, k) == bq : Nat}) -> &k:Nat -> {Nat.add(1n+ap, k) == 1n+bq : Nat}:
786 match w:
787 case (k, e):
788 (k, Equal.cong(Nat, Nat, x => 1n+x, Nat.add(ap, k), bq, e))
789
790def internal_div_le_wit(a: Nat, b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> &k:Nat -> {Nat.add(a, k) == b : Nat}:
791 match a b:
792 case 0n y:
793 (y, {==})
794 case 1n+ap 0n:
795 Empty.absurd(&k:Nat -> {Nat.add(1n+ap, k) == 0n : Nat}, internal_false_ne_true(h))
796 case 1n++ap 1n++bq:
797 internal_div_wit_succ(ap, bq, internal_div_le_wit(ap, bq, h))
798
799def internal_div_go_small(n: Nat, +k: Nat, +d: Nat, r: Nat) -> {d == Pair.fst(Nat, Nat, Nat.divmod.go(n, Nat.add(n, k), d, r)) : Nat}:
800 match n:
801 case 0n:
802 {==}
803 case 1n+np:
804 internal_div_go_small(np, k, d, 1n+r)
805
806def internal_div_zero_of_wit(+a: Nat, +b: Nat, w: &k:Nat -> {Nat.add(a, k) == b : Nat}) -> {Nat.div(a, 1n+b) == 0n : Nat}:
807 match w:
808 case (+k, e):
809 %e : {Nat.div(a, 1n+_) == 0n : Nat}
810 Equal.sym(Nat, 0n, Pair.fst(Nat, Nat, Nat.divmod.go(a, Nat.add(a, k), 0n, 0n)), internal_div_go_small(a, k, 0n, 0n))
811
812# A number at most b divides by 1 + b to zero: a <= b implies a / (1 + b) = 0.
813law div_eq_zero_of_le:
814 for +a: Nat
815 for +b: Nat
816 for h: le(a, b)
817 {Nat.div(a, 1n+b) == 0n : Nat}
818
819def div_eq_zero_of_le(a, b, h):
820 internal_div_zero_of_wit(a, b, internal_div_le_wit(a, b, h))
821
822def internal_div_le_succ_r(j: Nat, d: Nat, h: {True{} == Nat.is_le(j, d) : Bool}) -> {True{} == Nat.is_le(j, 1n+d) : Bool}:
823 match j d:
824 case 0n _:
825 {==}
826 case 1n+i 0n:
827 Empty.absurd({True{} == Nat.is_le(1n+i, 1n) : Bool}, internal_div_true_ne_false(h))
828 case 1n+i 1n+e:
829 internal_div_le_succ_r(i, e, h)
830
831def internal_div_go_d_ge(+j: Nat, n: Nat, m: Nat, +d: Nat, r: Nat, h: {True{} == Nat.is_le(j, d) : Bool}) -> {True{} == Nat.is_le(j, Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r))) : Bool}:
832 match n m:
833 case 0n _:
834 h
835 case 1n+np 0n:
836 internal_div_go_d_ge(j, np, r, 1n+d, 0n, internal_div_le_succ_r(j, d, h))
837 case 1n+np 1n+mp:
838 internal_div_go_d_ge(j, np, mp, d, 1n+r, h)
839
840def internal_div_mono_go(a: Nat, m: Nat, +d: Nat, r: Nat, +k: Nat) -> {True{} == Nat.is_le(Pair.fst(Nat, Nat, Nat.divmod.go(a, m, d, r)), Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(a, k), m, d, r))) : Bool}:
841 match a m:
842 case 0n _:
843 internal_div_go_d_ge(d, k, m, d, r, internal_div_le_refl(d))
844 case 1n+ap 0n:
845 internal_div_mono_go(ap, r, 1n+d, 0n, k)
846 case 1n+ap 1n+mp:
847 internal_div_mono_go(ap, mp, d, 1n+r, k)
848
849def internal_div_mono_wit(+a: Nat, +c: Nat, b: Nat, w: &k:Nat -> {Nat.add(a, k) == c : Nat}) -> le(Nat.div(a, 1n+b), Nat.div(c, 1n+b)):
850 match w:
851 case (+k, e):
852 %e : le(Nat.div(a, 1n+b), Nat.div(_, 1n+b))
853 Equal.sym(Bool, True{}, Nat.is_le(Nat.div(a, 1n+b), Nat.div(Nat.add(a, k), 1n+b)), internal_div_mono_go(a, b, 0n, 0n, k))
854
855# Division by a positive divisor is monotone: a <= c implies a / (1 + b) <= c / (1 + b).
856law div_le_div:
857 for +a: Nat
858 for +c: Nat
859 for b: Nat
860 for h: le(a, c)
861 le(Nat.div(a, 1n+b), Nat.div(c, 1n+b))
862
863def div_le_div(a, c, b, h):
864 internal_div_mono_wit(a, c, b, internal_div_le_wit(a, c, h))
865
866def internal_div_go_shift(n: Nat, m: Nat, +d: Nat, +r: Nat) -> {1n+Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)) == Pair.fst(Nat, Nat, Nat.divmod.go(n, m, 1n+d, r)) : Nat}:
867 match n m:
868 case 0n _:
869 {==}
870 case 1n+np 0n:
871 internal_div_go_shift(np, r, 1n+d, 0n)
872 case 1n+np 1n+mp:
873 internal_div_go_shift(np, mp, d, 1n+r)
874
875def internal_div_go_run(m: Nat, +a: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(a, Nat.add(m, r), 1n+d, 0n) == Nat.divmod.go(Nat.add(1n+m, a), m, d, r) : Nat & Nat}:
876 match m:
877 case 0n:
878 {==}
879 case 1n++mp:
880 %add_succ(mp, r) : {Nat.divmod.go(a, _, 1n+d, 0n) == Nat.divmod.go(1n+Nat.add(mp, a), mp, d, 1n+r) : Nat & Nat}
881 internal_div_go_run(mp, a, d, 1n+r)
882
883# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b).
884law add_div_left:
885 for +a: Nat
886 for +b: Nat
887 {Nat.div(Nat.add(1n+b, a), 1n+b) == 1n+Nat.div(a, 1n+b) : Nat}
888
889def add_div_left(a, b):
890 %internal_div_go_run(b, a, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n+Nat.div(a, 1n+b) : Nat}
891 %internal_div_add_zero_r(b) : {Pair.fst(Nat, Nat, Nat.divmod.go(a, _, 1n, 0n)) == 1n+Nat.div(a, 1n+b) : Nat}
892 Equal.sym(Nat, 1n+Nat.div(a, 1n+b), Pair.fst(Nat, Nat, Nat.divmod.go(a, b, 1n, 0n)), internal_div_go_shift(a, b, 0n, 0n))
893
894def internal_div_le_add_cancel(t: Nat, +x: Nat, +y: Nat) -> {Nat.is_le(x, y) == Nat.is_le(Nat.add(t, x), Nat.add(t, y)) : Bool}:
895 match t:
896 case 0n:
897 {==}
898 case 1n+tp:
899 internal_div_le_add_cancel(tp, x, y)
900
901def internal_div_gt_add(a: Nat, +y: Nat) -> {False{} == Nat.is_le(1n+Nat.add(a, y), a) : Bool}:
902 match a:
903 case 0n:
904 {==}
905 case 1n+ap:
906 internal_div_gt_add(ap, y)
907
908def internal_div_not_succ_le(a: Nat, bp: Nat, h: {False{} == Nat.is_le(1n+bp, a) : Bool}) -> {Nat.is_le(a, bp) == True{} : Bool}:
909 match a bp:
910 case 0n q:
911 Equal.sym(Bool, True{}, Nat.is_le(0n, q), internal_div_zero_le(q))
912 case 1n+ap 0n:
913 Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, internal_div_true_ne_false(Equal.sym(Bool, False{}, True{}, Equal.trans(Bool, False{}, Nat.is_le(0n, ap), True{}, h, Equal.sym(Bool, True{}, Nat.is_le(0n, ap), internal_div_zero_le(ap))))))
914 case 1n+ap 1n+q:
915 internal_div_not_succ_le(ap, q, h)
916
917def internal_div_le_big(+np: Nat, +a: Nat, +bp: Nat, w: &k:Nat -> {Nat.add(1n+bp, k) == a : Nat}, ih: @x:Nat -> {Nat.is_le(np, Nat.div(x, 1n+bp)) == Nat.is_le(Nat.mul(np, 1n+bp), x) : Bool}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
918 match w:
919 case (+k, e):
920 %e : {Nat.is_le(1n+np, Nat.div(_, 1n+bp)) == Nat.is_le(1n+Nat.add(bp, Nat.mul(np, 1n+bp)), _) : Bool}
921 %internal_div_le_add_cancel(bp, Nat.mul(np, 1n+bp), k) : {Nat.is_le(1n+np, Nat.div(1n+Nat.add(bp, k), 1n+bp)) == _ : Bool}
922 %Equal.sym(Nat, Nat.div(Nat.add(1n+bp, k), 1n+bp), 1n+Nat.div(k, 1n+bp), add_div_left(k, bp)) : {Nat.is_le(1n+np, _) == Nat.is_le(Nat.mul(np, 1n+bp), k) : Bool}
923 ih(k)
924
925def internal_div_le_small(+np: Nat, +a: Nat, +bp: Nat, w: &k:Nat -> {Nat.add(a, k) == bp : Nat}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
926 match w:
927 case (+k, e):
928 %e : {Nat.is_le(1n+np, Nat.div(a, 1n+_)) == Nat.is_le(1n+Nat.add(_, Nat.mul(np, 1n+_)), a) : Bool}
929 %internal_div_go_small(a, k, 0n, 0n) : {Nat.is_le(1n+np, _) == Nat.is_le(1n+Nat.add(Nat.add(a, k), Nat.mul(np, 1n+Nat.add(a, k))), a) : Bool}
930 %Equal.sym(Nat, Nat.add(Nat.add(a, k), Nat.mul(np, 1n+Nat.add(a, k))), Nat.add(a, Nat.add(k, Nat.mul(np, 1n+Nat.add(a, k)))), add_assoc(a, k, Nat.mul(np, 1n+Nat.add(a, k)))) : {False{} == Nat.is_le(1n+_, a) : Bool}
931 internal_div_gt_add(a, Nat.add(k, Nat.mul(np, 1n+Nat.add(a, k))))
932
933def internal_div_le_step(+np: Nat, +a: Nat, +bp: Nat, b: Bool, eb: {b == Nat.is_le(1n+bp, a) : Bool}, ih: @x:Nat -> {Nat.is_le(np, Nat.div(x, 1n+bp)) == Nat.is_le(Nat.mul(np, 1n+bp), x) : Bool}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
934 match b:
935 case True{}:
936 internal_div_le_big(np, a, bp, internal_div_le_wit(1n+bp, a, Equal.sym(Bool, True{}, Nat.is_le(1n+bp, a), eb)), ih)
937 case False{}:
938 internal_div_le_small(np, a, bp, internal_div_le_wit(a, bp, internal_div_not_succ_le(a, bp, eb)))
939
940# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a.
941law le_div_iff_mul_le:
942 for n: Nat
943 for +a: Nat
944 for +b: Nat
945 {Nat.is_le(n, Nat.div(a, 1n+b)) == Nat.is_le(Nat.mul(n, 1n+b), a) : Bool}
946
947def le_div_iff_mul_le(n, a, b):
948 match n:
949 case 0n:
950 %internal_div_zero_le(Nat.div(a, 1n+b)) : {_ == Nat.is_le(0n, a) : Bool}
951 %internal_div_zero_le(a) : {True{} == _ : Bool}
952 {==}
953 case 1n++np:
954 internal_div_le_step(np, a, b, Nat.is_le(1n+b, a), {==}, x => le_div_iff_mul_le(np, x, b))
955
956# Minimum is commutative.
957law min_comm:
958 for a: Nat
959 for b: Nat
960 {Nat.min(a, b) == Nat.min(b, a) : Nat}
961
962def min_comm(a, b):
963 match a b:
964 case 0n 0n:
965 {==}
966 case 0n 1n+q:
967 {==}
968 case 1n+p 0n:
969 {==}
970 case 1n++p 1n++q:
971 %min_comm(p, q) : {1n+Nat.min(p, q) == 1n+_ : Nat}
972 {==}
973
974# Maximum is commutative.
975law max_comm:
976 for a: Nat
977 for b: Nat
978 {Nat.max(a, b) == Nat.max(b, a) : Nat}
979
980def max_comm(a, b):
981 match a b:
982 case 0n 0n:
983 {==}
984 case 0n 1n+q:
985 {==}
986 case 1n+p 0n:
987 {==}
988 case 1n++p 1n++q:
989 %max_comm(p, q) : {1n+Nat.max(p, q) == 1n+_ : Nat}
990 {==}
991
992# The minimum of a natural and itself is itself.
993law min_self:
994 for a: Nat
995 {Nat.min(a, a) == a : Nat}
996
997def min_self(a):
998 match a:
999 case 0n:
1000 {==}
1001 case 1n++p:
1002 %min_self(p) : {1n+Nat.min(p, p) == 1n+_ : Nat}
1003 {==}
1004
1005# The maximum of a natural and itself is itself.
1006law max_self:
1007 for a: Nat
1008 {Nat.max(a, a) == a : Nat}
1009
1010def max_self(a):
1011 match a:
1012 case 0n:
1013 {==}
1014 case 1n++p:
1015 %max_self(p) : {1n+Nat.max(p, p) == 1n+_ : Nat}
1016 {==}
1017
1018# The minimum with zero is zero: min(a, 0) = 0.
1019law min_zero:
1020 for a: Nat
1021 {Nat.min(a, 0n) == 0n : Nat}
1022
1023def min_zero(a):
1024 match a:
1025 case 0n:
1026 {==}
1027 case 1n+p:
1028 {==}
1029
1030# The minimum with zero is zero: min(0, a) = 0.
1031law zero_min:
1032 for a: Nat
1033 {Nat.min(0n, a) == 0n : Nat}
1034
1035def zero_min(a):
1036 match a:
1037 case 0n:
1038 {==}
1039 case 1n+p:
1040 {==}
1041
1042# Zero is an identity for maximum: max(a, 0) = a.
1043law max_zero:
1044 for a: Nat
1045 {Nat.max(a, 0n) == a : Nat}
1046
1047def max_zero(a):
1048 match a:
1049 case 0n:
1050 {==}
1051 case 1n+p:
1052 {==}
1053
1054# Zero is an identity for maximum: max(0, a) = a.
1055law zero_max:
1056 for a: Nat
1057 {Nat.max(0n, a) == a : Nat}
1058
1059def zero_max(a):
1060 match a:
1061 case 0n:
1062 {==}
1063 case 1n+p:
1064 {==}
1065
1066# Minimum is associative.
1067law min_assoc:
1068 for a: Nat
1069 for b: Nat
1070 for c: Nat
1071 {Nat.min(Nat.min(a, b), c) == Nat.min(a, Nat.min(b, c)) : Nat}
1072
1073def min_assoc(a, b, c):
1074 match a b c:
1075 case 0n _ _:
1076 {==}
1077 case 1n+p 0n _:
1078 {==}
1079 case 1n+p 1n+q 0n:
1080 {==}
1081 case 1n++p 1n++q 1n++r:
1082 %min_assoc(p, q, r) : {1n+Nat.min(Nat.min(p, q), r) == 1n+_ : Nat}
1083 {==}
1084
1085# Maximum is associative.
1086law max_assoc:
1087 for a: Nat
1088 for b: Nat
1089 for c: Nat
1090 {Nat.max(Nat.max(a, b), c) == Nat.max(a, Nat.max(b, c)) : Nat}
1091
1092def max_assoc(a, b, c):
1093 match a b c:
1094 case 0n _ _:
1095 {==}
1096 case 1n+p 0n _:
1097 {==}
1098 case 1n+p 1n+q 0n:
1099 {==}
1100 case 1n++p 1n++q 1n++r:
1101 %max_assoc(p, q, r) : {1n+Nat.max(Nat.max(p, q), r) == 1n+_ : Nat}
1102 {==}
1103
1104# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
1105law min_add_max:
1106 for a: Nat
1107 for b: Nat
1108 {Nat.add(Nat.min(a, b), Nat.max(a, b)) == Nat.add(a, b) : Nat}
1109
1110def min_add_max(a, b):
1111 match a b:
1112 case 0n 0n:
1113 {==}
1114 case 0n 1n+q:
1115 {==}
1116 case 1n++p 0n:
1117 %add_zero(p) : {1n+_ == 1n+Nat.add(p, 0n) : Nat}
1118 {==}
1119 case 1n++p 1n++q:
1120 %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}
1121 %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}
1122 %min_add_max(p, q) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 2n+_ : Nat}
1123 {==}
1124
1125# The minimum is at most its left argument.
1126law min_le_left:
1127 for a: Nat
1128 for b: Nat
1129 le(Nat.min(a, b), a)
1130
1131def min_le_left(a, b):
1132 match a b:
1133 case 0n 0n:
1134 {==}
1135 case 0n 1n+q:
1136 {==}
1137 case 1n+p 0n:
1138 {==}
1139 case 1n+p 1n+q:
1140 min_le_left(p, q)
1141
1142# The minimum is at most its right argument.
1143law min_le_right:
1144 for a: Nat
1145 for b: Nat
1146 le(Nat.min(a, b), b)
1147
1148def min_le_right(a, b):
1149 match a b:
1150 case 0n 0n:
1151 {==}
1152 case 0n 1n+q:
1153 {==}
1154 case 1n+p 0n:
1155 {==}
1156 case 1n+p 1n+q:
1157 min_le_right(p, q)
1158
1159# The left argument is at most the maximum.
1160law le_max_left:
1161 for a: Nat
1162 for b: Nat
1163 le(a, Nat.max(a, b))
1164
1165def le_max_left(a, b):
1166 match a b:
1167 case 0n 0n:
1168 {==}
1169 case 0n 1n+q:
1170 {==}
1171 case 1n+p 0n:
1172 le_refl(1n+p)
1173 case 1n+p 1n+q:
1174 le_max_left(p, q)
1175
1176# The right argument is at most the maximum.
1177law le_max_right:
1178 for a: Nat
1179 for b: Nat
1180 le(b, Nat.max(a, b))
1181
1182def le_max_right(a, b):
1183 match a b:
1184 case 0n 0n:
1185 {==}
1186 case 0n 1n+q:
1187 le_refl(1n+q)
1188 case 1n+p 0n:
1189 {==}
1190 case 1n+p 1n+q:
1191 le_max_right(p, q)
1192
1193# Any natural to the power zero is one.
1194law pow_zero:
1195 for -a: Nat
1196 {Nat.pow(a, 0n) == 1n : Nat}
1197
1198def pow_zero(a):
1199 {==}
1200
1201# A power with a successor exponent: a^(n+1) = a * a^n.
1202law pow_succ:
1203 for -a: Nat
1204 for -n: Nat
1205 {Nat.pow(a, 1n+n) == Nat.mul(a, Nat.pow(a, n)) : Nat}
1206
1207def pow_succ(a, n):
1208 {==}
1209
1210# Any natural to the power one is itself.
1211law pow_one:
1212 for a: Nat
1213 {Nat.pow(a, 1n) == a : Nat}
1214
1215def pow_one(a):
1216 mul_one(a)
1217
1218# One to any power is one.
1219law one_pow:
1220 for n: Nat
1221 {Nat.pow(1n, n) == 1n : Nat}
1222
1223def one_pow(n):
1224 match n:
1225 case 0n:
1226 {==}
1227 case 1n++p:
1228 %Equal.sym(Nat, Nat.mul(1n, Nat.pow(1n, p)), Nat.pow(1n, p), one_mul(Nat.pow(1n, p))) : {_ == 1n : Nat}
1229 one_pow(p)
1230
1231# Exponents add under multiplication: a^(m+n) = a^m * a^n.
1232law pow_add:
1233 for a: Nat
1234 for m: Nat
1235 for n: Nat
1236 {Nat.pow(a, Nat.add(m, n)) == Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) : Nat}
1237
1238def pow_add(a, m, n):
1239 match m:
1240 case 0n:
1241 +a = a
1242 +n = n
1243 %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}
1244 {==}
1245 case 1n++p:
1246 +a = a
1247 +n = n
1248 %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}
1249 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)))
1250
1251# Doubling is adding a natural to itself.
1252law double_eq_add:
1253 for n: Nat
1254 {Nat.double(n) == Nat.add(n, n) : Nat}
1255
1256def double_eq_add(n):
1257 match n:
1258 case 0n:
1259 {==}
1260 case 1n++p:
1261 %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
1262 %double_eq_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
1263 {==}
1264
1265# Every natural tests equal to itself.
1266law is_eq_refl:
1267 for n: Nat
1268 {Nat.is_eq(n, n) == True{} : Bool}
1269
1270def is_eq_refl(n):
1271 match n:
1272 case 0n:
1273 {==}
1274 case 1n+p:
1275 is_eq_refl(p)
1276
1277# The equality test is symmetric.
1278law is_eq_comm:
1279 for a: Nat
1280 for b: Nat
1281 {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1282
1283def is_eq_comm(a, b):
1284 match a b:
1285 case 0n 0n:
1286 {==}
1287 case 0n 1n+q:
1288 {==}
1289 case 1n+p 0n:
1290 {==}
1291 case 1n++p 1n++q:
1292 %is_eq_comm(p, q) : {Nat.is_eq(p, q) == _ : Bool}
1293 {==}
1294
1295# If the equality test says true, the naturals are equal.
1296law eq_of_is_eq:
1297 for a: Nat
1298 for b: Nat
1299 for h: {Nat.is_eq(a, b) == True{} : Bool}
1300 {a == b : Nat}
1301
1302def eq_of_is_eq(a, b, h):
1303 match a b:
1304 case 0n 0n:
1305 {==}
1306 case 0n 1n+q:
1307 Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(h))
1308 case 1n+p 0n:
1309 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1310 case 1n++p 1n++q:
1311 %eq_of_is_eq(p, q, h) : {1n+p == 1n+_ : Nat}
1312 {==}
1313
1314# A >= b tests the same as b <= a.
1315law is_ge_eq_is_le:
1316 for a: Nat
1317 for b: Nat
1318 {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}
1319
1320def is_ge_eq_is_le(a, b):
1321 match a b:
1322 case 0n 0n:
1323 {==}
1324 case 0n 1n+q:
1325 {==}
1326 case 1n+p 0n:
1327 {==}
1328 case 1n++p 1n++q:
1329 %is_ge_eq_is_le(p, q) : {Nat.is_ge(p, q) == _ : Bool}
1330 {==}
1331
1332# A > b tests the same as b < a.
1333law is_gt_eq_is_lt:
1334 for a: Nat
1335 for b: Nat
1336 {Nat.is_gt(a, b) == Nat.is_lt(b, a) : Bool}
1337
1338def is_gt_eq_is_lt(a, b):
1339 match a b:
1340 case 0n 0n:
1341 {==}
1342 case 0n 1n+q:
1343 {==}
1344 case 1n+p 0n:
1345 {==}
1346 case 1n++p 1n++q:
1347 %is_gt_eq_is_lt(p, q) : {Nat.is_gt(p, q) == _ : Bool}
1348 {==}
1349
1350# A < b tests the same as a + 1 <= b.
1351law is_lt_eq_succ_le:
1352 for a: Nat
1353 for b: Nat
1354 {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}
1355
1356def is_lt_eq_succ_le(a, b):
1357 match a b:
1358 case 0n 0n:
1359 {==}
1360 case 0n 1n+q:
1361 match q:
1362 case 0n:
1363 {==}
1364 case 1n+r:
1365 {==}
1366 case 1n+p 0n:
1367 {==}
1368 case 1n+p 1n+q:
1369 is_lt_eq_succ_le(p, q)
1370
1371# Not (a <= b) tests the same as b < a.
1372law not_is_le:
1373 for a: Nat
1374 for b: Nat
1375 {Bool.not(Nat.is_le(a, b)) == Nat.is_lt(b, a) : Bool}
1376
1377def not_is_le(a, b):
1378 match a b:
1379 case 0n 0n:
1380 {==}
1381 case 0n 1n+q:
1382 {==}
1383 case 1n+p 0n:
1384 {==}
1385 case 1n+p 1n+q:
1386 not_is_le(p, q)
1387
1388# Not (a < b) tests the same as b <= a.
1389law not_is_lt:
1390 for a: Nat
1391 for b: Nat
1392 {Bool.not(Nat.is_lt(a, b)) == Nat.is_le(b, a) : Bool}
1393
1394def not_is_lt(a, b):
1395 match a b:
1396 case 0n 0n:
1397 {==}
1398 case 0n 1n+q:
1399 {==}
1400 case 1n+p 0n:
1401 {==}
1402 case 1n+p 1n+q:
1403 not_is_lt(p, q)
1404
1405# Every natural is less than its successor: n < n + 1.
1406law lt_succ_self:
1407 for n: Nat
1408 lt(n, 1n+n)
1409
1410def lt_succ_self(n):
1411 match n:
1412 case 0n:
1413 {==}
1414 case 1n+p:
1415 lt_succ_self(p)
1416
1417# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1418law succ_le_succ:
1419 for -a: Nat
1420 for -b: Nat
1421 for h: le(a, b)
1422 le(1n+a, 1n+b)
1423
1424def succ_le_succ(a, b, h):
1425 h
1426
1427# The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
1428law le_of_succ_le_succ:
1429 for -a: Nat
1430 for -b: Nat
1431 for h: le(1n+a, 1n+b)
1432 le(a, b)
1433
1434def le_of_succ_le_succ(a, b, h):
1435 h
1436
1437# A < b and b <= c imply a < c.
1438law lt_of_lt_of_le:
1439 for a: Nat
1440 for b: Nat
1441 for c: Nat
1442 for ab: lt(a, b)
1443 for bc: le(b, c)
1444 lt(a, c)
1445
1446def lt_of_lt_of_le(a, b, c, ab, bc):
1447 match a b c:
1448 case 0n 0n _:
1449 Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
1450 case 0n 1n+q 0n:
1451 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1452 case 0n 1n+q 1n+r:
1453 {==}
1454 case 1n+p 0n _:
1455 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1456 case 1n+p 1n+q 0n:
1457 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1458 case 1n+p 1n+q 1n+r:
1459 lt_of_lt_of_le(p, q, r, ab, bc)
1460
1461# A <= b and b < c imply a < c.
1462law lt_of_le_of_lt:
1463 for a: Nat
1464 for b: Nat
1465 for c: Nat
1466 for ab: le(a, b)
1467 for bc: lt(b, c)
1468 lt(a, c)
1469
1470def lt_of_le_of_lt(a, b, c, ab, bc):
1471 match a b c:
1472 case 0n 0n 0n:
1473 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1474 case 0n 1n+q 0n:
1475 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1476 case 0n _ 1n+r:
1477 {==}
1478 case 1n+p 0n _:
1479 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1480 case 1n+p 1n+q 0n:
1481 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1482 case 1n+p 1n+q 1n+r:
1483 lt_of_le_of_lt(p, q, r, ab, bc)
1484
1485# Adding on the left preserves the order: a <= b implies k + a <= k + b.
1486law add_le_add_left:
1487 for -a: Nat
1488 for -b: Nat
1489 for k: Nat
1490 for h: le(a, b)
1491 le(Nat.add(k, a), Nat.add(k, b))
1492
1493def add_le_add_left(a, b, k, h):
1494 match k:
1495 case 0n:
1496 h
1497 case 1n+p:
1498 add_le_add_left(a, b, p, h)
1499
1500# Adding on the right preserves the order: a <= b implies a + k <= b + k.
1501law add_le_add_right:
1502 for +a: Nat
1503 for +b: Nat
1504 for +k: Nat
1505 for h: le(a, b)
1506 le(Nat.add(a, k), Nat.add(b, k))
1507
1508def add_le_add_right(a, b, k, h):
1509 %add_comm(k, a) : le(_, Nat.add(b, k))
1510 %add_comm(k, b) : le(Nat.add(k, a), _)
1511 add_le_add_left(a, b, k, h)
1512
1513# Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b.
1514law add_le_add_iff_left:
1515 for k: Nat
1516 for -a: Nat
1517 for -b: Nat
1518 {Nat.is_le(a, b) == Nat.is_le(Nat.add(k, a), Nat.add(k, b)) : Bool}
1519
1520def add_le_add_iff_left(k, a, b):
1521 match k:
1522 case 0n:
1523 {==}
1524 case 1n+p:
1525 add_le_add_iff_left(p, a, b)
1526
1527# Adding two bounded summands stays bounded: a <= c and b <= d imply a + b <= c + d.
1528law add_le_add:
1529 for +a: Nat
1530 for +b: Nat
1531 for +c: Nat
1532 for +d: Nat
1533 for h1: le(a, c)
1534 for h2: le(b, d)
1535 le(Nat.add(a, b), Nat.add(c, d))
1536
1537def add_le_add(a, b, c, d, h1, h2):
1538 le_trans(Nat.add(a, b), Nat.add(c, b), Nat.add(c, d), add_le_add_right(a, c, b, h1), add_le_add_left(b, d, c, h2))
1539
1540# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both.
1541law le_and_le_sub_iff_add_le:
1542 for a: Nat
1543 for -b: Nat
1544 for c: Nat
1545 {Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) == Nat.is_le(Nat.add(a, b), c) : Bool}
1546
1547def le_and_le_sub_iff_add_le(a, b, c):
1548 match a c:
1549 case 0n 0n:
1550 {==}
1551 case 0n 1n+j:
1552 {==}
1553 case 1n+i 0n:
1554 {==}
1555 case 1n+i 1n+j:
1556 le_and_le_sub_iff_add_le(i, b, j)
1557
1558# The only natural at most zero is zero.
1559law le_zero_eq:
1560 for n: Nat
1561 for h: le(n, 0n)
1562 {n == 0n : Nat}
1563
1564def le_zero_eq(n, h):
1565 match n:
1566 case 0n:
1567 {==}
1568 case 1n+p:
1569 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1570
1571# No natural is less than zero.
1572law lt_zero:
1573 for n: Nat
1574 lt(n, 0n) -> Empty
1575
1576def lt_zero(n):
1577 match n:
1578 case 0n:
1579 h => internal_false_ne_true(h)
1580 case 1n+p:
1581 h => internal_false_ne_true(h)
1582
1583# A strict inequality rules out the reverse weak one: a < b implies b <= a is false.
1584law not_le_of_lt:
1585 for a: Nat
1586 for b: Nat
1587 for h: lt(a, b)
1588 {Nat.is_le(b, a) == False{} : Bool}
1589
1590def not_le_of_lt(a, b, h):
1591 match a b:
1592 case 0n 0n:
1593 Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, internal_false_ne_true(h))
1594 case 0n 1n+q:
1595 {==}
1596 case 1n+p 0n:
1597 Empty.absurd({Nat.is_le(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1598 case 1n+p 1n+q:
1599 not_le_of_lt(p, q, h)
1600
1601# A weak inequality rules out the reverse strict one: a <= b implies b < a is false.
1602law not_lt_of_le:
1603 for a: Nat
1604 for b: Nat
1605 for h: le(a, b)
1606 {Nat.is_lt(b, a) == False{} : Bool}
1607
1608def not_lt_of_le(a, b, h):
1609 match a b:
1610 case 0n 0n:
1611 {==}
1612 case 0n 1n+q:
1613 {==}
1614 case 1n+p 0n:
1615 Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1616 case 1n+p 1n+q:
1617 not_lt_of_le(p, q, h)
1618
1619# A failed weak test gives the reverse strict order: a <= b false implies b < a.
1620law lt_of_not_le:
1621 for a: Nat
1622 for b: Nat
1623 for h: {Nat.is_le(a, b) == False{} : Bool}
1624 lt(b, a)
1625
1626def lt_of_not_le(a, b, h):
1627 match a b:
1628 case 0n 0n:
1629 Empty.absurd(lt(0n, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1630 case 0n 1n+q:
1631 Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1632 case 1n+p 0n:
1633 {==}
1634 case 1n+p 1n+q:
1635 lt_of_not_le(p, q, h)
1636
1637# A failed strict test gives the reverse weak order: a < b false implies b <= a.
1638law le_of_not_lt:
1639 for a: Nat
1640 for b: Nat
1641 for h: {Nat.is_lt(a, b) == False{} : Bool}
1642 le(b, a)
1643
1644def le_of_not_lt(a, b, h):
1645 match a b:
1646 case 0n 0n:
1647 {==}
1648 case 0n 1n+q:
1649 Empty.absurd(le(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1650 case 1n+p 0n:
1651 {==}
1652 case 1n+p 1n+q:
1653 le_of_not_lt(p, q, h)
1654
1655# A number below both bounds is below their minimum: a < b and a < c imply a < min b c.
1656law lt_min:
1657 for a: Nat
1658 for b: Nat
1659 for c: Nat
1660 for hb: lt(a, b)
1661 for hc: lt(a, c)
1662 lt(a, Nat.min(b, c))
1663
1664def lt_min(a, b, c, hb, hc):
1665 match a b c:
1666 case _ 0n _:
1667 Empty.absurd(lt(a, Nat.min(0n, c)), lt_zero(a)(hb))
1668 case _ 1n+q 0n:
1669 Empty.absurd(lt(a, Nat.min(1n+q, 0n)), lt_zero(a)(hc))
1670 case 0n 1n+q 1n+r:
1671 {==}
1672 case 1n+p 1n+q 1n+r:
1673 lt_min(p, q, r, hb, hc)
1674
1675def internal_or_true_sym(x: Bool) -> {True{} == Bool.or(x, True{}) : Bool}:
1676 match x:
1677 case False{}:
1678 {==}
1679 case True{}:
1680 {==}
1681
1682def internal_or_false_sym(x: Bool) -> {x == Bool.or(x, False{}) : Bool}:
1683 match x:
1684 case False{}:
1685 {==}
1686 case True{}:
1687 {==}
1688
1689# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.
1690law min_le_iff:
1691 for a: Nat
1692 for b: Nat
1693 for c: Nat
1694 {Nat.is_le(Nat.min(a, b), c) == Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
1695
1696def min_le_iff(a, b, c):
1697 match a b c:
1698 case 0n 0n 0n:
1699 {==}
1700 case 0n 0n 1n+r:
1701 {==}
1702 case 0n 1n+q 0n:
1703 {==}
1704 case 0n 1n+q 1n+r:
1705 {==}
1706 case 1n+p 0n 0n:
1707 {==}
1708 case 1n+p 0n 1n+r:
1709 internal_or_true_sym(Nat.is_le(p, r))
1710 case 1n+p 1n+q 0n:
1711 {==}
1712 case 1n+p 1n+q 1n+r:
1713 min_le_iff(p, q, r)
1714
1715# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.
1716law lt_max_iff:
1717 for a: Nat
1718 for b: Nat
1719 for c: Nat
1720 {Nat.is_lt(a, Nat.max(b, c)) == Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}
1721
1722def lt_max_iff(a, b, c):
1723 match a b c:
1724 case 0n 0n 0n:
1725 {==}
1726 case 0n 0n 1n+r:
1727 {==}
1728 case 0n 1n+q 0n:
1729 {==}
1730 case 0n 1n+q 1n+r:
1731 {==}
1732 case 1n+p 0n 0n:
1733 {==}
1734 case 1n+p 0n 1n+r:
1735 {==}
1736 case 1n+p 1n+q 0n:
1737 internal_or_false_sym(Nat.is_lt(p, q))
1738 case 1n+p 1n+q 1n+r:
1739 lt_max_iff(p, q, r)
1740
1741# Subtracting a larger number gives zero: a <= b implies a - b = 0.
1742law sub_eq_zero_of_le:
1743 for a: Nat
1744 for b: Nat
1745 for h: le(a, b)
1746 {Nat.sub(a, b) == 0n : Nat}
1747
1748def sub_eq_zero_of_le(a, b, h):
1749 match a b:
1750 case 0n 0n:
1751 {==}
1752 case 0n 1n+q:
1753 {==}
1754 case 1n+p 0n:
1755 Empty.absurd({Nat.sub(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
1756 case 1n+p 1n+q:
1757 sub_eq_zero_of_le(p, q, h)
1758
1759# Above the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.
1760law succ_sub:
1761 for a: Nat
1762 for b: Nat
1763 for h: le(b, a)
1764 {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}
1765
1766def succ_sub(a, b, h):
1767 match a b:
1768 case 0n 0n:
1769 {==}
1770 case 1n+p 0n:
1771 {==}
1772 case 0n 1n+q:
1773 Empty.absurd({Nat.sub(1n, 1n+q) == 1n+Nat.sub(0n, 1n+q) : Nat}, internal_false_ne_true(h))
1774 case 1n+p 1n+q:
1775 succ_sub(p, q, h)
1776
1777# Adding back what was subtracted restores the number: a <= b implies a + (b - a) = b.
1778law add_sub_of_le:
1779 for a: Nat
1780 for b: Nat
1781 for h: le(a, b)
1782 {Nat.add(a, Nat.sub(b, a)) == b : Nat}
1783
1784def add_sub_of_le(a, b, h):
1785 match a b:
1786 case 0n 0n:
1787 {==}
1788 case 0n 1n+q:
1789 {==}
1790 case 1n+p 0n:
1791 Empty.absurd({Nat.add(1n+p, Nat.sub(0n, 1n+p)) == 0n : Nat}, internal_false_ne_true(h))
1792 case 1n++p 1n++q:
1793 %Equal.sym(Nat, Nat.add(p, Nat.sub(q, p)), q, add_sub_of_le(p, q, h)) : {1n+_ == 1n+q : Nat}
1794 {==}
1795
1796def internal_lt_sub_zero(a: Nat, p: Nat) -> {Nat.is_lt(a, Nat.sub(0n, 1n+p)) == Nat.is_lt(Nat.add(1n+p, a), 0n) : Bool}:
1797 match a:
1798 case 0n:
1799 {==}
1800 case 1n+x:
1801 {==}
1802
1803# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c.
1804law lt_sub_iff_add_lt:
1805 for a: Nat
1806 for b: Nat
1807 for c: Nat
1808 {Nat.is_lt(a, Nat.sub(c, b)) == Nat.is_lt(Nat.add(b, a), c) : Bool}
1809
1810def lt_sub_iff_add_lt(a, b, c):
1811 match b c:
1812 case 0n 0n:
1813 {==}
1814 case 0n 1n+r:
1815 {==}
1816 case 1n+p 0n:
1817 internal_lt_sub_zero(a, p)
1818 case 1n+p 1n+r:
1819 lt_sub_iff_add_lt(a, p, r)
1820
1821# A witnessed difference gives the order: a + k = b implies a <= b.
1822law le_of_add_eq:
1823 for a: Nat
1824 for k: Nat
1825 for -b: Nat
1826 for e: {Nat.add(a, k) == b : Nat}
1827 le(a, b)
1828
1829def le_of_add_eq(a, k, b, e):
1830 %e : {Nat.is_le(a, _) == True{} : Bool}
1831 le_add_right(a, k)
1832
1833# Multiplying on the right preserves the order: a <= b implies a * k <= b * k.
1834law mul_le_mul_right:
1835 for +a: Nat
1836 for +b: Nat
1837 for +k: Nat
1838 for h: le(a, b)
1839 le(Nat.mul(a, k), Nat.mul(b, k))
1840
1841def mul_le_mul_right(a, b, k, h):
1842 %sub_add_cancel(b, a, h) : {Nat.is_le(Nat.mul(a, k), Nat.mul(_, k)) == True{} : Bool}
1843 %Equal.sym(Nat, Nat.mul(Nat.add(Nat.sub(b, a), a), k), Nat.add(Nat.mul(Nat.sub(b, a), k), Nat.mul(a, k)), add_mul(Nat.sub(b, a), a, k)) : {Nat.is_le(Nat.mul(a, k), _) == True{} : Bool}
1844 %add_comm(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k)) : {Nat.is_le(Nat.mul(a, k), _) == True{} : Bool}
1845 le_add_right(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k))
1846
1847# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
1848
1849# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
1850law add_zero_sym:
1851 for x: Nat
1852 {x == Nat.add(x, 0n) : Nat}
1853
1854def add_zero_sym(x):
1855 Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
1856
1857# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
1858law zero_add_sym:
1859 for -x: Nat
1860 {x == Nat.add(0n, x) : Nat}
1861
1862def zero_add_sym(x):
1863 Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
1864
1865# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
1866law add_succ_sym:
1867 for n: Nat
1868 for -m: Nat
1869 {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
1870
1871def add_succ_sym(n, m):
1872 Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
1873
1874# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
1875law succ_add_sym:
1876 for -n: Nat
1877 for -m: Nat
1878 {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
1879
1880def succ_add_sym(n, m):
1881 Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
1882
1883# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
1884law add_comm_sym:
1885 for n: Nat
1886 for m: Nat
1887 {Nat.add(m, n) == Nat.add(n, m) : Nat}
1888
1889def add_comm_sym(n, m):
1890 Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
1891
1892# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
1893law add_assoc_sym:
1894 for a: Nat
1895 for -b: Nat
1896 for -c: Nat
1897 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
1898
1899def add_assoc_sym(a, b, c):
1900 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
1901
1902# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
1903law add_left_comm_sym:
1904 for a: Nat
1905 for b: Nat
1906 for -c: Nat
1907 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
1908
1909def add_left_comm_sym(a, b, c):
1910 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
1911
1912# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
1913law add_right_comm_sym:
1914 for a: Nat
1915 for b: Nat
1916 for c: Nat
1917 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
1918
1919def add_right_comm_sym(a, b, c):
1920 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
1921
1922# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
1923law add_add_add_comm_sym:
1924 for a: Nat
1925 for b: Nat
1926 for c: Nat
1927 for -d: Nat
1928 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
1929
1930def add_add_add_comm_sym(a, b, c, d):
1931 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))
1932
1933# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
1934law mul_zero_sym:
1935 for x: Nat
1936 {0n == Nat.mul(x, 0n) : Nat}
1937
1938def mul_zero_sym(x):
1939 Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
1940
1941# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
1942law zero_mul_sym:
1943 for -x: Nat
1944 {0n == Nat.mul(0n, x) : Nat}
1945
1946def zero_mul_sym(x):
1947 Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
1948
1949# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
1950law mul_one_sym:
1951 for x: Nat
1952 {x == Nat.mul(x, 1n) : Nat}
1953
1954def mul_one_sym(x):
1955 Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
1956
1957# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
1958law one_mul_sym:
1959 for x: Nat
1960 {x == Nat.mul(1n, x) : Nat}
1961
1962def one_mul_sym(x):
1963 Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
1964
1965# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
1966law mul_succ_sym:
1967 for n: Nat
1968 for m: Nat
1969 {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
1970
1971def mul_succ_sym(n, m):
1972 Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
1973
1974# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
1975law succ_mul_sym:
1976 for n: Nat
1977 for m: Nat
1978 {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
1979
1980def succ_mul_sym(n, m):
1981 Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
1982
1983# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
1984law mul_comm_sym:
1985 for n: Nat
1986 for m: Nat
1987 {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
1988
1989def mul_comm_sym(n, m):
1990 Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
1991
1992# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
1993law add_mul_sym:
1994 for a: Nat
1995 for -b: Nat
1996 for c: Nat
1997 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
1998
1999def add_mul_sym(a, b, c):
2000 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))
2001
2002# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
2003law mul_add_sym:
2004 for a: Nat
2005 for b: Nat
2006 for c: Nat
2007 {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
2008
2009def mul_add_sym(a, b, c):
2010 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))
2011
2012# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
2013law mul_assoc_sym:
2014 for a: Nat
2015 for b: Nat
2016 for c: Nat
2017 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
2018
2019def mul_assoc_sym(a, b, c):
2020 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
2021
2022# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
2023law sub_zero_sym:
2024 for n: Nat
2025 {n == Nat.sub(n, 0n) : Nat}
2026
2027def sub_zero_sym(n):
2028 Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
2029
2030# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
2031law zero_sub_sym:
2032 for n: Nat
2033 {0n == Nat.sub(0n, n) : Nat}
2034
2035def zero_sub_sym(n):
2036 Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
2037
2038# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
2039law sub_self_sym:
2040 for n: Nat
2041 {0n == Nat.sub(n, n) : Nat}
2042
2043def sub_self_sym(n):
2044 Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
2045
2046# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
2047law succ_sub_succ_sym:
2048 for -n: Nat
2049 for -m: Nat
2050 {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
2051
2052def succ_sub_succ_sym(n, m):
2053 Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
2054
2055# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
2056law add_sub_cancel_sym:
2057 for n: Nat
2058 for m: Nat
2059 {n == Nat.sub(Nat.add(n, m), m) : Nat}
2060
2061def add_sub_cancel_sym(n, m):
2062 Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
2063
2064# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
2065law add_sub_cancel_left_sym:
2066 for n: Nat
2067 for m: Nat
2068 {m == Nat.sub(Nat.add(n, m), n) : Nat}
2069
2070def add_sub_cancel_left_sym(n, m):
2071 Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
2072
2073# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
2074law sub_sub_sym:
2075 for n: Nat
2076 for m: Nat
2077 for k: Nat
2078 {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
2079
2080def sub_sub_sym(n, m, k):
2081 Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
2082
2083# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a, reversed to rewrite toward the simple side.
2084law div_mod_eq_sym:
2085 for +a: Nat
2086 for +b: Nat
2087 {a == Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) : Nat}
2088
2089def div_mod_eq_sym(a, b):
2090 Equal.sym(Nat, Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)), a, div_mod_eq(a, b))
2091
2092# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
2093law add_div_left_sym:
2094 for +a: Nat
2095 for +b: Nat
2096 {1n+Nat.div(a, 1n+b) == Nat.div(Nat.add(1n+b, a), 1n+b) : Nat}
2097
2098def add_div_left_sym(a, b):
2099 Equal.sym(Nat, Nat.div(Nat.add(1n+b, a), 1n+b), 1n+Nat.div(a, 1n+b), add_div_left(a, b))
2100
2101# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
2102law le_div_iff_mul_le_sym:
2103 for n: Nat
2104 for +a: Nat
2105 for +b: Nat
2106 {Nat.is_le(Nat.mul(n, 1n+b), a) == Nat.is_le(n, Nat.div(a, 1n+b)) : Bool}
2107
2108def le_div_iff_mul_le_sym(n, a, b):
2109 Equal.sym(Bool, Nat.is_le(n, Nat.div(a, 1n+b)), Nat.is_le(Nat.mul(n, 1n+b), a), le_div_iff_mul_le(n, a, b))
2110
2111# Minimum is commutative, reversed to rewrite toward the simple side.
2112law min_comm_sym:
2113 for a: Nat
2114 for b: Nat
2115 {Nat.min(b, a) == Nat.min(a, b) : Nat}
2116
2117def min_comm_sym(a, b):
2118 Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
2119
2120# Maximum is commutative, reversed to rewrite toward the simple side.
2121law max_comm_sym:
2122 for a: Nat
2123 for b: Nat
2124 {Nat.max(b, a) == Nat.max(a, b) : Nat}
2125
2126def max_comm_sym(a, b):
2127 Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
2128
2129# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
2130law min_self_sym:
2131 for a: Nat
2132 {a == Nat.min(a, a) : Nat}
2133
2134def min_self_sym(a):
2135 Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
2136
2137# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
2138law max_self_sym:
2139 for a: Nat
2140 {a == Nat.max(a, a) : Nat}
2141
2142def max_self_sym(a):
2143 Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
2144
2145# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
2146law min_zero_sym:
2147 for a: Nat
2148 {0n == Nat.min(a, 0n) : Nat}
2149
2150def min_zero_sym(a):
2151 Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
2152
2153# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
2154law zero_min_sym:
2155 for a: Nat
2156 {0n == Nat.min(0n, a) : Nat}
2157
2158def zero_min_sym(a):
2159 Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
2160
2161# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
2162law max_zero_sym:
2163 for a: Nat
2164 {a == Nat.max(a, 0n) : Nat}
2165
2166def max_zero_sym(a):
2167 Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
2168
2169# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
2170law zero_max_sym:
2171 for a: Nat
2172 {a == Nat.max(0n, a) : Nat}
2173
2174def zero_max_sym(a):
2175 Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
2176
2177# Minimum is associative, reversed to rewrite toward the simple side.
2178law min_assoc_sym:
2179 for a: Nat
2180 for b: Nat
2181 for c: Nat
2182 {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
2183
2184def min_assoc_sym(a, b, c):
2185 Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
2186
2187# Maximum is associative, reversed to rewrite toward the simple side.
2188law max_assoc_sym:
2189 for a: Nat
2190 for b: Nat
2191 for c: Nat
2192 {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
2193
2194def max_assoc_sym(a, b, c):
2195 Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
2196
2197# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
2198law min_add_max_sym:
2199 for a: Nat
2200 for b: Nat
2201 {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
2202
2203def min_add_max_sym(a, b):
2204 Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
2205
2206# Any natural to the power zero is one, reversed to rewrite toward the simple side.
2207law pow_zero_sym:
2208 for -a: Nat
2209 {1n == Nat.pow(a, 0n) : Nat}
2210
2211def pow_zero_sym(a):
2212 Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
2213
2214# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
2215law pow_succ_sym:
2216 for -a: Nat
2217 for -n: Nat
2218 {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
2219
2220def pow_succ_sym(a, n):
2221 Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
2222
2223# Any natural to the power one is itself, reversed to rewrite toward the simple side.
2224law pow_one_sym:
2225 for a: Nat
2226 {a == Nat.pow(a, 1n) : Nat}
2227
2228def pow_one_sym(a):
2229 Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
2230
2231# One to any power is one, reversed to rewrite toward the simple side.
2232law one_pow_sym:
2233 for n: Nat
2234 {1n == Nat.pow(1n, n) : Nat}
2235
2236def one_pow_sym(n):
2237 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
2238
2239# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
2240law pow_add_sym:
2241 for a: Nat
2242 for m: Nat
2243 for n: Nat
2244 {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
2245
2246def pow_add_sym(a, m, n):
2247 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))
2248
2249# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
2250law double_eq_add_sym:
2251 for n: Nat
2252 {Nat.add(n, n) == Nat.double(n) : Nat}
2253
2254def double_eq_add_sym(n):
2255 Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
2256
2257# Every natural tests equal to itself, reversed to rewrite toward the simple side.
2258law is_eq_refl_sym:
2259 for n: Nat
2260 {True{} == Nat.is_eq(n, n) : Bool}
2261
2262def is_eq_refl_sym(n):
2263 Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
2264
2265# The equality test is symmetric, reversed to rewrite toward the simple side.
2266law is_eq_comm_sym:
2267 for a: Nat
2268 for b: Nat
2269 {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
2270
2271def is_eq_comm_sym(a, b):
2272 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
2273
2274# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
2275law is_ge_eq_is_le_sym:
2276 for a: Nat
2277 for b: Nat
2278 {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
2279
2280def is_ge_eq_is_le_sym(a, b):
2281 Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
2282
2283# A > b tests the same as b < a, reversed to rewrite toward the simple side.
2284law is_gt_eq_is_lt_sym:
2285 for a: Nat
2286 for b: Nat
2287 {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
2288
2289def is_gt_eq_is_lt_sym(a, b):
2290 Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
2291
2292# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
2293law is_lt_eq_succ_le_sym:
2294 for a: Nat
2295 for b: Nat
2296 {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
2297
2298def is_lt_eq_succ_le_sym(a, b):
2299 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
2300
2301# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
2302law not_is_le_sym:
2303 for a: Nat
2304 for b: Nat
2305 {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
2306
2307def not_is_le_sym(a, b):
2308 Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
2309
2310# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
2311law not_is_lt_sym:
2312 for a: Nat
2313 for b: Nat
2314 {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
2315
2316def not_is_lt_sym(a, b):
2317 Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))
2318
2319# Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b, reversed to rewrite toward the simple side.
2320law add_le_add_iff_left_sym:
2321 for k: Nat
2322 for -a: Nat
2323 for -b: Nat
2324 {Nat.is_le(Nat.add(k, a), Nat.add(k, b)) == Nat.is_le(a, b) : Bool}
2325
2326def add_le_add_iff_left_sym(k, a, b):
2327 Equal.sym(Bool, Nat.is_le(a, b), Nat.is_le(Nat.add(k, a), Nat.add(k, b)), add_le_add_iff_left(k, a, b))
2328
2329# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both, reversed to rewrite toward the simple side.
2330law le_and_le_sub_iff_add_le_sym:
2331 for a: Nat
2332 for -b: Nat
2333 for c: Nat
2334 {Nat.is_le(Nat.add(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) : Bool}
2335
2336def le_and_le_sub_iff_add_le_sym(a, b, c):
2337 Equal.sym(Bool, Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))), Nat.is_le(Nat.add(a, b), c), le_and_le_sub_iff_add_le(a, b, c))
2338
2339# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c, reversed to rewrite toward the simple side.
2340law min_le_iff_sym:
2341 for a: Nat
2342 for b: Nat
2343 for c: Nat
2344 {Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.min(a, b), c) : Bool}
2345
2346def min_le_iff_sym(a, b, c):
2347 Equal.sym(Bool, Nat.is_le(Nat.min(a, b), c), Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)), min_le_iff(a, b, c))
2348
2349# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c, reversed to rewrite toward the simple side.
2350law lt_max_iff_sym:
2351 for a: Nat
2352 for b: Nat
2353 for c: Nat
2354 {Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.max(b, c)) : Bool}
2355
2356def lt_max_iff_sym(a, b, c):
2357 Equal.sym(Bool, Nat.is_lt(a, Nat.max(b, c)), Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)), lt_max_iff(a, b, c))
2358
2359# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
2360law lt_sub_iff_add_lt_sym:
2361 for a: Nat
2362 for b: Nat
2363 for c: Nat
2364 {Nat.is_lt(Nat.add(b, a), c) == Nat.is_lt(a, Nat.sub(c, b)) : Bool}
2365
2366def lt_sub_iff_add_lt_sym(a, b, c):
2367 Equal.sym(Bool, Nat.is_lt(a, Nat.sub(c, b)), Nat.is_lt(Nat.add(b, a), c), lt_sub_iff_add_lt(a, b, c))