nat.bend
bend-mathlib@0.7.1.0 · 4,777 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# Zero divided by anything is zero: 0 / b = 0.
1848law zero_div:
1849 for b: Nat
1850 {Nat.div(0n, b) == 0n : Nat}
1851
1852def zero_div(b):
1853 match b:
1854 case 0n:
1855 {==}
1856 case 1n+p:
1857 {==}
1858
1859# Zero modulo anything is zero: 0 % b = 0.
1860law zero_mod:
1861 for b: Nat
1862 {Nat.mod(0n, b) == 0n : Nat}
1863
1864def zero_mod(b):
1865 match b:
1866 case 0n:
1867 {==}
1868 case 1n+p:
1869 {==}
1870
1871def internal_div_go_one(a: Nat, +d: Nat) -> {(Nat.add(a, d), 0n) == Nat.divmod.go(a, 0n, d, 0n) : Nat & Nat}:
1872 match a:
1873 case 0n:
1874 {==}
1875 case 1n++p:
1876 %add_succ(p, d) : {(_, 0n) == Nat.divmod.go(p, 0n, 1n+d, 0n) : Nat & Nat}
1877 internal_div_go_one(p, 1n+d)
1878
1879# Dividing by one changes nothing: a / 1 = a.
1880law div_one:
1881 for a: Nat
1882 {Nat.div(a, 1n) == a : Nat}
1883
1884def div_one(a):
1885 +a = a
1886 %internal_div_go_one(a, 0n) : {Pair.fst(Nat, Nat, _) == a : Nat}
1887 add_zero(a)
1888
1889# Any natural modulo one is zero: a % 1 = 0.
1890law mod_one:
1891 for a: Nat
1892 {Nat.mod(a, 1n) == 0n : Nat}
1893
1894def mod_one(a):
1895 +a = a
1896 %internal_div_go_one(a, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1897 {==}
1898
1899def internal_div_go_self(m: Nat, -d: Nat, -r: Nat) -> {(1n+d, 0n) == Nat.divmod.go(1n+m, m, d, r) : Nat & Nat}:
1900 match m:
1901 case 0n:
1902 {==}
1903 case 1n+p:
1904 internal_div_go_self(p, d, 1n+r)
1905
1906# A natural modulo itself is zero: n % n = 0.
1907law mod_self:
1908 for n: Nat
1909 {Nat.mod(n, n) == 0n : Nat}
1910
1911def mod_self(n):
1912 match n:
1913 case 0n:
1914 {==}
1915 case 1n++p:
1916 %internal_div_go_self(p, 0n, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1917 {==}
1918
1919# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1.
1920law div_self:
1921 for b: Nat
1922 {Nat.div(1n+b, 1n+b) == 1n : Nat}
1923
1924def div_self(b):
1925 +b = b
1926 %internal_div_go_self(b, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n : Nat}
1927 {==}
1928
1929def internal_mod_go_le(n: Nat, m: Nat, -d: Nat, +r: Nat) -> le(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), Nat.add(r, m)):
1930 match n m:
1931 case 0n k:
1932 le_add_right(r, k)
1933 case 1n++np 0n:
1934 %internal_div_add_zero_r(r) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), _)
1935 internal_mod_go_le(np, r, 1n+d, 0n)
1936 case 1n++np 1n++mp:
1937 %Equal.sym(Nat, Nat.add(r, 1n+mp), 1n+Nat.add(r, mp), add_succ(r, mp)) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), _)
1938 internal_mod_go_le(np, mp, d, 1n+r)
1939
1940# A remainder is below its positive divisor: a % (1 + b) < 1 + b.
1941law mod_lt:
1942 for a: Nat
1943 for b: Nat
1944 lt(Nat.mod(a, 1n+b), 1n+b)
1945
1946def mod_lt(a, b):
1947 +a = a
1948 +b = b
1949 %Equal.sym(Bool, Nat.is_lt(Nat.mod(a, 1n+b), 1n+b), Nat.is_le(1n+Nat.mod(a, 1n+b), 1n+b), is_lt_eq_succ_le(Nat.mod(a, 1n+b), 1n+b)) : {_ == True{} : Bool}
1950 internal_mod_go_le(a, b, 0n, 0n)
1951
1952# A remainder never exceeds the dividend: a % b <= a.
1953law mod_le:
1954 for a: Nat
1955 for b: Nat
1956 le(Nat.mod(a, b), a)
1957
1958def mod_le(a, b):
1959 match b:
1960 case 0n:
1961 le_refl(a)
1962 case 1n++bp:
1963 +a = a
1964 +bp = bp
1965 le_of_add_eq(Nat.mod(a, 1n+bp), Nat.mul(Nat.div(a, 1n+bp), 1n+bp), a, Equal.trans(Nat, Nat.add(Nat.mod(a, 1n+bp), Nat.mul(Nat.div(a, 1n+bp), 1n+bp)), Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)), a, add_comm(Nat.mod(a, 1n+bp), Nat.mul(Nat.div(a, 1n+bp), 1n+bp)), div_mod_eq(a, bp)))
1966
1967def internal_div_le_self_eq(+q: Nat, +bp: Nat, +m: Nat, -a: Nat, e: {Nat.add(Nat.mul(q, 1n+bp), m) == a : Nat}) -> {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == a : Nat}:
1968 %e : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == _ : Nat}
1969 %mul_comm(1n+bp, q) : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == Nat.add(_, m) : Nat}
1970 Equal.sym(Nat, Nat.add(Nat.add(q, Nat.mul(bp, q)), m), Nat.add(q, Nat.add(Nat.mul(bp, q), m)), add_assoc(q, Nat.mul(bp, q), m))
1971
1972# A quotient never exceeds the dividend: a / b <= a.
1973law div_le_self:
1974 for a: Nat
1975 for b: Nat
1976 le(Nat.div(a, b), a)
1977
1978def div_le_self(a, b):
1979 match b:
1980 case 0n:
1981 zero_le(a)
1982 case 1n++bp:
1983 +a = a
1984 +bp = bp
1985 le_of_add_eq(Nat.div(a, 1n+bp), Nat.add(Nat.mul(bp, Nat.div(a, 1n+bp)), Nat.mod(a, 1n+bp)), a, internal_div_le_self_eq(Nat.div(a, 1n+bp), bp, Nat.mod(a, 1n+bp), a, div_mod_eq(a, bp)))
1986
1987def internal_mod_go_small(n: Nat, -k: Nat, -d: Nat, +r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, Nat.add(n, k), d, r)) == Nat.add(n, r) : Nat}:
1988 match n:
1989 case 0n:
1990 {==}
1991 case 1n++np:
1992 %add_succ(np, r) : {Pair.snd(Nat, Nat, Nat.divmod.go(np, Nat.add(np, k), d, 1n+r)) == _ : Nat}
1993 internal_mod_go_small(np, k, d, 1n+r)
1994
1995def internal_mod_eq_of_wit(+a: Nat, +b: Nat, w: &k:Nat -> {Nat.add(a, k) == b : Nat}) -> {Nat.mod(a, 1n+b) == a : Nat}:
1996 match w:
1997 case (+k, e):
1998 %e : {Nat.mod(a, 1n+_) == a : Nat}
1999 Equal.trans(Nat, Nat.mod(a, 1n+Nat.add(a, k)), Nat.add(a, 0n), a, internal_mod_go_small(a, k, 0n, 0n), add_zero(a))
2000
2001# A number below the divisor is its own remainder: a < b implies a % b = a.
2002law mod_eq_of_lt:
2003 for a: Nat
2004 for b: Nat
2005 for h: lt(a, b)
2006 {Nat.mod(a, b) == a : Nat}
2007
2008def mod_eq_of_lt(a, b, h):
2009 match b:
2010 case 0n:
2011 +a = a
2012 Empty.absurd({Nat.mod(a, 0n) == a : Nat}, lt_zero(a)(h))
2013 case 1n++bp:
2014 +a = a
2015 +bp = bp
2016 internal_mod_eq_of_wit(a, bp, internal_div_le_wit(a, bp, Equal.trans(Bool, Nat.is_le(1n+a, 1n+bp), Nat.is_lt(a, 1n+bp), True{}, Equal.sym(Bool, Nat.is_lt(a, 1n+bp), Nat.is_le(1n+a, 1n+bp), is_lt_eq_succ_le(a, 1n+bp)), h)))
2017
2018# Taking a remainder twice is taking it once: (a % n) % n = a % n.
2019law mod_mod:
2020 for a: Nat
2021 for n: Nat
2022 {Nat.mod(Nat.mod(a, n), n) == Nat.mod(a, n) : Nat}
2023
2024def mod_mod(a, n):
2025 match n:
2026 case 0n:
2027 {==}
2028 case 1n++b:
2029 +a = a
2030 +b = b
2031 mod_eq_of_lt(Nat.mod(a, 1n+b), 1n+b, mod_lt(a, b))
2032
2033def internal_mod_go_d(n: Nat, m: Nat, -d: Nat, -e: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, e, r)) : Nat}:
2034 match n m:
2035 case 0n _:
2036 {==}
2037 case 1n+np 0n:
2038 internal_mod_go_d(np, r, 1n+d, 1n+e, 0n)
2039 case 1n+np 1n+mp:
2040 internal_mod_go_d(np, mp, d, e, 1n+r)
2041
2042# Adding the divisor does not change the remainder: (b + a) % b = a % b.
2043law add_mod_left:
2044 for a: Nat
2045 for b: Nat
2046 {Nat.mod(Nat.add(b, a), b) == Nat.mod(a, b) : Nat}
2047
2048def add_mod_left(a, b):
2049 match b:
2050 case 0n:
2051 {==}
2052 case 1n++bp:
2053 +a = a
2054 %internal_div_go_run(bp, a, 0n, 0n) : {Pair.snd(Nat, Nat, _) == Nat.mod(a, 1n+bp) : Nat}
2055 %internal_div_add_zero_r(bp) : {Pair.snd(Nat, Nat, Nat.divmod.go(a, _, 1n, 0n)) == Nat.mod(a, 1n+bp) : Nat}
2056 internal_mod_go_d(a, bp, 1n, 0n, 0n)
2057
2058# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a.
2059law mul_div_cancel:
2060 for a: Nat
2061 for b: Nat
2062 {Nat.div(Nat.mul(a, 1n+b), 1n+b) == a : Nat}
2063
2064def mul_div_cancel(a, b):
2065 match a:
2066 case 0n:
2067 {==}
2068 case 1n++p:
2069 +b = b
2070 %Equal.sym(Nat, Nat.div(Nat.add(1n+b, Nat.mul(p, 1n+b)), 1n+b), 1n+Nat.div(Nat.mul(p, 1n+b), 1n+b), add_div_left(Nat.mul(p, 1n+b), b)) : {_ == 1n+p : Nat}
2071 %mul_div_cancel(p, b) : {1n+Nat.div(Nat.mul(p, 1n+b), 1n+b) == 1n+_ : Nat}
2072 {==}
2073
2074# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a.
2075law mul_div_cancel_left:
2076 for a: Nat
2077 for b: Nat
2078 {Nat.div(Nat.mul(1n+b, a), 1n+b) == a : Nat}
2079
2080def mul_div_cancel_left(a, b):
2081 +a = a
2082 +b = b
2083 %mul_comm(a, 1n+b) : {Nat.div(_, 1n+b) == a : Nat}
2084 mul_div_cancel(a, b)
2085
2086# A multiple of b leaves no remainder modulo b: (a * b) % b = 0.
2087law mul_mod_left:
2088 for a: Nat
2089 for b: Nat
2090 {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}
2091
2092def mul_mod_left(a, b):
2093 match a b:
2094 case _ 0n:
2095 mul_zero(a)
2096 case 0n 1n+bp:
2097 {==}
2098 case 1n++p 1n++bp:
2099 Equal.trans(Nat, Nat.mod(Nat.add(1n+bp, Nat.mul(p, 1n+bp)), 1n+bp), Nat.mod(Nat.mul(p, 1n+bp), 1n+bp), 0n, add_mod_left(Nat.mul(p, 1n+bp), 1n+bp), mul_mod_left(p, 1n+bp))
2100
2101# A multiple of a leaves no remainder modulo a: (a * b) % a = 0.
2102law mul_mod_right:
2103 for a: Nat
2104 for b: Nat
2105 {Nat.mod(Nat.mul(a, b), a) == 0n : Nat}
2106
2107def mul_mod_right(a, b):
2108 +a = a
2109 +b = b
2110 %mul_comm(b, a) : {Nat.mod(_, a) == 0n : Nat}
2111 mul_mod_left(b, a)
2112
2113# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a.
2114law mod_add_div:
2115 for a: Nat
2116 for b: Nat
2117 {Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) == a : Nat}
2118
2119def mod_add_div(a, b):
2120 match b:
2121 case 0n:
2122 add_zero(a)
2123 case 1n++bp:
2124 +a = a
2125 %add_comm(Nat.mul(1n+bp, Nat.div(a, 1n+bp)), Nat.mod(a, 1n+bp)) : {_ == a : Nat}
2126 %mul_comm(Nat.div(a, 1n+bp), 1n+bp) : {Nat.add(_, Nat.mod(a, 1n+bp)) == a : Nat}
2127 div_mod_eq(a, bp)
2128
2129# The quotient times the divisor never exceeds the dividend: (a / b) * b <= a.
2130law div_mul_le_self:
2131 for a: Nat
2132 for b: Nat
2133 le(Nat.mul(Nat.div(a, b), b), a)
2134
2135def div_mul_le_self(a, b):
2136 match b:
2137 case 0n:
2138 zero_le(a)
2139 case 1n++bp:
2140 +a = a
2141 le_of_add_eq(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp), a, div_mod_eq(a, bp))
2142
2143# Left commutativity of multiplication: a * (b * c) = b * (a * c).
2144law mul_left_comm:
2145 for a: Nat
2146 for b: Nat
2147 for c: Nat
2148 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
2149
2150def mul_left_comm(a, b, c):
2151 +a = a
2152 +b = b
2153 +c = c
2154 %mul_assoc(a, b, c) : {_ == Nat.mul(b, Nat.mul(a, c)) : Nat}
2155 %mul_comm(b, a) : {Nat.mul(_, c) == Nat.mul(b, Nat.mul(a, c)) : Nat}
2156 mul_assoc(b, a, c)
2157
2158# Right commutativity of multiplication: (a * b) * c = (a * c) * b.
2159law mul_right_comm:
2160 for a: Nat
2161 for b: Nat
2162 for c: Nat
2163 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
2164
2165def mul_right_comm(a, b, c):
2166 +a = a
2167 +b = b
2168 +c = c
2169 %Equal.sym(Nat, Nat.mul(Nat.mul(a, c), b), Nat.mul(a, Nat.mul(c, b)), mul_assoc(a, c, b)) : {Nat.mul(Nat.mul(a, b), c) == _ : Nat}
2170 %mul_comm(b, c) : {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, _) : Nat}
2171 mul_assoc(a, b, c)
2172
2173# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d).
2174law mul_mul_mul_comm:
2175 for a: Nat
2176 for b: Nat
2177 for c: Nat
2178 for d: Nat
2179 {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
2180
2181def mul_mul_mul_comm(a, b, c, d):
2182 +a = a
2183 +b = b
2184 +c = c
2185 +d = d
2186 %Equal.sym(Nat, Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), Nat.mul(a, Nat.mul(c, Nat.mul(b, d))), mul_assoc(a, c, Nat.mul(b, d))) : {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == _ : Nat}
2187 %mul_left_comm(b, c, d) : {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(a, _) : Nat}
2188 mul_assoc(a, b, Nat.mul(c, d))
2189
2190# Zero to a positive power is zero: 0^(n+1) = 0.
2191law zero_pow:
2192 for -n: Nat
2193 {Nat.pow(0n, 1n+n) == 0n : Nat}
2194
2195def zero_pow(n):
2196 {==}
2197
2198# A power of a product is the product of the powers: (a * b)^n = a^n * b^n.
2199law mul_pow:
2200 for +a: Nat
2201 for +b: Nat
2202 for n: Nat
2203 {Nat.pow(Nat.mul(a, b), n) == Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) : Nat}
2204
2205def mul_pow(a, b, n):
2206 match n:
2207 case 0n:
2208 {==}
2209 case 1n++p:
2210 %Equal.sym(Nat, Nat.pow(Nat.mul(a, b), p), Nat.mul(Nat.pow(a, p), Nat.pow(b, p)), mul_pow(a, b, p)) : {Nat.mul(Nat.mul(a, b), _) == Nat.mul(Nat.mul(a, Nat.pow(a, p)), Nat.mul(b, Nat.pow(b, p))) : Nat}
2211 mul_mul_mul_comm(a, b, Nat.pow(a, p), Nat.pow(b, p))
2212
2213# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n.
2214law pow_mul:
2215 for a: Nat
2216 for m: Nat
2217 for n: Nat
2218 {Nat.pow(a, Nat.mul(m, n)) == Nat.pow(Nat.pow(a, m), n) : Nat}
2219
2220def pow_mul(a, m, n):
2221 match m:
2222 case 0n:
2223 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
2224 case 1n++p:
2225 +a = a
2226 +n = n
2227 %Equal.sym(Nat, Nat.pow(Nat.mul(a, Nat.pow(a, p)), n), Nat.mul(Nat.pow(a, n), Nat.pow(Nat.pow(a, p), n)), mul_pow(a, Nat.pow(a, p), n)) : {Nat.pow(a, Nat.add(n, Nat.mul(p, n))) == _ : Nat}
2228 %pow_mul(a, p, n) : {Nat.pow(a, Nat.add(n, Nat.mul(p, n))) == Nat.mul(Nat.pow(a, n), _) : Nat}
2229 pow_add(a, n, Nat.mul(p, n))
2230
2231# A power of a positive base is at least one: 1 <= (1 + a)^n.
2232law one_le_pow:
2233 for n: Nat
2234 for a: Nat
2235 le(1n, Nat.pow(1n+a, n))
2236
2237def one_le_pow(n, a):
2238 match n:
2239 case 0n:
2240 {==}
2241 case 1n++p:
2242 +a = a
2243 le_trans(1n, Nat.pow(1n+a, p), Nat.add(Nat.pow(1n+a, p), Nat.mul(a, Nat.pow(1n+a, p))), one_le_pow(p, a), le_add_right(Nat.pow(1n+a, p), Nat.mul(a, Nat.pow(1n+a, p))))
2244
2245# A power of a positive base is positive: 0 < (1 + a)^n.
2246law pow_pos:
2247 for n: Nat
2248 for a: Nat
2249 lt(0n, Nat.pow(1n+a, n))
2250
2251def pow_pos(n, a):
2252 +n = n
2253 +a = a
2254 %Equal.sym(Bool, Nat.is_lt(0n, Nat.pow(1n+a, n)), Nat.is_le(1n, Nat.pow(1n+a, n)), is_lt_eq_succ_le(0n, Nat.pow(1n+a, n))) : {_ == True{} : Bool}
2255 one_le_pow(n, a)
2256
2257# Adding on the left never decreases a natural: n <= m + n.
2258law le_add_left:
2259 for n: Nat
2260 for m: Nat
2261 le(n, Nat.add(m, n))
2262
2263def le_add_left(n, m):
2264 match m:
2265 case 0n:
2266 le_refl(n)
2267 case 1n++p:
2268 +n = n
2269 le_trans(n, Nat.add(p, n), 1n+Nat.add(p, n), le_add_left(n, p), le_succ(Nat.add(p, n)))
2270
2271# A common left summand cancels in a difference: (k + n) - (k + m) = n - m.
2272law add_sub_add_left:
2273 for k: Nat
2274 for -n: Nat
2275 for -m: Nat
2276 {Nat.sub(Nat.add(k, n), Nat.add(k, m)) == Nat.sub(n, m) : Nat}
2277
2278def add_sub_add_left(k, n, m):
2279 match k:
2280 case 0n:
2281 {==}
2282 case 1n+p:
2283 add_sub_add_left(p, n, m)
2284
2285# A common right summand cancels in a difference: (n + k) - (m + k) = n - m.
2286law add_sub_add_right:
2287 for n: Nat
2288 for k: Nat
2289 for m: Nat
2290 {Nat.sub(Nat.add(n, k), Nat.add(m, k)) == Nat.sub(n, m) : Nat}
2291
2292def add_sub_add_right(n, k, m):
2293 +n = n
2294 +k = k
2295 +m = m
2296 %add_comm(k, n) : {Nat.sub(_, Nat.add(m, k)) == Nat.sub(n, m) : Nat}
2297 %add_comm(k, m) : {Nat.sub(Nat.add(k, n), _) == Nat.sub(n, m) : Nat}
2298 add_sub_add_left(k, n, m)
2299
2300# Subtracting a part of the right summand: k <= m implies (n + m) - k = n + (m - k).
2301law add_sub_assoc:
2302 for k: Nat
2303 for m: Nat
2304 for h: le(k, m)
2305 for n: Nat
2306 {Nat.sub(Nat.add(n, m), k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2307
2308def add_sub_assoc(k, m, h, n):
2309 +k = k
2310 +m = m
2311 +n = n
2312 %sub_add_cancel(m, k, h) : {Nat.sub(Nat.add(n, _), k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2313 %add_assoc(n, Nat.sub(m, k), k) : {Nat.sub(_, k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2314 add_sub_cancel(Nat.add(n, Nat.sub(m, k)), k)
2315
2316# Subtracting a difference from its minuend: m <= n implies n - (n - m) = m.
2317law sub_sub_self:
2318 for n: Nat
2319 for m: Nat
2320 for h: le(m, n)
2321 {Nat.sub(n, Nat.sub(n, m)) == m : Nat}
2322
2323def sub_sub_self(n, m, h):
2324 match n m:
2325 case 0n 0n:
2326 {==}
2327 case 0n 1n+q:
2328 Empty.absurd({Nat.sub(0n, Nat.sub(0n, 1n+q)) == 1n+q : Nat}, internal_false_ne_true(h))
2329 case 1n+p 0n:
2330 sub_self(p)
2331 case 1n++p 1n++q:
2332 Equal.trans(Nat, Nat.sub(1n+p, Nat.sub(p, q)), 1n+Nat.sub(p, Nat.sub(p, q)), 1n+q, succ_sub(p, Nat.sub(p, q), sub_le(p, q)), Equal.cong(Nat, Nat, x => 1n+x, Nat.sub(p, Nat.sub(p, q)), q, sub_sub_self(p, q, h)))
2333
2334# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k.
2335law sub_mul:
2336 for n: Nat
2337 for m: Nat
2338 for k: Nat
2339 {Nat.mul(Nat.sub(n, m), k) == Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) : Nat}
2340
2341def sub_mul(n, m, k):
2342 match n m:
2343 case 0n _:
2344 {==}
2345 case 1n++p 0n:
2346 +k = k
2347 Equal.sym(Nat, Nat.sub(Nat.mul(1n+p, k), 0n), Nat.mul(1n+p, k), sub_zero(Nat.mul(1n+p, k)))
2348 case 1n++p 1n++q:
2349 +k = k
2350 %Equal.sym(Nat, Nat.sub(Nat.add(k, Nat.mul(p, k)), Nat.add(k, Nat.mul(q, k))), Nat.sub(Nat.mul(p, k), Nat.mul(q, k)), add_sub_add_left(k, Nat.mul(p, k), Nat.mul(q, k))) : {Nat.mul(Nat.sub(p, q), k) == _ : Nat}
2351 sub_mul(p, q, k)
2352
2353# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k.
2354law mul_sub:
2355 for n: Nat
2356 for m: Nat
2357 for k: Nat
2358 {Nat.mul(n, Nat.sub(m, k)) == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}
2359
2360def mul_sub(n, m, k):
2361 +n = n
2362 +m = m
2363 +k = k
2364 %mul_comm(Nat.sub(m, k), n) : {_ == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}
2365 %mul_comm(m, n) : {Nat.mul(Nat.sub(m, k), n) == Nat.sub(_, Nat.mul(n, k)) : Nat}
2366 %mul_comm(k, n) : {Nat.mul(Nat.sub(m, k), n) == Nat.sub(Nat.mul(m, n), _) : Nat}
2367 sub_mul(m, k, n)
2368
2369# The minimum is the smaller argument on the left: a <= b implies min a b = a.
2370law min_eq_left:
2371 for a: Nat
2372 for b: Nat
2373 for h: le(a, b)
2374 {Nat.min(a, b) == a : Nat}
2375
2376def min_eq_left(a, b, h):
2377 match a b:
2378 case 0n _:
2379 {==}
2380 case 1n+p 0n:
2381 Empty.absurd({Nat.min(1n+p, 0n) == 1n+p : Nat}, internal_false_ne_true(h))
2382 case 1n++p 1n+q:
2383 %min_eq_left(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
2384 {==}
2385
2386# The minimum is the smaller argument on the right: b <= a implies min a b = b.
2387law min_eq_right:
2388 for a: Nat
2389 for b: Nat
2390 for h: le(b, a)
2391 {Nat.min(a, b) == b : Nat}
2392
2393def min_eq_right(a, b, h):
2394 match a b:
2395 case 0n 0n:
2396 {==}
2397 case 0n 1n+q:
2398 Empty.absurd({Nat.min(0n, 1n+q) == 1n+q : Nat}, internal_false_ne_true(h))
2399 case 1n+p 0n:
2400 {==}
2401 case 1n+p 1n++q:
2402 %min_eq_right(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
2403 {==}
2404
2405# The maximum is the larger argument on the left: b <= a implies max a b = a.
2406law max_eq_left:
2407 for a: Nat
2408 for b: Nat
2409 for h: le(b, a)
2410 {Nat.max(a, b) == a : Nat}
2411
2412def max_eq_left(a, b, h):
2413 match a b:
2414 case 0n 0n:
2415 {==}
2416 case 0n 1n+q:
2417 Empty.absurd({Nat.max(0n, 1n+q) == 0n : Nat}, internal_false_ne_true(h))
2418 case 1n+p 0n:
2419 {==}
2420 case 1n++p 1n+q:
2421 %max_eq_left(p, q, h) : {1n+Nat.max(p, q) == 1n+_ : Nat}
2422 {==}
2423
2424# The maximum is the larger argument on the right: a <= b implies max a b = b.
2425law max_eq_right:
2426 for a: Nat
2427 for b: Nat
2428 for h: le(a, b)
2429 {Nat.max(a, b) == b : Nat}
2430
2431def max_eq_right(a, b, h):
2432 match a b:
2433 case 0n _:
2434 {==}
2435 case 1n+p 0n:
2436 Empty.absurd({Nat.max(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
2437 case 1n+p 1n++q:
2438 %max_eq_right(p, q, h) : {1n+Nat.max(p, q) == 1n+_ : Nat}
2439 {==}
2440
2441def internal_and_false_sym(x: Bool) -> {False{} == Bool.and(x, False{}) : Bool}:
2442 match x:
2443 case False{}:
2444 {==}
2445 case True{}:
2446 {==}
2447
2448def internal_and_true_sym(x: Bool) -> {x == Bool.and(x, True{}) : Bool}:
2449 match x:
2450 case False{}:
2451 {==}
2452 case True{}:
2453 {==}
2454
2455# A number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c (Mathlib's le_min_iff; the implication is le_min_of_le_of_le).
2456law le_min:
2457 for a: Nat
2458 for b: Nat
2459 for c: Nat
2460 {Nat.is_le(a, Nat.min(b, c)) == Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)) : Bool}
2461
2462def le_min(a, b, c):
2463 match a b c:
2464 case 0n 0n 0n:
2465 {==}
2466 case 0n 0n 1n+r:
2467 {==}
2468 case 0n 1n+q 0n:
2469 {==}
2470 case 0n 1n+q 1n+r:
2471 {==}
2472 case 1n+p 0n _:
2473 {==}
2474 case 1n+p 1n+q 0n:
2475 internal_and_false_sym(Nat.is_le(p, q))
2476 case 1n+p 1n+q 1n+r:
2477 le_min(p, q, r)
2478
2479# The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c (Mathlib's max_le_iff; the implication is max_le_of_le_of_le).
2480law max_le:
2481 for a: Nat
2482 for b: Nat
2483 for c: Nat
2484 {Nat.is_le(Nat.max(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
2485
2486def max_le(a, b, c):
2487 match a b c:
2488 case 0n _ 0n:
2489 {==}
2490 case 0n _ 1n+r:
2491 {==}
2492 case 1n+p 0n 0n:
2493 {==}
2494 case 1n+p 0n 1n+r:
2495 internal_and_true_sym(Nat.is_le(p, r))
2496 case 1n+p 1n+q 0n:
2497 {==}
2498 case 1n+p 1n+q 1n+r:
2499 max_le(p, q, r)
2500
2501# Multiplying on the left preserves the order: a <= b implies k * a <= k * b.
2502law mul_le_mul_left:
2503 for a: Nat
2504 for b: Nat
2505 for k: Nat
2506 for h: le(a, b)
2507 le(Nat.mul(k, a), Nat.mul(k, b))
2508
2509def mul_le_mul_left(a, b, k, h):
2510 +a = a
2511 +b = b
2512 +k = k
2513 %mul_comm(a, k) : le(_, Nat.mul(k, b))
2514 %mul_comm(b, k) : le(Nat.mul(a, k), _)
2515 mul_le_mul_right(a, b, k, h)
2516
2517# Multiplying two bounded factors stays bounded: a <= c and b <= d imply a * b <= c * d.
2518law mul_le_mul:
2519 for a: Nat
2520 for b: Nat
2521 for c: Nat
2522 for d: Nat
2523 for h1: le(a, c)
2524 for h2: le(b, d)
2525 le(Nat.mul(a, b), Nat.mul(c, d))
2526
2527def mul_le_mul(a, b, c, d, h1, h2):
2528 +a = a
2529 +b = b
2530 +c = c
2531 +d = d
2532 le_trans(Nat.mul(a, b), Nat.mul(c, b), Nat.mul(c, d), mul_le_mul_right(a, c, b, h1), mul_le_mul_left(b, d, c, h2))
2533
2534# Every successor is positive: 0 < n + 1.
2535law succ_pos:
2536 for -n: Nat
2537 lt(0n, 1n+n)
2538
2539def succ_pos(n):
2540 {==}
2541
2542# Below a successor means at most: m < n + 1 tests as m <= n.
2543law lt_succ_iff:
2544 for m: Nat
2545 for n: Nat
2546 {Nat.is_lt(m, 1n+n) == Nat.is_le(m, n) : Bool}
2547
2548def lt_succ_iff(m, n):
2549 is_lt_eq_succ_le(m, 1n+n)
2550
2551# The successor preserves the strict order: a < b implies a + 1 < b + 1.
2552law succ_lt_succ:
2553 for -a: Nat
2554 for -b: Nat
2555 for h: lt(a, b)
2556 lt(1n+a, 1n+b)
2557
2558def succ_lt_succ(a, b, h):
2559 h
2560
2561# The strict order of successors is the strict order of the naturals: a + 1 < b + 1 implies a < b.
2562law lt_of_succ_lt_succ:
2563 for -a: Nat
2564 for -b: Nat
2565 for h: lt(1n+a, 1n+b)
2566 lt(a, b)
2567
2568def lt_of_succ_lt_succ(a, b, h):
2569 h
2570
2571# Below a successor is at most: m < n + 1 implies m <= n.
2572law le_of_lt_succ:
2573 for m: Nat
2574 for n: Nat
2575 for h: lt(m, 1n+n)
2576 le(m, n)
2577
2578def le_of_lt_succ(m, n, h):
2579 Equal.trans(Bool, Nat.is_le(m, n), Nat.is_lt(m, 1n+n), True{}, Equal.sym(Bool, Nat.is_lt(m, 1n+n), Nat.is_le(m, n), lt_succ_iff(m, n)), h)
2580
2581# At most is below the successor: m <= n implies m < n + 1.
2582law lt_succ_of_le:
2583 for m: Nat
2584 for n: Nat
2585 for h: le(m, n)
2586 lt(m, 1n+n)
2587
2588def lt_succ_of_le(m, n, h):
2589 Equal.trans(Bool, Nat.is_lt(m, 1n+n), Nat.is_le(m, n), True{}, lt_succ_iff(m, n), h)
2590
2591# A strict inequality gives the weak one from the successor: n < m implies n + 1 <= m.
2592law succ_le_of_lt:
2593 for n: Nat
2594 for m: Nat
2595 for h: lt(n, m)
2596 le(1n+n, m)
2597
2598def succ_le_of_lt(n, m, h):
2599 Equal.trans(Bool, Nat.is_le(1n+n, m), Nat.is_lt(n, m), True{}, Equal.sym(Bool, Nat.is_lt(n, m), Nat.is_le(1n+n, m), is_lt_eq_succ_le(n, m)), h)
2600
2601# A weak inequality from the successor gives the strict one: n + 1 <= m implies n < m.
2602law lt_of_succ_le:
2603 for n: Nat
2604 for m: Nat
2605 for h: le(1n+n, m)
2606 lt(n, m)
2607
2608def lt_of_succ_le(n, m, h):
2609 Equal.trans(Bool, Nat.is_lt(n, m), Nat.is_le(1n+n, m), True{}, is_lt_eq_succ_le(n, m), h)
2610
2611# The strict order is asymmetric: a < b rules out b < a.
2612law lt_asymm:
2613 for a: Nat
2614 for b: Nat
2615 for h: lt(a, b)
2616 lt(b, a) -> Empty
2617
2618def lt_asymm(a, b, h):
2619 +a = a
2620 h2 => lt_irrefl(a)(lt_trans(a, b, a, h, h2))
2621
2622# At most means below or equal: a <= b tests as a < b or a = b.
2623law le_iff_lt_or_eq:
2624 for a: Nat
2625 for b: Nat
2626 {Nat.is_le(a, b) == Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)) : Bool}
2627
2628def le_iff_lt_or_eq(a, b):
2629 match a b:
2630 case 0n 0n:
2631 {==}
2632 case 0n 1n+q:
2633 {==}
2634 case 1n+p 0n:
2635 {==}
2636 case 1n+p 1n+q:
2637 le_iff_lt_or_eq(p, q)
2638
2639# Below means at most and different: a < b tests as a <= b and not a = b.
2640law lt_iff_le_and_ne:
2641 for a: Nat
2642 for b: Nat
2643 {Nat.is_lt(a, b) == Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))) : Bool}
2644
2645def lt_iff_le_and_ne(a, b):
2646 match a b:
2647 case 0n 0n:
2648 {==}
2649 case 0n 1n+q:
2650 {==}
2651 case 1n+p 0n:
2652 {==}
2653 case 1n+p 1n+q:
2654 lt_iff_le_and_ne(p, q)
2655
2656# A natural that does not test equal to zero is positive.
2657law pos_of_ne_zero:
2658 for n: Nat
2659 for h: {Nat.is_eq(n, 0n) == False{} : Bool}
2660 lt(0n, n)
2661
2662def pos_of_ne_zero(n, h):
2663 match n:
2664 case 0n:
2665 Empty.absurd(lt(0n, 0n), internal_div_true_ne_false(h))
2666 case 1n+p:
2667 {==}
2668
2669# Adding on the right keeps a strict bound: n < m implies n < m + k.
2670law lt_add_right:
2671 for n: Nat
2672 for m: Nat
2673 for -k: Nat
2674 for h: lt(n, m)
2675 lt(n, Nat.add(m, k))
2676
2677def lt_add_right(n, m, k, h):
2678 match n m:
2679 case 0n 0n:
2680 Empty.absurd(lt(0n, Nat.add(0n, k)), internal_false_ne_true(h))
2681 case 0n 1n+q:
2682 {==}
2683 case 1n+p 0n:
2684 Empty.absurd(lt(1n+p, Nat.add(0n, k)), internal_false_ne_true(h))
2685 case 1n+p 1n+q:
2686 lt_add_right(p, q, k, h)
2687
2688# Adding a positive amount on the right strictly increases: n < n + (1 + k).
2689law lt_add_of_pos_right:
2690 for n: Nat
2691 for -k: Nat
2692 lt(n, Nat.add(n, 1n+k))
2693
2694def lt_add_of_pos_right(n, k):
2695 match n:
2696 case 0n:
2697 {==}
2698 case 1n+p:
2699 lt_add_of_pos_right(p, k)
2700
2701# Adding a positive amount on the left strictly increases: n < (1 + k) + n.
2702law lt_add_of_pos_left:
2703 for n: Nat
2704 for k: Nat
2705 lt(n, Nat.add(1n+k, n))
2706
2707def lt_add_of_pos_left(n, k):
2708 +n = n
2709 +k = k
2710 lt_succ_of_le(n, Nat.add(k, n), le_add_left(n, k))
2711
2712# Adding on the left preserves the strict order: a < b implies k + a < k + b.
2713law add_lt_add_left:
2714 for -a: Nat
2715 for -b: Nat
2716 for k: Nat
2717 for h: lt(a, b)
2718 lt(Nat.add(k, a), Nat.add(k, b))
2719
2720def add_lt_add_left(a, b, k, h):
2721 match k:
2722 case 0n:
2723 h
2724 case 1n+p:
2725 add_lt_add_left(a, b, p, h)
2726
2727# Adding on the right preserves the strict order: a < b implies a + k < b + k.
2728law add_lt_add_right:
2729 for a: Nat
2730 for b: Nat
2731 for k: Nat
2732 for h: lt(a, b)
2733 lt(Nat.add(a, k), Nat.add(b, k))
2734
2735def add_lt_add_right(a, b, k, h):
2736 +a = a
2737 +b = b
2738 +k = k
2739 %add_comm(k, a) : lt(_, Nat.add(b, k))
2740 %add_comm(k, b) : lt(Nat.add(k, a), _)
2741 add_lt_add_left(a, b, k, h)
2742
2743# Adding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b.
2744law add_lt_add_iff_left:
2745 for k: Nat
2746 for -a: Nat
2747 for -b: Nat
2748 {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(k, a), Nat.add(k, b)) : Bool}
2749
2750def add_lt_add_iff_left(k, a, b):
2751 match k:
2752 case 0n:
2753 {==}
2754 case 1n+p:
2755 add_lt_add_iff_left(p, a, b)
2756
2757# Adding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k.
2758law add_lt_add_iff_right:
2759 for a: Nat
2760 for b: Nat
2761 for k: Nat
2762 {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(a, k), Nat.add(b, k)) : Bool}
2763
2764def add_lt_add_iff_right(a, b, k):
2765 +a = a
2766 +b = b
2767 +k = k
2768 %add_comm(k, a) : {Nat.is_lt(a, b) == Nat.is_lt(_, Nat.add(b, k)) : Bool}
2769 %add_comm(k, b) : {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(k, a), _) : Bool}
2770 add_lt_add_iff_left(k, a, b)
2771
2772# A common left summand cancels in a strict inequality: k + a < k + b implies a < b.
2773law lt_of_add_lt_add_left:
2774 for k: Nat
2775 for -a: Nat
2776 for -b: Nat
2777 for h: lt(Nat.add(k, a), Nat.add(k, b))
2778 lt(a, b)
2779
2780def lt_of_add_lt_add_left(k, a, b, h):
2781 match k:
2782 case 0n:
2783 h
2784 case 1n+p:
2785 lt_of_add_lt_add_left(p, a, b, h)
2786
2787# A common right summand cancels in a strict inequality: a + k < b + k implies a < b.
2788law lt_of_add_lt_add_right:
2789 for a: Nat
2790 for b: Nat
2791 for k: Nat
2792 for h: lt(Nat.add(a, k), Nat.add(b, k))
2793 lt(a, b)
2794
2795def lt_of_add_lt_add_right(a, b, k, h):
2796 Equal.trans(Bool, Nat.is_lt(a, b), Nat.is_lt(Nat.add(a, k), Nat.add(b, k)), True{}, add_lt_add_iff_right(a, b, k), h)
2797
2798# Adding two strict bounds keeps a strict bound: a < c and b < d imply a + b < c + d.
2799law add_lt_add:
2800 for a: Nat
2801 for b: Nat
2802 for c: Nat
2803 for d: Nat
2804 for h1: lt(a, c)
2805 for h2: lt(b, d)
2806 lt(Nat.add(a, b), Nat.add(c, d))
2807
2808def add_lt_add(a, b, c, d, h1, h2):
2809 +a = a
2810 +b = b
2811 +c = c
2812 +d = d
2813 lt_trans(Nat.add(a, b), Nat.add(c, b), Nat.add(c, d), add_lt_add_right(a, c, b, h1), add_lt_add_left(b, d, c, h2))
2814
2815# A positive left factor never decreases: m <= (1 + n) * m.
2816law le_mul_of_pos_left:
2817 for m: Nat
2818 for n: Nat
2819 le(m, Nat.mul(1n+n, m))
2820
2821def le_mul_of_pos_left(m, n):
2822 +m = m
2823 le_add_right(m, Nat.mul(n, m))
2824
2825# A positive right factor never decreases: m <= m * (1 + n).
2826law le_mul_of_pos_right:
2827 for m: Nat
2828 for n: Nat
2829 le(m, Nat.mul(m, 1n+n))
2830
2831def le_mul_of_pos_right(m, n):
2832 +m = m
2833 +n = n
2834 %mul_comm(1n+n, m) : le(m, _)
2835 le_mul_of_pos_left(m, n)
2836
2837# Multiplying on the left by a positive factor preserves the strict order: a < b implies (1 + k) * a < (1 + k) * b.
2838law mul_lt_mul_of_pos_left:
2839 for a: Nat
2840 for b: Nat
2841 for k: Nat
2842 for h: lt(a, b)
2843 lt(Nat.mul(1n+k, a), Nat.mul(1n+k, b))
2844
2845def mul_lt_mul_of_pos_left(a, b, k, h):
2846 +a = a
2847 +b = b
2848 +k = k
2849 +h = h
2850 lt_of_lt_of_le(Nat.add(a, Nat.mul(k, a)), Nat.add(b, Nat.mul(k, a)), Nat.add(b, Nat.mul(k, b)), add_lt_add_right(a, b, Nat.mul(k, a), h), add_le_add_left(Nat.mul(k, a), Nat.mul(k, b), b, mul_le_mul_left(a, b, k, le_of_lt(a, b, h))))
2851
2852# Multiplying on the right by a positive factor preserves the strict order: a < b implies a * (1 + k) < b * (1 + k).
2853law mul_lt_mul_of_pos_right:
2854 for a: Nat
2855 for b: Nat
2856 for k: Nat
2857 for h: lt(a, b)
2858 lt(Nat.mul(a, 1n+k), Nat.mul(b, 1n+k))
2859
2860def mul_lt_mul_of_pos_right(a, b, k, h):
2861 +a = a
2862 +b = b
2863 +k = k
2864 %mul_comm(1n+k, a) : lt(_, Nat.mul(b, 1n+k))
2865 %mul_comm(1n+k, b) : lt(Nat.mul(1n+k, a), _)
2866 mul_lt_mul_of_pos_left(a, b, k, h)
2867
2868def internal_lt_of_not_le(+a: Nat, +b: Nat, v: Bool, e: {v == Nat.is_lt(a, b) : Bool}, f: le(b, a) -> Empty) -> lt(a, b):
2869 match v:
2870 case True{}:
2871 Equal.sym(Bool, True{}, Nat.is_lt(a, b), e)
2872 case False{}:
2873 Empty.absurd(lt(a, b), f(le_of_not_lt(a, b, Equal.sym(Bool, False{}, Nat.is_lt(a, b), e))))
2874
2875# A common left factor cancels in a strict inequality: k * a < k * b implies a < b.
2876law lt_of_mul_lt_mul_left:
2877 for k: Nat
2878 for a: Nat
2879 for b: Nat
2880 for h: lt(Nat.mul(k, a), Nat.mul(k, b))
2881 lt(a, b)
2882
2883def lt_of_mul_lt_mul_left(k, a, b, h):
2884 +k = k
2885 +a = a
2886 +b = b
2887 internal_lt_of_not_le(a, b, Nat.is_lt(a, b), {==}, hb => internal_false_ne_true(Equal.trans(Bool, False{}, Nat.is_le(Nat.mul(k, b), Nat.mul(k, a)), True{}, Equal.sym(Bool, Nat.is_le(Nat.mul(k, b), Nat.mul(k, a)), False{}, not_le_of_lt(Nat.mul(k, a), Nat.mul(k, b), h)), mul_le_mul_left(b, a, k, hb))))
2888
2889# A common right factor cancels in a strict inequality: a * k < b * k implies a < b.
2890law lt_of_mul_lt_mul_right:
2891 for a: Nat
2892 for b: Nat
2893 for k: Nat
2894 for h: lt(Nat.mul(a, k), Nat.mul(b, k))
2895 lt(a, b)
2896
2897def lt_of_mul_lt_mul_right(a, b, k, h):
2898 +k = k
2899 +a = a
2900 +b = b
2901 internal_lt_of_not_le(a, b, Nat.is_lt(a, b), {==}, hb => internal_false_ne_true(Equal.trans(Bool, False{}, Nat.is_le(Nat.mul(b, k), Nat.mul(a, k)), True{}, Equal.sym(Bool, Nat.is_le(Nat.mul(b, k), Nat.mul(a, k)), False{}, not_le_of_lt(Nat.mul(a, k), Nat.mul(b, k), h)), mul_le_mul_right(b, a, k, hb))))
2902
2903# Multiplying two strict bounds keeps a strict bound: a < c and b < d imply a * b < c * d.
2904law mul_lt_mul_of_lt_of_lt:
2905 for a: Nat
2906 for b: Nat
2907 for c: Nat
2908 for d: Nat
2909 for h1: lt(a, c)
2910 for h2: lt(b, d)
2911 lt(Nat.mul(a, b), Nat.mul(c, d))
2912
2913def mul_lt_mul_of_lt_of_lt(a, b, c, d, h1, h2):
2914 match c:
2915 case 0n:
2916 Empty.absurd(lt(Nat.mul(a, b), Nat.mul(0n, d)), lt_zero(a)(h1))
2917 case 1n++cp:
2918 +a = a
2919 +b = b
2920 +d = d
2921 lt_of_le_of_lt(Nat.mul(a, b), Nat.mul(1n+cp, b), Nat.mul(1n+cp, d), mul_le_mul_right(a, 1n+cp, b, le_of_lt(a, 1n+cp, h1)), mul_lt_mul_of_pos_left(b, d, cp, h2))
2922
2923# Squares are monotone: a <= b implies a * a <= b * b.
2924law mul_self_le_mul_self:
2925 for a: Nat
2926 for b: Nat
2927 for h: le(a, b)
2928 le(Nat.mul(a, a), Nat.mul(b, b))
2929
2930def mul_self_le_mul_self(a, b, h):
2931 +a = a
2932 +b = b
2933 +h = h
2934 mul_le_mul(a, a, b, b, h, h)
2935
2936# Squares are strictly monotone: a < b implies a * a < b * b.
2937law mul_self_lt_mul_self:
2938 for a: Nat
2939 for b: Nat
2940 for h: lt(a, b)
2941 lt(Nat.mul(a, a), Nat.mul(b, b))
2942
2943def mul_self_lt_mul_self(a, b, h):
2944 +a = a
2945 +b = b
2946 +h = h
2947 mul_lt_mul_of_lt_of_lt(a, a, b, b, h, h)
2948
2949# Subtracting a positive amount from a positive number decreases it: (1 + n) - (1 + m) < 1 + n.
2950law sub_lt:
2951 for n: Nat
2952 for m: Nat
2953 lt(Nat.sub(1n+n, 1n+m), 1n+n)
2954
2955def sub_lt(n, m):
2956 +n = n
2957 +m = m
2958 lt_succ_of_le(Nat.sub(n, m), n, sub_le(n, m))
2959
2960# Subtracting more gives less: n <= m implies k - m <= k - n.
2961law sub_le_sub_left:
2962 for n: Nat
2963 for m: Nat
2964 for h: le(n, m)
2965 for k: Nat
2966 le(Nat.sub(k, m), Nat.sub(k, n))
2967
2968def sub_le_sub_left(n, m, h, k):
2969 +n = n
2970 +m = m
2971 +k = k
2972 %add_sub_of_le(n, m, h) : le(Nat.sub(k, _), Nat.sub(k, n))
2973 %sub_sub(k, n, Nat.sub(m, n)) : le(_, Nat.sub(k, n))
2974 sub_le(Nat.sub(k, n), Nat.sub(m, n))
2975
2976# Subtraction on the right preserves the order: n <= m implies n - k <= m - k.
2977law sub_le_sub_right:
2978 for n: Nat
2979 for m: Nat
2980 for h: le(n, m)
2981 for k: Nat
2982 le(Nat.sub(n, k), Nat.sub(m, k))
2983
2984def sub_le_sub_right(n, m, h, k):
2985 match n m k:
2986 case 0n _ _:
2987 +k = k
2988 %Equal.sym(Nat, Nat.sub(0n, k), 0n, zero_sub(k)) : le(_, Nat.sub(m, k))
2989 zero_le(Nat.sub(m, k))
2990 case 1n+p 0n _:
2991 Empty.absurd(le(Nat.sub(1n+p, k), Nat.sub(0n, k)), internal_false_ne_true(h))
2992 case 1n+p 1n+q 0n:
2993 h
2994 case 1n+p 1n+q 1n+r:
2995 sub_le_sub_right(p, q, h, r)
2996
2997# A strict bound on a sum bounds a difference: a + b < c implies a < c - b.
2998law lt_sub_of_add_lt:
2999 for a: Nat
3000 for b: Nat
3001 for c: Nat
3002 for h: lt(Nat.add(a, b), c)
3003 lt(a, Nat.sub(c, b))
3004
3005def lt_sub_of_add_lt(a, b, c, h):
3006 +a = a
3007 +b = b
3008 %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)) : {_ == True{} : Bool}
3009 %add_comm(a, b) : {Nat.is_lt(_, c) == True{} : Bool}
3010 h
3011
3012# A difference is positive below the minuend: m < n implies 0 < n - m.
3013law sub_pos_of_lt:
3014 for m: Nat
3015 for n: Nat
3016 for h: lt(m, n)
3017 lt(0n, Nat.sub(n, m))
3018
3019def sub_pos_of_lt(m, n, h):
3020 lt_sub_of_add_lt(0n, m, n, h)
3021
3022# Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c).
3023law min_max_distrib_left:
3024 for a: Nat
3025 for b: Nat
3026 for c: Nat
3027 {Nat.min(a, Nat.max(b, c)) == Nat.max(Nat.min(a, b), Nat.min(a, c)) : Nat}
3028
3029def min_max_distrib_left(a, b, c):
3030 match a b c:
3031 case 0n _ _:
3032 {==}
3033 case 1n+p 0n 0n:
3034 {==}
3035 case 1n+p 0n 1n+r:
3036 {==}
3037 case 1n+p 1n+q 0n:
3038 {==}
3039 case 1n+p 1n+q 1n+r:
3040 %min_max_distrib_left(p, q, r) : {1n+Nat.min(p, Nat.max(q, r)) == 1n+_ : Nat}
3041 {==}
3042
3043# Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c).
3044law max_min_distrib_left:
3045 for a: Nat
3046 for b: Nat
3047 for c: Nat
3048 {Nat.max(a, Nat.min(b, c)) == Nat.min(Nat.max(a, b), Nat.max(a, c)) : Nat}
3049
3050def max_min_distrib_left(a, b, c):
3051 match a b c:
3052 case 0n _ _:
3053 {==}
3054 case 1n++p 0n 0n:
3055 %Equal.sym(Nat, Nat.min(p, p), p, min_self(p)) : {1n+p == 1n+_ : Nat}
3056 {==}
3057 case 1n++p 0n 1n++r:
3058 %Equal.sym(Nat, Nat.min(p, Nat.max(p, r)), p, min_eq_left(p, Nat.max(p, r), le_max_left(p, r))) : {1n+p == 1n+_ : Nat}
3059 {==}
3060 case 1n++p 1n++q 0n:
3061 %Equal.sym(Nat, Nat.min(Nat.max(p, q), p), p, min_eq_right(Nat.max(p, q), p, le_max_left(p, q))) : {1n+p == 1n+_ : Nat}
3062 {==}
3063 case 1n+p 1n+q 1n+r:
3064 %max_min_distrib_left(p, q, r) : {1n+Nat.max(p, Nat.min(q, r)) == 1n+_ : Nat}
3065 {==}
3066
3067# A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c.
3068law min_add_add_left:
3069 for a: Nat
3070 for -b: Nat
3071 for -c: Nat
3072 {Nat.min(Nat.add(a, b), Nat.add(a, c)) == Nat.add(a, Nat.min(b, c)) : Nat}
3073
3074def min_add_add_left(a, b, c):
3075 match a:
3076 case 0n:
3077 {==}
3078 case 1n+p:
3079 %min_add_add_left(p, b, c) : {1n+Nat.min(Nat.add(p, b), Nat.add(p, c)) == 1n+_ : Nat}
3080 {==}
3081
3082# A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c.
3083law min_add_add_right:
3084 for a: Nat
3085 for b: Nat
3086 for c: Nat
3087 {Nat.min(Nat.add(a, c), Nat.add(b, c)) == Nat.add(Nat.min(a, b), c) : Nat}
3088
3089def min_add_add_right(a, b, c):
3090 +a = a
3091 +b = b
3092 +c = c
3093 %add_comm(c, a) : {Nat.min(_, Nat.add(b, c)) == Nat.add(Nat.min(a, b), c) : Nat}
3094 %add_comm(c, b) : {Nat.min(Nat.add(c, a), _) == Nat.add(Nat.min(a, b), c) : Nat}
3095 %add_comm(c, Nat.min(a, b)) : {Nat.min(Nat.add(c, a), Nat.add(c, b)) == _ : Nat}
3096 min_add_add_left(c, a, b)
3097
3098# A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c.
3099law max_add_add_left:
3100 for a: Nat
3101 for -b: Nat
3102 for -c: Nat
3103 {Nat.max(Nat.add(a, b), Nat.add(a, c)) == Nat.add(a, Nat.max(b, c)) : Nat}
3104
3105def max_add_add_left(a, b, c):
3106 match a:
3107 case 0n:
3108 {==}
3109 case 1n+p:
3110 %max_add_add_left(p, b, c) : {1n+Nat.max(Nat.add(p, b), Nat.add(p, c)) == 1n+_ : Nat}
3111 {==}
3112
3113# A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c.
3114law max_add_add_right:
3115 for a: Nat
3116 for b: Nat
3117 for c: Nat
3118 {Nat.max(Nat.add(a, c), Nat.add(b, c)) == Nat.add(Nat.max(a, b), c) : Nat}
3119
3120def max_add_add_right(a, b, c):
3121 +a = a
3122 +b = b
3123 +c = c
3124 %add_comm(c, a) : {Nat.max(_, Nat.add(b, c)) == Nat.add(Nat.max(a, b), c) : Nat}
3125 %add_comm(c, b) : {Nat.max(Nat.add(c, a), _) == Nat.add(Nat.max(a, b), c) : Nat}
3126 %add_comm(c, Nat.max(a, b)) : {Nat.max(Nat.add(c, a), Nat.add(c, b)) == _ : Nat}
3127 max_add_add_left(c, a, b)
3128
3129# The minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c.
3130law min_lt_iff:
3131 for a: Nat
3132 for b: Nat
3133 for c: Nat
3134 {Nat.is_lt(Nat.min(a, b), c) == Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)) : Bool}
3135
3136def min_lt_iff(a, b, c):
3137 match a b c:
3138 case 0n 0n 0n:
3139 {==}
3140 case 0n 0n 1n+r:
3141 {==}
3142 case 0n 1n+q 0n:
3143 {==}
3144 case 0n 1n+q 1n+r:
3145 {==}
3146 case 1n+p 0n 0n:
3147 {==}
3148 case 1n+p 0n 1n+r:
3149 internal_or_true_sym(Nat.is_lt(p, r))
3150 case 1n+p 1n+q 0n:
3151 {==}
3152 case 1n+p 1n+q 1n+r:
3153 min_lt_iff(p, q, r)
3154
3155# A number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c.
3156law lt_min_iff:
3157 for a: Nat
3158 for b: Nat
3159 for c: Nat
3160 {Nat.is_lt(a, Nat.min(b, c)) == Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}
3161
3162def lt_min_iff(a, b, c):
3163 match a b c:
3164 case 0n 0n 0n:
3165 {==}
3166 case 0n 0n 1n+r:
3167 {==}
3168 case 0n 1n+q 0n:
3169 {==}
3170 case 0n 1n+q 1n+r:
3171 {==}
3172 case 1n+p 0n 0n:
3173 {==}
3174 case 1n+p 0n 1n+r:
3175 {==}
3176 case 1n+p 1n+q 0n:
3177 internal_and_false_sym(Nat.is_lt(p, q))
3178 case 1n+p 1n+q 1n+r:
3179 lt_min_iff(p, q, r)
3180
3181# The maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c.
3182law max_lt_iff:
3183 for a: Nat
3184 for b: Nat
3185 for c: Nat
3186 {Nat.is_lt(Nat.max(a, b), c) == Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)) : Bool}
3187
3188def max_lt_iff(a, b, c):
3189 match a b c:
3190 case 0n 0n 0n:
3191 {==}
3192 case 0n 0n 1n+r:
3193 {==}
3194 case 0n 1n+q 0n:
3195 {==}
3196 case 0n 1n+q 1n+r:
3197 {==}
3198 case 1n+p 0n 0n:
3199 {==}
3200 case 1n+p 0n 1n+r:
3201 internal_and_true_sym(Nat.is_lt(p, r))
3202 case 1n+p 1n+q 0n:
3203 {==}
3204 case 1n+p 1n+q 1n+r:
3205 max_lt_iff(p, q, r)
3206
3207# A number is at most the maximum exactly when it is at most one argument: a <= max b c tests as a <= b or a <= c.
3208law le_max_iff:
3209 for a: Nat
3210 for b: Nat
3211 for c: Nat
3212 {Nat.is_le(a, Nat.max(b, c)) == Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)) : Bool}
3213
3214def le_max_iff(a, b, c):
3215 match a b c:
3216 case 0n 0n 0n:
3217 {==}
3218 case 0n 0n 1n+r:
3219 {==}
3220 case 0n 1n+q 0n:
3221 {==}
3222 case 0n 1n+q 1n+r:
3223 {==}
3224 case 1n+p 0n 0n:
3225 {==}
3226 case 1n+p 0n 1n+r:
3227 {==}
3228 case 1n+p 1n+q 0n:
3229 internal_or_false_sym(Nat.is_le(p, q))
3230 case 1n+p 1n+q 1n+r:
3231 le_max_iff(p, q, r)
3232
3233# A bound by the left argument bounds the maximum: a <= b implies a <= max b c.
3234law le_max_of_le_left:
3235 for a: Nat
3236 for b: Nat
3237 for c: Nat
3238 for h: le(a, b)
3239 le(a, Nat.max(b, c))
3240
3241def le_max_of_le_left(a, b, c, h):
3242 +b = b
3243 +c = c
3244 le_trans(a, b, Nat.max(b, c), h, le_max_left(b, c))
3245
3246# A bound by the right argument bounds the maximum: a <= c implies a <= max b c.
3247law le_max_of_le_right:
3248 for a: Nat
3249 for b: Nat
3250 for c: Nat
3251 for h: le(a, c)
3252 le(a, Nat.max(b, c))
3253
3254def le_max_of_le_right(a, b, c, h):
3255 +b = b
3256 +c = c
3257 le_trans(a, c, Nat.max(b, c), h, le_max_right(b, c))
3258
3259# A bounded left argument bounds the minimum: a <= c implies min a b <= c.
3260law min_le_of_left_le:
3261 for a: Nat
3262 for b: Nat
3263 for c: Nat
3264 for h: le(a, c)
3265 le(Nat.min(a, b), c)
3266
3267def min_le_of_left_le(a, b, c, h):
3268 +a = a
3269 +b = b
3270 le_trans(Nat.min(a, b), a, c, min_le_left(a, b), h)
3271
3272# A bounded right argument bounds the minimum: b <= c implies min a b <= c.
3273law min_le_of_right_le:
3274 for a: Nat
3275 for b: Nat
3276 for c: Nat
3277 for h: le(b, c)
3278 le(Nat.min(a, b), c)
3279
3280def min_le_of_right_le(a, b, c, h):
3281 +a = a
3282 +b = b
3283 le_trans(Nat.min(a, b), b, c, min_le_right(a, b), h)
3284
3285# Minimum is monotone in both arguments: a <= c and b <= d imply min a b <= min c d.
3286law min_le_min:
3287 for a: Nat
3288 for b: Nat
3289 for c: Nat
3290 for d: Nat
3291 for h1: le(a, c)
3292 for h2: le(b, d)
3293 le(Nat.min(a, b), Nat.min(c, d))
3294
3295def min_le_min(a, b, c, d, h1, h2):
3296 +a = a
3297 +b = b
3298 +c = c
3299 +d = d
3300 %Equal.sym(Bool, Nat.is_le(Nat.min(a, b), Nat.min(c, d)), Bool.and(Nat.is_le(Nat.min(a, b), c), Nat.is_le(Nat.min(a, b), d)), le_min(Nat.min(a, b), c, d)) : {_ == True{} : Bool}
3301 %Equal.sym(Bool, Nat.is_le(Nat.min(a, b), c), True{}, min_le_of_left_le(a, b, c, h1)) : {Bool.and(_, Nat.is_le(Nat.min(a, b), d)) == True{} : Bool}
3302 min_le_of_right_le(a, b, d, h2)
3303
3304# Maximum is monotone in both arguments: a <= c and b <= d imply max a b <= max c d.
3305law max_le_max:
3306 for a: Nat
3307 for b: Nat
3308 for c: Nat
3309 for d: Nat
3310 for h1: le(a, c)
3311 for h2: le(b, d)
3312 le(Nat.max(a, b), Nat.max(c, d))
3313
3314def max_le_max(a, b, c, d, h1, h2):
3315 +a = a
3316 +b = b
3317 +c = c
3318 +d = d
3319 %Equal.sym(Bool, Nat.is_le(Nat.max(a, b), Nat.max(c, d)), Bool.and(Nat.is_le(a, Nat.max(c, d)), Nat.is_le(b, Nat.max(c, d))), max_le(a, b, Nat.max(c, d))) : {_ == True{} : Bool}
3320 %Equal.sym(Bool, Nat.is_le(a, Nat.max(c, d)), True{}, le_max_of_le_left(a, c, d, h1)) : {Bool.and(_, Nat.is_le(b, Nat.max(c, d))) == True{} : Bool}
3321 le_max_of_le_right(b, c, d, h2)
3322
3323# Powers are monotone in the base: a <= b implies a^n <= b^n.
3324law pow_le_pow_left:
3325 for a: Nat
3326 for b: Nat
3327 for h: le(a, b)
3328 for n: Nat
3329 le(Nat.pow(a, n), Nat.pow(b, n))
3330
3331def pow_le_pow_left(a, b, h, n):
3332 match n:
3333 case 0n:
3334 {==}
3335 case 1n++p:
3336 +a = a
3337 +b = b
3338 +h = h
3339 mul_le_mul(a, Nat.pow(a, p), b, Nat.pow(b, p), h, pow_le_pow_left(a, b, h, p))
3340
3341# Powers of a positive base are monotone in the exponent: i <= j implies (1 + a)^i <= (1 + a)^j.
3342law pow_le_pow_right:
3343 for a: Nat
3344 for i: Nat
3345 for j: Nat
3346 for h: le(i, j)
3347 le(Nat.pow(1n+a, i), Nat.pow(1n+a, j))
3348
3349def pow_le_pow_right(a, i, j, h):
3350 match i j:
3351 case 0n y:
3352 one_le_pow(y, a)
3353 case 1n+p 0n:
3354 Empty.absurd(le(Nat.pow(1n+a, 1n+p), Nat.pow(1n+a, 0n)), internal_false_ne_true(h))
3355 case 1n++p 1n++q:
3356 +a = a
3357 mul_le_mul_left(Nat.pow(1n+a, p), Nat.pow(1n+a, q), 1n+a, pow_le_pow_right(a, p, q, h))
3358
3359def internal_lt_mul_two_add(a: Nat, x: Nat, hx: lt(0n, x)) -> lt(x, Nat.mul(2n+a, x)):
3360 match x:
3361 case 0n:
3362 Empty.absurd(lt(0n, Nat.mul(2n+a, 0n)), internal_false_ne_true(hx))
3363 case 1n++y:
3364 lt_add_of_pos_right(y, Nat.add(y, Nat.mul(a, 1n+y)))
3365
3366# Powers of a base above one are strictly monotone in the exponent: i < j implies (2 + a)^i < (2 + a)^j.
3367law pow_lt_pow_right:
3368 for a: Nat
3369 for i: Nat
3370 for j: Nat
3371 for h: lt(i, j)
3372 lt(Nat.pow(2n+a, i), Nat.pow(2n+a, j))
3373
3374def pow_lt_pow_right(a, i, j, h):
3375 match i j:
3376 case 0n 0n:
3377 Empty.absurd(lt(Nat.pow(2n+a, 0n), Nat.pow(2n+a, 0n)), internal_false_ne_true(h))
3378 case 0n 1n+q:
3379 +a = a
3380 +q = q
3381 lt_of_le_of_lt(1n, Nat.pow(2n+a, q), Nat.mul(2n+a, Nat.pow(2n+a, q)), one_le_pow(q, 1n+a), internal_lt_mul_two_add(a, Nat.pow(2n+a, q), pow_pos(q, 1n+a)))
3382 case 1n+p 0n:
3383 Empty.absurd(lt(Nat.pow(2n+a, 1n+p), Nat.pow(2n+a, 0n)), internal_false_ne_true(h))
3384 case 1n++p 1n++q:
3385 +a = a
3386 mul_lt_mul_of_pos_left(Nat.pow(2n+a, p), Nat.pow(2n+a, q), 1n+a, pow_lt_pow_right(a, p, q, h))
3387
3388# Positive powers are strictly monotone in the base: a < b implies a^(1 + n) < b^(1 + n).
3389law pow_lt_pow_left:
3390 for a: Nat
3391 for b: Nat
3392 for h: lt(a, b)
3393 for n: Nat
3394 lt(Nat.pow(a, 1n+n), Nat.pow(b, 1n+n))
3395
3396def pow_lt_pow_left(a, b, h, n):
3397 match n:
3398 case 0n:
3399 +a = a
3400 +b = b
3401 %Equal.sym(Nat, Nat.mul(a, 1n), a, mul_one(a)) : lt(_, Nat.mul(b, 1n))
3402 %Equal.sym(Nat, Nat.mul(b, 1n), b, mul_one(b)) : lt(a, _)
3403 h
3404 case 1n++p:
3405 +a = a
3406 +b = b
3407 +h = h
3408 mul_lt_mul_of_lt_of_lt(a, Nat.pow(a, 1n+p), b, Nat.pow(b, 1n+p), h, pow_lt_pow_left(a, b, h, p))
3409
3410# Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z.
3411law add_mul_div_right:
3412 for x: Nat
3413 for z: Nat
3414 for b: Nat
3415 {Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}
3416
3417def add_mul_div_right(x, z, b):
3418 match z:
3419 case 0n:
3420 +x = x
3421 +b = b
3422 %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.div(_, 1n+b) == Nat.add(Nat.div(x, 1n+b), 0n) : Nat}
3423 Equal.sym(Nat, Nat.add(Nat.div(x, 1n+b), 0n), Nat.div(x, 1n+b), add_zero(Nat.div(x, 1n+b)))
3424 case 1n++w:
3425 +x = x
3426 +b = b
3427 %Equal.sym(Nat, Nat.add(x, Nat.add(1n+b, Nat.mul(w, 1n+b))), Nat.add(1n+b, Nat.add(x, Nat.mul(w, 1n+b))), add_left_comm(x, 1n+b, Nat.mul(w, 1n+b))) : {Nat.div(_, 1n+b) == Nat.add(Nat.div(x, 1n+b), 1n+w) : Nat}
3428 %Equal.sym(Nat, Nat.div(Nat.add(1n+b, Nat.add(x, Nat.mul(w, 1n+b))), 1n+b), 1n+Nat.div(Nat.add(x, Nat.mul(w, 1n+b)), 1n+b), add_div_left(Nat.add(x, Nat.mul(w, 1n+b)), b)) : {_ == Nat.add(Nat.div(x, 1n+b), 1n+w) : Nat}
3429 %Equal.sym(Nat, Nat.div(Nat.add(x, Nat.mul(w, 1n+b)), 1n+b), Nat.add(Nat.div(x, 1n+b), w), add_mul_div_right(x, w, b)) : {1n+_ == Nat.add(Nat.div(x, 1n+b), 1n+w) : Nat}
3430 Equal.sym(Nat, Nat.add(Nat.div(x, 1n+b), 1n+w), 1n+Nat.add(Nat.div(x, 1n+b), w), add_succ(Nat.div(x, 1n+b), w))
3431
3432# Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z.
3433law add_mul_div_left:
3434 for x: Nat
3435 for z: Nat
3436 for b: Nat
3437 {Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}
3438
3439def add_mul_div_left(x, z, b):
3440 +x = x
3441 +z = z
3442 +b = b
3443 %mul_comm(z, 1n+b) : {Nat.div(Nat.add(x, _), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}
3444 add_mul_div_right(x, z, b)
3445
3446# Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b.
3447law add_mul_mod_self_right:
3448 for a: Nat
3449 for b: Nat
3450 for c: Nat
3451 {Nat.mod(Nat.add(a, Nat.mul(c, b)), b) == Nat.mod(a, b) : Nat}
3452
3453def add_mul_mod_self_right(a, b, c):
3454 match c:
3455 case 0n:
3456 +a = a
3457 %Equal.sym(Nat, Nat.add(a, 0n), a, add_zero(a)) : {Nat.mod(_, b) == Nat.mod(a, b) : Nat}
3458 {==}
3459 case 1n++w:
3460 +a = a
3461 +b = b
3462 %Equal.sym(Nat, Nat.add(a, Nat.add(b, Nat.mul(w, b))), Nat.add(b, Nat.add(a, Nat.mul(w, b))), add_left_comm(a, b, Nat.mul(w, b))) : {Nat.mod(_, b) == Nat.mod(a, b) : Nat}
3463 Equal.trans(Nat, Nat.mod(Nat.add(b, Nat.add(a, Nat.mul(w, b))), b), Nat.mod(Nat.add(a, Nat.mul(w, b)), b), Nat.mod(a, b), add_mod_left(Nat.add(a, Nat.mul(w, b)), b), add_mul_mod_self_right(a, b, w))
3464
3465# Adding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b.
3466law add_mul_mod_self_left:
3467 for a: Nat
3468 for b: Nat
3469 for c: Nat
3470 {Nat.mod(Nat.add(a, Nat.mul(b, c)), b) == Nat.mod(a, b) : Nat}
3471
3472def add_mul_mod_self_left(a, b, c):
3473 +a = a
3474 +b = b
3475 +c = c
3476 %mul_comm(c, b) : {Nat.mod(Nat.add(a, _), b) == Nat.mod(a, b) : Nat}
3477 add_mul_mod_self_right(a, b, c)
3478
3479def internal_lt_one_succ(y: Nat, h: lt(y, 1n)) -> {Bool.or(Nat.is_eq(1n+y, 0n), Nat.is_eq(1n+y, 1n)) == True{} : Bool}:
3480 match y:
3481 case 0n:
3482 {==}
3483 case 1n+z:
3484 Empty.absurd({Bool.or(Nat.is_eq(2n+z, 0n), Nat.is_eq(2n+z, 1n)) == True{} : Bool}, lt_zero(z)(h))
3485
3486def internal_lt_two(x: Nat, h: lt(x, 2n)) -> {Bool.or(Nat.is_eq(x, 0n), Nat.is_eq(x, 1n)) == True{} : Bool}:
3487 match x:
3488 case 0n:
3489 {==}
3490 case 1n+y:
3491 internal_lt_one_succ(y, h)
3492
3493# A remainder modulo two is zero or one.
3494law mod_two_eq_zero_or_one:
3495 for n: Nat
3496 {Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)) == True{} : Bool}
3497
3498def mod_two_eq_zero_or_one(n):
3499 +n = n
3500 internal_lt_two(Nat.mod(n, 2n), mod_lt(n, 1n))
3501
3502# The divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a.
3503law div_add_mod:
3504 for a: Nat
3505 for b: Nat
3506 {Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)) == a : Nat}
3507
3508def div_add_mod(a, b):
3509 +a = a
3510 +b = b
3511 %add_comm(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) : {_ == a : Nat}
3512 mod_add_div(a, b)
3513
3514# Two times n is n + n.
3515law two_mul:
3516 for n: Nat
3517 {Nat.mul(2n, n) == Nat.add(n, n) : Nat}
3518
3519def two_mul(n):
3520 +n = n
3521 %Equal.sym(Nat, Nat.add(n, 0n), n, add_zero(n)) : {Nat.add(n, _) == Nat.add(n, n) : Nat}
3522 {==}
3523
3524# Doubling is multiplying by two: double n = 2 * n.
3525law double_eq_two_mul:
3526 for n: Nat
3527 {Nat.double(n) == Nat.mul(2n, n) : Nat}
3528
3529def double_eq_two_mul(n):
3530 +n = n
3531 %Equal.sym(Nat, Nat.mul(2n, n), Nat.add(n, n), two_mul(n)) : {Nat.double(n) == _ : Nat}
3532 double_eq_add(n)
3533
3534# Doubling distributes over addition: double (a + b) = double a + double b.
3535law double_add:
3536 for a: Nat
3537 for b: Nat
3538 {Nat.double(Nat.add(a, b)) == Nat.add(Nat.double(a), Nat.double(b)) : Nat}
3539
3540def double_add(a, b):
3541 +a = a
3542 +b = b
3543 %Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(Nat.add(a, b), Nat.add(a, b)), double_eq_add(Nat.add(a, b))) : {_ == Nat.add(Nat.double(a), Nat.double(b)) : Nat}
3544 %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), double_eq_add(a)) : {Nat.add(Nat.add(a, b), Nat.add(a, b)) == Nat.add(_, Nat.double(b)) : Nat}
3545 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : {Nat.add(Nat.add(a, b), Nat.add(a, b)) == Nat.add(Nat.add(a, a), _) : Nat}
3546 add_add_add_comm(a, b, a, b)
3547
3548# Doubling a product doubles its left factor: double (a * b) = double a * b.
3549law double_mul:
3550 for a: Nat
3551 for b: Nat
3552 {Nat.double(Nat.mul(a, b)) == Nat.mul(Nat.double(a), b) : Nat}
3553
3554def double_mul(a, b):
3555 +a = a
3556 +b = b
3557 %Equal.sym(Nat, Nat.double(Nat.mul(a, b)), Nat.add(Nat.mul(a, b), Nat.mul(a, b)), double_eq_add(Nat.mul(a, b))) : {_ == Nat.mul(Nat.double(a), b) : Nat}
3558 %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), double_eq_add(a)) : {Nat.add(Nat.mul(a, b), Nat.mul(a, b)) == Nat.mul(_, b) : Nat}
3559 Equal.sym(Nat, Nat.mul(Nat.add(a, a), b), Nat.add(Nat.mul(a, b), Nat.mul(a, b)), add_mul(a, a, b))
3560
3561# Multiplying by a doubled factor doubles the product: a * double b = double (a * b).
3562law mul_double:
3563 for a: Nat
3564 for b: Nat
3565 {Nat.mul(a, Nat.double(b)) == Nat.double(Nat.mul(a, b)) : Nat}
3566
3567def mul_double(a, b):
3568 +a = a
3569 +b = b
3570 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : {Nat.mul(a, _) == Nat.double(Nat.mul(a, b)) : Nat}
3571 %Equal.sym(Nat, Nat.double(Nat.mul(a, b)), Nat.add(Nat.mul(a, b), Nat.mul(a, b)), double_eq_add(Nat.mul(a, b))) : {Nat.mul(a, Nat.add(b, b)) == _ : Nat}
3572 mul_add(a, b, b)
3573
3574# Doubling distributes over truncated subtraction: double (a - b) = double a - double b.
3575law double_sub:
3576 for a: Nat
3577 for b: Nat
3578 {Nat.double(Nat.sub(a, b)) == Nat.sub(Nat.double(a), Nat.double(b)) : Nat}
3579
3580def double_sub(a, b):
3581 match a b:
3582 case 0n _:
3583 {==}
3584 case 1n+p 0n:
3585 {==}
3586 case 1n+p 1n+q:
3587 double_sub(p, q)
3588
3589# A natural is at most its double: n <= double n.
3590law le_double:
3591 for n: Nat
3592 le(n, Nat.double(n))
3593
3594def le_double(n):
3595 +n = n
3596 %Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n)) : le(n, _)
3597 le_add_right(n, n)
3598
3599# Doubling preserves the order: a <= b implies double a <= double b.
3600law double_le_double:
3601 for a: Nat
3602 for b: Nat
3603 for h: le(a, b)
3604 le(Nat.double(a), Nat.double(b))
3605
3606def double_le_double(a, b, h):
3607 +a = a
3608 +b = b
3609 +h = h
3610 %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), double_eq_add(a)) : le(_, Nat.double(b))
3611 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : le(Nat.add(a, a), _)
3612 add_le_add(a, a, b, b, h, h)
3613
3614# Doubling preserves the strict order: a < b implies double a < double b.
3615law double_lt_double:
3616 for a: Nat
3617 for b: Nat
3618 for h: lt(a, b)
3619 lt(Nat.double(a), Nat.double(b))
3620
3621def double_lt_double(a, b, h):
3622 +a = a
3623 +b = b
3624 +h = h
3625 %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), double_eq_add(a)) : lt(_, Nat.double(b))
3626 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : lt(Nat.add(a, a), _)
3627 add_lt_add(a, a, b, b, h, h)
3628
3629# Twice the half plus the parity is the number: double (n / 2) + n % 2 = n.
3630law double_div_two_add_mod_two:
3631 for n: Nat
3632 {Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) == n : Nat}
3633
3634def double_div_two_add_mod_two(n):
3635 +n = n
3636 %Equal.sym(Nat, Nat.double(Nat.div(n, 2n)), Nat.mul(2n, Nat.div(n, 2n)), double_eq_two_mul(Nat.div(n, 2n))) : {Nat.add(_, Nat.mod(n, 2n)) == n : Nat}
3637 div_add_mod(n, 2n)
3638
3639# Adding the same amount on the right does not change the order test: a <= b tests as a + k <= b + k.
3640law add_le_add_iff_right:
3641 for a: Nat
3642 for b: Nat
3643 for k: Nat
3644 {Nat.is_le(a, b) == Nat.is_le(Nat.add(a, k), Nat.add(b, k)) : Bool}
3645
3646def add_le_add_iff_right(a, b, k):
3647 +a = a
3648 +b = b
3649 +k = k
3650 %add_comm(k, a) : {Nat.is_le(a, b) == Nat.is_le(_, Nat.add(b, k)) : Bool}
3651 %add_comm(k, b) : {Nat.is_le(a, b) == Nat.is_le(Nat.add(k, a), _) : Bool}
3652 add_le_add_iff_left(k, a, b)
3653
3654# Adding the same amount on the left does not change the equality test: a = b tests as k + a = k + b.
3655law add_left_cancel_iff:
3656 for k: Nat
3657 for -a: Nat
3658 for -b: Nat
3659 {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(k, a), Nat.add(k, b)) : Bool}
3660
3661def add_left_cancel_iff(k, a, b):
3662 match k:
3663 case 0n:
3664 {==}
3665 case 1n+p:
3666 add_left_cancel_iff(p, a, b)
3667
3668# Adding the same amount on the right does not change the equality test: a = b tests as a + k = b + k.
3669law add_right_cancel_iff:
3670 for a: Nat
3671 for b: Nat
3672 for k: Nat
3673 {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(a, k), Nat.add(b, k)) : Bool}
3674
3675def add_right_cancel_iff(a, b, k):
3676 +a = a
3677 +b = b
3678 +k = k
3679 %add_comm(k, a) : {Nat.is_eq(a, b) == Nat.is_eq(_, Nat.add(b, k)) : Bool}
3680 %add_comm(k, b) : {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(k, a), _) : Bool}
3681 add_left_cancel_iff(k, a, b)
3682
3683# Subtracting from the left summand commutes with adding the right one: k <= n implies (n + m) - k = (n - k) + m.
3684law sub_add_comm:
3685 for n: Nat
3686 for m: Nat
3687 for k: Nat
3688 for h: le(k, n)
3689 {Nat.sub(Nat.add(n, m), k) == Nat.add(Nat.sub(n, k), m) : Nat}
3690
3691def sub_add_comm(n, m, k, h):
3692 +n = n
3693 +m = m
3694 +k = k
3695 %add_comm(m, n) : {Nat.sub(_, k) == Nat.add(Nat.sub(n, k), m) : Nat}
3696 %add_comm(m, Nat.sub(n, k)) : {Nat.sub(Nat.add(m, n), k) == _ : Nat}
3697 add_sub_assoc(k, n, h, m)
3698
3699# A lower bound of both b and c is a lower bound of their minimum: a <= b and a <= c imply a <= min b c.
3700law le_min_of_le_of_le:
3701 for a: Nat
3702 for b: Nat
3703 for c: Nat
3704 for hb: le(a, b)
3705 for hc: le(a, c)
3706 le(a, Nat.min(b, c))
3707
3708def le_min_of_le_of_le(a, b, c, hb, hc):
3709 +a = a
3710 +b = b
3711 +c = c
3712 %Equal.sym(Bool, Nat.is_le(a, Nat.min(b, c)), Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)), le_min(a, b, c)) : {_ == True{} : Bool}
3713 %Equal.sym(Bool, Nat.is_le(a, b), True{}, hb) : {Bool.and(_, Nat.is_le(a, c)) == True{} : Bool}
3714 hc
3715
3716# An upper bound of both a and b bounds their maximum: a <= c and b <= c imply max a b <= c.
3717law max_le_of_le_of_le:
3718 for a: Nat
3719 for b: Nat
3720 for c: Nat
3721 for ha: le(a, c)
3722 for hb: le(b, c)
3723 le(Nat.max(a, b), c)
3724
3725def max_le_of_le_of_le(a, b, c, ha, hb):
3726 +a = a
3727 +b = b
3728 +c = c
3729 %Equal.sym(Bool, Nat.is_le(Nat.max(a, b), c), Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)), max_le(a, b, c)) : {_ == True{} : Bool}
3730 %Equal.sym(Bool, Nat.is_le(a, c), True{}, ha) : {Bool.and(_, Nat.is_le(b, c)) == True{} : Bool}
3731 hb
3732
3733# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
3734
3735# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
3736law add_zero_sym:
3737 for x: Nat
3738 {x == Nat.add(x, 0n) : Nat}
3739
3740def add_zero_sym(x):
3741 Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
3742
3743# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
3744law zero_add_sym:
3745 for -x: Nat
3746 {x == Nat.add(0n, x) : Nat}
3747
3748def zero_add_sym(x):
3749 Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
3750
3751# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
3752law add_succ_sym:
3753 for n: Nat
3754 for -m: Nat
3755 {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
3756
3757def add_succ_sym(n, m):
3758 Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
3759
3760# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
3761law succ_add_sym:
3762 for -n: Nat
3763 for -m: Nat
3764 {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
3765
3766def succ_add_sym(n, m):
3767 Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
3768
3769# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
3770law add_comm_sym:
3771 for n: Nat
3772 for m: Nat
3773 {Nat.add(m, n) == Nat.add(n, m) : Nat}
3774
3775def add_comm_sym(n, m):
3776 Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
3777
3778# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
3779law add_assoc_sym:
3780 for a: Nat
3781 for -b: Nat
3782 for -c: Nat
3783 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
3784
3785def add_assoc_sym(a, b, c):
3786 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
3787
3788# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
3789law add_left_comm_sym:
3790 for a: Nat
3791 for b: Nat
3792 for -c: Nat
3793 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
3794
3795def add_left_comm_sym(a, b, c):
3796 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
3797
3798# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
3799law add_right_comm_sym:
3800 for a: Nat
3801 for b: Nat
3802 for c: Nat
3803 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
3804
3805def add_right_comm_sym(a, b, c):
3806 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
3807
3808# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
3809law add_add_add_comm_sym:
3810 for a: Nat
3811 for b: Nat
3812 for c: Nat
3813 for -d: Nat
3814 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
3815
3816def add_add_add_comm_sym(a, b, c, d):
3817 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))
3818
3819# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
3820law mul_zero_sym:
3821 for x: Nat
3822 {0n == Nat.mul(x, 0n) : Nat}
3823
3824def mul_zero_sym(x):
3825 Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
3826
3827# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
3828law zero_mul_sym:
3829 for -x: Nat
3830 {0n == Nat.mul(0n, x) : Nat}
3831
3832def zero_mul_sym(x):
3833 Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
3834
3835# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
3836law mul_one_sym:
3837 for x: Nat
3838 {x == Nat.mul(x, 1n) : Nat}
3839
3840def mul_one_sym(x):
3841 Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
3842
3843# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
3844law one_mul_sym:
3845 for x: Nat
3846 {x == Nat.mul(1n, x) : Nat}
3847
3848def one_mul_sym(x):
3849 Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
3850
3851# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
3852law mul_succ_sym:
3853 for n: Nat
3854 for m: Nat
3855 {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
3856
3857def mul_succ_sym(n, m):
3858 Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
3859
3860# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
3861law succ_mul_sym:
3862 for n: Nat
3863 for m: Nat
3864 {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
3865
3866def succ_mul_sym(n, m):
3867 Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
3868
3869# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
3870law mul_comm_sym:
3871 for n: Nat
3872 for m: Nat
3873 {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
3874
3875def mul_comm_sym(n, m):
3876 Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
3877
3878# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
3879law add_mul_sym:
3880 for a: Nat
3881 for -b: Nat
3882 for c: Nat
3883 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
3884
3885def add_mul_sym(a, b, c):
3886 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))
3887
3888# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
3889law mul_add_sym:
3890 for a: Nat
3891 for b: Nat
3892 for c: Nat
3893 {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
3894
3895def mul_add_sym(a, b, c):
3896 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))
3897
3898# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
3899law mul_assoc_sym:
3900 for a: Nat
3901 for b: Nat
3902 for c: Nat
3903 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
3904
3905def mul_assoc_sym(a, b, c):
3906 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
3907
3908# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
3909law sub_zero_sym:
3910 for n: Nat
3911 {n == Nat.sub(n, 0n) : Nat}
3912
3913def sub_zero_sym(n):
3914 Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
3915
3916# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
3917law zero_sub_sym:
3918 for n: Nat
3919 {0n == Nat.sub(0n, n) : Nat}
3920
3921def zero_sub_sym(n):
3922 Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
3923
3924# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
3925law sub_self_sym:
3926 for n: Nat
3927 {0n == Nat.sub(n, n) : Nat}
3928
3929def sub_self_sym(n):
3930 Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
3931
3932# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
3933law succ_sub_succ_sym:
3934 for -n: Nat
3935 for -m: Nat
3936 {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
3937
3938def succ_sub_succ_sym(n, m):
3939 Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
3940
3941# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
3942law add_sub_cancel_sym:
3943 for n: Nat
3944 for m: Nat
3945 {n == Nat.sub(Nat.add(n, m), m) : Nat}
3946
3947def add_sub_cancel_sym(n, m):
3948 Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
3949
3950# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
3951law add_sub_cancel_left_sym:
3952 for n: Nat
3953 for m: Nat
3954 {m == Nat.sub(Nat.add(n, m), n) : Nat}
3955
3956def add_sub_cancel_left_sym(n, m):
3957 Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
3958
3959# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
3960law sub_sub_sym:
3961 for n: Nat
3962 for m: Nat
3963 for k: Nat
3964 {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
3965
3966def sub_sub_sym(n, m, k):
3967 Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
3968
3969# 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.
3970law div_mod_eq_sym:
3971 for +a: Nat
3972 for +b: Nat
3973 {a == Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) : Nat}
3974
3975def div_mod_eq_sym(a, b):
3976 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))
3977
3978# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
3979law add_div_left_sym:
3980 for +a: Nat
3981 for +b: Nat
3982 {1n+Nat.div(a, 1n+b) == Nat.div(Nat.add(1n+b, a), 1n+b) : Nat}
3983
3984def add_div_left_sym(a, b):
3985 Equal.sym(Nat, Nat.div(Nat.add(1n+b, a), 1n+b), 1n+Nat.div(a, 1n+b), add_div_left(a, b))
3986
3987# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
3988law le_div_iff_mul_le_sym:
3989 for n: Nat
3990 for +a: Nat
3991 for +b: Nat
3992 {Nat.is_le(Nat.mul(n, 1n+b), a) == Nat.is_le(n, Nat.div(a, 1n+b)) : Bool}
3993
3994def le_div_iff_mul_le_sym(n, a, b):
3995 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))
3996
3997# Minimum is commutative, reversed to rewrite toward the simple side.
3998law min_comm_sym:
3999 for a: Nat
4000 for b: Nat
4001 {Nat.min(b, a) == Nat.min(a, b) : Nat}
4002
4003def min_comm_sym(a, b):
4004 Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
4005
4006# Maximum is commutative, reversed to rewrite toward the simple side.
4007law max_comm_sym:
4008 for a: Nat
4009 for b: Nat
4010 {Nat.max(b, a) == Nat.max(a, b) : Nat}
4011
4012def max_comm_sym(a, b):
4013 Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
4014
4015# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
4016law min_self_sym:
4017 for a: Nat
4018 {a == Nat.min(a, a) : Nat}
4019
4020def min_self_sym(a):
4021 Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
4022
4023# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
4024law max_self_sym:
4025 for a: Nat
4026 {a == Nat.max(a, a) : Nat}
4027
4028def max_self_sym(a):
4029 Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
4030
4031# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
4032law min_zero_sym:
4033 for a: Nat
4034 {0n == Nat.min(a, 0n) : Nat}
4035
4036def min_zero_sym(a):
4037 Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
4038
4039# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
4040law zero_min_sym:
4041 for a: Nat
4042 {0n == Nat.min(0n, a) : Nat}
4043
4044def zero_min_sym(a):
4045 Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
4046
4047# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
4048law max_zero_sym:
4049 for a: Nat
4050 {a == Nat.max(a, 0n) : Nat}
4051
4052def max_zero_sym(a):
4053 Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
4054
4055# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
4056law zero_max_sym:
4057 for a: Nat
4058 {a == Nat.max(0n, a) : Nat}
4059
4060def zero_max_sym(a):
4061 Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
4062
4063# Minimum is associative, reversed to rewrite toward the simple side.
4064law min_assoc_sym:
4065 for a: Nat
4066 for b: Nat
4067 for c: Nat
4068 {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
4069
4070def min_assoc_sym(a, b, c):
4071 Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
4072
4073# Maximum is associative, reversed to rewrite toward the simple side.
4074law max_assoc_sym:
4075 for a: Nat
4076 for b: Nat
4077 for c: Nat
4078 {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
4079
4080def max_assoc_sym(a, b, c):
4081 Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
4082
4083# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
4084law min_add_max_sym:
4085 for a: Nat
4086 for b: Nat
4087 {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
4088
4089def min_add_max_sym(a, b):
4090 Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
4091
4092# Any natural to the power zero is one, reversed to rewrite toward the simple side.
4093law pow_zero_sym:
4094 for -a: Nat
4095 {1n == Nat.pow(a, 0n) : Nat}
4096
4097def pow_zero_sym(a):
4098 Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
4099
4100# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
4101law pow_succ_sym:
4102 for -a: Nat
4103 for -n: Nat
4104 {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
4105
4106def pow_succ_sym(a, n):
4107 Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
4108
4109# Any natural to the power one is itself, reversed to rewrite toward the simple side.
4110law pow_one_sym:
4111 for a: Nat
4112 {a == Nat.pow(a, 1n) : Nat}
4113
4114def pow_one_sym(a):
4115 Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
4116
4117# One to any power is one, reversed to rewrite toward the simple side.
4118law one_pow_sym:
4119 for n: Nat
4120 {1n == Nat.pow(1n, n) : Nat}
4121
4122def one_pow_sym(n):
4123 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
4124
4125# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
4126law pow_add_sym:
4127 for a: Nat
4128 for m: Nat
4129 for n: Nat
4130 {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
4131
4132def pow_add_sym(a, m, n):
4133 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))
4134
4135# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
4136law double_eq_add_sym:
4137 for n: Nat
4138 {Nat.add(n, n) == Nat.double(n) : Nat}
4139
4140def double_eq_add_sym(n):
4141 Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
4142
4143# Every natural tests equal to itself, reversed to rewrite toward the simple side.
4144law is_eq_refl_sym:
4145 for n: Nat
4146 {True{} == Nat.is_eq(n, n) : Bool}
4147
4148def is_eq_refl_sym(n):
4149 Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
4150
4151# The equality test is symmetric, reversed to rewrite toward the simple side.
4152law is_eq_comm_sym:
4153 for a: Nat
4154 for b: Nat
4155 {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
4156
4157def is_eq_comm_sym(a, b):
4158 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
4159
4160# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
4161law is_ge_eq_is_le_sym:
4162 for a: Nat
4163 for b: Nat
4164 {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
4165
4166def is_ge_eq_is_le_sym(a, b):
4167 Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
4168
4169# A > b tests the same as b < a, reversed to rewrite toward the simple side.
4170law is_gt_eq_is_lt_sym:
4171 for a: Nat
4172 for b: Nat
4173 {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
4174
4175def is_gt_eq_is_lt_sym(a, b):
4176 Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
4177
4178# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
4179law is_lt_eq_succ_le_sym:
4180 for a: Nat
4181 for b: Nat
4182 {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
4183
4184def is_lt_eq_succ_le_sym(a, b):
4185 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
4186
4187# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
4188law not_is_le_sym:
4189 for a: Nat
4190 for b: Nat
4191 {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
4192
4193def not_is_le_sym(a, b):
4194 Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
4195
4196# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
4197law not_is_lt_sym:
4198 for a: Nat
4199 for b: Nat
4200 {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
4201
4202def not_is_lt_sym(a, b):
4203 Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))
4204
4205# 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.
4206law add_le_add_iff_left_sym:
4207 for k: Nat
4208 for -a: Nat
4209 for -b: Nat
4210 {Nat.is_le(Nat.add(k, a), Nat.add(k, b)) == Nat.is_le(a, b) : Bool}
4211
4212def add_le_add_iff_left_sym(k, a, b):
4213 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))
4214
4215# 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.
4216law le_and_le_sub_iff_add_le_sym:
4217 for a: Nat
4218 for -b: Nat
4219 for c: Nat
4220 {Nat.is_le(Nat.add(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) : Bool}
4221
4222def le_and_le_sub_iff_add_le_sym(a, b, c):
4223 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))
4224
4225# 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.
4226law min_le_iff_sym:
4227 for a: Nat
4228 for b: Nat
4229 for c: Nat
4230 {Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.min(a, b), c) : Bool}
4231
4232def min_le_iff_sym(a, b, c):
4233 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))
4234
4235# 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.
4236law lt_max_iff_sym:
4237 for a: Nat
4238 for b: Nat
4239 for c: Nat
4240 {Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.max(b, c)) : Bool}
4241
4242def lt_max_iff_sym(a, b, c):
4243 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))
4244
4245# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
4246law lt_sub_iff_add_lt_sym:
4247 for a: Nat
4248 for b: Nat
4249 for c: Nat
4250 {Nat.is_lt(Nat.add(b, a), c) == Nat.is_lt(a, Nat.sub(c, b)) : Bool}
4251
4252def lt_sub_iff_add_lt_sym(a, b, c):
4253 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))
4254
4255# Zero divided by anything is zero: 0 / b = 0, reversed to rewrite toward the simple side.
4256law zero_div_sym:
4257 for b: Nat
4258 {0n == Nat.div(0n, b) : Nat}
4259
4260def zero_div_sym(b):
4261 Equal.sym(Nat, Nat.div(0n, b), 0n, zero_div(b))
4262
4263# Zero modulo anything is zero: 0 % b = 0, reversed to rewrite toward the simple side.
4264law zero_mod_sym:
4265 for b: Nat
4266 {0n == Nat.mod(0n, b) : Nat}
4267
4268def zero_mod_sym(b):
4269 Equal.sym(Nat, Nat.mod(0n, b), 0n, zero_mod(b))
4270
4271# Dividing by one changes nothing: a / 1 = a, reversed to rewrite toward the simple side.
4272law div_one_sym:
4273 for a: Nat
4274 {a == Nat.div(a, 1n) : Nat}
4275
4276def div_one_sym(a):
4277 Equal.sym(Nat, Nat.div(a, 1n), a, div_one(a))
4278
4279# Any natural modulo one is zero: a % 1 = 0, reversed to rewrite toward the simple side.
4280law mod_one_sym:
4281 for a: Nat
4282 {0n == Nat.mod(a, 1n) : Nat}
4283
4284def mod_one_sym(a):
4285 Equal.sym(Nat, Nat.mod(a, 1n), 0n, mod_one(a))
4286
4287# A natural modulo itself is zero: n % n = 0, reversed to rewrite toward the simple side.
4288law mod_self_sym:
4289 for n: Nat
4290 {0n == Nat.mod(n, n) : Nat}
4291
4292def mod_self_sym(n):
4293 Equal.sym(Nat, Nat.mod(n, n), 0n, mod_self(n))
4294
4295# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1, reversed to rewrite toward the simple side.
4296law div_self_sym:
4297 for b: Nat
4298 {1n == Nat.div(1n+b, 1n+b) : Nat}
4299
4300def div_self_sym(b):
4301 Equal.sym(Nat, Nat.div(1n+b, 1n+b), 1n, div_self(b))
4302
4303# Taking a remainder twice is taking it once: (a % n) % n = a % n, reversed to rewrite toward the simple side.
4304law mod_mod_sym:
4305 for a: Nat
4306 for n: Nat
4307 {Nat.mod(a, n) == Nat.mod(Nat.mod(a, n), n) : Nat}
4308
4309def mod_mod_sym(a, n):
4310 Equal.sym(Nat, Nat.mod(Nat.mod(a, n), n), Nat.mod(a, n), mod_mod(a, n))
4311
4312# Adding the divisor does not change the remainder: (b + a) % b = a % b, reversed to rewrite toward the simple side.
4313law add_mod_left_sym:
4314 for a: Nat
4315 for b: Nat
4316 {Nat.mod(a, b) == Nat.mod(Nat.add(b, a), b) : Nat}
4317
4318def add_mod_left_sym(a, b):
4319 Equal.sym(Nat, Nat.mod(Nat.add(b, a), b), Nat.mod(a, b), add_mod_left(a, b))
4320
4321# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a, reversed to rewrite toward the simple side.
4322law mul_div_cancel_sym:
4323 for a: Nat
4324 for b: Nat
4325 {a == Nat.div(Nat.mul(a, 1n+b), 1n+b) : Nat}
4326
4327def mul_div_cancel_sym(a, b):
4328 Equal.sym(Nat, Nat.div(Nat.mul(a, 1n+b), 1n+b), a, mul_div_cancel(a, b))
4329
4330# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a, reversed to rewrite toward the simple side.
4331law mul_div_cancel_left_sym:
4332 for a: Nat
4333 for b: Nat
4334 {a == Nat.div(Nat.mul(1n+b, a), 1n+b) : Nat}
4335
4336def mul_div_cancel_left_sym(a, b):
4337 Equal.sym(Nat, Nat.div(Nat.mul(1n+b, a), 1n+b), a, mul_div_cancel_left(a, b))
4338
4339# A multiple of b leaves no remainder modulo b: (a * b) % b = 0, reversed to rewrite toward the simple side.
4340law mul_mod_left_sym:
4341 for a: Nat
4342 for b: Nat
4343 {0n == Nat.mod(Nat.mul(a, b), b) : Nat}
4344
4345def mul_mod_left_sym(a, b):
4346 Equal.sym(Nat, Nat.mod(Nat.mul(a, b), b), 0n, mul_mod_left(a, b))
4347
4348# A multiple of a leaves no remainder modulo a: (a * b) % a = 0, reversed to rewrite toward the simple side.
4349law mul_mod_right_sym:
4350 for a: Nat
4351 for b: Nat
4352 {0n == Nat.mod(Nat.mul(a, b), a) : Nat}
4353
4354def mul_mod_right_sym(a, b):
4355 Equal.sym(Nat, Nat.mod(Nat.mul(a, b), a), 0n, mul_mod_right(a, b))
4356
4357# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a, reversed to rewrite toward the simple side.
4358law mod_add_div_sym:
4359 for a: Nat
4360 for b: Nat
4361 {a == Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) : Nat}
4362
4363def mod_add_div_sym(a, b):
4364 Equal.sym(Nat, Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))), a, mod_add_div(a, b))
4365
4366# Left commutativity of multiplication: a * (b * c) = b * (a * c), reversed to rewrite toward the simple side.
4367law mul_left_comm_sym:
4368 for a: Nat
4369 for b: Nat
4370 for c: Nat
4371 {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
4372
4373def mul_left_comm_sym(a, b, c):
4374 Equal.sym(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)), mul_left_comm(a, b, c))
4375
4376# Right commutativity of multiplication: (a * b) * c = (a * c) * b, reversed to rewrite toward the simple side.
4377law mul_right_comm_sym:
4378 for a: Nat
4379 for b: Nat
4380 for c: Nat
4381 {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
4382
4383def mul_right_comm_sym(a, b, c):
4384 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(Nat.mul(a, c), b), mul_right_comm(a, b, c))
4385
4386# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d), reversed to rewrite toward the simple side.
4387law mul_mul_mul_comm_sym:
4388 for a: Nat
4389 for b: Nat
4390 for c: Nat
4391 for d: Nat
4392 {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
4393
4394def mul_mul_mul_comm_sym(a, b, c, d):
4395 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), Nat.mul(c, d)), Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), mul_mul_mul_comm(a, b, c, d))
4396
4397# Zero to a positive power is zero: 0^(n+1) = 0, reversed to rewrite toward the simple side.
4398law zero_pow_sym:
4399 for -n: Nat
4400 {0n == Nat.pow(0n, 1n+n) : Nat}
4401
4402def zero_pow_sym(n):
4403 Equal.sym(Nat, Nat.pow(0n, 1n+n), 0n, zero_pow(n))
4404
4405# A power of a product is the product of the powers: (a * b)^n = a^n * b^n, reversed to rewrite toward the simple side.
4406law mul_pow_sym:
4407 for +a: Nat
4408 for +b: Nat
4409 for n: Nat
4410 {Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) == Nat.pow(Nat.mul(a, b), n) : Nat}
4411
4412def mul_pow_sym(a, b, n):
4413 Equal.sym(Nat, Nat.pow(Nat.mul(a, b), n), Nat.mul(Nat.pow(a, n), Nat.pow(b, n)), mul_pow(a, b, n))
4414
4415# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n, reversed to rewrite toward the simple side.
4416law pow_mul_sym:
4417 for a: Nat
4418 for m: Nat
4419 for n: Nat
4420 {Nat.pow(Nat.pow(a, m), n) == Nat.pow(a, Nat.mul(m, n)) : Nat}
4421
4422def pow_mul_sym(a, m, n):
4423 Equal.sym(Nat, Nat.pow(a, Nat.mul(m, n)), Nat.pow(Nat.pow(a, m), n), pow_mul(a, m, n))
4424
4425# A common left summand cancels in a difference: (k + n) - (k + m) = n - m, reversed to rewrite toward the simple side.
4426law add_sub_add_left_sym:
4427 for k: Nat
4428 for -n: Nat
4429 for -m: Nat
4430 {Nat.sub(n, m) == Nat.sub(Nat.add(k, n), Nat.add(k, m)) : Nat}
4431
4432def add_sub_add_left_sym(k, n, m):
4433 Equal.sym(Nat, Nat.sub(Nat.add(k, n), Nat.add(k, m)), Nat.sub(n, m), add_sub_add_left(k, n, m))
4434
4435# A common right summand cancels in a difference: (n + k) - (m + k) = n - m, reversed to rewrite toward the simple side.
4436law add_sub_add_right_sym:
4437 for n: Nat
4438 for k: Nat
4439 for m: Nat
4440 {Nat.sub(n, m) == Nat.sub(Nat.add(n, k), Nat.add(m, k)) : Nat}
4441
4442def add_sub_add_right_sym(n, k, m):
4443 Equal.sym(Nat, Nat.sub(Nat.add(n, k), Nat.add(m, k)), Nat.sub(n, m), add_sub_add_right(n, k, m))
4444
4445# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k, reversed to rewrite toward the simple side.
4446law sub_mul_sym:
4447 for n: Nat
4448 for m: Nat
4449 for k: Nat
4450 {Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) == Nat.mul(Nat.sub(n, m), k) : Nat}
4451
4452def sub_mul_sym(n, m, k):
4453 Equal.sym(Nat, Nat.mul(Nat.sub(n, m), k), Nat.sub(Nat.mul(n, k), Nat.mul(m, k)), sub_mul(n, m, k))
4454
4455# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k, reversed to rewrite toward the simple side.
4456law mul_sub_sym:
4457 for n: Nat
4458 for m: Nat
4459 for k: Nat
4460 {Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) == Nat.mul(n, Nat.sub(m, k)) : Nat}
4461
4462def mul_sub_sym(n, m, k):
4463 Equal.sym(Nat, Nat.mul(n, Nat.sub(m, k)), Nat.sub(Nat.mul(n, m), Nat.mul(n, k)), mul_sub(n, m, k))
4464
4465# A number is at most the minimum exactly when it is at most both: a <= min b c tests as a <= b and a <= c (Mathlib's le_min_iff; the implication is le_min_of_le_of_le), reversed to rewrite toward the simple side.
4466law le_min_sym:
4467 for a: Nat
4468 for b: Nat
4469 for c: Nat
4470 {Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)) == Nat.is_le(a, Nat.min(b, c)) : Bool}
4471
4472def le_min_sym(a, b, c):
4473 Equal.sym(Bool, Nat.is_le(a, Nat.min(b, c)), Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)), le_min(a, b, c))
4474
4475# The maximum is at most c exactly when both arguments are: max a b <= c tests as a <= c and b <= c (Mathlib's max_le_iff; the implication is max_le_of_le_of_le), reversed to rewrite toward the simple side.
4476law max_le_sym:
4477 for a: Nat
4478 for b: Nat
4479 for c: Nat
4480 {Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.max(a, b), c) : Bool}
4481
4482def max_le_sym(a, b, c):
4483 Equal.sym(Bool, Nat.is_le(Nat.max(a, b), c), Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)), max_le(a, b, c))
4484
4485# Below a successor means at most: m < n + 1 tests as m <= n, reversed to rewrite toward the simple side.
4486law lt_succ_iff_sym:
4487 for m: Nat
4488 for n: Nat
4489 {Nat.is_le(m, n) == Nat.is_lt(m, 1n+n) : Bool}
4490
4491def lt_succ_iff_sym(m, n):
4492 Equal.sym(Bool, Nat.is_lt(m, 1n+n), Nat.is_le(m, n), lt_succ_iff(m, n))
4493
4494# At most means below or equal: a <= b tests as a < b or a = b, reversed to rewrite toward the simple side.
4495law le_iff_lt_or_eq_sym:
4496 for a: Nat
4497 for b: Nat
4498 {Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)) == Nat.is_le(a, b) : Bool}
4499
4500def le_iff_lt_or_eq_sym(a, b):
4501 Equal.sym(Bool, Nat.is_le(a, b), Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)), le_iff_lt_or_eq(a, b))
4502
4503# Below means at most and different: a < b tests as a <= b and not a = b, reversed to rewrite toward the simple side.
4504law lt_iff_le_and_ne_sym:
4505 for a: Nat
4506 for b: Nat
4507 {Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))) == Nat.is_lt(a, b) : Bool}
4508
4509def lt_iff_le_and_ne_sym(a, b):
4510 Equal.sym(Bool, Nat.is_lt(a, b), Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))), lt_iff_le_and_ne(a, b))
4511
4512# Adding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b, reversed to rewrite toward the simple side.
4513law add_lt_add_iff_left_sym:
4514 for k: Nat
4515 for -a: Nat
4516 for -b: Nat
4517 {Nat.is_lt(Nat.add(k, a), Nat.add(k, b)) == Nat.is_lt(a, b) : Bool}
4518
4519def add_lt_add_iff_left_sym(k, a, b):
4520 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_lt(Nat.add(k, a), Nat.add(k, b)), add_lt_add_iff_left(k, a, b))
4521
4522# Adding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k, reversed to rewrite toward the simple side.
4523law add_lt_add_iff_right_sym:
4524 for a: Nat
4525 for b: Nat
4526 for k: Nat
4527 {Nat.is_lt(Nat.add(a, k), Nat.add(b, k)) == Nat.is_lt(a, b) : Bool}
4528
4529def add_lt_add_iff_right_sym(a, b, k):
4530 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_lt(Nat.add(a, k), Nat.add(b, k)), add_lt_add_iff_right(a, b, k))
4531
4532# Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c), reversed to rewrite toward the simple side.
4533law min_max_distrib_left_sym:
4534 for a: Nat
4535 for b: Nat
4536 for c: Nat
4537 {Nat.max(Nat.min(a, b), Nat.min(a, c)) == Nat.min(a, Nat.max(b, c)) : Nat}
4538
4539def min_max_distrib_left_sym(a, b, c):
4540 Equal.sym(Nat, Nat.min(a, Nat.max(b, c)), Nat.max(Nat.min(a, b), Nat.min(a, c)), min_max_distrib_left(a, b, c))
4541
4542# Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c), reversed to rewrite toward the simple side.
4543law max_min_distrib_left_sym:
4544 for a: Nat
4545 for b: Nat
4546 for c: Nat
4547 {Nat.min(Nat.max(a, b), Nat.max(a, c)) == Nat.max(a, Nat.min(b, c)) : Nat}
4548
4549def max_min_distrib_left_sym(a, b, c):
4550 Equal.sym(Nat, Nat.max(a, Nat.min(b, c)), Nat.min(Nat.max(a, b), Nat.max(a, c)), max_min_distrib_left(a, b, c))
4551
4552# A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c, reversed to rewrite toward the simple side.
4553law min_add_add_left_sym:
4554 for a: Nat
4555 for -b: Nat
4556 for -c: Nat
4557 {Nat.add(a, Nat.min(b, c)) == Nat.min(Nat.add(a, b), Nat.add(a, c)) : Nat}
4558
4559def min_add_add_left_sym(a, b, c):
4560 Equal.sym(Nat, Nat.min(Nat.add(a, b), Nat.add(a, c)), Nat.add(a, Nat.min(b, c)), min_add_add_left(a, b, c))
4561
4562# A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c, reversed to rewrite toward the simple side.
4563law min_add_add_right_sym:
4564 for a: Nat
4565 for b: Nat
4566 for c: Nat
4567 {Nat.add(Nat.min(a, b), c) == Nat.min(Nat.add(a, c), Nat.add(b, c)) : Nat}
4568
4569def min_add_add_right_sym(a, b, c):
4570 Equal.sym(Nat, Nat.min(Nat.add(a, c), Nat.add(b, c)), Nat.add(Nat.min(a, b), c), min_add_add_right(a, b, c))
4571
4572# A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c, reversed to rewrite toward the simple side.
4573law max_add_add_left_sym:
4574 for a: Nat
4575 for -b: Nat
4576 for -c: Nat
4577 {Nat.add(a, Nat.max(b, c)) == Nat.max(Nat.add(a, b), Nat.add(a, c)) : Nat}
4578
4579def max_add_add_left_sym(a, b, c):
4580 Equal.sym(Nat, Nat.max(Nat.add(a, b), Nat.add(a, c)), Nat.add(a, Nat.max(b, c)), max_add_add_left(a, b, c))
4581
4582# A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c, reversed to rewrite toward the simple side.
4583law max_add_add_right_sym:
4584 for a: Nat
4585 for b: Nat
4586 for c: Nat
4587 {Nat.add(Nat.max(a, b), c) == Nat.max(Nat.add(a, c), Nat.add(b, c)) : Nat}
4588
4589def max_add_add_right_sym(a, b, c):
4590 Equal.sym(Nat, Nat.max(Nat.add(a, c), Nat.add(b, c)), Nat.add(Nat.max(a, b), c), max_add_add_right(a, b, c))
4591
4592# The minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c, reversed to rewrite toward the simple side.
4593law min_lt_iff_sym:
4594 for a: Nat
4595 for b: Nat
4596 for c: Nat
4597 {Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)) == Nat.is_lt(Nat.min(a, b), c) : Bool}
4598
4599def min_lt_iff_sym(a, b, c):
4600 Equal.sym(Bool, Nat.is_lt(Nat.min(a, b), c), Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)), min_lt_iff(a, b, c))
4601
4602# A number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c, reversed to rewrite toward the simple side.
4603law lt_min_iff_sym:
4604 for a: Nat
4605 for b: Nat
4606 for c: Nat
4607 {Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.min(b, c)) : Bool}
4608
4609def lt_min_iff_sym(a, b, c):
4610 Equal.sym(Bool, Nat.is_lt(a, Nat.min(b, c)), Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)), lt_min_iff(a, b, c))
4611
4612# The maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c, reversed to rewrite toward the simple side.
4613law max_lt_iff_sym:
4614 for a: Nat
4615 for b: Nat
4616 for c: Nat
4617 {Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)) == Nat.is_lt(Nat.max(a, b), c) : Bool}
4618
4619def max_lt_iff_sym(a, b, c):
4620 Equal.sym(Bool, Nat.is_lt(Nat.max(a, b), c), Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)), max_lt_iff(a, b, c))
4621
4622# A number is at most the maximum exactly when it is at most one argument: a <= max b c tests as a <= b or a <= c, reversed to rewrite toward the simple side.
4623law le_max_iff_sym:
4624 for a: Nat
4625 for b: Nat
4626 for c: Nat
4627 {Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)) == Nat.is_le(a, Nat.max(b, c)) : Bool}
4628
4629def le_max_iff_sym(a, b, c):
4630 Equal.sym(Bool, Nat.is_le(a, Nat.max(b, c)), Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)), le_max_iff(a, b, c))
4631
4632# Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.
4633law add_mul_div_right_sym:
4634 for x: Nat
4635 for z: Nat
4636 for b: Nat
4637 {Nat.add(Nat.div(x, 1n+b), z) == Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b) : Nat}
4638
4639def add_mul_div_right_sym(x, z, b):
4640 Equal.sym(Nat, Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b), Nat.add(Nat.div(x, 1n+b), z), add_mul_div_right(x, z, b))
4641
4642# Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z, reversed to rewrite toward the simple side.
4643law add_mul_div_left_sym:
4644 for x: Nat
4645 for z: Nat
4646 for b: Nat
4647 {Nat.add(Nat.div(x, 1n+b), z) == Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b) : Nat}
4648
4649def add_mul_div_left_sym(x, z, b):
4650 Equal.sym(Nat, Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b), Nat.add(Nat.div(x, 1n+b), z), add_mul_div_left(x, z, b))
4651
4652# Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b, reversed to rewrite toward the simple side.
4653law add_mul_mod_self_right_sym:
4654 for a: Nat
4655 for b: Nat
4656 for c: Nat
4657 {Nat.mod(a, b) == Nat.mod(Nat.add(a, Nat.mul(c, b)), b) : Nat}
4658
4659def add_mul_mod_self_right_sym(a, b, c):
4660 Equal.sym(Nat, Nat.mod(Nat.add(a, Nat.mul(c, b)), b), Nat.mod(a, b), add_mul_mod_self_right(a, b, c))
4661
4662# Adding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b, reversed to rewrite toward the simple side.
4663law add_mul_mod_self_left_sym:
4664 for a: Nat
4665 for b: Nat
4666 for c: Nat
4667 {Nat.mod(a, b) == Nat.mod(Nat.add(a, Nat.mul(b, c)), b) : Nat}
4668
4669def add_mul_mod_self_left_sym(a, b, c):
4670 Equal.sym(Nat, Nat.mod(Nat.add(a, Nat.mul(b, c)), b), Nat.mod(a, b), add_mul_mod_self_left(a, b, c))
4671
4672# A remainder modulo two is zero or one, reversed to rewrite toward the simple side.
4673law mod_two_eq_zero_or_one_sym:
4674 for n: Nat
4675 {True{} == Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)) : Bool}
4676
4677def mod_two_eq_zero_or_one_sym(n):
4678 Equal.sym(Bool, Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)), True{}, mod_two_eq_zero_or_one(n))
4679
4680# The divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a, reversed to rewrite toward the simple side.
4681law div_add_mod_sym:
4682 for a: Nat
4683 for b: Nat
4684 {a == Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)) : Nat}
4685
4686def div_add_mod_sym(a, b):
4687 Equal.sym(Nat, Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)), a, div_add_mod(a, b))
4688
4689# Two times n is n + n, reversed to rewrite toward the simple side.
4690law two_mul_sym:
4691 for n: Nat
4692 {Nat.add(n, n) == Nat.mul(2n, n) : Nat}
4693
4694def two_mul_sym(n):
4695 Equal.sym(Nat, Nat.mul(2n, n), Nat.add(n, n), two_mul(n))
4696
4697# Doubling is multiplying by two: double n = 2 * n, reversed to rewrite toward the simple side.
4698law double_eq_two_mul_sym:
4699 for n: Nat
4700 {Nat.mul(2n, n) == Nat.double(n) : Nat}
4701
4702def double_eq_two_mul_sym(n):
4703 Equal.sym(Nat, Nat.double(n), Nat.mul(2n, n), double_eq_two_mul(n))
4704
4705# Doubling distributes over addition: double (a + b) = double a + double b, reversed to rewrite toward the simple side.
4706law double_add_sym:
4707 for a: Nat
4708 for b: Nat
4709 {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}
4710
4711def double_add_sym(a, b):
4712 Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(Nat.double(a), Nat.double(b)), double_add(a, b))
4713
4714# Doubling a product doubles its left factor: double (a * b) = double a * b, reversed to rewrite toward the simple side.
4715law double_mul_sym:
4716 for a: Nat
4717 for b: Nat
4718 {Nat.mul(Nat.double(a), b) == Nat.double(Nat.mul(a, b)) : Nat}
4719
4720def double_mul_sym(a, b):
4721 Equal.sym(Nat, Nat.double(Nat.mul(a, b)), Nat.mul(Nat.double(a), b), double_mul(a, b))
4722
4723# Multiplying by a doubled factor doubles the product: a * double b = double (a * b), reversed to rewrite toward the simple side.
4724law mul_double_sym:
4725 for a: Nat
4726 for b: Nat
4727 {Nat.double(Nat.mul(a, b)) == Nat.mul(a, Nat.double(b)) : Nat}
4728
4729def mul_double_sym(a, b):
4730 Equal.sym(Nat, Nat.mul(a, Nat.double(b)), Nat.double(Nat.mul(a, b)), mul_double(a, b))
4731
4732# Doubling distributes over truncated subtraction: double (a - b) = double a - double b, reversed to rewrite toward the simple side.
4733law double_sub_sym:
4734 for a: Nat
4735 for b: Nat
4736 {Nat.sub(Nat.double(a), Nat.double(b)) == Nat.double(Nat.sub(a, b)) : Nat}
4737
4738def double_sub_sym(a, b):
4739 Equal.sym(Nat, Nat.double(Nat.sub(a, b)), Nat.sub(Nat.double(a), Nat.double(b)), double_sub(a, b))
4740
4741# Twice the half plus the parity is the number: double (n / 2) + n % 2 = n, reversed to rewrite toward the simple side.
4742law double_div_two_add_mod_two_sym:
4743 for n: Nat
4744 {n == Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}
4745
4746def double_div_two_add_mod_two_sym(n):
4747 Equal.sym(Nat, Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)), n, double_div_two_add_mod_two(n))
4748
4749# Adding the same amount on the right does not change the order test: a <= b tests as a + k <= b + k, reversed to rewrite toward the simple side.
4750law add_le_add_iff_right_sym:
4751 for a: Nat
4752 for b: Nat
4753 for k: Nat
4754 {Nat.is_le(Nat.add(a, k), Nat.add(b, k)) == Nat.is_le(a, b) : Bool}
4755
4756def add_le_add_iff_right_sym(a, b, k):
4757 Equal.sym(Bool, Nat.is_le(a, b), Nat.is_le(Nat.add(a, k), Nat.add(b, k)), add_le_add_iff_right(a, b, k))
4758
4759# Adding the same amount on the left does not change the equality test: a = b tests as k + a = k + b, reversed to rewrite toward the simple side.
4760law add_left_cancel_iff_sym:
4761 for k: Nat
4762 for -a: Nat
4763 for -b: Nat
4764 {Nat.is_eq(Nat.add(k, a), Nat.add(k, b)) == Nat.is_eq(a, b) : Bool}
4765
4766def add_left_cancel_iff_sym(k, a, b):
4767 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(Nat.add(k, a), Nat.add(k, b)), add_left_cancel_iff(k, a, b))
4768
4769# Adding the same amount on the right does not change the equality test: a = b tests as a + k = b + k, reversed to rewrite toward the simple side.
4770law add_right_cancel_iff_sym:
4771 for a: Nat
4772 for b: Nat
4773 for k: Nat
4774 {Nat.is_eq(Nat.add(a, k), Nat.add(b, k)) == Nat.is_eq(a, b) : Bool}
4775
4776def add_right_cancel_iff_sym(a, b, k):
4777 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(Nat.add(a, k), Nat.add(b, k)), add_right_cancel_iff(a, b, k))