nat.bend
bend-mathlib@0.4.0.0 · 2,289 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(Nat.div.fin(Nat.divmod.go(n, m, d, r)), 1n+bp), Nat.mod.fin(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(Nat.div.fin(Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Nat.mod.fin(Nat.divmod.go(np, r, 1n+d, 0n))) == _ : Nat}
766 %add_comm(r, Nat.mul(d, 1n+bp)) : {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Nat.mod.fin(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(Nat.div.fin(Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Nat.mod.fin(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(Nat.div.fin(Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Nat.mod.fin(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(Nat.div.fin(Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Nat.mod.fin(Nat.divmod.go(np, mp, d, 1n+r))) == _ : Nat}
772 %add_succ(Nat.mul(d, 1n+bp), r) : {Nat.add(Nat.mul(Nat.div.fin(Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Nat.mod.fin(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 == Nat.div.fin(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, Nat.div.fin(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, Nat.div.fin(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(Nat.div.fin(Nat.divmod.go(a, m, d, r)), Nat.div.fin(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+Nat.div.fin(Nat.divmod.go(n, m, d, r)) == Nat.div.fin(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) : {Nat.div.fin(_) == 1n+Nat.div(a, 1n+b) : Nat}
891 %internal_div_add_zero_r(b) : {Nat.div.fin(Nat.divmod.go(a, _, 1n, 0n)) == 1n+Nat.div(a, 1n+b) : Nat}
892 Equal.sym(Nat, 1n+Nat.div(a, 1n+b), Nat.div.fin(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# The only natural at most zero is zero.
1501law le_zero_eq:
1502 for n: Nat
1503 for h: le(n, 0n)
1504 {n == 0n : Nat}
1505
1506def le_zero_eq(n, h):
1507 match n:
1508 case 0n:
1509 {==}
1510 case 1n+p:
1511 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1512
1513# No natural is less than zero.
1514law lt_zero:
1515 for n: Nat
1516 lt(n, 0n) -> Empty
1517
1518def lt_zero(n):
1519 match n:
1520 case 0n:
1521 h => internal_false_ne_true(h)
1522 case 1n+p:
1523 h => internal_false_ne_true(h)
1524
1525# A strict inequality rules out the reverse weak one: a < b implies b <= a is false.
1526law not_le_of_lt:
1527 for a: Nat
1528 for b: Nat
1529 for h: lt(a, b)
1530 {Nat.is_le(b, a) == False{} : Bool}
1531
1532def not_le_of_lt(a, b, h):
1533 match a b:
1534 case 0n 0n:
1535 Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, internal_false_ne_true(h))
1536 case 0n 1n+q:
1537 {==}
1538 case 1n+p 0n:
1539 Empty.absurd({Nat.is_le(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1540 case 1n+p 1n+q:
1541 not_le_of_lt(p, q, h)
1542
1543# A weak inequality rules out the reverse strict one: a <= b implies b < a is false.
1544law not_lt_of_le:
1545 for a: Nat
1546 for b: Nat
1547 for h: le(a, b)
1548 {Nat.is_lt(b, a) == False{} : Bool}
1549
1550def not_lt_of_le(a, b, h):
1551 match a b:
1552 case 0n 0n:
1553 {==}
1554 case 0n 1n+q:
1555 {==}
1556 case 1n+p 0n:
1557 Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1558 case 1n+p 1n+q:
1559 not_lt_of_le(p, q, h)
1560
1561# A failed weak test gives the reverse strict order: a <= b false implies b < a.
1562law lt_of_not_le:
1563 for a: Nat
1564 for b: Nat
1565 for h: {Nat.is_le(a, b) == False{} : Bool}
1566 lt(b, a)
1567
1568def lt_of_not_le(a, b, h):
1569 match a b:
1570 case 0n 0n:
1571 Empty.absurd(lt(0n, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1572 case 0n 1n+q:
1573 Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1574 case 1n+p 0n:
1575 {==}
1576 case 1n+p 1n+q:
1577 lt_of_not_le(p, q, h)
1578
1579# A failed strict test gives the reverse weak order: a < b false implies b <= a.
1580law le_of_not_lt:
1581 for a: Nat
1582 for b: Nat
1583 for h: {Nat.is_lt(a, b) == False{} : Bool}
1584 le(b, a)
1585
1586def le_of_not_lt(a, b, h):
1587 match a b:
1588 case 0n 0n:
1589 {==}
1590 case 0n 1n+q:
1591 Empty.absurd(le(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1592 case 1n+p 0n:
1593 {==}
1594 case 1n+p 1n+q:
1595 le_of_not_lt(p, q, h)
1596
1597# A number below both bounds is below their minimum: a < b and a < c imply a < min b c.
1598law lt_min:
1599 for a: Nat
1600 for b: Nat
1601 for c: Nat
1602 for hb: lt(a, b)
1603 for hc: lt(a, c)
1604 lt(a, Nat.min(b, c))
1605
1606def lt_min(a, b, c, hb, hc):
1607 match a b c:
1608 case _ 0n _:
1609 Empty.absurd(lt(a, Nat.min(0n, c)), lt_zero(a)(hb))
1610 case _ 1n+q 0n:
1611 Empty.absurd(lt(a, Nat.min(1n+q, 0n)), lt_zero(a)(hc))
1612 case 0n 1n+q 1n+r:
1613 {==}
1614 case 1n+p 1n+q 1n+r:
1615 lt_min(p, q, r, hb, hc)
1616
1617def internal_or_true_sym(x: Bool) -> {True{} == Bool.or(x, True{}) : Bool}:
1618 match x:
1619 case False{}:
1620 {==}
1621 case True{}:
1622 {==}
1623
1624def internal_or_false_sym(x: Bool) -> {x == Bool.or(x, False{}) : Bool}:
1625 match x:
1626 case False{}:
1627 {==}
1628 case True{}:
1629 {==}
1630
1631# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.
1632law min_le_iff:
1633 for a: Nat
1634 for b: Nat
1635 for c: Nat
1636 {Nat.is_le(Nat.min(a, b), c) == Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
1637
1638def min_le_iff(a, b, c):
1639 match a b c:
1640 case 0n 0n 0n:
1641 {==}
1642 case 0n 0n 1n+r:
1643 {==}
1644 case 0n 1n+q 0n:
1645 {==}
1646 case 0n 1n+q 1n+r:
1647 {==}
1648 case 1n+p 0n 0n:
1649 {==}
1650 case 1n+p 0n 1n+r:
1651 internal_or_true_sym(Nat.is_le(p, r))
1652 case 1n+p 1n+q 0n:
1653 {==}
1654 case 1n+p 1n+q 1n+r:
1655 min_le_iff(p, q, r)
1656
1657# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.
1658law lt_max_iff:
1659 for a: Nat
1660 for b: Nat
1661 for c: Nat
1662 {Nat.is_lt(a, Nat.max(b, c)) == Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}
1663
1664def lt_max_iff(a, b, c):
1665 match a b c:
1666 case 0n 0n 0n:
1667 {==}
1668 case 0n 0n 1n+r:
1669 {==}
1670 case 0n 1n+q 0n:
1671 {==}
1672 case 0n 1n+q 1n+r:
1673 {==}
1674 case 1n+p 0n 0n:
1675 {==}
1676 case 1n+p 0n 1n+r:
1677 {==}
1678 case 1n+p 1n+q 0n:
1679 internal_or_false_sym(Nat.is_lt(p, q))
1680 case 1n+p 1n+q 1n+r:
1681 lt_max_iff(p, q, r)
1682
1683# Subtracting a larger number gives zero: a <= b implies a - b = 0.
1684law sub_eq_zero_of_le:
1685 for a: Nat
1686 for b: Nat
1687 for h: le(a, b)
1688 {Nat.sub(a, b) == 0n : Nat}
1689
1690def sub_eq_zero_of_le(a, b, h):
1691 match a b:
1692 case 0n 0n:
1693 {==}
1694 case 0n 1n+q:
1695 {==}
1696 case 1n+p 0n:
1697 Empty.absurd({Nat.sub(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
1698 case 1n+p 1n+q:
1699 sub_eq_zero_of_le(p, q, h)
1700
1701# Above the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.
1702law succ_sub:
1703 for a: Nat
1704 for b: Nat
1705 for h: le(b, a)
1706 {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}
1707
1708def succ_sub(a, b, h):
1709 match a b:
1710 case 0n 0n:
1711 {==}
1712 case 1n+p 0n:
1713 {==}
1714 case 0n 1n+q:
1715 Empty.absurd({Nat.sub(1n, 1n+q) == 1n+Nat.sub(0n, 1n+q) : Nat}, internal_false_ne_true(h))
1716 case 1n+p 1n+q:
1717 succ_sub(p, q, h)
1718
1719# Adding back what was subtracted restores the number: a <= b implies a + (b - a) = b.
1720law add_sub_of_le:
1721 for a: Nat
1722 for b: Nat
1723 for h: le(a, b)
1724 {Nat.add(a, Nat.sub(b, a)) == b : Nat}
1725
1726def add_sub_of_le(a, b, h):
1727 match a b:
1728 case 0n 0n:
1729 {==}
1730 case 0n 1n+q:
1731 {==}
1732 case 1n+p 0n:
1733 Empty.absurd({Nat.add(1n+p, Nat.sub(0n, 1n+p)) == 0n : Nat}, internal_false_ne_true(h))
1734 case 1n++p 1n++q:
1735 %Equal.sym(Nat, Nat.add(p, Nat.sub(q, p)), q, add_sub_of_le(p, q, h)) : {1n+_ == 1n+q : Nat}
1736 {==}
1737
1738def 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}:
1739 match a:
1740 case 0n:
1741 {==}
1742 case 1n+x:
1743 {==}
1744
1745# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c.
1746law lt_sub_iff_add_lt:
1747 for a: Nat
1748 for b: Nat
1749 for c: Nat
1750 {Nat.is_lt(a, Nat.sub(c, b)) == Nat.is_lt(Nat.add(b, a), c) : Bool}
1751
1752def lt_sub_iff_add_lt(a, b, c):
1753 match b c:
1754 case 0n 0n:
1755 {==}
1756 case 0n 1n+r:
1757 {==}
1758 case 1n+p 0n:
1759 internal_lt_sub_zero(a, p)
1760 case 1n+p 1n+r:
1761 lt_sub_iff_add_lt(a, p, r)
1762
1763# A witnessed difference gives the order: a + k = b implies a <= b.
1764law le_of_add_eq:
1765 for a: Nat
1766 for k: Nat
1767 for -b: Nat
1768 for e: {Nat.add(a, k) == b : Nat}
1769 le(a, b)
1770
1771def le_of_add_eq(a, k, b, e):
1772 %e : {Nat.is_le(a, _) == True{} : Bool}
1773 le_add_right(a, k)
1774
1775# Multiplying on the right preserves the order: a <= b implies a * k <= b * k.
1776law mul_le_mul_right:
1777 for +a: Nat
1778 for +b: Nat
1779 for +k: Nat
1780 for h: le(a, b)
1781 le(Nat.mul(a, k), Nat.mul(b, k))
1782
1783def mul_le_mul_right(a, b, k, h):
1784 %sub_add_cancel(b, a, h) : {Nat.is_le(Nat.mul(a, k), Nat.mul(_, k)) == True{} : Bool}
1785 %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}
1786 %add_comm(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k)) : {Nat.is_le(Nat.mul(a, k), _) == True{} : Bool}
1787 le_add_right(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k))
1788
1789# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
1790
1791# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
1792law add_zero_sym:
1793 for x: Nat
1794 {x == Nat.add(x, 0n) : Nat}
1795
1796def add_zero_sym(x):
1797 Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
1798
1799# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
1800law zero_add_sym:
1801 for -x: Nat
1802 {x == Nat.add(0n, x) : Nat}
1803
1804def zero_add_sym(x):
1805 Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
1806
1807# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
1808law add_succ_sym:
1809 for n: Nat
1810 for -m: Nat
1811 {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
1812
1813def add_succ_sym(n, m):
1814 Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
1815
1816# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
1817law succ_add_sym:
1818 for -n: Nat
1819 for -m: Nat
1820 {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
1821
1822def succ_add_sym(n, m):
1823 Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
1824
1825# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
1826law add_comm_sym:
1827 for n: Nat
1828 for m: Nat
1829 {Nat.add(m, n) == Nat.add(n, m) : Nat}
1830
1831def add_comm_sym(n, m):
1832 Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
1833
1834# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
1835law add_assoc_sym:
1836 for a: Nat
1837 for -b: Nat
1838 for -c: Nat
1839 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
1840
1841def add_assoc_sym(a, b, c):
1842 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
1843
1844# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
1845law add_left_comm_sym:
1846 for a: Nat
1847 for b: Nat
1848 for -c: Nat
1849 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
1850
1851def add_left_comm_sym(a, b, c):
1852 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
1853
1854# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
1855law add_right_comm_sym:
1856 for a: Nat
1857 for b: Nat
1858 for c: Nat
1859 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
1860
1861def add_right_comm_sym(a, b, c):
1862 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
1863
1864# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
1865law add_add_add_comm_sym:
1866 for a: Nat
1867 for b: Nat
1868 for c: Nat
1869 for -d: Nat
1870 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
1871
1872def add_add_add_comm_sym(a, b, c, d):
1873 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))
1874
1875# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
1876law mul_zero_sym:
1877 for x: Nat
1878 {0n == Nat.mul(x, 0n) : Nat}
1879
1880def mul_zero_sym(x):
1881 Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
1882
1883# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
1884law zero_mul_sym:
1885 for -x: Nat
1886 {0n == Nat.mul(0n, x) : Nat}
1887
1888def zero_mul_sym(x):
1889 Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
1890
1891# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
1892law mul_one_sym:
1893 for x: Nat
1894 {x == Nat.mul(x, 1n) : Nat}
1895
1896def mul_one_sym(x):
1897 Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
1898
1899# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
1900law one_mul_sym:
1901 for x: Nat
1902 {x == Nat.mul(1n, x) : Nat}
1903
1904def one_mul_sym(x):
1905 Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
1906
1907# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
1908law mul_succ_sym:
1909 for n: Nat
1910 for m: Nat
1911 {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
1912
1913def mul_succ_sym(n, m):
1914 Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
1915
1916# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
1917law succ_mul_sym:
1918 for n: Nat
1919 for m: Nat
1920 {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
1921
1922def succ_mul_sym(n, m):
1923 Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
1924
1925# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
1926law mul_comm_sym:
1927 for n: Nat
1928 for m: Nat
1929 {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
1930
1931def mul_comm_sym(n, m):
1932 Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
1933
1934# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
1935law add_mul_sym:
1936 for a: Nat
1937 for -b: Nat
1938 for c: Nat
1939 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
1940
1941def add_mul_sym(a, b, c):
1942 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))
1943
1944# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
1945law mul_add_sym:
1946 for a: Nat
1947 for b: Nat
1948 for c: Nat
1949 {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
1950
1951def mul_add_sym(a, b, c):
1952 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))
1953
1954# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
1955law mul_assoc_sym:
1956 for a: Nat
1957 for b: Nat
1958 for c: Nat
1959 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
1960
1961def mul_assoc_sym(a, b, c):
1962 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
1963
1964# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
1965law sub_zero_sym:
1966 for n: Nat
1967 {n == Nat.sub(n, 0n) : Nat}
1968
1969def sub_zero_sym(n):
1970 Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
1971
1972# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
1973law zero_sub_sym:
1974 for n: Nat
1975 {0n == Nat.sub(0n, n) : Nat}
1976
1977def zero_sub_sym(n):
1978 Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
1979
1980# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
1981law sub_self_sym:
1982 for n: Nat
1983 {0n == Nat.sub(n, n) : Nat}
1984
1985def sub_self_sym(n):
1986 Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
1987
1988# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
1989law succ_sub_succ_sym:
1990 for -n: Nat
1991 for -m: Nat
1992 {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
1993
1994def succ_sub_succ_sym(n, m):
1995 Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
1996
1997# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
1998law add_sub_cancel_sym:
1999 for n: Nat
2000 for m: Nat
2001 {n == Nat.sub(Nat.add(n, m), m) : Nat}
2002
2003def add_sub_cancel_sym(n, m):
2004 Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
2005
2006# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
2007law add_sub_cancel_left_sym:
2008 for n: Nat
2009 for m: Nat
2010 {m == Nat.sub(Nat.add(n, m), n) : Nat}
2011
2012def add_sub_cancel_left_sym(n, m):
2013 Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
2014
2015# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
2016law sub_sub_sym:
2017 for n: Nat
2018 for m: Nat
2019 for k: Nat
2020 {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
2021
2022def sub_sub_sym(n, m, k):
2023 Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
2024
2025# 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.
2026law div_mod_eq_sym:
2027 for +a: Nat
2028 for +b: Nat
2029 {a == Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) : Nat}
2030
2031def div_mod_eq_sym(a, b):
2032 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))
2033
2034# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
2035law add_div_left_sym:
2036 for +a: Nat
2037 for +b: Nat
2038 {1n+Nat.div(a, 1n+b) == Nat.div(Nat.add(1n+b, a), 1n+b) : Nat}
2039
2040def add_div_left_sym(a, b):
2041 Equal.sym(Nat, Nat.div(Nat.add(1n+b, a), 1n+b), 1n+Nat.div(a, 1n+b), add_div_left(a, b))
2042
2043# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
2044law le_div_iff_mul_le_sym:
2045 for n: Nat
2046 for +a: Nat
2047 for +b: Nat
2048 {Nat.is_le(Nat.mul(n, 1n+b), a) == Nat.is_le(n, Nat.div(a, 1n+b)) : Bool}
2049
2050def le_div_iff_mul_le_sym(n, a, b):
2051 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))
2052
2053# Minimum is commutative, reversed to rewrite toward the simple side.
2054law min_comm_sym:
2055 for a: Nat
2056 for b: Nat
2057 {Nat.min(b, a) == Nat.min(a, b) : Nat}
2058
2059def min_comm_sym(a, b):
2060 Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
2061
2062# Maximum is commutative, reversed to rewrite toward the simple side.
2063law max_comm_sym:
2064 for a: Nat
2065 for b: Nat
2066 {Nat.max(b, a) == Nat.max(a, b) : Nat}
2067
2068def max_comm_sym(a, b):
2069 Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
2070
2071# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
2072law min_self_sym:
2073 for a: Nat
2074 {a == Nat.min(a, a) : Nat}
2075
2076def min_self_sym(a):
2077 Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
2078
2079# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
2080law max_self_sym:
2081 for a: Nat
2082 {a == Nat.max(a, a) : Nat}
2083
2084def max_self_sym(a):
2085 Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
2086
2087# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
2088law min_zero_sym:
2089 for a: Nat
2090 {0n == Nat.min(a, 0n) : Nat}
2091
2092def min_zero_sym(a):
2093 Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
2094
2095# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
2096law zero_min_sym:
2097 for a: Nat
2098 {0n == Nat.min(0n, a) : Nat}
2099
2100def zero_min_sym(a):
2101 Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
2102
2103# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
2104law max_zero_sym:
2105 for a: Nat
2106 {a == Nat.max(a, 0n) : Nat}
2107
2108def max_zero_sym(a):
2109 Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
2110
2111# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
2112law zero_max_sym:
2113 for a: Nat
2114 {a == Nat.max(0n, a) : Nat}
2115
2116def zero_max_sym(a):
2117 Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
2118
2119# Minimum is associative, reversed to rewrite toward the simple side.
2120law min_assoc_sym:
2121 for a: Nat
2122 for b: Nat
2123 for c: Nat
2124 {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
2125
2126def min_assoc_sym(a, b, c):
2127 Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
2128
2129# Maximum is associative, reversed to rewrite toward the simple side.
2130law max_assoc_sym:
2131 for a: Nat
2132 for b: Nat
2133 for c: Nat
2134 {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
2135
2136def max_assoc_sym(a, b, c):
2137 Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
2138
2139# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
2140law min_add_max_sym:
2141 for a: Nat
2142 for b: Nat
2143 {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
2144
2145def min_add_max_sym(a, b):
2146 Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
2147
2148# Any natural to the power zero is one, reversed to rewrite toward the simple side.
2149law pow_zero_sym:
2150 for -a: Nat
2151 {1n == Nat.pow(a, 0n) : Nat}
2152
2153def pow_zero_sym(a):
2154 Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
2155
2156# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
2157law pow_succ_sym:
2158 for -a: Nat
2159 for -n: Nat
2160 {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
2161
2162def pow_succ_sym(a, n):
2163 Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
2164
2165# Any natural to the power one is itself, reversed to rewrite toward the simple side.
2166law pow_one_sym:
2167 for a: Nat
2168 {a == Nat.pow(a, 1n) : Nat}
2169
2170def pow_one_sym(a):
2171 Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
2172
2173# One to any power is one, reversed to rewrite toward the simple side.
2174law one_pow_sym:
2175 for n: Nat
2176 {1n == Nat.pow(1n, n) : Nat}
2177
2178def one_pow_sym(n):
2179 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
2180
2181# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
2182law pow_add_sym:
2183 for a: Nat
2184 for m: Nat
2185 for n: Nat
2186 {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
2187
2188def pow_add_sym(a, m, n):
2189 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))
2190
2191# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
2192law double_eq_add_sym:
2193 for n: Nat
2194 {Nat.add(n, n) == Nat.double(n) : Nat}
2195
2196def double_eq_add_sym(n):
2197 Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
2198
2199# Every natural tests equal to itself, reversed to rewrite toward the simple side.
2200law is_eq_refl_sym:
2201 for n: Nat
2202 {True{} == Nat.is_eq(n, n) : Bool}
2203
2204def is_eq_refl_sym(n):
2205 Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
2206
2207# The equality test is symmetric, reversed to rewrite toward the simple side.
2208law is_eq_comm_sym:
2209 for a: Nat
2210 for b: Nat
2211 {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
2212
2213def is_eq_comm_sym(a, b):
2214 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
2215
2216# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
2217law is_ge_eq_is_le_sym:
2218 for a: Nat
2219 for b: Nat
2220 {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
2221
2222def is_ge_eq_is_le_sym(a, b):
2223 Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
2224
2225# A > b tests the same as b < a, reversed to rewrite toward the simple side.
2226law is_gt_eq_is_lt_sym:
2227 for a: Nat
2228 for b: Nat
2229 {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
2230
2231def is_gt_eq_is_lt_sym(a, b):
2232 Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
2233
2234# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
2235law is_lt_eq_succ_le_sym:
2236 for a: Nat
2237 for b: Nat
2238 {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
2239
2240def is_lt_eq_succ_le_sym(a, b):
2241 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
2242
2243# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
2244law not_is_le_sym:
2245 for a: Nat
2246 for b: Nat
2247 {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
2248
2249def not_is_le_sym(a, b):
2250 Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
2251
2252# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
2253law not_is_lt_sym:
2254 for a: Nat
2255 for b: Nat
2256 {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
2257
2258def not_is_lt_sym(a, b):
2259 Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))
2260
2261# 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.
2262law min_le_iff_sym:
2263 for a: Nat
2264 for b: Nat
2265 for c: Nat
2266 {Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.min(a, b), c) : Bool}
2267
2268def min_le_iff_sym(a, b, c):
2269 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))
2270
2271# 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.
2272law lt_max_iff_sym:
2273 for a: Nat
2274 for b: Nat
2275 for c: Nat
2276 {Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.max(b, c)) : Bool}
2277
2278def lt_max_iff_sym(a, b, c):
2279 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))
2280
2281# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
2282law lt_sub_iff_add_lt_sym:
2283 for a: Nat
2284 for b: Nat
2285 for c: Nat
2286 {Nat.is_lt(Nat.add(b, a), c) == Nat.is_lt(a, Nat.sub(c, b)) : Bool}
2287
2288def lt_sub_iff_add_lt_sym(a, b, c):
2289 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))