nat.bend
bend-mathlib@0.7.5.0 · 4,834 lines · 0 definitions
1# bend-mathlib/nat.bend: Nat arithmetic (add, mul, sub, div, mod, min, max, pow, double) and order
2# (le, lt, ge, gt).
3import Base
4
5# Zero is a right identity for addition: x + 0 = x.
6law add_zero:
7 for x: Nat
8 {Nat.add(x, 0n) == x : Nat}
9
10def add_zero(x):
11 match x:
12 case 0n:
13 {==}
14 case 1n+p:
15 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
16 {==}
17
18# Zero is a left identity for addition: 0 + x = x.
19law zero_add:
20 for -x: Nat
21 {Nat.add(0n, x) == x : Nat}
22
23def zero_add(x):
24 {==}
25
26# Adding a successor on the right: n + (m + 1) = (n + m) + 1.
27law add_succ:
28 for n: Nat
29 for -m: Nat
30 {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
31
32def add_succ(n, m):
33 match n:
34 case 0n:
35 {==}
36 case 1n+p:
37 %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
38 {==}
39
40# Adding a successor on the left: (n + 1) + m = (n + m) + 1.
41law succ_add:
42 for -n: Nat
43 for -m: Nat
44 {Nat.add(1n+n, m) == 1n+Nat.add(n, m) : Nat}
45
46def succ_add(n, m):
47 {==}
48
49# Addition is commutative: n + m = m + n.
50law add_comm:
51 for n: Nat
52 for m: Nat
53 {Nat.add(n, m) == Nat.add(m, n) : Nat}
54
55def add_comm(n, m):
56 match n m:
57 case 0n 0n:
58 {==}
59 case 0n 1n+q:
60 %add_zero(q) : {1n+_ == 1n+Nat.add(q, 0n) : Nat}
61 {==}
62 case 1n+p 0n:
63 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
64 {==}
65 case 1n++p 1n++q:
66 %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}
67 %Equal.sym(Nat, Nat.add(q, 1n+p), 1n+Nat.add(q, p), add_succ(q, p)) : {2n+Nat.add(p, q) == 1n+_ : Nat}
68 %add_comm(p, q) : {2n+Nat.add(p, q) == 2n+_ : Nat}
69 {==}
70
71# Addition is associative: (a + b) + c = a + (b + c).
72law add_assoc:
73 for a: Nat
74 for -b: Nat
75 for -c: Nat
76 {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
77
78def add_assoc(a, b, c):
79 match a:
80 case 0n:
81 {==}
82 case 1n+p:
83 %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
84 {==}
85
86# Left commutativity of addition: a + (b + c) = b + (a + c).
87law add_left_comm:
88 for a: Nat
89 for b: Nat
90 for -c: Nat
91 {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
92
93def add_left_comm(a, b, c):
94 match a:
95 case 0n:
96 {==}
97 case 1n+p:
98 +b = b
99 %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}
100 %add_left_comm(p, b, c) : {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
101 {==}
102
103# Right commutativity of addition: (a + b) + c = (a + c) + b.
104law add_right_comm:
105 for a: Nat
106 for b: Nat
107 for c: Nat
108 {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
109
110def add_right_comm(a, b, c):
111 match a:
112 case 0n:
113 add_comm(b, c)
114 case 1n+p:
115 %add_right_comm(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
116 {==}
117
118# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d).
119law add_add_add_comm:
120 for a: Nat
121 for b: Nat
122 for c: Nat
123 for -d: Nat
124 {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
125
126def add_add_add_comm(a, b, c, d):
127 match a:
128 case 0n:
129 add_left_comm(b, c, d)
130 case 1n+p:
131 %add_add_add_comm(p, b, c, d) : {1n+Nat.add(Nat.add(p, b), Nat.add(c, d)) == 1n+_ : Nat}
132 {==}
133
134def internal_pred(n: Nat) -> Nat:
135 match n:
136 case 0n:
137 0n
138 case 1n+p:
139 p
140
141# The successor function is injective: a + 1 = b + 1 implies a = b.
142law succ_inj:
143 for -a: Nat
144 for -b: Nat
145 for e: {1n+a == 1n+b : Nat}
146 {a == b : Nat}
147
148def succ_inj(a, b, e):
149 %e : {a == internal_pred(_) : Nat}
150 {==}
151
152def internal_zero_ne_succ(-n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
153 %e : Bool.pick(Type, Nat.is_eq(_, 0n), Unit, Empty)
154 Unit{}
155
156# Zero is not a successor.
157law zero_ne_succ:
158 for -n: Nat
159 {0n != 1n+n : Nat}
160
161def zero_ne_succ(n):
162 e => internal_zero_ne_succ(n, e)
163
164def internal_succ_ne_zero(-n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
165 %e : Bool.pick(Type, Nat.is_eq(_, 0n), Empty, Unit)
166 Unit{}
167
168# A successor is not zero.
169law succ_ne_zero:
170 for -n: Nat
171 {1n+n != 0n : Nat}
172
173def succ_ne_zero(n):
174 e => internal_succ_ne_zero(n, e)
175
176# Addition cancels on the left: a + b = a + c implies b = c.
177law add_left_cancel:
178 for a: Nat
179 for -b: Nat
180 for -c: Nat
181 for e: {Nat.add(a, b) == Nat.add(a, c) : Nat}
182 {b == c : Nat}
183
184def add_left_cancel(a, b, c, e):
185 match a:
186 case 0n:
187 e
188 case 1n+p:
189 add_left_cancel(p, b, c, succ_inj(Nat.add(p, b), Nat.add(p, c), e))
190
191# Addition cancels on the right: a + b = c + b implies a = c.
192law add_right_cancel:
193 for a: Nat
194 for b: Nat
195 for c: Nat
196 for e: {Nat.add(a, b) == Nat.add(c, b) : Nat}
197 {a == c : Nat}
198
199def add_right_cancel(a, b, c, e):
200 +b = b
201 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))))
202
203# Zero absorbs multiplication on the right: x * 0 = 0.
204law mul_zero:
205 for x: Nat
206 {Nat.mul(x, 0n) == 0n : Nat}
207
208def mul_zero(x):
209 match x:
210 case 0n:
211 {==}
212 case 1n+p:
213 mul_zero(p)
214
215# Zero absorbs multiplication on the left: 0 * x = 0.
216law zero_mul:
217 for -x: Nat
218 {Nat.mul(0n, x) == 0n : Nat}
219
220def zero_mul(x):
221 {==}
222
223# One is a right identity for multiplication: x * 1 = x.
224law mul_one:
225 for x: Nat
226 {Nat.mul(x, 1n) == x : Nat}
227
228def mul_one(x):
229 match x:
230 case 0n:
231 {==}
232 case 1n+p:
233 %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
234 {==}
235
236# One is a left identity for multiplication: 1 * x = x.
237law one_mul:
238 for x: Nat
239 {Nat.mul(1n, x) == x : Nat}
240
241def one_mul(x):
242 add_zero(x)
243
244# Multiplying by a successor on the right: n * (m + 1) = n * m + n.
245law mul_succ:
246 for n: Nat
247 for m: Nat
248 {Nat.mul(n, 1n+m) == Nat.add(Nat.mul(n, m), n) : Nat}
249
250def mul_succ(n, m):
251 match n:
252 case 0n:
253 {==}
254 case 1n++p:
255 +m = m
256 %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}
257 %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}
258 %mul_succ(p, m) : {1n+Nat.add(m, Nat.mul(p, 1n+m)) == 1n+Nat.add(m, _) : Nat}
259 {==}
260
261# Multiplying by a successor on the left: (n + 1) * m = n * m + m.
262law succ_mul:
263 for n: Nat
264 for m: Nat
265 {Nat.mul(1n+n, m) == Nat.add(Nat.mul(n, m), m) : Nat}
266
267def succ_mul(n, m):
268 +m = m
269 add_comm(m, Nat.mul(n, m))
270
271# Multiplication is commutative: n * m = m * n.
272law mul_comm:
273 for n: Nat
274 for m: Nat
275 {Nat.mul(n, m) == Nat.mul(m, n) : Nat}
276
277def mul_comm(n, m):
278 match n:
279 case 0n:
280 %mul_zero(m) : {_ == Nat.mul(m, 0n) : Nat}
281 {==}
282 case 1n++p:
283 +m = m
284 %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}
285 %mul_comm(p, m) : {Nat.add(m, Nat.mul(p, m)) == Nat.add(_, m) : Nat}
286 add_comm(m, Nat.mul(p, m))
287
288# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c.
289law add_mul:
290 for a: Nat
291 for -b: Nat
292 for c: Nat
293 {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
294
295def add_mul(a, b, c):
296 match a:
297 case 0n:
298 {==}
299 case 1n+p:
300 +c = c
301 %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}
302 %add_mul(p, b, c) : {Nat.add(c, Nat.mul(Nat.add(p, b), c)) == Nat.add(c, _) : Nat}
303 {==}
304
305# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c.
306law mul_add:
307 for a: Nat
308 for b: Nat
309 for c: Nat
310 {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
311
312def mul_add(a, b, c):
313 match a:
314 case 0n:
315 {==}
316 case 1n++p:
317 +b = b
318 +c = c
319 %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}
320 add_add_add_comm(b, c, Nat.mul(p, b), Nat.mul(p, c))
321
322# Multiplication is associative: (a * b) * c = a * (b * c).
323law mul_assoc:
324 for a: Nat
325 for b: Nat
326 for c: Nat
327 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
328
329def mul_assoc(a, b, c):
330 match a:
331 case 0n:
332 {==}
333 case 1n+p:
334 +b = b
335 +c = c
336 %mul_assoc(p, b, c) : {Nat.mul(Nat.add(b, Nat.mul(p, b)), c) == Nat.add(Nat.mul(b, c), _) : Nat}
337 add_mul(b, Nat.mul(p, b), c)
338
339# The order a <= b on naturals, as a reusable proposition.
340def le(a: Nat, b: Nat) -> Data:
341 {Nat.is_le(a, b) == True{} : Bool}
342
343# The strict order a < b on naturals, as a reusable proposition.
344def lt(a: Nat, b: Nat) -> Data:
345 {Nat.is_lt(a, b) == True{} : Bool}
346
347# The order a >= b on naturals, as a reusable proposition.
348def ge(a: Nat, b: Nat) -> Data:
349 {Nat.is_ge(a, b) == True{} : Bool}
350
351# The strict order a > b on naturals, as a reusable proposition.
352def gt(a: Nat, b: Nat) -> Data:
353 {Nat.is_gt(a, b) == True{} : Bool}
354
355def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
356 %e : Bool.pick(Type, _, Empty, Unit)
357 Unit{}
358
359# Every natural is at most itself: a <= a.
360law le_refl:
361 for a: Nat
362 le(a, a)
363
364def le_refl(a):
365 match a:
366 case 0n:
367 {==}
368 case 1n+p:
369 le_refl(p)
370
371# Zero is at most every natural: 0 <= b.
372law zero_le:
373 for b: Nat
374 le(0n, b)
375
376def zero_le(b):
377 match b:
378 case 0n:
379 {==}
380 case 1n+p:
381 {==}
382
383# Every natural is at most its successor: n <= n + 1.
384law le_succ:
385 for n: Nat
386 le(n, 1n+n)
387
388def le_succ(n):
389 match n:
390 case 0n:
391 {==}
392 case 1n+p:
393 le_succ(p)
394
395# Adding on the right never decreases a natural: n <= n + k.
396law le_add_right:
397 for n: Nat
398 for k: Nat
399 le(n, Nat.add(n, k))
400
401def le_add_right(n, k):
402 match n:
403 case 0n:
404 zero_le(k)
405 case 1n+p:
406 le_add_right(p, k)
407
408# The order is transitive: a <= b and b <= c imply a <= c.
409law le_trans:
410 for a: Nat
411 for b: Nat
412 for c: Nat
413 for ab: le(a, b)
414 for bc: le(b, c)
415 le(a, c)
416
417def le_trans(a, b, c, ab, bc):
418 match a b c:
419 case 0n _ 0n:
420 {==}
421 case 0n _ 1n+r:
422 {==}
423 case 1n+p 0n _:
424 Empty.absurd(le(1n+p, c), internal_false_ne_true(ab))
425 case 1n+p 1n+q 0n:
426 Empty.absurd(le(1n+p, 0n), internal_false_ne_true(bc))
427 case 1n+p 1n+q 1n+r:
428 le_trans(p, q, r, ab, bc)
429
430# The order is antisymmetric: a <= b and b <= a imply a = b.
431law le_antisymm:
432 for a: Nat
433 for b: Nat
434 for ab: le(a, b)
435 for ba: le(b, a)
436 {a == b : Nat}
437
438def le_antisymm(a, b, ab, ba):
439 match a b:
440 case 0n 0n:
441 {==}
442 case 0n 1n+q:
443 Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(ba))
444 case 1n+p 0n:
445 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(ab))
446 case 1n+p 1n+q:
447 %le_antisymm(p, q, ab, ba) : {1n+p == 1n+_ : Nat}
448 {==}
449
450# The order is total: a <= b or b <= a.
451law le_total:
452 for a: Nat
453 for b: Nat
454 Or(le(a, b), le(b, a))
455
456def le_total(a, b):
457 match a b:
458 case 0n 0n:
459 Inl{{==}}
460 case 0n 1n+q:
461 Inl{{==}}
462 case 1n+p 0n:
463 Inr{{==}}
464 case 1n+p 1n+q:
465 le_total(p, q)
466
467# The order is total, as a reusable sum: a <= b or b <= a.
468law le_total_d:
469 for a: Nat
470 for b: Nat
471 Either<&2, &2, le(a, b), le(b, a)>
472
473def le_total_d(a, b):
474 match a b:
475 case 0n 0n:
476 Inl{{==}}
477 case 0n 1n+q:
478 Inl{{==}}
479 case 1n+p 0n:
480 Inr{{==}}
481 case 1n+p 1n+q:
482 le_total_d(p, q)
483
484# No natural is less than itself.
485law lt_irrefl:
486 for a: Nat
487 lt(a, a) -> Empty
488
489def lt_irrefl(a):
490 match a:
491 case 0n:
492 h => internal_false_ne_true(h)
493 case 1n+p:
494 lt_irrefl(p)
495
496# The strict order is transitive: a < b and b < c imply a < c.
497law lt_trans:
498 for a: Nat
499 for b: Nat
500 for c: Nat
501 for ab: lt(a, b)
502 for bc: lt(b, c)
503 lt(a, c)
504
505def lt_trans(a, b, c, ab, bc):
506 match a b c:
507 case 0n 0n _:
508 Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
509 case 0n 1n+q 0n:
510 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
511 case 0n 1n+q 1n+r:
512 {==}
513 case 1n+p 0n _:
514 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
515 case 1n+p 1n+q 0n:
516 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
517 case 1n+p 1n+q 1n+r:
518 lt_trans(p, q, r, ab, bc)
519
520# A strict inequality implies the weak one: a < b implies a <= b.
521law le_of_lt:
522 for a: Nat
523 for b: Nat
524 for h: lt(a, b)
525 le(a, b)
526
527def le_of_lt(a, b, h):
528 match a b:
529 case 0n 0n:
530 {==}
531 case 0n 1n+q:
532 {==}
533 case 1n+p 0n:
534 Empty.absurd(le(1n+p, 0n), internal_false_ne_true(h))
535 case 1n+p 1n+q:
536 le_of_lt(p, q, h)
537
538# Flipping a >= b gives b <= a.
539law le_of_ge:
540 for a: Nat
541 for b: Nat
542 for h: ge(a, b)
543 le(b, a)
544
545def le_of_ge(a, b, h):
546 match a b:
547 case 0n 0n:
548 {==}
549 case 0n 1n+q:
550 Empty.absurd(le(1n+q, 0n), internal_false_ne_true(h))
551 case 1n+p 0n:
552 {==}
553 case 1n+p 1n+q:
554 le_of_ge(p, q, h)
555
556# Flipping b <= a gives a >= b.
557law ge_of_le:
558 for a: Nat
559 for b: Nat
560 for h: le(b, a)
561 ge(a, b)
562
563def ge_of_le(a, b, h):
564 match a b:
565 case 0n 0n:
566 {==}
567 case 0n 1n+q:
568 Empty.absurd(ge(0n, 1n+q), internal_false_ne_true(h))
569 case 1n+p 0n:
570 {==}
571 case 1n+p 1n+q:
572 ge_of_le(p, q, h)
573
574# Flipping a > b gives b < a.
575law lt_of_gt:
576 for a: Nat
577 for b: Nat
578 for h: gt(a, b)
579 lt(b, a)
580
581def lt_of_gt(a, b, h):
582 match a b:
583 case 0n 0n:
584 Empty.absurd(lt(0n, 0n), internal_false_ne_true(h))
585 case 0n 1n+q:
586 Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(h))
587 case 1n+p 0n:
588 {==}
589 case 1n+p 1n+q:
590 lt_of_gt(p, q, h)
591
592# Flipping b < a gives a > b.
593law gt_of_lt:
594 for a: Nat
595 for b: Nat
596 for h: lt(b, a)
597 gt(a, b)
598
599def gt_of_lt(a, b, h):
600 match a b:
601 case 0n 0n:
602 Empty.absurd(gt(0n, 0n), internal_false_ne_true(h))
603 case 0n 1n+q:
604 Empty.absurd(gt(0n, 1n+q), internal_false_ne_true(h))
605 case 1n+p 0n:
606 {==}
607 case 1n+p 1n+q:
608 gt_of_lt(p, q, h)
609
610# Subtracting zero changes nothing: n - 0 = n.
611law sub_zero:
612 for n: Nat
613 {Nat.sub(n, 0n) == n : Nat}
614
615def sub_zero(n):
616 match n:
617 case 0n:
618 {==}
619 case 1n+p:
620 {==}
621
622# Truncated subtraction from zero is zero: 0 - n = 0.
623law zero_sub:
624 for n: Nat
625 {Nat.sub(0n, n) == 0n : Nat}
626
627def zero_sub(n):
628 match n:
629 case 0n:
630 {==}
631 case 1n+p:
632 {==}
633
634# A natural minus itself is zero: n - n = 0.
635law sub_self:
636 for n: Nat
637 {Nat.sub(n, n) == 0n : Nat}
638
639def sub_self(n):
640 match n:
641 case 0n:
642 {==}
643 case 1n+p:
644 sub_self(p)
645
646# Subtracting successors: (n + 1) - (m + 1) = n - m.
647law succ_sub_succ:
648 for -n: Nat
649 for -m: Nat
650 {Nat.sub(1n+n, 1n+m) == Nat.sub(n, m) : Nat}
651
652def succ_sub_succ(n, m):
653 {==}
654
655# Adding then subtracting m cancels: (n + m) - m = n.
656law add_sub_cancel:
657 for n: Nat
658 for m: Nat
659 {Nat.sub(Nat.add(n, m), m) == n : Nat}
660
661def add_sub_cancel(n, m):
662 match m:
663 case 0n:
664 +n = n
665 %Equal.sym(Nat, Nat.add(n, 0n), n, add_zero(n)) : {Nat.sub(_, 0n) == n : Nat}
666 sub_zero(n)
667 case 1n++q:
668 +n = n
669 %Equal.sym(Nat, Nat.add(n, 1n+q), 1n+Nat.add(n, q), add_succ(n, q)) : {Nat.sub(_, 1n+q) == n : Nat}
670 add_sub_cancel(n, q)
671
672# Adding then subtracting n cancels: (n + m) - n = m.
673law add_sub_cancel_left:
674 for n: Nat
675 for m: Nat
676 {Nat.sub(Nat.add(n, m), n) == m : Nat}
677
678def add_sub_cancel_left(n, m):
679 match n:
680 case 0n:
681 sub_zero(m)
682 case 1n+p:
683 add_sub_cancel_left(p, m)
684
685# If m <= n, subtracting and adding m back gives n: (n - m) + m = n.
686law sub_add_cancel:
687 for n: Nat
688 for m: Nat
689 for h: le(m, n)
690 {Nat.add(Nat.sub(n, m), m) == n : Nat}
691
692def sub_add_cancel(n, m, h):
693 match n m:
694 case 0n 0n:
695 {==}
696 case 0n 1n+q:
697 Empty.absurd({1n+q == 0n : Nat}, internal_false_ne_true(h))
698 case 1n++p 0n:
699 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
700 {==}
701 case 1n++p 1n++q:
702 %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}
703 %Equal.sym(Nat, Nat.add(Nat.sub(p, q), q), p, sub_add_cancel(p, q, h)) : {1n+_ == 1n+p : Nat}
704 {==}
705
706# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k).
707law sub_sub:
708 for n: Nat
709 for m: Nat
710 for k: Nat
711 {Nat.sub(Nat.sub(n, m), k) == Nat.sub(n, Nat.add(m, k)) : Nat}
712
713def sub_sub(n, m, k):
714 match n m:
715 case 0n 0n:
716 {==}
717 case 0n 1n+q:
718 zero_sub(k)
719 case 1n+p 0n:
720 {==}
721 case 1n+p 1n+q:
722 sub_sub(p, q, k)
723
724# Truncated subtraction never increases: n - m <= n.
725law sub_le:
726 for n: Nat
727 for m: Nat
728 le(Nat.sub(n, m), n)
729
730def sub_le(n, m):
731 match n m:
732 case 0n 0n:
733 {==}
734 case 0n 1n+q:
735 {==}
736 case 1n+p 0n:
737 le_refl(1n+p)
738 case 1n++p 1n++q:
739 le_trans(Nat.sub(p, q), p, 1n+p, sub_le(p, q), le_succ(p))
740
741def internal_div_true_ne_false(h: {True{} == False{} : Bool}) -> Empty:
742 internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h))
743
744def internal_div_add_zero_r(a: Nat) -> {a == Nat.add(a, 0n) : Nat}:
745 Equal.sym(Nat, Nat.add(a, 0n), a, add_zero(a))
746
747def internal_div_le_refl(a: Nat) -> {True{} == Nat.is_le(a, a) : Bool}:
748 Equal.sym(Bool, Nat.is_le(a, a), True{}, le_refl(a))
749
750def internal_div_zero_le(x: Nat) -> {True{} == Nat.is_le(0n, x) : Bool}:
751 Equal.sym(Bool, Nat.is_le(0n, x), True{}, zero_le(x))
752
753def internal_div_block_start(-bp: Nat, +r: Nat, h: {bp == Nat.add(r, 0n) : Nat}) -> {bp == r : Nat}:
754 %add_zero(r) : {bp == _ : Nat}
755 h
756
757def 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}:
758 %add_succ(r, mp) : {bp == _ : Nat}
759 h
760
761def 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}:
762 match n m:
763 case 0n _:
764 {==}
765 case 1n++np 0n:
766 %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}
767 %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}
768 %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}
769 %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}
770 internal_div_go_eq(np, r, bp, 1n+d, 0n, internal_div_block_start(bp, r, h))
771 case 1n++np 1n++mp:
772 %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}
773 %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}
774 internal_div_go_eq(np, mp, bp, d, 1n+r, internal_div_block_step(bp, r, mp, h))
775
776# The division equation, for a positive divisor 1 + b: (a / (1 + b)) * (1 + b) + a % (1 + b) = a.
777law div_mod_eq:
778 for +a: Nat
779 for +b: Nat
780 {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == a : Nat}
781
782def div_mod_eq(a, b):
783 %add_zero(a) : {Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) == _ : Nat}
784 internal_div_go_eq(a, b, b, 0n, 0n, {==})
785
786def 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}:
787 match w:
788 case (k, e):
789 (k, Equal.cong(Nat, Nat, x => 1n+x, Nat.add(ap, k), bq, e))
790
791def internal_div_le_wit(a: Nat, b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> &k:Nat -> {Nat.add(a, k) == b : Nat}:
792 match a b:
793 case 0n y:
794 (y, {==})
795 case 1n+ap 0n:
796 Empty.absurd(&k:Nat -> {Nat.add(1n+ap, k) == 0n : Nat}, internal_false_ne_true(h))
797 case 1n++ap 1n++bq:
798 internal_div_wit_succ(ap, bq, internal_div_le_wit(ap, bq, h))
799
800def 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}:
801 match n:
802 case 0n:
803 {==}
804 case 1n+np:
805 internal_div_go_small(np, k, d, 1n+r)
806
807def 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}:
808 match w:
809 case (+k, e):
810 %e : {Nat.div(a, 1n+_) == 0n : Nat}
811 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))
812
813# A number at most b divides by 1 + b to zero: a <= b implies a / (1 + b) = 0.
814law div_eq_zero_of_le:
815 for +a: Nat
816 for +b: Nat
817 for h: le(a, b)
818 {Nat.div(a, 1n+b) == 0n : Nat}
819
820def div_eq_zero_of_le(a, b, h):
821 internal_div_zero_of_wit(a, b, internal_div_le_wit(a, b, h))
822
823def 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}:
824 match j d:
825 case 0n _:
826 {==}
827 case 1n+i 0n:
828 Empty.absurd({True{} == Nat.is_le(1n+i, 1n) : Bool}, internal_div_true_ne_false(h))
829 case 1n+i 1n+e:
830 internal_div_le_succ_r(i, e, h)
831
832def 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}:
833 match n m:
834 case 0n _:
835 h
836 case 1n+np 0n:
837 internal_div_go_d_ge(j, np, r, 1n+d, 0n, internal_div_le_succ_r(j, d, h))
838 case 1n+np 1n+mp:
839 internal_div_go_d_ge(j, np, mp, d, 1n+r, h)
840
841def 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}:
842 match a m:
843 case 0n _:
844 internal_div_go_d_ge(d, k, m, d, r, internal_div_le_refl(d))
845 case 1n+ap 0n:
846 internal_div_mono_go(ap, r, 1n+d, 0n, k)
847 case 1n+ap 1n+mp:
848 internal_div_mono_go(ap, mp, d, 1n+r, k)
849
850def 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)):
851 match w:
852 case (+k, e):
853 %e : le(Nat.div(a, 1n+b), Nat.div(_, 1n+b))
854 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))
855
856# Division by a positive divisor is monotone: a <= c implies a / (1 + b) <= c / (1 + b).
857law div_le_div:
858 for +a: Nat
859 for +c: Nat
860 for b: Nat
861 for h: le(a, c)
862 le(Nat.div(a, 1n+b), Nat.div(c, 1n+b))
863
864def div_le_div(a, c, b, h):
865 internal_div_mono_wit(a, c, b, internal_div_le_wit(a, c, h))
866
867def 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}:
868 match n m:
869 case 0n _:
870 {==}
871 case 1n+np 0n:
872 internal_div_go_shift(np, r, 1n+d, 0n)
873 case 1n+np 1n+mp:
874 internal_div_go_shift(np, mp, d, 1n+r)
875
876def 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}:
877 match m:
878 case 0n:
879 {==}
880 case 1n++mp:
881 %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}
882 internal_div_go_run(mp, a, d, 1n+r)
883
884# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b).
885law add_div_left:
886 for +a: Nat
887 for +b: Nat
888 {Nat.div(Nat.add(1n+b, a), 1n+b) == 1n+Nat.div(a, 1n+b) : Nat}
889
890def add_div_left(a, b):
891 %internal_div_go_run(b, a, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n+Nat.div(a, 1n+b) : Nat}
892 %internal_div_add_zero_r(b) : {Pair.fst(Nat, Nat, Nat.divmod.go(a, _, 1n, 0n)) == 1n+Nat.div(a, 1n+b) : Nat}
893 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))
894
895def 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}:
896 match t:
897 case 0n:
898 {==}
899 case 1n+tp:
900 internal_div_le_add_cancel(tp, x, y)
901
902def internal_div_gt_add(a: Nat, +y: Nat) -> {False{} == Nat.is_le(1n+Nat.add(a, y), a) : Bool}:
903 match a:
904 case 0n:
905 {==}
906 case 1n+ap:
907 internal_div_gt_add(ap, y)
908
909def 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}:
910 match a bp:
911 case 0n q:
912 Equal.sym(Bool, True{}, Nat.is_le(0n, q), internal_div_zero_le(q))
913 case 1n+ap 0n:
914 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))))))
915 case 1n+ap 1n+q:
916 internal_div_not_succ_le(ap, q, h)
917
918def 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}:
919 match w:
920 case (+k, e):
921 %e : {Nat.is_le(1n+np, Nat.div(_, 1n+bp)) == Nat.is_le(1n+Nat.add(bp, Nat.mul(np, 1n+bp)), _) : Bool}
922 %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}
923 %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}
924 ih(k)
925
926def 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}:
927 match w:
928 case (+k, e):
929 %e : {Nat.is_le(1n+np, Nat.div(a, 1n+_)) == Nat.is_le(1n+Nat.add(_, Nat.mul(np, 1n+_)), a) : Bool}
930 %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}
931 %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}
932 internal_div_gt_add(a, Nat.add(k, Nat.mul(np, 1n+Nat.add(a, k))))
933
934def 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}:
935 match b:
936 case True{}:
937 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)
938 case False{}:
939 internal_div_le_small(np, a, bp, internal_div_le_wit(a, bp, internal_div_not_succ_le(a, bp, eb)))
940
941# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a.
942law le_div_iff_mul_le:
943 for n: Nat
944 for +a: Nat
945 for +b: Nat
946 {Nat.is_le(n, Nat.div(a, 1n+b)) == Nat.is_le(Nat.mul(n, 1n+b), a) : Bool}
947
948def le_div_iff_mul_le(n, a, b):
949 match n:
950 case 0n:
951 %internal_div_zero_le(Nat.div(a, 1n+b)) : {_ == Nat.is_le(0n, a) : Bool}
952 %internal_div_zero_le(a) : {True{} == _ : Bool}
953 {==}
954 case 1n++np:
955 internal_div_le_step(np, a, b, Nat.is_le(1n+b, a), {==}, x => le_div_iff_mul_le(np, x, b))
956
957# Minimum is commutative.
958law min_comm:
959 for a: Nat
960 for b: Nat
961 {Nat.min(a, b) == Nat.min(b, a) : Nat}
962
963def min_comm(a, b):
964 match a b:
965 case 0n 0n:
966 {==}
967 case 0n 1n+q:
968 {==}
969 case 1n+p 0n:
970 {==}
971 case 1n++p 1n++q:
972 %min_comm(p, q) : {1n+Nat.min(p, q) == 1n+_ : Nat}
973 {==}
974
975# Maximum is commutative.
976law max_comm:
977 for a: Nat
978 for b: Nat
979 {Nat.max(a, b) == Nat.max(b, a) : Nat}
980
981def max_comm(a, b):
982 match a b:
983 case 0n 0n:
984 {==}
985 case 0n 1n+q:
986 {==}
987 case 1n+p 0n:
988 {==}
989 case 1n++p 1n++q:
990 %max_comm(p, q) : {1n+Nat.max(p, q) == 1n+_ : Nat}
991 {==}
992
993# The minimum of a natural and itself is itself.
994law min_self:
995 for a: Nat
996 {Nat.min(a, a) == a : Nat}
997
998def min_self(a):
999 match a:
1000 case 0n:
1001 {==}
1002 case 1n++p:
1003 %min_self(p) : {1n+Nat.min(p, p) == 1n+_ : Nat}
1004 {==}
1005
1006# The maximum of a natural and itself is itself.
1007law max_self:
1008 for a: Nat
1009 {Nat.max(a, a) == a : Nat}
1010
1011def max_self(a):
1012 match a:
1013 case 0n:
1014 {==}
1015 case 1n++p:
1016 %max_self(p) : {1n+Nat.max(p, p) == 1n+_ : Nat}
1017 {==}
1018
1019# The minimum with zero is zero: min(a, 0) = 0.
1020law min_zero:
1021 for a: Nat
1022 {Nat.min(a, 0n) == 0n : Nat}
1023
1024def min_zero(a):
1025 match a:
1026 case 0n:
1027 {==}
1028 case 1n+p:
1029 {==}
1030
1031# The minimum with zero is zero: min(0, a) = 0.
1032law zero_min:
1033 for a: Nat
1034 {Nat.min(0n, a) == 0n : Nat}
1035
1036def zero_min(a):
1037 match a:
1038 case 0n:
1039 {==}
1040 case 1n+p:
1041 {==}
1042
1043# Zero is an identity for maximum: max(a, 0) = a.
1044law max_zero:
1045 for a: Nat
1046 {Nat.max(a, 0n) == a : Nat}
1047
1048def max_zero(a):
1049 match a:
1050 case 0n:
1051 {==}
1052 case 1n+p:
1053 {==}
1054
1055# Zero is an identity for maximum: max(0, a) = a.
1056law zero_max:
1057 for a: Nat
1058 {Nat.max(0n, a) == a : Nat}
1059
1060def zero_max(a):
1061 match a:
1062 case 0n:
1063 {==}
1064 case 1n+p:
1065 {==}
1066
1067# Minimum is associative.
1068law min_assoc:
1069 for a: Nat
1070 for b: Nat
1071 for c: Nat
1072 {Nat.min(Nat.min(a, b), c) == Nat.min(a, Nat.min(b, c)) : Nat}
1073
1074def min_assoc(a, b, c):
1075 match a b c:
1076 case 0n _ _:
1077 {==}
1078 case 1n+p 0n _:
1079 {==}
1080 case 1n+p 1n+q 0n:
1081 {==}
1082 case 1n++p 1n++q 1n++r:
1083 %min_assoc(p, q, r) : {1n+Nat.min(Nat.min(p, q), r) == 1n+_ : Nat}
1084 {==}
1085
1086# Maximum is associative.
1087law max_assoc:
1088 for a: Nat
1089 for b: Nat
1090 for c: Nat
1091 {Nat.max(Nat.max(a, b), c) == Nat.max(a, Nat.max(b, c)) : Nat}
1092
1093def max_assoc(a, b, c):
1094 match a b c:
1095 case 0n _ _:
1096 {==}
1097 case 1n+p 0n _:
1098 {==}
1099 case 1n+p 1n+q 0n:
1100 {==}
1101 case 1n++p 1n++q 1n++r:
1102 %max_assoc(p, q, r) : {1n+Nat.max(Nat.max(p, q), r) == 1n+_ : Nat}
1103 {==}
1104
1105# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b.
1106law min_add_max:
1107 for a: Nat
1108 for b: Nat
1109 {Nat.add(Nat.min(a, b), Nat.max(a, b)) == Nat.add(a, b) : Nat}
1110
1111def min_add_max(a, b):
1112 match a b:
1113 case 0n 0n:
1114 {==}
1115 case 0n 1n+q:
1116 {==}
1117 case 1n++p 0n:
1118 %add_zero(p) : {1n+_ == 1n+Nat.add(p, 0n) : Nat}
1119 {==}
1120 case 1n++p 1n++q:
1121 %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}
1122 %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}
1123 %min_add_max(p, q) : {2n+Nat.add(Nat.min(p, q), Nat.max(p, q)) == 2n+_ : Nat}
1124 {==}
1125
1126# The minimum is at most its left argument.
1127law min_le_left:
1128 for a: Nat
1129 for b: Nat
1130 le(Nat.min(a, b), a)
1131
1132def min_le_left(a, b):
1133 match a b:
1134 case 0n 0n:
1135 {==}
1136 case 0n 1n+q:
1137 {==}
1138 case 1n+p 0n:
1139 {==}
1140 case 1n+p 1n+q:
1141 min_le_left(p, q)
1142
1143# The minimum is at most its right argument.
1144law min_le_right:
1145 for a: Nat
1146 for b: Nat
1147 le(Nat.min(a, b), b)
1148
1149def min_le_right(a, b):
1150 match a b:
1151 case 0n 0n:
1152 {==}
1153 case 0n 1n+q:
1154 {==}
1155 case 1n+p 0n:
1156 {==}
1157 case 1n+p 1n+q:
1158 min_le_right(p, q)
1159
1160# The left argument is at most the maximum.
1161law le_max_left:
1162 for a: Nat
1163 for b: Nat
1164 le(a, Nat.max(a, b))
1165
1166def le_max_left(a, b):
1167 match a b:
1168 case 0n 0n:
1169 {==}
1170 case 0n 1n+q:
1171 {==}
1172 case 1n+p 0n:
1173 le_refl(1n+p)
1174 case 1n+p 1n+q:
1175 le_max_left(p, q)
1176
1177# The right argument is at most the maximum.
1178law le_max_right:
1179 for a: Nat
1180 for b: Nat
1181 le(b, Nat.max(a, b))
1182
1183def le_max_right(a, b):
1184 match a b:
1185 case 0n 0n:
1186 {==}
1187 case 0n 1n+q:
1188 le_refl(1n+q)
1189 case 1n+p 0n:
1190 {==}
1191 case 1n+p 1n+q:
1192 le_max_right(p, q)
1193
1194# Any natural to the power zero is one.
1195law pow_zero:
1196 for -a: Nat
1197 {Nat.pow(a, 0n) == 1n : Nat}
1198
1199def pow_zero(a):
1200 {==}
1201
1202# A power with a successor exponent: a^(n+1) = a * a^n.
1203law pow_succ:
1204 for -a: Nat
1205 for -n: Nat
1206 {Nat.pow(a, 1n+n) == Nat.mul(a, Nat.pow(a, n)) : Nat}
1207
1208def pow_succ(a, n):
1209 {==}
1210
1211# Any natural to the power one is itself.
1212law pow_one:
1213 for a: Nat
1214 {Nat.pow(a, 1n) == a : Nat}
1215
1216def pow_one(a):
1217 mul_one(a)
1218
1219# One to any power is one.
1220law one_pow:
1221 for n: Nat
1222 {Nat.pow(1n, n) == 1n : Nat}
1223
1224def one_pow(n):
1225 match n:
1226 case 0n:
1227 {==}
1228 case 1n++p:
1229 %Equal.sym(Nat, Nat.mul(1n, Nat.pow(1n, p)), Nat.pow(1n, p), one_mul(Nat.pow(1n, p))) : {_ == 1n : Nat}
1230 one_pow(p)
1231
1232# Exponents add under multiplication: a^(m+n) = a^m * a^n.
1233law pow_add:
1234 for a: Nat
1235 for m: Nat
1236 for n: Nat
1237 {Nat.pow(a, Nat.add(m, n)) == Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) : Nat}
1238
1239def pow_add(a, m, n):
1240 match m:
1241 case 0n:
1242 +a = a
1243 +n = n
1244 %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}
1245 {==}
1246 case 1n++p:
1247 +a = a
1248 +n = n
1249 %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}
1250 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)))
1251
1252# Doubling is adding a natural to itself.
1253law double_eq_add:
1254 for n: Nat
1255 {Nat.double(n) == Nat.add(n, n) : Nat}
1256
1257def double_eq_add(n):
1258 match n:
1259 case 0n:
1260 {==}
1261 case 1n++p:
1262 %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
1263 %double_eq_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
1264 {==}
1265
1266# Every natural tests equal to itself.
1267law is_eq_refl:
1268 for n: Nat
1269 {Nat.is_eq(n, n) == True{} : Bool}
1270
1271def is_eq_refl(n):
1272 match n:
1273 case 0n:
1274 {==}
1275 case 1n+p:
1276 is_eq_refl(p)
1277
1278# The equality test is symmetric.
1279law is_eq_comm:
1280 for a: Nat
1281 for b: Nat
1282 {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1283
1284def is_eq_comm(a, b):
1285 match a b:
1286 case 0n 0n:
1287 {==}
1288 case 0n 1n+q:
1289 {==}
1290 case 1n+p 0n:
1291 {==}
1292 case 1n++p 1n++q:
1293 %is_eq_comm(p, q) : {Nat.is_eq(p, q) == _ : Bool}
1294 {==}
1295
1296# If the equality test says true, the naturals are equal.
1297law eq_of_is_eq:
1298 for a: Nat
1299 for b: Nat
1300 for h: {Nat.is_eq(a, b) == True{} : Bool}
1301 {a == b : Nat}
1302
1303def eq_of_is_eq(a, b, h):
1304 match a b:
1305 case 0n 0n:
1306 {==}
1307 case 0n 1n+q:
1308 Empty.absurd({0n == 1n+q : Nat}, internal_false_ne_true(h))
1309 case 1n+p 0n:
1310 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1311 case 1n++p 1n++q:
1312 %eq_of_is_eq(p, q, h) : {1n+p == 1n+_ : Nat}
1313 {==}
1314
1315# A >= b tests the same as b <= a.
1316law is_ge_eq_is_le:
1317 for a: Nat
1318 for b: Nat
1319 {Nat.is_ge(a, b) == Nat.is_le(b, a) : Bool}
1320
1321def is_ge_eq_is_le(a, b):
1322 match a b:
1323 case 0n 0n:
1324 {==}
1325 case 0n 1n+q:
1326 {==}
1327 case 1n+p 0n:
1328 {==}
1329 case 1n++p 1n++q:
1330 %is_ge_eq_is_le(p, q) : {Nat.is_ge(p, q) == _ : Bool}
1331 {==}
1332
1333# A > b tests the same as b < a.
1334law is_gt_eq_is_lt:
1335 for a: Nat
1336 for b: Nat
1337 {Nat.is_gt(a, b) == Nat.is_lt(b, a) : Bool}
1338
1339def is_gt_eq_is_lt(a, b):
1340 match a b:
1341 case 0n 0n:
1342 {==}
1343 case 0n 1n+q:
1344 {==}
1345 case 1n+p 0n:
1346 {==}
1347 case 1n++p 1n++q:
1348 %is_gt_eq_is_lt(p, q) : {Nat.is_gt(p, q) == _ : Bool}
1349 {==}
1350
1351# A < b tests the same as a + 1 <= b.
1352law is_lt_eq_succ_le:
1353 for a: Nat
1354 for b: Nat
1355 {Nat.is_lt(a, b) == Nat.is_le(1n+a, b) : Bool}
1356
1357def is_lt_eq_succ_le(a, b):
1358 match a b:
1359 case 0n 0n:
1360 {==}
1361 case 0n 1n+q:
1362 match q:
1363 case 0n:
1364 {==}
1365 case 1n+r:
1366 {==}
1367 case 1n+p 0n:
1368 {==}
1369 case 1n+p 1n+q:
1370 is_lt_eq_succ_le(p, q)
1371
1372# Not (a <= b) tests the same as b < a.
1373law not_is_le:
1374 for a: Nat
1375 for b: Nat
1376 {Bool.not(Nat.is_le(a, b)) == Nat.is_lt(b, a) : Bool}
1377
1378def not_is_le(a, b):
1379 match a b:
1380 case 0n 0n:
1381 {==}
1382 case 0n 1n+q:
1383 {==}
1384 case 1n+p 0n:
1385 {==}
1386 case 1n+p 1n+q:
1387 not_is_le(p, q)
1388
1389# Not (a < b) tests the same as b <= a.
1390law not_is_lt:
1391 for a: Nat
1392 for b: Nat
1393 {Bool.not(Nat.is_lt(a, b)) == Nat.is_le(b, a) : Bool}
1394
1395def not_is_lt(a, b):
1396 match a b:
1397 case 0n 0n:
1398 {==}
1399 case 0n 1n+q:
1400 {==}
1401 case 1n+p 0n:
1402 {==}
1403 case 1n+p 1n+q:
1404 not_is_lt(p, q)
1405
1406# Every natural is less than its successor: n < n + 1.
1407law lt_succ_self:
1408 for n: Nat
1409 lt(n, 1n+n)
1410
1411def lt_succ_self(n):
1412 match n:
1413 case 0n:
1414 {==}
1415 case 1n+p:
1416 lt_succ_self(p)
1417
1418# The successor preserves the order: a <= b implies a + 1 <= b + 1.
1419law succ_le_succ:
1420 for -a: Nat
1421 for -b: Nat
1422 for h: le(a, b)
1423 le(1n+a, 1n+b)
1424
1425def succ_le_succ(a, b, h):
1426 h
1427
1428# The order of successors is the order of the naturals: a + 1 <= b + 1 implies a <= b.
1429law le_of_succ_le_succ:
1430 for -a: Nat
1431 for -b: Nat
1432 for h: le(1n+a, 1n+b)
1433 le(a, b)
1434
1435def le_of_succ_le_succ(a, b, h):
1436 h
1437
1438# A < b and b <= c imply a < c.
1439law lt_of_lt_of_le:
1440 for a: Nat
1441 for b: Nat
1442 for c: Nat
1443 for ab: lt(a, b)
1444 for bc: le(b, c)
1445 lt(a, c)
1446
1447def lt_of_lt_of_le(a, b, c, ab, bc):
1448 match a b c:
1449 case 0n 0n _:
1450 Empty.absurd(lt(0n, c), internal_false_ne_true(ab))
1451 case 0n 1n+q 0n:
1452 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1453 case 0n 1n+q 1n+r:
1454 {==}
1455 case 1n+p 0n _:
1456 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1457 case 1n+p 1n+q 0n:
1458 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1459 case 1n+p 1n+q 1n+r:
1460 lt_of_lt_of_le(p, q, r, ab, bc)
1461
1462# A <= b and b < c imply a < c.
1463law lt_of_le_of_lt:
1464 for a: Nat
1465 for b: Nat
1466 for c: Nat
1467 for ab: le(a, b)
1468 for bc: lt(b, c)
1469 lt(a, c)
1470
1471def lt_of_le_of_lt(a, b, c, ab, bc):
1472 match a b c:
1473 case 0n 0n 0n:
1474 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1475 case 0n 1n+q 0n:
1476 Empty.absurd(lt(0n, 0n), internal_false_ne_true(bc))
1477 case 0n _ 1n+r:
1478 {==}
1479 case 1n+p 0n _:
1480 Empty.absurd(lt(1n+p, c), internal_false_ne_true(ab))
1481 case 1n+p 1n+q 0n:
1482 Empty.absurd(lt(1n+p, 0n), internal_false_ne_true(bc))
1483 case 1n+p 1n+q 1n+r:
1484 lt_of_le_of_lt(p, q, r, ab, bc)
1485
1486# Adding on the left preserves the order: a <= b implies k + a <= k + b.
1487law add_le_add_left:
1488 for -a: Nat
1489 for -b: Nat
1490 for k: Nat
1491 for h: le(a, b)
1492 le(Nat.add(k, a), Nat.add(k, b))
1493
1494def add_le_add_left(a, b, k, h):
1495 match k:
1496 case 0n:
1497 h
1498 case 1n+p:
1499 add_le_add_left(a, b, p, h)
1500
1501# Adding on the right preserves the order: a <= b implies a + k <= b + k.
1502law add_le_add_right:
1503 for +a: Nat
1504 for +b: Nat
1505 for +k: Nat
1506 for h: le(a, b)
1507 le(Nat.add(a, k), Nat.add(b, k))
1508
1509def add_le_add_right(a, b, k, h):
1510 %add_comm(k, a) : le(_, Nat.add(b, k))
1511 %add_comm(k, b) : le(Nat.add(k, a), _)
1512 add_le_add_left(a, b, k, h)
1513
1514# Adding the same amount on the left does not change the order test: a <= b tests as k + a <= k + b.
1515law add_le_add_iff_left:
1516 for k: Nat
1517 for -a: Nat
1518 for -b: Nat
1519 {Nat.is_le(a, b) == Nat.is_le(Nat.add(k, a), Nat.add(k, b)) : Bool}
1520
1521def add_le_add_iff_left(k, a, b):
1522 match k:
1523 case 0n:
1524 {==}
1525 case 1n+p:
1526 add_le_add_iff_left(p, a, b)
1527
1528# Adding two bounded summands stays bounded: a <= c and b <= d imply a + b <= c + d.
1529law add_le_add:
1530 for +a: Nat
1531 for +b: Nat
1532 for +c: Nat
1533 for +d: Nat
1534 for h1: le(a, c)
1535 for h2: le(b, d)
1536 le(Nat.add(a, b), Nat.add(c, d))
1537
1538def add_le_add(a, b, c, d, h1, h2):
1539 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))
1540
1541# A sum is at most c exactly when a <= c and b <= c - a: a + b <= c tests as both.
1542law le_and_le_sub_iff_add_le:
1543 for a: Nat
1544 for -b: Nat
1545 for c: Nat
1546 {Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) == Nat.is_le(Nat.add(a, b), c) : Bool}
1547
1548def le_and_le_sub_iff_add_le(a, b, c):
1549 match a c:
1550 case 0n 0n:
1551 {==}
1552 case 0n 1n+j:
1553 {==}
1554 case 1n+i 0n:
1555 {==}
1556 case 1n+i 1n+j:
1557 le_and_le_sub_iff_add_le(i, b, j)
1558
1559# The only natural at most zero is zero.
1560law le_zero_eq:
1561 for n: Nat
1562 for h: le(n, 0n)
1563 {n == 0n : Nat}
1564
1565def le_zero_eq(n, h):
1566 match n:
1567 case 0n:
1568 {==}
1569 case 1n+p:
1570 Empty.absurd({1n+p == 0n : Nat}, internal_false_ne_true(h))
1571
1572# No natural is less than zero.
1573law lt_zero:
1574 for n: Nat
1575 lt(n, 0n) -> Empty
1576
1577def lt_zero(n):
1578 match n:
1579 case 0n:
1580 h => internal_false_ne_true(h)
1581 case 1n+p:
1582 h => internal_false_ne_true(h)
1583
1584# A strict inequality rules out the reverse weak one: a < b implies b <= a is false.
1585law not_le_of_lt:
1586 for a: Nat
1587 for b: Nat
1588 for h: lt(a, b)
1589 {Nat.is_le(b, a) == False{} : Bool}
1590
1591def not_le_of_lt(a, b, h):
1592 match a b:
1593 case 0n 0n:
1594 Empty.absurd({Nat.is_le(0n, 0n) == False{} : Bool}, internal_false_ne_true(h))
1595 case 0n 1n+q:
1596 {==}
1597 case 1n+p 0n:
1598 Empty.absurd({Nat.is_le(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1599 case 1n+p 1n+q:
1600 not_le_of_lt(p, q, h)
1601
1602# A weak inequality rules out the reverse strict one: a <= b implies b < a is false.
1603law not_lt_of_le:
1604 for a: Nat
1605 for b: Nat
1606 for h: le(a, b)
1607 {Nat.is_lt(b, a) == False{} : Bool}
1608
1609def not_lt_of_le(a, b, h):
1610 match a b:
1611 case 0n 0n:
1612 {==}
1613 case 0n 1n+q:
1614 {==}
1615 case 1n+p 0n:
1616 Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, internal_false_ne_true(h))
1617 case 1n+p 1n+q:
1618 not_lt_of_le(p, q, h)
1619
1620# A failed weak test gives the reverse strict order: a <= b false implies b < a.
1621law lt_of_not_le:
1622 for a: Nat
1623 for b: Nat
1624 for h: {Nat.is_le(a, b) == False{} : Bool}
1625 lt(b, a)
1626
1627def lt_of_not_le(a, b, h):
1628 match a b:
1629 case 0n 0n:
1630 Empty.absurd(lt(0n, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1631 case 0n 1n+q:
1632 Empty.absurd(lt(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1633 case 1n+p 0n:
1634 {==}
1635 case 1n+p 1n+q:
1636 lt_of_not_le(p, q, h)
1637
1638# A failed strict test gives the reverse weak order: a < b false implies b <= a.
1639law le_of_not_lt:
1640 for a: Nat
1641 for b: Nat
1642 for h: {Nat.is_lt(a, b) == False{} : Bool}
1643 le(b, a)
1644
1645def le_of_not_lt(a, b, h):
1646 match a b:
1647 case 0n 0n:
1648 {==}
1649 case 0n 1n+q:
1650 Empty.absurd(le(1n+q, 0n), internal_false_ne_true(Equal.sym(Bool, True{}, False{}, h)))
1651 case 1n+p 0n:
1652 {==}
1653 case 1n+p 1n+q:
1654 le_of_not_lt(p, q, h)
1655
1656# A number below both bounds is below their minimum: a < b and a < c imply a < min b c.
1657law lt_min:
1658 for a: Nat
1659 for b: Nat
1660 for c: Nat
1661 for hb: lt(a, b)
1662 for hc: lt(a, c)
1663 lt(a, Nat.min(b, c))
1664
1665def lt_min(a, b, c, hb, hc):
1666 match a b c:
1667 case _ 0n _:
1668 Empty.absurd(lt(a, Nat.min(0n, c)), lt_zero(a)(hb))
1669 case _ 1n+q 0n:
1670 Empty.absurd(lt(a, Nat.min(1n+q, 0n)), lt_zero(a)(hc))
1671 case 0n 1n+q 1n+r:
1672 {==}
1673 case 1n+p 1n+q 1n+r:
1674 lt_min(p, q, r, hb, hc)
1675
1676def internal_or_true_sym(x: Bool) -> {True{} == Bool.or(x, True{}) : Bool}:
1677 match x:
1678 case False{}:
1679 {==}
1680 case True{}:
1681 {==}
1682
1683def internal_or_false_sym(x: Bool) -> {x == Bool.or(x, False{}) : Bool}:
1684 match x:
1685 case False{}:
1686 {==}
1687 case True{}:
1688 {==}
1689
1690# The minimum is at most c exactly when one argument is: min a b <= c tests as a <= c or b <= c.
1691law min_le_iff:
1692 for a: Nat
1693 for b: Nat
1694 for c: Nat
1695 {Nat.is_le(Nat.min(a, b), c) == Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
1696
1697def min_le_iff(a, b, c):
1698 match a b c:
1699 case 0n 0n 0n:
1700 {==}
1701 case 0n 0n 1n+r:
1702 {==}
1703 case 0n 1n+q 0n:
1704 {==}
1705 case 0n 1n+q 1n+r:
1706 {==}
1707 case 1n+p 0n 0n:
1708 {==}
1709 case 1n+p 0n 1n+r:
1710 internal_or_true_sym(Nat.is_le(p, r))
1711 case 1n+p 1n+q 0n:
1712 {==}
1713 case 1n+p 1n+q 1n+r:
1714 min_le_iff(p, q, r)
1715
1716# The maximum is above a exactly when one argument is: a < max b c tests as a < b or a < c.
1717law lt_max_iff:
1718 for a: Nat
1719 for b: Nat
1720 for c: Nat
1721 {Nat.is_lt(a, Nat.max(b, c)) == Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}
1722
1723def lt_max_iff(a, b, c):
1724 match a b c:
1725 case 0n 0n 0n:
1726 {==}
1727 case 0n 0n 1n+r:
1728 {==}
1729 case 0n 1n+q 0n:
1730 {==}
1731 case 0n 1n+q 1n+r:
1732 {==}
1733 case 1n+p 0n 0n:
1734 {==}
1735 case 1n+p 0n 1n+r:
1736 {==}
1737 case 1n+p 1n+q 0n:
1738 internal_or_false_sym(Nat.is_lt(p, q))
1739 case 1n+p 1n+q 1n+r:
1740 lt_max_iff(p, q, r)
1741
1742# Subtracting a larger number gives zero: a <= b implies a - b = 0.
1743law sub_eq_zero_of_le:
1744 for a: Nat
1745 for b: Nat
1746 for h: le(a, b)
1747 {Nat.sub(a, b) == 0n : Nat}
1748
1749def sub_eq_zero_of_le(a, b, h):
1750 match a b:
1751 case 0n 0n:
1752 {==}
1753 case 0n 1n+q:
1754 {==}
1755 case 1n+p 0n:
1756 Empty.absurd({Nat.sub(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
1757 case 1n+p 1n+q:
1758 sub_eq_zero_of_le(p, q, h)
1759
1760# Above the subtrahend, a successor subtracts to a successor: b <= a implies (a + 1) - b = (a - b) + 1.
1761law succ_sub:
1762 for a: Nat
1763 for b: Nat
1764 for h: le(b, a)
1765 {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}
1766
1767def succ_sub(a, b, h):
1768 match a b:
1769 case 0n 0n:
1770 {==}
1771 case 1n+p 0n:
1772 {==}
1773 case 0n 1n+q:
1774 Empty.absurd({Nat.sub(1n, 1n+q) == 1n+Nat.sub(0n, 1n+q) : Nat}, internal_false_ne_true(h))
1775 case 1n+p 1n+q:
1776 succ_sub(p, q, h)
1777
1778# Adding back what was subtracted restores the number: a <= b implies a + (b - a) = b.
1779law add_sub_of_le:
1780 for a: Nat
1781 for b: Nat
1782 for h: le(a, b)
1783 {Nat.add(a, Nat.sub(b, a)) == b : Nat}
1784
1785def add_sub_of_le(a, b, h):
1786 match a b:
1787 case 0n 0n:
1788 {==}
1789 case 0n 1n+q:
1790 {==}
1791 case 1n+p 0n:
1792 Empty.absurd({Nat.add(1n+p, Nat.sub(0n, 1n+p)) == 0n : Nat}, internal_false_ne_true(h))
1793 case 1n++p 1n++q:
1794 %Equal.sym(Nat, Nat.add(p, Nat.sub(q, p)), q, add_sub_of_le(p, q, h)) : {1n+_ == 1n+q : Nat}
1795 {==}
1796
1797def 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}:
1798 match a:
1799 case 0n:
1800 {==}
1801 case 1n+x:
1802 {==}
1803
1804# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c.
1805law lt_sub_iff_add_lt:
1806 for a: Nat
1807 for b: Nat
1808 for c: Nat
1809 {Nat.is_lt(a, Nat.sub(c, b)) == Nat.is_lt(Nat.add(b, a), c) : Bool}
1810
1811def lt_sub_iff_add_lt(a, b, c):
1812 match b c:
1813 case 0n 0n:
1814 {==}
1815 case 0n 1n+r:
1816 {==}
1817 case 1n+p 0n:
1818 internal_lt_sub_zero(a, p)
1819 case 1n+p 1n+r:
1820 lt_sub_iff_add_lt(a, p, r)
1821
1822# A witnessed difference gives the order: a + k = b implies a <= b.
1823law le_of_add_eq:
1824 for a: Nat
1825 for k: Nat
1826 for -b: Nat
1827 for e: {Nat.add(a, k) == b : Nat}
1828 le(a, b)
1829
1830def le_of_add_eq(a, k, b, e):
1831 %e : {Nat.is_le(a, _) == True{} : Bool}
1832 le_add_right(a, k)
1833
1834# Multiplying on the right preserves the order: a <= b implies a * k <= b * k.
1835law mul_le_mul_right:
1836 for +a: Nat
1837 for +b: Nat
1838 for +k: Nat
1839 for h: le(a, b)
1840 le(Nat.mul(a, k), Nat.mul(b, k))
1841
1842def mul_le_mul_right(a, b, k, h):
1843 %sub_add_cancel(b, a, h) : {Nat.is_le(Nat.mul(a, k), Nat.mul(_, k)) == True{} : Bool}
1844 %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}
1845 %add_comm(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k)) : {Nat.is_le(Nat.mul(a, k), _) == True{} : Bool}
1846 le_add_right(Nat.mul(a, k), Nat.mul(Nat.sub(b, a), k))
1847
1848# Zero divided by anything is zero: 0 / b = 0.
1849law zero_div:
1850 for b: Nat
1851 {Nat.div(0n, b) == 0n : Nat}
1852
1853def zero_div(b):
1854 match b:
1855 case 0n:
1856 {==}
1857 case 1n+p:
1858 {==}
1859
1860# Zero modulo anything is zero: 0 % b = 0.
1861law zero_mod:
1862 for b: Nat
1863 {Nat.mod(0n, b) == 0n : Nat}
1864
1865def zero_mod(b):
1866 match b:
1867 case 0n:
1868 {==}
1869 case 1n+p:
1870 {==}
1871
1872def internal_div_go_one(a: Nat, +d: Nat) -> {(Nat.add(a, d), 0n) == Nat.divmod.go(a, 0n, d, 0n) : Nat & Nat}:
1873 match a:
1874 case 0n:
1875 {==}
1876 case 1n++p:
1877 %add_succ(p, d) : {(_, 0n) == Nat.divmod.go(p, 0n, 1n+d, 0n) : Nat & Nat}
1878 internal_div_go_one(p, 1n+d)
1879
1880# Dividing by one changes nothing: a / 1 = a.
1881law div_one:
1882 for a: Nat
1883 {Nat.div(a, 1n) == a : Nat}
1884
1885def div_one(a):
1886 +a = a
1887 %internal_div_go_one(a, 0n) : {Pair.fst(Nat, Nat, _) == a : Nat}
1888 add_zero(a)
1889
1890# Any natural modulo one is zero: a % 1 = 0.
1891law mod_one:
1892 for a: Nat
1893 {Nat.mod(a, 1n) == 0n : Nat}
1894
1895def mod_one(a):
1896 +a = a
1897 %internal_div_go_one(a, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1898 {==}
1899
1900def internal_div_go_self(m: Nat, -d: Nat, -r: Nat) -> {(1n+d, 0n) == Nat.divmod.go(1n+m, m, d, r) : Nat & Nat}:
1901 match m:
1902 case 0n:
1903 {==}
1904 case 1n+p:
1905 internal_div_go_self(p, d, 1n+r)
1906
1907# A natural modulo itself is zero: n % n = 0.
1908law mod_self:
1909 for n: Nat
1910 {Nat.mod(n, n) == 0n : Nat}
1911
1912def mod_self(n):
1913 match n:
1914 case 0n:
1915 {==}
1916 case 1n++p:
1917 %internal_div_go_self(p, 0n, 0n) : {Pair.snd(Nat, Nat, _) == 0n : Nat}
1918 {==}
1919
1920# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1.
1921law div_self:
1922 for b: Nat
1923 {Nat.div(1n+b, 1n+b) == 1n : Nat}
1924
1925def div_self(b):
1926 +b = b
1927 %internal_div_go_self(b, 0n, 0n) : {Pair.fst(Nat, Nat, _) == 1n : Nat}
1928 {==}
1929
1930def 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)):
1931 match n m:
1932 case 0n k:
1933 le_add_right(r, k)
1934 case 1n++np 0n:
1935 %internal_div_add_zero_r(r) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), _)
1936 internal_mod_go_le(np, r, 1n+d, 0n)
1937 case 1n++np 1n++mp:
1938 %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)), _)
1939 internal_mod_go_le(np, mp, d, 1n+r)
1940
1941# A remainder is below its positive divisor: a % (1 + b) < 1 + b.
1942law mod_lt:
1943 for a: Nat
1944 for b: Nat
1945 lt(Nat.mod(a, 1n+b), 1n+b)
1946
1947def mod_lt(a, b):
1948 +a = a
1949 +b = b
1950 %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}
1951 internal_mod_go_le(a, b, 0n, 0n)
1952
1953# A remainder never exceeds the dividend: a % b <= a.
1954law mod_le:
1955 for a: Nat
1956 for b: Nat
1957 le(Nat.mod(a, b), a)
1958
1959def mod_le(a, b):
1960 match b:
1961 case 0n:
1962 le_refl(a)
1963 case 1n++bp:
1964 +a = a
1965 +bp = bp
1966 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)))
1967
1968def 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}:
1969 %e : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == _ : Nat}
1970 %mul_comm(1n+bp, q) : {Nat.add(q, Nat.add(Nat.mul(bp, q), m)) == Nat.add(_, m) : Nat}
1971 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))
1972
1973# A quotient never exceeds the dividend: a / b <= a.
1974law div_le_self:
1975 for a: Nat
1976 for b: Nat
1977 le(Nat.div(a, b), a)
1978
1979def div_le_self(a, b):
1980 match b:
1981 case 0n:
1982 zero_le(a)
1983 case 1n++bp:
1984 +a = a
1985 +bp = bp
1986 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)))
1987
1988def 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}:
1989 match n:
1990 case 0n:
1991 {==}
1992 case 1n++np:
1993 %add_succ(np, r) : {Pair.snd(Nat, Nat, Nat.divmod.go(np, Nat.add(np, k), d, 1n+r)) == _ : Nat}
1994 internal_mod_go_small(np, k, d, 1n+r)
1995
1996def 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}:
1997 match w:
1998 case (+k, e):
1999 %e : {Nat.mod(a, 1n+_) == a : Nat}
2000 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))
2001
2002# A number below the divisor is its own remainder: a < b implies a % b = a.
2003law mod_eq_of_lt:
2004 for a: Nat
2005 for b: Nat
2006 for h: lt(a, b)
2007 {Nat.mod(a, b) == a : Nat}
2008
2009def mod_eq_of_lt(a, b, h):
2010 match b:
2011 case 0n:
2012 +a = a
2013 Empty.absurd({Nat.mod(a, 0n) == a : Nat}, lt_zero(a)(h))
2014 case 1n++bp:
2015 +a = a
2016 +bp = bp
2017 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)))
2018
2019# Taking a remainder twice is taking it once: (a % n) % n = a % n.
2020law mod_mod:
2021 for a: Nat
2022 for n: Nat
2023 {Nat.mod(Nat.mod(a, n), n) == Nat.mod(a, n) : Nat}
2024
2025def mod_mod(a, n):
2026 match n:
2027 case 0n:
2028 {==}
2029 case 1n++b:
2030 +a = a
2031 +b = b
2032 mod_eq_of_lt(Nat.mod(a, 1n+b), 1n+b, mod_lt(a, b))
2033
2034def 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}:
2035 match n m:
2036 case 0n _:
2037 {==}
2038 case 1n+np 0n:
2039 internal_mod_go_d(np, r, 1n+d, 1n+e, 0n)
2040 case 1n+np 1n+mp:
2041 internal_mod_go_d(np, mp, d, e, 1n+r)
2042
2043# Adding the divisor does not change the remainder: (b + a) % b = a % b.
2044law add_mod_left:
2045 for a: Nat
2046 for b: Nat
2047 {Nat.mod(Nat.add(b, a), b) == Nat.mod(a, b) : Nat}
2048
2049def add_mod_left(a, b):
2050 match b:
2051 case 0n:
2052 {==}
2053 case 1n++bp:
2054 +a = a
2055 %internal_div_go_run(bp, a, 0n, 0n) : {Pair.snd(Nat, Nat, _) == Nat.mod(a, 1n+bp) : Nat}
2056 %internal_div_add_zero_r(bp) : {Pair.snd(Nat, Nat, Nat.divmod.go(a, _, 1n, 0n)) == Nat.mod(a, 1n+bp) : Nat}
2057 internal_mod_go_d(a, bp, 1n, 0n, 0n)
2058
2059# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a.
2060law mul_div_cancel:
2061 for a: Nat
2062 for b: Nat
2063 {Nat.div(Nat.mul(a, 1n+b), 1n+b) == a : Nat}
2064
2065def mul_div_cancel(a, b):
2066 match a:
2067 case 0n:
2068 {==}
2069 case 1n++p:
2070 +b = b
2071 %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}
2072 %mul_div_cancel(p, b) : {1n+Nat.div(Nat.mul(p, 1n+b), 1n+b) == 1n+_ : Nat}
2073 {==}
2074
2075# Multiplying on the left by a positive divisor then dividing by it cancels: ((1 + b) * a) / (1 + b) = a.
2076law mul_div_cancel_left:
2077 for a: Nat
2078 for b: Nat
2079 {Nat.div(Nat.mul(1n+b, a), 1n+b) == a : Nat}
2080
2081def mul_div_cancel_left(a, b):
2082 +a = a
2083 +b = b
2084 %mul_comm(a, 1n+b) : {Nat.div(_, 1n+b) == a : Nat}
2085 mul_div_cancel(a, b)
2086
2087# A multiple of b leaves no remainder modulo b: (a * b) % b = 0.
2088law mul_mod_left:
2089 for a: Nat
2090 for b: Nat
2091 {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}
2092
2093def mul_mod_left(a, b):
2094 match a b:
2095 case _ 0n:
2096 mul_zero(a)
2097 case 0n 1n+bp:
2098 {==}
2099 case 1n++p 1n++bp:
2100 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))
2101
2102# A multiple of a leaves no remainder modulo a: (a * b) % a = 0.
2103law mul_mod_right:
2104 for a: Nat
2105 for b: Nat
2106 {Nat.mod(Nat.mul(a, b), a) == 0n : Nat}
2107
2108def mul_mod_right(a, b):
2109 +a = a
2110 +b = b
2111 %mul_comm(b, a) : {Nat.mod(_, a) == 0n : Nat}
2112 mul_mod_left(b, a)
2113
2114# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a.
2115law mod_add_div:
2116 for a: Nat
2117 for b: Nat
2118 {Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) == a : Nat}
2119
2120def mod_add_div(a, b):
2121 match b:
2122 case 0n:
2123 add_zero(a)
2124 case 1n++bp:
2125 +a = a
2126 %add_comm(Nat.mul(1n+bp, Nat.div(a, 1n+bp)), Nat.mod(a, 1n+bp)) : {_ == a : Nat}
2127 %mul_comm(Nat.div(a, 1n+bp), 1n+bp) : {Nat.add(_, Nat.mod(a, 1n+bp)) == a : Nat}
2128 div_mod_eq(a, bp)
2129
2130# The quotient times the divisor never exceeds the dividend: (a / b) * b <= a.
2131law div_mul_le_self:
2132 for a: Nat
2133 for b: Nat
2134 le(Nat.mul(Nat.div(a, b), b), a)
2135
2136def div_mul_le_self(a, b):
2137 match b:
2138 case 0n:
2139 zero_le(a)
2140 case 1n++bp:
2141 +a = a
2142 le_of_add_eq(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp), a, div_mod_eq(a, bp))
2143
2144# Left commutativity of multiplication: a * (b * c) = b * (a * c).
2145law mul_left_comm:
2146 for a: Nat
2147 for b: Nat
2148 for c: Nat
2149 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
2150
2151def mul_left_comm(a, b, c):
2152 +a = a
2153 +b = b
2154 +c = c
2155 %mul_assoc(a, b, c) : {_ == Nat.mul(b, Nat.mul(a, c)) : Nat}
2156 %mul_comm(b, a) : {Nat.mul(_, c) == Nat.mul(b, Nat.mul(a, c)) : Nat}
2157 mul_assoc(b, a, c)
2158
2159# Right commutativity of multiplication: (a * b) * c = (a * c) * b.
2160law mul_right_comm:
2161 for a: Nat
2162 for b: Nat
2163 for c: Nat
2164 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
2165
2166def mul_right_comm(a, b, c):
2167 +a = a
2168 +b = b
2169 +c = c
2170 %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}
2171 %mul_comm(b, c) : {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, _) : Nat}
2172 mul_assoc(a, b, c)
2173
2174# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d).
2175law mul_mul_mul_comm:
2176 for a: Nat
2177 for b: Nat
2178 for c: Nat
2179 for d: Nat
2180 {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
2181
2182def mul_mul_mul_comm(a, b, c, d):
2183 +a = a
2184 +b = b
2185 +c = c
2186 +d = d
2187 %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}
2188 %mul_left_comm(b, c, d) : {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(a, _) : Nat}
2189 mul_assoc(a, b, Nat.mul(c, d))
2190
2191# Zero to a positive power is zero: 0^(n+1) = 0.
2192law zero_pow:
2193 for -n: Nat
2194 {Nat.pow(0n, 1n+n) == 0n : Nat}
2195
2196def zero_pow(n):
2197 {==}
2198
2199# A power of a product is the product of the powers: (a * b)^n = a^n * b^n.
2200law mul_pow:
2201 for +a: Nat
2202 for +b: Nat
2203 for n: Nat
2204 {Nat.pow(Nat.mul(a, b), n) == Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) : Nat}
2205
2206def mul_pow(a, b, n):
2207 match n:
2208 case 0n:
2209 {==}
2210 case 1n++p:
2211 %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}
2212 mul_mul_mul_comm(a, b, Nat.pow(a, p), Nat.pow(b, p))
2213
2214# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n.
2215law pow_mul:
2216 for a: Nat
2217 for m: Nat
2218 for n: Nat
2219 {Nat.pow(a, Nat.mul(m, n)) == Nat.pow(Nat.pow(a, m), n) : Nat}
2220
2221def pow_mul(a, m, n):
2222 match m:
2223 case 0n:
2224 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
2225 case 1n++p:
2226 +a = a
2227 +n = n
2228 %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}
2229 %pow_mul(a, p, n) : {Nat.pow(a, Nat.add(n, Nat.mul(p, n))) == Nat.mul(Nat.pow(a, n), _) : Nat}
2230 pow_add(a, n, Nat.mul(p, n))
2231
2232# A power of a positive base is at least one: 1 <= (1 + a)^n.
2233law one_le_pow:
2234 for n: Nat
2235 for a: Nat
2236 le(1n, Nat.pow(1n+a, n))
2237
2238def one_le_pow(n, a):
2239 match n:
2240 case 0n:
2241 {==}
2242 case 1n++p:
2243 +a = a
2244 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))))
2245
2246# A power of a positive base is positive: 0 < (1 + a)^n.
2247law pow_pos:
2248 for n: Nat
2249 for a: Nat
2250 lt(0n, Nat.pow(1n+a, n))
2251
2252def pow_pos(n, a):
2253 +n = n
2254 +a = a
2255 %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}
2256 one_le_pow(n, a)
2257
2258# Adding on the left never decreases a natural: n <= m + n.
2259law le_add_left:
2260 for n: Nat
2261 for m: Nat
2262 le(n, Nat.add(m, n))
2263
2264def le_add_left(n, m):
2265 match m:
2266 case 0n:
2267 le_refl(n)
2268 case 1n++p:
2269 +n = n
2270 le_trans(n, Nat.add(p, n), 1n+Nat.add(p, n), le_add_left(n, p), le_succ(Nat.add(p, n)))
2271
2272# A common left summand cancels in a difference: (k + n) - (k + m) = n - m.
2273law add_sub_add_left:
2274 for k: Nat
2275 for -n: Nat
2276 for -m: Nat
2277 {Nat.sub(Nat.add(k, n), Nat.add(k, m)) == Nat.sub(n, m) : Nat}
2278
2279def add_sub_add_left(k, n, m):
2280 match k:
2281 case 0n:
2282 {==}
2283 case 1n+p:
2284 add_sub_add_left(p, n, m)
2285
2286# A common right summand cancels in a difference: (n + k) - (m + k) = n - m.
2287law add_sub_add_right:
2288 for n: Nat
2289 for k: Nat
2290 for m: Nat
2291 {Nat.sub(Nat.add(n, k), Nat.add(m, k)) == Nat.sub(n, m) : Nat}
2292
2293def add_sub_add_right(n, k, m):
2294 +n = n
2295 +k = k
2296 +m = m
2297 %add_comm(k, n) : {Nat.sub(_, Nat.add(m, k)) == Nat.sub(n, m) : Nat}
2298 %add_comm(k, m) : {Nat.sub(Nat.add(k, n), _) == Nat.sub(n, m) : Nat}
2299 add_sub_add_left(k, n, m)
2300
2301# Subtracting a part of the right summand: k <= m implies (n + m) - k = n + (m - k).
2302law add_sub_assoc:
2303 for k: Nat
2304 for m: Nat
2305 for h: le(k, m)
2306 for n: Nat
2307 {Nat.sub(Nat.add(n, m), k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2308
2309def add_sub_assoc(k, m, h, n):
2310 +k = k
2311 +m = m
2312 +n = n
2313 %sub_add_cancel(m, k, h) : {Nat.sub(Nat.add(n, _), k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2314 %add_assoc(n, Nat.sub(m, k), k) : {Nat.sub(_, k) == Nat.add(n, Nat.sub(m, k)) : Nat}
2315 add_sub_cancel(Nat.add(n, Nat.sub(m, k)), k)
2316
2317# Subtracting a difference from its minuend: m <= n implies n - (n - m) = m.
2318law sub_sub_self:
2319 for n: Nat
2320 for m: Nat
2321 for h: le(m, n)
2322 {Nat.sub(n, Nat.sub(n, m)) == m : Nat}
2323
2324def sub_sub_self(n, m, h):
2325 match n m:
2326 case 0n 0n:
2327 {==}
2328 case 0n 1n+q:
2329 Empty.absurd({Nat.sub(0n, Nat.sub(0n, 1n+q)) == 1n+q : Nat}, internal_false_ne_true(h))
2330 case 1n+p 0n:
2331 sub_self(p)
2332 case 1n++p 1n++q:
2333 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)))
2334
2335# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k.
2336law sub_mul:
2337 for n: Nat
2338 for m: Nat
2339 for k: Nat
2340 {Nat.mul(Nat.sub(n, m), k) == Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) : Nat}
2341
2342def sub_mul(n, m, k):
2343 match n m:
2344 case 0n _:
2345 {==}
2346 case 1n++p 0n:
2347 +k = k
2348 Equal.sym(Nat, Nat.sub(Nat.mul(1n+p, k), 0n), Nat.mul(1n+p, k), sub_zero(Nat.mul(1n+p, k)))
2349 case 1n++p 1n++q:
2350 +k = k
2351 %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}
2352 sub_mul(p, q, k)
2353
2354# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k.
2355law mul_sub:
2356 for n: Nat
2357 for m: Nat
2358 for k: Nat
2359 {Nat.mul(n, Nat.sub(m, k)) == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}
2360
2361def mul_sub(n, m, k):
2362 +n = n
2363 +m = m
2364 +k = k
2365 %mul_comm(Nat.sub(m, k), n) : {_ == Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) : Nat}
2366 %mul_comm(m, n) : {Nat.mul(Nat.sub(m, k), n) == Nat.sub(_, Nat.mul(n, k)) : Nat}
2367 %mul_comm(k, n) : {Nat.mul(Nat.sub(m, k), n) == Nat.sub(Nat.mul(m, n), _) : Nat}
2368 sub_mul(m, k, n)
2369
2370# The minimum is the smaller argument on the left: a <= b implies min a b = a.
2371law min_eq_left:
2372 for a: Nat
2373 for b: Nat
2374 for h: le(a, b)
2375 {Nat.min(a, b) == a : Nat}
2376
2377def min_eq_left(a, b, h):
2378 match a b:
2379 case 0n _:
2380 {==}
2381 case 1n+p 0n:
2382 Empty.absurd({Nat.min(1n+p, 0n) == 1n+p : Nat}, internal_false_ne_true(h))
2383 case 1n++p 1n+q:
2384 %min_eq_left(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
2385 {==}
2386
2387# The minimum is the smaller argument on the right: b <= a implies min a b = b.
2388law min_eq_right:
2389 for a: Nat
2390 for b: Nat
2391 for h: le(b, a)
2392 {Nat.min(a, b) == b : Nat}
2393
2394def min_eq_right(a, b, h):
2395 match a b:
2396 case 0n 0n:
2397 {==}
2398 case 0n 1n+q:
2399 Empty.absurd({Nat.min(0n, 1n+q) == 1n+q : Nat}, internal_false_ne_true(h))
2400 case 1n+p 0n:
2401 {==}
2402 case 1n+p 1n++q:
2403 %min_eq_right(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
2404 {==}
2405
2406# The maximum is the larger argument on the left: b <= a implies max a b = a.
2407law max_eq_left:
2408 for a: Nat
2409 for b: Nat
2410 for h: le(b, a)
2411 {Nat.max(a, b) == a : Nat}
2412
2413def max_eq_left(a, b, h):
2414 match a b:
2415 case 0n 0n:
2416 {==}
2417 case 0n 1n+q:
2418 Empty.absurd({Nat.max(0n, 1n+q) == 0n : Nat}, internal_false_ne_true(h))
2419 case 1n+p 0n:
2420 {==}
2421 case 1n++p 1n+q:
2422 %max_eq_left(p, q, h) : {1n+Nat.max(p, q) == 1n+_ : Nat}
2423 {==}
2424
2425# The maximum is the larger argument on the right: a <= b implies max a b = b.
2426law max_eq_right:
2427 for a: Nat
2428 for b: Nat
2429 for h: le(a, b)
2430 {Nat.max(a, b) == b : Nat}
2431
2432def max_eq_right(a, b, h):
2433 match a b:
2434 case 0n _:
2435 {==}
2436 case 1n+p 0n:
2437 Empty.absurd({Nat.max(1n+p, 0n) == 0n : Nat}, internal_false_ne_true(h))
2438 case 1n+p 1n++q:
2439 %max_eq_right(p, q, h) : {1n+Nat.max(p, q) == 1n+_ : Nat}
2440 {==}
2441
2442def internal_and_false_sym(x: Bool) -> {False{} == Bool.and(x, False{}) : Bool}:
2443 match x:
2444 case False{}:
2445 {==}
2446 case True{}:
2447 {==}
2448
2449def internal_and_true_sym(x: Bool) -> {x == Bool.and(x, True{}) : Bool}:
2450 match x:
2451 case False{}:
2452 {==}
2453 case True{}:
2454 {==}
2455
2456# 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).
2457law le_min:
2458 for a: Nat
2459 for b: Nat
2460 for c: Nat
2461 {Nat.is_le(a, Nat.min(b, c)) == Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)) : Bool}
2462
2463def le_min(a, b, c):
2464 match a b c:
2465 case 0n 0n 0n:
2466 {==}
2467 case 0n 0n 1n+r:
2468 {==}
2469 case 0n 1n+q 0n:
2470 {==}
2471 case 0n 1n+q 1n+r:
2472 {==}
2473 case 1n+p 0n _:
2474 {==}
2475 case 1n+p 1n+q 0n:
2476 internal_and_false_sym(Nat.is_le(p, q))
2477 case 1n+p 1n+q 1n+r:
2478 le_min(p, q, r)
2479
2480# 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).
2481law max_le:
2482 for a: Nat
2483 for b: Nat
2484 for c: Nat
2485 {Nat.is_le(Nat.max(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) : Bool}
2486
2487def max_le(a, b, c):
2488 match a b c:
2489 case 0n _ 0n:
2490 {==}
2491 case 0n _ 1n+r:
2492 {==}
2493 case 1n+p 0n 0n:
2494 {==}
2495 case 1n+p 0n 1n+r:
2496 internal_and_true_sym(Nat.is_le(p, r))
2497 case 1n+p 1n+q 0n:
2498 {==}
2499 case 1n+p 1n+q 1n+r:
2500 max_le(p, q, r)
2501
2502# Multiplying on the left preserves the order: a <= b implies k * a <= k * b.
2503law mul_le_mul_left:
2504 for a: Nat
2505 for b: Nat
2506 for k: Nat
2507 for h: le(a, b)
2508 le(Nat.mul(k, a), Nat.mul(k, b))
2509
2510def mul_le_mul_left(a, b, k, h):
2511 +a = a
2512 +b = b
2513 +k = k
2514 %mul_comm(a, k) : le(_, Nat.mul(k, b))
2515 %mul_comm(b, k) : le(Nat.mul(a, k), _)
2516 mul_le_mul_right(a, b, k, h)
2517
2518# Multiplying two bounded factors stays bounded: a <= c and b <= d imply a * b <= c * d.
2519law mul_le_mul:
2520 for a: Nat
2521 for b: Nat
2522 for c: Nat
2523 for d: Nat
2524 for h1: le(a, c)
2525 for h2: le(b, d)
2526 le(Nat.mul(a, b), Nat.mul(c, d))
2527
2528def mul_le_mul(a, b, c, d, h1, h2):
2529 +a = a
2530 +b = b
2531 +c = c
2532 +d = d
2533 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))
2534
2535# Every successor is positive: 0 < n + 1.
2536law succ_pos:
2537 for -n: Nat
2538 lt(0n, 1n+n)
2539
2540def succ_pos(n):
2541 {==}
2542
2543# Below a successor means at most: m < n + 1 tests as m <= n.
2544law lt_succ_iff:
2545 for m: Nat
2546 for n: Nat
2547 {Nat.is_lt(m, 1n+n) == Nat.is_le(m, n) : Bool}
2548
2549def lt_succ_iff(m, n):
2550 is_lt_eq_succ_le(m, 1n+n)
2551
2552# The successor preserves the strict order: a < b implies a + 1 < b + 1.
2553law succ_lt_succ:
2554 for -a: Nat
2555 for -b: Nat
2556 for h: lt(a, b)
2557 lt(1n+a, 1n+b)
2558
2559def succ_lt_succ(a, b, h):
2560 h
2561
2562# The strict order of successors is the strict order of the naturals: a + 1 < b + 1 implies a < b.
2563law lt_of_succ_lt_succ:
2564 for -a: Nat
2565 for -b: Nat
2566 for h: lt(1n+a, 1n+b)
2567 lt(a, b)
2568
2569def lt_of_succ_lt_succ(a, b, h):
2570 h
2571
2572# Below a successor is at most: m < n + 1 implies m <= n.
2573law le_of_lt_succ:
2574 for m: Nat
2575 for n: Nat
2576 for h: lt(m, 1n+n)
2577 le(m, n)
2578
2579def le_of_lt_succ(m, n, h):
2580 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)
2581
2582# At most is below the successor: m <= n implies m < n + 1.
2583law lt_succ_of_le:
2584 for m: Nat
2585 for n: Nat
2586 for h: le(m, n)
2587 lt(m, 1n+n)
2588
2589def lt_succ_of_le(m, n, h):
2590 Equal.trans(Bool, Nat.is_lt(m, 1n+n), Nat.is_le(m, n), True{}, lt_succ_iff(m, n), h)
2591
2592# A strict inequality gives the weak one from the successor: n < m implies n + 1 <= m.
2593law succ_le_of_lt:
2594 for n: Nat
2595 for m: Nat
2596 for h: lt(n, m)
2597 le(1n+n, m)
2598
2599def succ_le_of_lt(n, m, h):
2600 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)
2601
2602# A weak inequality from the successor gives the strict one: n + 1 <= m implies n < m.
2603law lt_of_succ_le:
2604 for n: Nat
2605 for m: Nat
2606 for h: le(1n+n, m)
2607 lt(n, m)
2608
2609def lt_of_succ_le(n, m, h):
2610 Equal.trans(Bool, Nat.is_lt(n, m), Nat.is_le(1n+n, m), True{}, is_lt_eq_succ_le(n, m), h)
2611
2612# The strict order is asymmetric: a < b rules out b < a.
2613law lt_asymm:
2614 for a: Nat
2615 for b: Nat
2616 for h: lt(a, b)
2617 lt(b, a) -> Empty
2618
2619def lt_asymm(a, b, h):
2620 +a = a
2621 h2 => lt_irrefl(a)(lt_trans(a, b, a, h, h2))
2622
2623# At most means below or equal: a <= b tests as a < b or a = b.
2624law le_iff_lt_or_eq:
2625 for a: Nat
2626 for b: Nat
2627 {Nat.is_le(a, b) == Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)) : Bool}
2628
2629def le_iff_lt_or_eq(a, b):
2630 match a b:
2631 case 0n 0n:
2632 {==}
2633 case 0n 1n+q:
2634 {==}
2635 case 1n+p 0n:
2636 {==}
2637 case 1n+p 1n+q:
2638 le_iff_lt_or_eq(p, q)
2639
2640# Below means at most and different: a < b tests as a <= b and not a = b.
2641law lt_iff_le_and_ne:
2642 for a: Nat
2643 for b: Nat
2644 {Nat.is_lt(a, b) == Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))) : Bool}
2645
2646def lt_iff_le_and_ne(a, b):
2647 match a b:
2648 case 0n 0n:
2649 {==}
2650 case 0n 1n+q:
2651 {==}
2652 case 1n+p 0n:
2653 {==}
2654 case 1n+p 1n+q:
2655 lt_iff_le_and_ne(p, q)
2656
2657# A natural that does not test equal to zero is positive.
2658law pos_of_ne_zero:
2659 for n: Nat
2660 for h: {Nat.is_eq(n, 0n) == False{} : Bool}
2661 lt(0n, n)
2662
2663def pos_of_ne_zero(n, h):
2664 match n:
2665 case 0n:
2666 Empty.absurd(lt(0n, 0n), internal_div_true_ne_false(h))
2667 case 1n+p:
2668 {==}
2669
2670# Adding on the right keeps a strict bound: n < m implies n < m + k.
2671law lt_add_right:
2672 for n: Nat
2673 for m: Nat
2674 for -k: Nat
2675 for h: lt(n, m)
2676 lt(n, Nat.add(m, k))
2677
2678def lt_add_right(n, m, k, h):
2679 match n m:
2680 case 0n 0n:
2681 Empty.absurd(lt(0n, Nat.add(0n, k)), internal_false_ne_true(h))
2682 case 0n 1n+q:
2683 {==}
2684 case 1n+p 0n:
2685 Empty.absurd(lt(1n+p, Nat.add(0n, k)), internal_false_ne_true(h))
2686 case 1n+p 1n+q:
2687 lt_add_right(p, q, k, h)
2688
2689# Adding a positive amount on the right strictly increases: n < n + (1 + k).
2690law lt_add_of_pos_right:
2691 for n: Nat
2692 for -k: Nat
2693 lt(n, Nat.add(n, 1n+k))
2694
2695def lt_add_of_pos_right(n, k):
2696 match n:
2697 case 0n:
2698 {==}
2699 case 1n+p:
2700 lt_add_of_pos_right(p, k)
2701
2702# Adding a positive amount on the left strictly increases: n < (1 + k) + n.
2703law lt_add_of_pos_left:
2704 for n: Nat
2705 for k: Nat
2706 lt(n, Nat.add(1n+k, n))
2707
2708def lt_add_of_pos_left(n, k):
2709 +n = n
2710 +k = k
2711 lt_succ_of_le(n, Nat.add(k, n), le_add_left(n, k))
2712
2713# Adding on the left preserves the strict order: a < b implies k + a < k + b.
2714law add_lt_add_left:
2715 for -a: Nat
2716 for -b: Nat
2717 for k: Nat
2718 for h: lt(a, b)
2719 lt(Nat.add(k, a), Nat.add(k, b))
2720
2721def add_lt_add_left(a, b, k, h):
2722 match k:
2723 case 0n:
2724 h
2725 case 1n+p:
2726 add_lt_add_left(a, b, p, h)
2727
2728# Adding on the right preserves the strict order: a < b implies a + k < b + k.
2729law add_lt_add_right:
2730 for a: Nat
2731 for b: Nat
2732 for k: Nat
2733 for h: lt(a, b)
2734 lt(Nat.add(a, k), Nat.add(b, k))
2735
2736def add_lt_add_right(a, b, k, h):
2737 +a = a
2738 +b = b
2739 +k = k
2740 %add_comm(k, a) : lt(_, Nat.add(b, k))
2741 %add_comm(k, b) : lt(Nat.add(k, a), _)
2742 add_lt_add_left(a, b, k, h)
2743
2744# Adding the same amount on the left does not change the strict order test: a < b tests as k + a < k + b.
2745law add_lt_add_iff_left:
2746 for k: Nat
2747 for -a: Nat
2748 for -b: Nat
2749 {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(k, a), Nat.add(k, b)) : Bool}
2750
2751def add_lt_add_iff_left(k, a, b):
2752 match k:
2753 case 0n:
2754 {==}
2755 case 1n+p:
2756 add_lt_add_iff_left(p, a, b)
2757
2758# Adding the same amount on the right does not change the strict order test: a < b tests as a + k < b + k.
2759law add_lt_add_iff_right:
2760 for a: Nat
2761 for b: Nat
2762 for k: Nat
2763 {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(a, k), Nat.add(b, k)) : Bool}
2764
2765def add_lt_add_iff_right(a, b, k):
2766 +a = a
2767 +b = b
2768 +k = k
2769 %add_comm(k, a) : {Nat.is_lt(a, b) == Nat.is_lt(_, Nat.add(b, k)) : Bool}
2770 %add_comm(k, b) : {Nat.is_lt(a, b) == Nat.is_lt(Nat.add(k, a), _) : Bool}
2771 add_lt_add_iff_left(k, a, b)
2772
2773# A common left summand cancels in a strict inequality: k + a < k + b implies a < b.
2774law lt_of_add_lt_add_left:
2775 for k: Nat
2776 for -a: Nat
2777 for -b: Nat
2778 for h: lt(Nat.add(k, a), Nat.add(k, b))
2779 lt(a, b)
2780
2781def lt_of_add_lt_add_left(k, a, b, h):
2782 match k:
2783 case 0n:
2784 h
2785 case 1n+p:
2786 lt_of_add_lt_add_left(p, a, b, h)
2787
2788# A common right summand cancels in a strict inequality: a + k < b + k implies a < b.
2789law lt_of_add_lt_add_right:
2790 for a: Nat
2791 for b: Nat
2792 for k: Nat
2793 for h: lt(Nat.add(a, k), Nat.add(b, k))
2794 lt(a, b)
2795
2796def lt_of_add_lt_add_right(a, b, k, h):
2797 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)
2798
2799# Adding two strict bounds keeps a strict bound: a < c and b < d imply a + b < c + d.
2800law add_lt_add:
2801 for a: Nat
2802 for b: Nat
2803 for c: Nat
2804 for d: Nat
2805 for h1: lt(a, c)
2806 for h2: lt(b, d)
2807 lt(Nat.add(a, b), Nat.add(c, d))
2808
2809def add_lt_add(a, b, c, d, h1, h2):
2810 +a = a
2811 +b = b
2812 +c = c
2813 +d = d
2814 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))
2815
2816# A positive left factor never decreases: m <= (1 + n) * m.
2817law le_mul_of_pos_left:
2818 for m: Nat
2819 for n: Nat
2820 le(m, Nat.mul(1n+n, m))
2821
2822def le_mul_of_pos_left(m, n):
2823 +m = m
2824 le_add_right(m, Nat.mul(n, m))
2825
2826# A positive right factor never decreases: m <= m * (1 + n).
2827law le_mul_of_pos_right:
2828 for m: Nat
2829 for n: Nat
2830 le(m, Nat.mul(m, 1n+n))
2831
2832def le_mul_of_pos_right(m, n):
2833 +m = m
2834 +n = n
2835 %mul_comm(1n+n, m) : le(m, _)
2836 le_mul_of_pos_left(m, n)
2837
2838# Multiplying on the left by a positive factor preserves the strict order: a < b implies (1 + k) * a < (1 + k) * b.
2839law mul_lt_mul_of_pos_left:
2840 for a: Nat
2841 for b: Nat
2842 for k: Nat
2843 for h: lt(a, b)
2844 lt(Nat.mul(1n+k, a), Nat.mul(1n+k, b))
2845
2846def mul_lt_mul_of_pos_left(a, b, k, h):
2847 +a = a
2848 +b = b
2849 +k = k
2850 +h = h
2851 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))))
2852
2853# Multiplying on the right by a positive factor preserves the strict order: a < b implies a * (1 + k) < b * (1 + k).
2854law mul_lt_mul_of_pos_right:
2855 for a: Nat
2856 for b: Nat
2857 for k: Nat
2858 for h: lt(a, b)
2859 lt(Nat.mul(a, 1n+k), Nat.mul(b, 1n+k))
2860
2861def mul_lt_mul_of_pos_right(a, b, k, h):
2862 +a = a
2863 +b = b
2864 +k = k
2865 %mul_comm(1n+k, a) : lt(_, Nat.mul(b, 1n+k))
2866 %mul_comm(1n+k, b) : lt(Nat.mul(1n+k, a), _)
2867 mul_lt_mul_of_pos_left(a, b, k, h)
2868
2869def 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):
2870 match v:
2871 case True{}:
2872 Equal.sym(Bool, True{}, Nat.is_lt(a, b), e)
2873 case False{}:
2874 Empty.absurd(lt(a, b), f(le_of_not_lt(a, b, Equal.sym(Bool, False{}, Nat.is_lt(a, b), e))))
2875
2876# A common left factor cancels in a strict inequality: k * a < k * b implies a < b.
2877law lt_of_mul_lt_mul_left:
2878 for k: Nat
2879 for a: Nat
2880 for b: Nat
2881 for h: lt(Nat.mul(k, a), Nat.mul(k, b))
2882 lt(a, b)
2883
2884def lt_of_mul_lt_mul_left(k, a, b, h):
2885 +k = k
2886 +a = a
2887 +b = b
2888 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))))
2889
2890# A common right factor cancels in a strict inequality: a * k < b * k implies a < b.
2891law lt_of_mul_lt_mul_right:
2892 for a: Nat
2893 for b: Nat
2894 for k: Nat
2895 for h: lt(Nat.mul(a, k), Nat.mul(b, k))
2896 lt(a, b)
2897
2898def lt_of_mul_lt_mul_right(a, b, k, h):
2899 +k = k
2900 +a = a
2901 +b = b
2902 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))))
2903
2904# Multiplying two strict bounds keeps a strict bound: a < c and b < d imply a * b < c * d.
2905law mul_lt_mul_of_lt_of_lt:
2906 for a: Nat
2907 for b: Nat
2908 for c: Nat
2909 for d: Nat
2910 for h1: lt(a, c)
2911 for h2: lt(b, d)
2912 lt(Nat.mul(a, b), Nat.mul(c, d))
2913
2914def mul_lt_mul_of_lt_of_lt(a, b, c, d, h1, h2):
2915 match c:
2916 case 0n:
2917 Empty.absurd(lt(Nat.mul(a, b), Nat.mul(0n, d)), lt_zero(a)(h1))
2918 case 1n++cp:
2919 +a = a
2920 +b = b
2921 +d = d
2922 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))
2923
2924# Squares are monotone: a <= b implies a * a <= b * b.
2925law mul_self_le_mul_self:
2926 for a: Nat
2927 for b: Nat
2928 for h: le(a, b)
2929 le(Nat.mul(a, a), Nat.mul(b, b))
2930
2931def mul_self_le_mul_self(a, b, h):
2932 +a = a
2933 +b = b
2934 +h = h
2935 mul_le_mul(a, a, b, b, h, h)
2936
2937# Squares are strictly monotone: a < b implies a * a < b * b.
2938law mul_self_lt_mul_self:
2939 for a: Nat
2940 for b: Nat
2941 for h: lt(a, b)
2942 lt(Nat.mul(a, a), Nat.mul(b, b))
2943
2944def mul_self_lt_mul_self(a, b, h):
2945 +a = a
2946 +b = b
2947 +h = h
2948 mul_lt_mul_of_lt_of_lt(a, a, b, b, h, h)
2949
2950# Subtracting a positive amount from a positive number decreases it: (1 + n) - (1 + m) < 1 + n.
2951law sub_lt:
2952 for n: Nat
2953 for m: Nat
2954 lt(Nat.sub(1n+n, 1n+m), 1n+n)
2955
2956def sub_lt(n, m):
2957 +n = n
2958 +m = m
2959 lt_succ_of_le(Nat.sub(n, m), n, sub_le(n, m))
2960
2961# Subtracting more gives less: n <= m implies k - m <= k - n.
2962law sub_le_sub_left:
2963 for n: Nat
2964 for m: Nat
2965 for h: le(n, m)
2966 for k: Nat
2967 le(Nat.sub(k, m), Nat.sub(k, n))
2968
2969def sub_le_sub_left(n, m, h, k):
2970 +n = n
2971 +m = m
2972 +k = k
2973 %add_sub_of_le(n, m, h) : le(Nat.sub(k, _), Nat.sub(k, n))
2974 %sub_sub(k, n, Nat.sub(m, n)) : le(_, Nat.sub(k, n))
2975 sub_le(Nat.sub(k, n), Nat.sub(m, n))
2976
2977# Subtraction on the right preserves the order: n <= m implies n - k <= m - k.
2978law sub_le_sub_right:
2979 for n: Nat
2980 for m: Nat
2981 for h: le(n, m)
2982 for k: Nat
2983 le(Nat.sub(n, k), Nat.sub(m, k))
2984
2985def sub_le_sub_right(n, m, h, k):
2986 match n m k:
2987 case 0n _ _:
2988 +k = k
2989 %Equal.sym(Nat, Nat.sub(0n, k), 0n, zero_sub(k)) : le(_, Nat.sub(m, k))
2990 zero_le(Nat.sub(m, k))
2991 case 1n+p 0n _:
2992 Empty.absurd(le(Nat.sub(1n+p, k), Nat.sub(0n, k)), internal_false_ne_true(h))
2993 case 1n+p 1n+q 0n:
2994 h
2995 case 1n+p 1n+q 1n+r:
2996 sub_le_sub_right(p, q, h, r)
2997
2998# A strict bound on a sum bounds a difference: a + b < c implies a < c - b.
2999law lt_sub_of_add_lt:
3000 for a: Nat
3001 for b: Nat
3002 for c: Nat
3003 for h: lt(Nat.add(a, b), c)
3004 lt(a, Nat.sub(c, b))
3005
3006def lt_sub_of_add_lt(a, b, c, h):
3007 +a = a
3008 +b = b
3009 %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}
3010 %add_comm(a, b) : {Nat.is_lt(_, c) == True{} : Bool}
3011 h
3012
3013# A difference is positive below the minuend: m < n implies 0 < n - m.
3014law sub_pos_of_lt:
3015 for m: Nat
3016 for n: Nat
3017 for h: lt(m, n)
3018 lt(0n, Nat.sub(n, m))
3019
3020def sub_pos_of_lt(m, n, h):
3021 lt_sub_of_add_lt(0n, m, n, h)
3022
3023# Minimum distributes over maximum on the left: min a (max b c) = max (min a b) (min a c).
3024law min_max_distrib_left:
3025 for a: Nat
3026 for b: Nat
3027 for c: Nat
3028 {Nat.min(a, Nat.max(b, c)) == Nat.max(Nat.min(a, b), Nat.min(a, c)) : Nat}
3029
3030def min_max_distrib_left(a, b, c):
3031 match a b c:
3032 case 0n _ _:
3033 {==}
3034 case 1n+p 0n 0n:
3035 {==}
3036 case 1n+p 0n 1n+r:
3037 {==}
3038 case 1n+p 1n+q 0n:
3039 {==}
3040 case 1n+p 1n+q 1n+r:
3041 %min_max_distrib_left(p, q, r) : {1n+Nat.min(p, Nat.max(q, r)) == 1n+_ : Nat}
3042 {==}
3043
3044# Maximum distributes over minimum on the left: max a (min b c) = min (max a b) (max a c).
3045law max_min_distrib_left:
3046 for a: Nat
3047 for b: Nat
3048 for c: Nat
3049 {Nat.max(a, Nat.min(b, c)) == Nat.min(Nat.max(a, b), Nat.max(a, c)) : Nat}
3050
3051def max_min_distrib_left(a, b, c):
3052 match a b c:
3053 case 0n _ _:
3054 {==}
3055 case 1n++p 0n 0n:
3056 %Equal.sym(Nat, Nat.min(p, p), p, min_self(p)) : {1n+p == 1n+_ : Nat}
3057 {==}
3058 case 1n++p 0n 1n++r:
3059 %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}
3060 {==}
3061 case 1n++p 1n++q 0n:
3062 %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}
3063 {==}
3064 case 1n+p 1n+q 1n+r:
3065 %max_min_distrib_left(p, q, r) : {1n+Nat.max(p, Nat.min(q, r)) == 1n+_ : Nat}
3066 {==}
3067
3068# A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c.
3069law min_add_add_left:
3070 for a: Nat
3071 for -b: Nat
3072 for -c: Nat
3073 {Nat.min(Nat.add(a, b), Nat.add(a, c)) == Nat.add(a, Nat.min(b, c)) : Nat}
3074
3075def min_add_add_left(a, b, c):
3076 match a:
3077 case 0n:
3078 {==}
3079 case 1n+p:
3080 %min_add_add_left(p, b, c) : {1n+Nat.min(Nat.add(p, b), Nat.add(p, c)) == 1n+_ : Nat}
3081 {==}
3082
3083# A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c.
3084law min_add_add_right:
3085 for a: Nat
3086 for b: Nat
3087 for c: Nat
3088 {Nat.min(Nat.add(a, c), Nat.add(b, c)) == Nat.add(Nat.min(a, b), c) : Nat}
3089
3090def min_add_add_right(a, b, c):
3091 +a = a
3092 +b = b
3093 +c = c
3094 %add_comm(c, a) : {Nat.min(_, Nat.add(b, c)) == Nat.add(Nat.min(a, b), c) : Nat}
3095 %add_comm(c, b) : {Nat.min(Nat.add(c, a), _) == Nat.add(Nat.min(a, b), c) : Nat}
3096 %add_comm(c, Nat.min(a, b)) : {Nat.min(Nat.add(c, a), Nat.add(c, b)) == _ : Nat}
3097 min_add_add_left(c, a, b)
3098
3099# A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c.
3100law max_add_add_left:
3101 for a: Nat
3102 for -b: Nat
3103 for -c: Nat
3104 {Nat.max(Nat.add(a, b), Nat.add(a, c)) == Nat.add(a, Nat.max(b, c)) : Nat}
3105
3106def max_add_add_left(a, b, c):
3107 match a:
3108 case 0n:
3109 {==}
3110 case 1n+p:
3111 %max_add_add_left(p, b, c) : {1n+Nat.max(Nat.add(p, b), Nat.add(p, c)) == 1n+_ : Nat}
3112 {==}
3113
3114# A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c.
3115law max_add_add_right:
3116 for a: Nat
3117 for b: Nat
3118 for c: Nat
3119 {Nat.max(Nat.add(a, c), Nat.add(b, c)) == Nat.add(Nat.max(a, b), c) : Nat}
3120
3121def max_add_add_right(a, b, c):
3122 +a = a
3123 +b = b
3124 +c = c
3125 %add_comm(c, a) : {Nat.max(_, Nat.add(b, c)) == Nat.add(Nat.max(a, b), c) : Nat}
3126 %add_comm(c, b) : {Nat.max(Nat.add(c, a), _) == Nat.add(Nat.max(a, b), c) : Nat}
3127 %add_comm(c, Nat.max(a, b)) : {Nat.max(Nat.add(c, a), Nat.add(c, b)) == _ : Nat}
3128 max_add_add_left(c, a, b)
3129
3130# The minimum is below c exactly when one argument is: min a b < c tests as a < c or b < c.
3131law min_lt_iff:
3132 for a: Nat
3133 for b: Nat
3134 for c: Nat
3135 {Nat.is_lt(Nat.min(a, b), c) == Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)) : Bool}
3136
3137def min_lt_iff(a, b, c):
3138 match a b c:
3139 case 0n 0n 0n:
3140 {==}
3141 case 0n 0n 1n+r:
3142 {==}
3143 case 0n 1n+q 0n:
3144 {==}
3145 case 0n 1n+q 1n+r:
3146 {==}
3147 case 1n+p 0n 0n:
3148 {==}
3149 case 1n+p 0n 1n+r:
3150 internal_or_true_sym(Nat.is_lt(p, r))
3151 case 1n+p 1n+q 0n:
3152 {==}
3153 case 1n+p 1n+q 1n+r:
3154 min_lt_iff(p, q, r)
3155
3156# A number is below the minimum exactly when it is below both: a < min b c tests as a < b and a < c.
3157law lt_min_iff:
3158 for a: Nat
3159 for b: Nat
3160 for c: Nat
3161 {Nat.is_lt(a, Nat.min(b, c)) == Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)) : Bool}
3162
3163def lt_min_iff(a, b, c):
3164 match a b c:
3165 case 0n 0n 0n:
3166 {==}
3167 case 0n 0n 1n+r:
3168 {==}
3169 case 0n 1n+q 0n:
3170 {==}
3171 case 0n 1n+q 1n+r:
3172 {==}
3173 case 1n+p 0n 0n:
3174 {==}
3175 case 1n+p 0n 1n+r:
3176 {==}
3177 case 1n+p 1n+q 0n:
3178 internal_and_false_sym(Nat.is_lt(p, q))
3179 case 1n+p 1n+q 1n+r:
3180 lt_min_iff(p, q, r)
3181
3182# The maximum is below c exactly when both arguments are: max a b < c tests as a < c and b < c.
3183law max_lt_iff:
3184 for a: Nat
3185 for b: Nat
3186 for c: Nat
3187 {Nat.is_lt(Nat.max(a, b), c) == Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)) : Bool}
3188
3189def max_lt_iff(a, b, c):
3190 match a b c:
3191 case 0n 0n 0n:
3192 {==}
3193 case 0n 0n 1n+r:
3194 {==}
3195 case 0n 1n+q 0n:
3196 {==}
3197 case 0n 1n+q 1n+r:
3198 {==}
3199 case 1n+p 0n 0n:
3200 {==}
3201 case 1n+p 0n 1n+r:
3202 internal_and_true_sym(Nat.is_lt(p, r))
3203 case 1n+p 1n+q 0n:
3204 {==}
3205 case 1n+p 1n+q 1n+r:
3206 max_lt_iff(p, q, r)
3207
3208# 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.
3209law le_max_iff:
3210 for a: Nat
3211 for b: Nat
3212 for c: Nat
3213 {Nat.is_le(a, Nat.max(b, c)) == Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)) : Bool}
3214
3215def le_max_iff(a, b, c):
3216 match a b c:
3217 case 0n 0n 0n:
3218 {==}
3219 case 0n 0n 1n+r:
3220 {==}
3221 case 0n 1n+q 0n:
3222 {==}
3223 case 0n 1n+q 1n+r:
3224 {==}
3225 case 1n+p 0n 0n:
3226 {==}
3227 case 1n+p 0n 1n+r:
3228 {==}
3229 case 1n+p 1n+q 0n:
3230 internal_or_false_sym(Nat.is_le(p, q))
3231 case 1n+p 1n+q 1n+r:
3232 le_max_iff(p, q, r)
3233
3234# A bound by the left argument bounds the maximum: a <= b implies a <= max b c.
3235law le_max_of_le_left:
3236 for a: Nat
3237 for b: Nat
3238 for c: Nat
3239 for h: le(a, b)
3240 le(a, Nat.max(b, c))
3241
3242def le_max_of_le_left(a, b, c, h):
3243 +b = b
3244 +c = c
3245 le_trans(a, b, Nat.max(b, c), h, le_max_left(b, c))
3246
3247# A bound by the right argument bounds the maximum: a <= c implies a <= max b c.
3248law le_max_of_le_right:
3249 for a: Nat
3250 for b: Nat
3251 for c: Nat
3252 for h: le(a, c)
3253 le(a, Nat.max(b, c))
3254
3255def le_max_of_le_right(a, b, c, h):
3256 +b = b
3257 +c = c
3258 le_trans(a, c, Nat.max(b, c), h, le_max_right(b, c))
3259
3260# A bounded left argument bounds the minimum: a <= c implies min a b <= c.
3261law min_le_of_left_le:
3262 for a: Nat
3263 for b: Nat
3264 for c: Nat
3265 for h: le(a, c)
3266 le(Nat.min(a, b), c)
3267
3268def min_le_of_left_le(a, b, c, h):
3269 +a = a
3270 +b = b
3271 le_trans(Nat.min(a, b), a, c, min_le_left(a, b), h)
3272
3273# A bounded right argument bounds the minimum: b <= c implies min a b <= c.
3274law min_le_of_right_le:
3275 for a: Nat
3276 for b: Nat
3277 for c: Nat
3278 for h: le(b, c)
3279 le(Nat.min(a, b), c)
3280
3281def min_le_of_right_le(a, b, c, h):
3282 +a = a
3283 +b = b
3284 le_trans(Nat.min(a, b), b, c, min_le_right(a, b), h)
3285
3286# Minimum is monotone in both arguments: a <= c and b <= d imply min a b <= min c d.
3287law min_le_min:
3288 for a: Nat
3289 for b: Nat
3290 for c: Nat
3291 for d: Nat
3292 for h1: le(a, c)
3293 for h2: le(b, d)
3294 le(Nat.min(a, b), Nat.min(c, d))
3295
3296def min_le_min(a, b, c, d, h1, h2):
3297 +a = a
3298 +b = b
3299 +c = c
3300 +d = d
3301 %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}
3302 %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}
3303 min_le_of_right_le(a, b, d, h2)
3304
3305# Maximum is monotone in both arguments: a <= c and b <= d imply max a b <= max c d.
3306law max_le_max:
3307 for a: Nat
3308 for b: Nat
3309 for c: Nat
3310 for d: Nat
3311 for h1: le(a, c)
3312 for h2: le(b, d)
3313 le(Nat.max(a, b), Nat.max(c, d))
3314
3315def max_le_max(a, b, c, d, h1, h2):
3316 +a = a
3317 +b = b
3318 +c = c
3319 +d = d
3320 %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}
3321 %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}
3322 le_max_of_le_right(b, c, d, h2)
3323
3324# Powers are monotone in the base: a <= b implies a^n <= b^n.
3325law pow_le_pow_left:
3326 for a: Nat
3327 for b: Nat
3328 for h: le(a, b)
3329 for n: Nat
3330 le(Nat.pow(a, n), Nat.pow(b, n))
3331
3332def pow_le_pow_left(a, b, h, n):
3333 match n:
3334 case 0n:
3335 {==}
3336 case 1n++p:
3337 +a = a
3338 +b = b
3339 +h = h
3340 mul_le_mul(a, Nat.pow(a, p), b, Nat.pow(b, p), h, pow_le_pow_left(a, b, h, p))
3341
3342# Powers of a positive base are monotone in the exponent: i <= j implies (1 + a)^i <= (1 + a)^j.
3343law pow_le_pow_right:
3344 for a: Nat
3345 for i: Nat
3346 for j: Nat
3347 for h: le(i, j)
3348 le(Nat.pow(1n+a, i), Nat.pow(1n+a, j))
3349
3350def pow_le_pow_right(a, i, j, h):
3351 match i j:
3352 case 0n y:
3353 one_le_pow(y, a)
3354 case 1n+p 0n:
3355 Empty.absurd(le(Nat.pow(1n+a, 1n+p), Nat.pow(1n+a, 0n)), internal_false_ne_true(h))
3356 case 1n++p 1n++q:
3357 +a = a
3358 mul_le_mul_left(Nat.pow(1n+a, p), Nat.pow(1n+a, q), 1n+a, pow_le_pow_right(a, p, q, h))
3359
3360def internal_lt_mul_two_add(a: Nat, x: Nat, hx: lt(0n, x)) -> lt(x, Nat.mul(2n+a, x)):
3361 match x:
3362 case 0n:
3363 Empty.absurd(lt(0n, Nat.mul(2n+a, 0n)), internal_false_ne_true(hx))
3364 case 1n++y:
3365 lt_add_of_pos_right(y, Nat.add(y, Nat.mul(a, 1n+y)))
3366
3367# Powers of a base above one are strictly monotone in the exponent: i < j implies (2 + a)^i < (2 + a)^j.
3368law pow_lt_pow_right:
3369 for a: Nat
3370 for i: Nat
3371 for j: Nat
3372 for h: lt(i, j)
3373 lt(Nat.pow(2n+a, i), Nat.pow(2n+a, j))
3374
3375def pow_lt_pow_right(a, i, j, h):
3376 match i j:
3377 case 0n 0n:
3378 Empty.absurd(lt(Nat.pow(2n+a, 0n), Nat.pow(2n+a, 0n)), internal_false_ne_true(h))
3379 case 0n 1n+q:
3380 +a = a
3381 +q = q
3382 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)))
3383 case 1n+p 0n:
3384 Empty.absurd(lt(Nat.pow(2n+a, 1n+p), Nat.pow(2n+a, 0n)), internal_false_ne_true(h))
3385 case 1n++p 1n++q:
3386 +a = a
3387 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))
3388
3389# Positive powers are strictly monotone in the base: a < b implies a^(1 + n) < b^(1 + n).
3390law pow_lt_pow_left:
3391 for a: Nat
3392 for b: Nat
3393 for h: lt(a, b)
3394 for n: Nat
3395 lt(Nat.pow(a, 1n+n), Nat.pow(b, 1n+n))
3396
3397def pow_lt_pow_left(a, b, h, n):
3398 match n:
3399 case 0n:
3400 +a = a
3401 +b = b
3402 %Equal.sym(Nat, Nat.mul(a, 1n), a, mul_one(a)) : lt(_, Nat.mul(b, 1n))
3403 %Equal.sym(Nat, Nat.mul(b, 1n), b, mul_one(b)) : lt(a, _)
3404 h
3405 case 1n++p:
3406 +a = a
3407 +b = b
3408 +h = h
3409 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))
3410
3411# Adding a multiple of a positive divisor adds to the quotient: (x + z * (1 + b)) / (1 + b) = x / (1 + b) + z.
3412law add_mul_div_right:
3413 for x: Nat
3414 for z: Nat
3415 for b: Nat
3416 {Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}
3417
3418def add_mul_div_right(x, z, b):
3419 match z:
3420 case 0n:
3421 +x = x
3422 +b = b
3423 %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.div(_, 1n+b) == Nat.add(Nat.div(x, 1n+b), 0n) : Nat}
3424 Equal.sym(Nat, Nat.add(Nat.div(x, 1n+b), 0n), Nat.div(x, 1n+b), add_zero(Nat.div(x, 1n+b)))
3425 case 1n++w:
3426 +x = x
3427 +b = b
3428 %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}
3429 %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}
3430 %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}
3431 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))
3432
3433# Adding a multiple of a positive divisor adds to the quotient: (x + (1 + b) * z) / (1 + b) = x / (1 + b) + z.
3434law add_mul_div_left:
3435 for x: Nat
3436 for z: Nat
3437 for b: Nat
3438 {Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}
3439
3440def add_mul_div_left(x, z, b):
3441 +x = x
3442 +z = z
3443 +b = b
3444 %mul_comm(z, 1n+b) : {Nat.div(Nat.add(x, _), 1n+b) == Nat.add(Nat.div(x, 1n+b), z) : Nat}
3445 add_mul_div_right(x, z, b)
3446
3447# Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b.
3448law add_mul_mod_self_right:
3449 for a: Nat
3450 for b: Nat
3451 for c: Nat
3452 {Nat.mod(Nat.add(a, Nat.mul(c, b)), b) == Nat.mod(a, b) : Nat}
3453
3454def add_mul_mod_self_right(a, b, c):
3455 match c:
3456 case 0n:
3457 +a = a
3458 %Equal.sym(Nat, Nat.add(a, 0n), a, add_zero(a)) : {Nat.mod(_, b) == Nat.mod(a, b) : Nat}
3459 {==}
3460 case 1n++w:
3461 +a = a
3462 +b = b
3463 %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}
3464 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))
3465
3466# Adding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b.
3467law add_mul_mod_self_left:
3468 for a: Nat
3469 for b: Nat
3470 for c: Nat
3471 {Nat.mod(Nat.add(a, Nat.mul(b, c)), b) == Nat.mod(a, b) : Nat}
3472
3473def add_mul_mod_self_left(a, b, c):
3474 +a = a
3475 +b = b
3476 +c = c
3477 %mul_comm(c, b) : {Nat.mod(Nat.add(a, _), b) == Nat.mod(a, b) : Nat}
3478 add_mul_mod_self_right(a, b, c)
3479
3480def 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}:
3481 match y:
3482 case 0n:
3483 {==}
3484 case 1n+z:
3485 Empty.absurd({Bool.or(Nat.is_eq(2n+z, 0n), Nat.is_eq(2n+z, 1n)) == True{} : Bool}, lt_zero(z)(h))
3486
3487def internal_lt_two(x: Nat, h: lt(x, 2n)) -> {Bool.or(Nat.is_eq(x, 0n), Nat.is_eq(x, 1n)) == True{} : Bool}:
3488 match x:
3489 case 0n:
3490 {==}
3491 case 1n+y:
3492 internal_lt_one_succ(y, h)
3493
3494# A remainder modulo two is zero or one.
3495law mod_two_eq_zero_or_one:
3496 for n: Nat
3497 {Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)) == True{} : Bool}
3498
3499def mod_two_eq_zero_or_one(n):
3500 +n = n
3501 internal_lt_two(Nat.mod(n, 2n), mod_lt(n, 1n))
3502
3503# The divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a.
3504law div_add_mod:
3505 for a: Nat
3506 for b: Nat
3507 {Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)) == a : Nat}
3508
3509def div_add_mod(a, b):
3510 +a = a
3511 +b = b
3512 %add_comm(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) : {_ == a : Nat}
3513 mod_add_div(a, b)
3514
3515# Two times n is n + n.
3516law two_mul:
3517 for n: Nat
3518 {Nat.mul(2n, n) == Nat.add(n, n) : Nat}
3519
3520def two_mul(n):
3521 +n = n
3522 %Equal.sym(Nat, Nat.add(n, 0n), n, add_zero(n)) : {Nat.add(n, _) == Nat.add(n, n) : Nat}
3523 {==}
3524
3525# Doubling is multiplying by two: double n = 2 * n.
3526law double_eq_two_mul:
3527 for n: Nat
3528 {Nat.double(n) == Nat.mul(2n, n) : Nat}
3529
3530def double_eq_two_mul(n):
3531 +n = n
3532 %Equal.sym(Nat, Nat.mul(2n, n), Nat.add(n, n), two_mul(n)) : {Nat.double(n) == _ : Nat}
3533 double_eq_add(n)
3534
3535# Doubling distributes over addition: double (a + b) = double a + double b.
3536law double_add:
3537 for a: Nat
3538 for b: Nat
3539 {Nat.double(Nat.add(a, b)) == Nat.add(Nat.double(a), Nat.double(b)) : Nat}
3540
3541def double_add(a, b):
3542 +a = a
3543 +b = b
3544 %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}
3545 %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}
3546 %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}
3547 add_add_add_comm(a, b, a, b)
3548
3549# Doubling a product doubles its left factor: double (a * b) = double a * b.
3550law double_mul:
3551 for a: Nat
3552 for b: Nat
3553 {Nat.double(Nat.mul(a, b)) == Nat.mul(Nat.double(a), b) : Nat}
3554
3555def double_mul(a, b):
3556 +a = a
3557 +b = b
3558 %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}
3559 %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}
3560 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))
3561
3562# Multiplying by a doubled factor doubles the product: a * double b = double (a * b).
3563law mul_double:
3564 for a: Nat
3565 for b: Nat
3566 {Nat.mul(a, Nat.double(b)) == Nat.double(Nat.mul(a, b)) : Nat}
3567
3568def mul_double(a, b):
3569 +a = a
3570 +b = b
3571 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : {Nat.mul(a, _) == Nat.double(Nat.mul(a, b)) : Nat}
3572 %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}
3573 mul_add(a, b, b)
3574
3575# Doubling distributes over truncated subtraction: double (a - b) = double a - double b.
3576law double_sub:
3577 for a: Nat
3578 for b: Nat
3579 {Nat.double(Nat.sub(a, b)) == Nat.sub(Nat.double(a), Nat.double(b)) : Nat}
3580
3581def double_sub(a, b):
3582 match a b:
3583 case 0n _:
3584 {==}
3585 case 1n+p 0n:
3586 {==}
3587 case 1n+p 1n+q:
3588 double_sub(p, q)
3589
3590# A natural is at most its double: n <= double n.
3591law le_double:
3592 for n: Nat
3593 le(n, Nat.double(n))
3594
3595def le_double(n):
3596 +n = n
3597 %Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n)) : le(n, _)
3598 le_add_right(n, n)
3599
3600# Doubling preserves the order: a <= b implies double a <= double b.
3601law double_le_double:
3602 for a: Nat
3603 for b: Nat
3604 for h: le(a, b)
3605 le(Nat.double(a), Nat.double(b))
3606
3607def double_le_double(a, b, h):
3608 +a = a
3609 +b = b
3610 +h = h
3611 %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), double_eq_add(a)) : le(_, Nat.double(b))
3612 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : le(Nat.add(a, a), _)
3613 add_le_add(a, a, b, b, h, h)
3614
3615# Doubling preserves the strict order: a < b implies double a < double b.
3616law double_lt_double:
3617 for a: Nat
3618 for b: Nat
3619 for h: lt(a, b)
3620 lt(Nat.double(a), Nat.double(b))
3621
3622def double_lt_double(a, b, h):
3623 +a = a
3624 +b = b
3625 +h = h
3626 %Equal.sym(Nat, Nat.double(a), Nat.add(a, a), double_eq_add(a)) : lt(_, Nat.double(b))
3627 %Equal.sym(Nat, Nat.double(b), Nat.add(b, b), double_eq_add(b)) : lt(Nat.add(a, a), _)
3628 add_lt_add(a, a, b, b, h, h)
3629
3630# Twice the half plus the parity is the number: double (n / 2) + n % 2 = n.
3631law double_div_two_add_mod_two:
3632 for n: Nat
3633 {Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) == n : Nat}
3634
3635def double_div_two_add_mod_two(n):
3636 +n = n
3637 %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}
3638 div_add_mod(n, 2n)
3639
3640# Adding the same amount on the right does not change the order test: a <= b tests as a + k <= b + k.
3641law add_le_add_iff_right:
3642 for a: Nat
3643 for b: Nat
3644 for k: Nat
3645 {Nat.is_le(a, b) == Nat.is_le(Nat.add(a, k), Nat.add(b, k)) : Bool}
3646
3647def add_le_add_iff_right(a, b, k):
3648 +a = a
3649 +b = b
3650 +k = k
3651 %add_comm(k, a) : {Nat.is_le(a, b) == Nat.is_le(_, Nat.add(b, k)) : Bool}
3652 %add_comm(k, b) : {Nat.is_le(a, b) == Nat.is_le(Nat.add(k, a), _) : Bool}
3653 add_le_add_iff_left(k, a, b)
3654
3655# Adding the same amount on the left does not change the equality test: a = b tests as k + a = k + b.
3656law add_left_cancel_iff:
3657 for k: Nat
3658 for -a: Nat
3659 for -b: Nat
3660 {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(k, a), Nat.add(k, b)) : Bool}
3661
3662def add_left_cancel_iff(k, a, b):
3663 match k:
3664 case 0n:
3665 {==}
3666 case 1n+p:
3667 add_left_cancel_iff(p, a, b)
3668
3669# Adding the same amount on the right does not change the equality test: a = b tests as a + k = b + k.
3670law add_right_cancel_iff:
3671 for a: Nat
3672 for b: Nat
3673 for k: Nat
3674 {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(a, k), Nat.add(b, k)) : Bool}
3675
3676def add_right_cancel_iff(a, b, k):
3677 +a = a
3678 +b = b
3679 +k = k
3680 %add_comm(k, a) : {Nat.is_eq(a, b) == Nat.is_eq(_, Nat.add(b, k)) : Bool}
3681 %add_comm(k, b) : {Nat.is_eq(a, b) == Nat.is_eq(Nat.add(k, a), _) : Bool}
3682 add_left_cancel_iff(k, a, b)
3683
3684# Subtracting from the left summand commutes with adding the right one: k <= n implies (n + m) - k = (n - k) + m.
3685law sub_add_comm:
3686 for n: Nat
3687 for m: Nat
3688 for k: Nat
3689 for h: le(k, n)
3690 {Nat.sub(Nat.add(n, m), k) == Nat.add(Nat.sub(n, k), m) : Nat}
3691
3692def sub_add_comm(n, m, k, h):
3693 +n = n
3694 +m = m
3695 +k = k
3696 %add_comm(m, n) : {Nat.sub(_, k) == Nat.add(Nat.sub(n, k), m) : Nat}
3697 %add_comm(m, Nat.sub(n, k)) : {Nat.sub(Nat.add(m, n), k) == _ : Nat}
3698 add_sub_assoc(k, n, h, m)
3699
3700# 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.
3701law le_min_of_le_of_le:
3702 for a: Nat
3703 for b: Nat
3704 for c: Nat
3705 for hb: le(a, b)
3706 for hc: le(a, c)
3707 le(a, Nat.min(b, c))
3708
3709def le_min_of_le_of_le(a, b, c, hb, hc):
3710 +a = a
3711 +b = b
3712 +c = c
3713 %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}
3714 %Equal.sym(Bool, Nat.is_le(a, b), True{}, hb) : {Bool.and(_, Nat.is_le(a, c)) == True{} : Bool}
3715 hc
3716
3717# An upper bound of both a and b bounds their maximum: a <= c and b <= c imply max a b <= c.
3718law max_le_of_le_of_le:
3719 for a: Nat
3720 for b: Nat
3721 for c: Nat
3722 for ha: le(a, c)
3723 for hb: le(b, c)
3724 le(Nat.max(a, b), c)
3725
3726def max_le_of_le_of_le(a, b, c, ha, hb):
3727 +a = a
3728 +b = b
3729 +c = c
3730 %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}
3731 %Equal.sym(Bool, Nat.is_le(a, c), True{}, ha) : {Bool.and(_, Nat.is_le(b, c)) == True{} : Bool}
3732 hb
3733
3734# Multiplying n by two gives n + n.
3735law mul_two:
3736 for n: Nat
3737 {Nat.mul(n, 2n) == Nat.add(n, n) : Nat}
3738
3739def mul_two(n):
3740 +n = n
3741 %mul_comm(2n, n) : {_ == Nat.add(n, n) : Nat}
3742 two_mul(n)
3743
3744# Squaring n gives n times n.
3745law pow_two:
3746 for n: Nat
3747 {Nat.pow(n, 2n) == Nat.mul(n, n) : Nat}
3748
3749def pow_two(n):
3750 +n = n
3751 %Equal.sym(Nat, Nat.mul(n, 1n), n, mul_one(n)) : {Nat.mul(n, _) == Nat.mul(n, n) : Nat}
3752 {==}
3753
3754# The minimum of two numbers is at most their maximum.
3755law min_le_max:
3756 for a: Nat
3757 for b: Nat
3758 {Nat.is_le(Nat.min(a, b), Nat.max(a, b)) == True{} : Bool}
3759
3760def min_le_max(a, b):
3761 +a = a
3762 +b = b
3763 le_trans(Nat.min(a, b), a, Nat.max(a, b), min_le_left(a, b), le_max_left(a, b))
3764
3765# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
3766
3767# Zero is a right identity for addition: x + 0 = x, reversed to rewrite toward the simple side.
3768law add_zero_sym:
3769 for x: Nat
3770 {x == Nat.add(x, 0n) : Nat}
3771
3772def add_zero_sym(x):
3773 Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x))
3774
3775# Zero is a left identity for addition: 0 + x = x, reversed to rewrite toward the simple side.
3776law zero_add_sym:
3777 for -x: Nat
3778 {x == Nat.add(0n, x) : Nat}
3779
3780def zero_add_sym(x):
3781 Equal.sym(Nat, Nat.add(0n, x), x, zero_add(x))
3782
3783# Adding a successor on the right: n + (m + 1) = (n + m) + 1, reversed to rewrite toward the simple side.
3784law add_succ_sym:
3785 for n: Nat
3786 for -m: Nat
3787 {1n+Nat.add(n, m) == Nat.add(n, 1n+m) : Nat}
3788
3789def add_succ_sym(n, m):
3790 Equal.sym(Nat, Nat.add(n, 1n+m), 1n+Nat.add(n, m), add_succ(n, m))
3791
3792# Adding a successor on the left: (n + 1) + m = (n + m) + 1, reversed to rewrite toward the simple side.
3793law succ_add_sym:
3794 for -n: Nat
3795 for -m: Nat
3796 {1n+Nat.add(n, m) == Nat.add(1n+n, m) : Nat}
3797
3798def succ_add_sym(n, m):
3799 Equal.sym(Nat, Nat.add(1n+n, m), 1n+Nat.add(n, m), succ_add(n, m))
3800
3801# Addition is commutative: n + m = m + n, reversed to rewrite toward the simple side.
3802law add_comm_sym:
3803 for n: Nat
3804 for m: Nat
3805 {Nat.add(m, n) == Nat.add(n, m) : Nat}
3806
3807def add_comm_sym(n, m):
3808 Equal.sym(Nat, Nat.add(n, m), Nat.add(m, n), add_comm(n, m))
3809
3810# Addition is associative: (a + b) + c = a + (b + c), reversed to rewrite toward the simple side.
3811law add_assoc_sym:
3812 for a: Nat
3813 for -b: Nat
3814 for -c: Nat
3815 {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}
3816
3817def add_assoc_sym(a, b, c):
3818 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(a, Nat.add(b, c)), add_assoc(a, b, c))
3819
3820# Left commutativity of addition: a + (b + c) = b + (a + c), reversed to rewrite toward the simple side.
3821law add_left_comm_sym:
3822 for a: Nat
3823 for b: Nat
3824 for -c: Nat
3825 {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
3826
3827def add_left_comm_sym(a, b, c):
3828 Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), add_left_comm(a, b, c))
3829
3830# Right commutativity of addition: (a + b) + c = (a + c) + b, reversed to rewrite toward the simple side.
3831law add_right_comm_sym:
3832 for a: Nat
3833 for b: Nat
3834 for c: Nat
3835 {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
3836
3837def add_right_comm_sym(a, b, c):
3838 Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), add_right_comm(a, b, c))
3839
3840# Four-way regrouping of a sum: (a + b) + (c + d) = (a + c) + (b + d), reversed to rewrite toward the simple side.
3841law add_add_add_comm_sym:
3842 for a: Nat
3843 for b: Nat
3844 for c: Nat
3845 for -d: Nat
3846 {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
3847
3848def add_add_add_comm_sym(a, b, c, d):
3849 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))
3850
3851# Zero absorbs multiplication on the right: x * 0 = 0, reversed to rewrite toward the simple side.
3852law mul_zero_sym:
3853 for x: Nat
3854 {0n == Nat.mul(x, 0n) : Nat}
3855
3856def mul_zero_sym(x):
3857 Equal.sym(Nat, Nat.mul(x, 0n), 0n, mul_zero(x))
3858
3859# Zero absorbs multiplication on the left: 0 * x = 0, reversed to rewrite toward the simple side.
3860law zero_mul_sym:
3861 for -x: Nat
3862 {0n == Nat.mul(0n, x) : Nat}
3863
3864def zero_mul_sym(x):
3865 Equal.sym(Nat, Nat.mul(0n, x), 0n, zero_mul(x))
3866
3867# One is a right identity for multiplication: x * 1 = x, reversed to rewrite toward the simple side.
3868law mul_one_sym:
3869 for x: Nat
3870 {x == Nat.mul(x, 1n) : Nat}
3871
3872def mul_one_sym(x):
3873 Equal.sym(Nat, Nat.mul(x, 1n), x, mul_one(x))
3874
3875# One is a left identity for multiplication: 1 * x = x, reversed to rewrite toward the simple side.
3876law one_mul_sym:
3877 for x: Nat
3878 {x == Nat.mul(1n, x) : Nat}
3879
3880def one_mul_sym(x):
3881 Equal.sym(Nat, Nat.mul(1n, x), x, one_mul(x))
3882
3883# Multiplying by a successor on the right: n * (m + 1) = n * m + n, reversed to rewrite toward the simple side.
3884law mul_succ_sym:
3885 for n: Nat
3886 for m: Nat
3887 {Nat.add(Nat.mul(n, m), n) == Nat.mul(n, 1n+m) : Nat}
3888
3889def mul_succ_sym(n, m):
3890 Equal.sym(Nat, Nat.mul(n, 1n+m), Nat.add(Nat.mul(n, m), n), mul_succ(n, m))
3891
3892# Multiplying by a successor on the left: (n + 1) * m = n * m + m, reversed to rewrite toward the simple side.
3893law succ_mul_sym:
3894 for n: Nat
3895 for m: Nat
3896 {Nat.add(Nat.mul(n, m), m) == Nat.mul(1n+n, m) : Nat}
3897
3898def succ_mul_sym(n, m):
3899 Equal.sym(Nat, Nat.mul(1n+n, m), Nat.add(Nat.mul(n, m), m), succ_mul(n, m))
3900
3901# Multiplication is commutative: n * m = m * n, reversed to rewrite toward the simple side.
3902law mul_comm_sym:
3903 for n: Nat
3904 for m: Nat
3905 {Nat.mul(m, n) == Nat.mul(n, m) : Nat}
3906
3907def mul_comm_sym(n, m):
3908 Equal.sym(Nat, Nat.mul(n, m), Nat.mul(m, n), mul_comm(n, m))
3909
3910# Multiplication distributes over addition on the right: (a + b) * c = a * c + b * c, reversed to rewrite toward the simple side.
3911law add_mul_sym:
3912 for a: Nat
3913 for -b: Nat
3914 for c: Nat
3915 {Nat.add(Nat.mul(a, c), Nat.mul(b, c)) == Nat.mul(Nat.add(a, b), c) : Nat}
3916
3917def add_mul_sym(a, b, c):
3918 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))
3919
3920# Multiplication distributes over addition on the left: a * (b + c) = a * b + a * c, reversed to rewrite toward the simple side.
3921law mul_add_sym:
3922 for a: Nat
3923 for b: Nat
3924 for c: Nat
3925 {Nat.add(Nat.mul(a, b), Nat.mul(a, c)) == Nat.mul(a, Nat.add(b, c)) : Nat}
3926
3927def mul_add_sym(a, b, c):
3928 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))
3929
3930# Multiplication is associative: (a * b) * c = a * (b * c), reversed to rewrite toward the simple side.
3931law mul_assoc_sym:
3932 for a: Nat
3933 for b: Nat
3934 for c: Nat
3935 {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}
3936
3937def mul_assoc_sym(a, b, c):
3938 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(a, Nat.mul(b, c)), mul_assoc(a, b, c))
3939
3940# Subtracting zero changes nothing: n - 0 = n, reversed to rewrite toward the simple side.
3941law sub_zero_sym:
3942 for n: Nat
3943 {n == Nat.sub(n, 0n) : Nat}
3944
3945def sub_zero_sym(n):
3946 Equal.sym(Nat, Nat.sub(n, 0n), n, sub_zero(n))
3947
3948# Truncated subtraction from zero is zero: 0 - n = 0, reversed to rewrite toward the simple side.
3949law zero_sub_sym:
3950 for n: Nat
3951 {0n == Nat.sub(0n, n) : Nat}
3952
3953def zero_sub_sym(n):
3954 Equal.sym(Nat, Nat.sub(0n, n), 0n, zero_sub(n))
3955
3956# A natural minus itself is zero: n - n = 0, reversed to rewrite toward the simple side.
3957law sub_self_sym:
3958 for n: Nat
3959 {0n == Nat.sub(n, n) : Nat}
3960
3961def sub_self_sym(n):
3962 Equal.sym(Nat, Nat.sub(n, n), 0n, sub_self(n))
3963
3964# Subtracting successors: (n + 1) - (m + 1) = n - m, reversed to rewrite toward the simple side.
3965law succ_sub_succ_sym:
3966 for -n: Nat
3967 for -m: Nat
3968 {Nat.sub(n, m) == Nat.sub(1n+n, 1n+m) : Nat}
3969
3970def succ_sub_succ_sym(n, m):
3971 Equal.sym(Nat, Nat.sub(1n+n, 1n+m), Nat.sub(n, m), succ_sub_succ(n, m))
3972
3973# Adding then subtracting m cancels: (n + m) - m = n, reversed to rewrite toward the simple side.
3974law add_sub_cancel_sym:
3975 for n: Nat
3976 for m: Nat
3977 {n == Nat.sub(Nat.add(n, m), m) : Nat}
3978
3979def add_sub_cancel_sym(n, m):
3980 Equal.sym(Nat, Nat.sub(Nat.add(n, m), m), n, add_sub_cancel(n, m))
3981
3982# Adding then subtracting n cancels: (n + m) - n = m, reversed to rewrite toward the simple side.
3983law add_sub_cancel_left_sym:
3984 for n: Nat
3985 for m: Nat
3986 {m == Nat.sub(Nat.add(n, m), n) : Nat}
3987
3988def add_sub_cancel_left_sym(n, m):
3989 Equal.sym(Nat, Nat.sub(Nat.add(n, m), n), m, add_sub_cancel_left(n, m))
3990
3991# Subtracting twice is subtracting the sum: (n - m) - k = n - (m + k), reversed to rewrite toward the simple side.
3992law sub_sub_sym:
3993 for n: Nat
3994 for m: Nat
3995 for k: Nat
3996 {Nat.sub(n, Nat.add(m, k)) == Nat.sub(Nat.sub(n, m), k) : Nat}
3997
3998def sub_sub_sym(n, m, k):
3999 Equal.sym(Nat, Nat.sub(Nat.sub(n, m), k), Nat.sub(n, Nat.add(m, k)), sub_sub(n, m, k))
4000
4001# 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.
4002law div_mod_eq_sym:
4003 for +a: Nat
4004 for +b: Nat
4005 {a == Nat.add(Nat.mul(Nat.div(a, 1n+b), 1n+b), Nat.mod(a, 1n+b)) : Nat}
4006
4007def div_mod_eq_sym(a, b):
4008 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))
4009
4010# Adding the divisor adds one to the quotient: ((1 + b) + a) / (1 + b) = 1 + a / (1 + b), reversed to rewrite toward the simple side.
4011law add_div_left_sym:
4012 for +a: Nat
4013 for +b: Nat
4014 {1n+Nat.div(a, 1n+b) == Nat.div(Nat.add(1n+b, a), 1n+b) : Nat}
4015
4016def add_div_left_sym(a, b):
4017 Equal.sym(Nat, Nat.div(Nat.add(1n+b, a), 1n+b), 1n+Nat.div(a, 1n+b), add_div_left(a, b))
4018
4019# A quotient is compared by multiplying back: n <= a / (1 + b) tests as n * (1 + b) <= a, reversed to rewrite toward the simple side.
4020law le_div_iff_mul_le_sym:
4021 for n: Nat
4022 for +a: Nat
4023 for +b: Nat
4024 {Nat.is_le(Nat.mul(n, 1n+b), a) == Nat.is_le(n, Nat.div(a, 1n+b)) : Bool}
4025
4026def le_div_iff_mul_le_sym(n, a, b):
4027 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))
4028
4029# Minimum is commutative, reversed to rewrite toward the simple side.
4030law min_comm_sym:
4031 for a: Nat
4032 for b: Nat
4033 {Nat.min(b, a) == Nat.min(a, b) : Nat}
4034
4035def min_comm_sym(a, b):
4036 Equal.sym(Nat, Nat.min(a, b), Nat.min(b, a), min_comm(a, b))
4037
4038# Maximum is commutative, reversed to rewrite toward the simple side.
4039law max_comm_sym:
4040 for a: Nat
4041 for b: Nat
4042 {Nat.max(b, a) == Nat.max(a, b) : Nat}
4043
4044def max_comm_sym(a, b):
4045 Equal.sym(Nat, Nat.max(a, b), Nat.max(b, a), max_comm(a, b))
4046
4047# The minimum of a natural and itself is itself, reversed to rewrite toward the simple side.
4048law min_self_sym:
4049 for a: Nat
4050 {a == Nat.min(a, a) : Nat}
4051
4052def min_self_sym(a):
4053 Equal.sym(Nat, Nat.min(a, a), a, min_self(a))
4054
4055# The maximum of a natural and itself is itself, reversed to rewrite toward the simple side.
4056law max_self_sym:
4057 for a: Nat
4058 {a == Nat.max(a, a) : Nat}
4059
4060def max_self_sym(a):
4061 Equal.sym(Nat, Nat.max(a, a), a, max_self(a))
4062
4063# The minimum with zero is zero: min(a, 0) = 0, reversed to rewrite toward the simple side.
4064law min_zero_sym:
4065 for a: Nat
4066 {0n == Nat.min(a, 0n) : Nat}
4067
4068def min_zero_sym(a):
4069 Equal.sym(Nat, Nat.min(a, 0n), 0n, min_zero(a))
4070
4071# The minimum with zero is zero: min(0, a) = 0, reversed to rewrite toward the simple side.
4072law zero_min_sym:
4073 for a: Nat
4074 {0n == Nat.min(0n, a) : Nat}
4075
4076def zero_min_sym(a):
4077 Equal.sym(Nat, Nat.min(0n, a), 0n, zero_min(a))
4078
4079# Zero is an identity for maximum: max(a, 0) = a, reversed to rewrite toward the simple side.
4080law max_zero_sym:
4081 for a: Nat
4082 {a == Nat.max(a, 0n) : Nat}
4083
4084def max_zero_sym(a):
4085 Equal.sym(Nat, Nat.max(a, 0n), a, max_zero(a))
4086
4087# Zero is an identity for maximum: max(0, a) = a, reversed to rewrite toward the simple side.
4088law zero_max_sym:
4089 for a: Nat
4090 {a == Nat.max(0n, a) : Nat}
4091
4092def zero_max_sym(a):
4093 Equal.sym(Nat, Nat.max(0n, a), a, zero_max(a))
4094
4095# Minimum is associative, reversed to rewrite toward the simple side.
4096law min_assoc_sym:
4097 for a: Nat
4098 for b: Nat
4099 for c: Nat
4100 {Nat.min(a, Nat.min(b, c)) == Nat.min(Nat.min(a, b), c) : Nat}
4101
4102def min_assoc_sym(a, b, c):
4103 Equal.sym(Nat, Nat.min(Nat.min(a, b), c), Nat.min(a, Nat.min(b, c)), min_assoc(a, b, c))
4104
4105# Maximum is associative, reversed to rewrite toward the simple side.
4106law max_assoc_sym:
4107 for a: Nat
4108 for b: Nat
4109 for c: Nat
4110 {Nat.max(a, Nat.max(b, c)) == Nat.max(Nat.max(a, b), c) : Nat}
4111
4112def max_assoc_sym(a, b, c):
4113 Equal.sym(Nat, Nat.max(Nat.max(a, b), c), Nat.max(a, Nat.max(b, c)), max_assoc(a, b, c))
4114
4115# The minimum plus the maximum is the sum: min(a, b) + max(a, b) = a + b, reversed to rewrite toward the simple side.
4116law min_add_max_sym:
4117 for a: Nat
4118 for b: Nat
4119 {Nat.add(a, b) == Nat.add(Nat.min(a, b), Nat.max(a, b)) : Nat}
4120
4121def min_add_max_sym(a, b):
4122 Equal.sym(Nat, Nat.add(Nat.min(a, b), Nat.max(a, b)), Nat.add(a, b), min_add_max(a, b))
4123
4124# Any natural to the power zero is one, reversed to rewrite toward the simple side.
4125law pow_zero_sym:
4126 for -a: Nat
4127 {1n == Nat.pow(a, 0n) : Nat}
4128
4129def pow_zero_sym(a):
4130 Equal.sym(Nat, Nat.pow(a, 0n), 1n, pow_zero(a))
4131
4132# A power with a successor exponent: a^(n+1) = a * a^n, reversed to rewrite toward the simple side.
4133law pow_succ_sym:
4134 for -a: Nat
4135 for -n: Nat
4136 {Nat.mul(a, Nat.pow(a, n)) == Nat.pow(a, 1n+n) : Nat}
4137
4138def pow_succ_sym(a, n):
4139 Equal.sym(Nat, Nat.pow(a, 1n+n), Nat.mul(a, Nat.pow(a, n)), pow_succ(a, n))
4140
4141# Any natural to the power one is itself, reversed to rewrite toward the simple side.
4142law pow_one_sym:
4143 for a: Nat
4144 {a == Nat.pow(a, 1n) : Nat}
4145
4146def pow_one_sym(a):
4147 Equal.sym(Nat, Nat.pow(a, 1n), a, pow_one(a))
4148
4149# One to any power is one, reversed to rewrite toward the simple side.
4150law one_pow_sym:
4151 for n: Nat
4152 {1n == Nat.pow(1n, n) : Nat}
4153
4154def one_pow_sym(n):
4155 Equal.sym(Nat, Nat.pow(1n, n), 1n, one_pow(n))
4156
4157# Exponents add under multiplication: a^(m+n) = a^m * a^n, reversed to rewrite toward the simple side.
4158law pow_add_sym:
4159 for a: Nat
4160 for m: Nat
4161 for n: Nat
4162 {Nat.mul(Nat.pow(a, m), Nat.pow(a, n)) == Nat.pow(a, Nat.add(m, n)) : Nat}
4163
4164def pow_add_sym(a, m, n):
4165 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))
4166
4167# Doubling is adding a natural to itself, reversed to rewrite toward the simple side.
4168law double_eq_add_sym:
4169 for n: Nat
4170 {Nat.add(n, n) == Nat.double(n) : Nat}
4171
4172def double_eq_add_sym(n):
4173 Equal.sym(Nat, Nat.double(n), Nat.add(n, n), double_eq_add(n))
4174
4175# Every natural tests equal to itself, reversed to rewrite toward the simple side.
4176law is_eq_refl_sym:
4177 for n: Nat
4178 {True{} == Nat.is_eq(n, n) : Bool}
4179
4180def is_eq_refl_sym(n):
4181 Equal.sym(Bool, Nat.is_eq(n, n), True{}, is_eq_refl(n))
4182
4183# The equality test is symmetric, reversed to rewrite toward the simple side.
4184law is_eq_comm_sym:
4185 for a: Nat
4186 for b: Nat
4187 {Nat.is_eq(b, a) == Nat.is_eq(a, b) : Bool}
4188
4189def is_eq_comm_sym(a, b):
4190 Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_comm(a, b))
4191
4192# A >= b tests the same as b <= a, reversed to rewrite toward the simple side.
4193law is_ge_eq_is_le_sym:
4194 for a: Nat
4195 for b: Nat
4196 {Nat.is_le(b, a) == Nat.is_ge(a, b) : Bool}
4197
4198def is_ge_eq_is_le_sym(a, b):
4199 Equal.sym(Bool, Nat.is_ge(a, b), Nat.is_le(b, a), is_ge_eq_is_le(a, b))
4200
4201# A > b tests the same as b < a, reversed to rewrite toward the simple side.
4202law is_gt_eq_is_lt_sym:
4203 for a: Nat
4204 for b: Nat
4205 {Nat.is_lt(b, a) == Nat.is_gt(a, b) : Bool}
4206
4207def is_gt_eq_is_lt_sym(a, b):
4208 Equal.sym(Bool, Nat.is_gt(a, b), Nat.is_lt(b, a), is_gt_eq_is_lt(a, b))
4209
4210# A < b tests the same as a + 1 <= b, reversed to rewrite toward the simple side.
4211law is_lt_eq_succ_le_sym:
4212 for a: Nat
4213 for b: Nat
4214 {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
4215
4216def is_lt_eq_succ_le_sym(a, b):
4217 Equal.sym(Bool, Nat.is_lt(a, b), Nat.is_le(1n+a, b), is_lt_eq_succ_le(a, b))
4218
4219# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
4220law not_is_le_sym:
4221 for a: Nat
4222 for b: Nat
4223 {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}
4224
4225def not_is_le_sym(a, b):
4226 Equal.sym(Bool, Bool.not(Nat.is_le(a, b)), Nat.is_lt(b, a), not_is_le(a, b))
4227
4228# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
4229law not_is_lt_sym:
4230 for a: Nat
4231 for b: Nat
4232 {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}
4233
4234def not_is_lt_sym(a, b):
4235 Equal.sym(Bool, Bool.not(Nat.is_lt(a, b)), Nat.is_le(b, a), not_is_lt(a, b))
4236
4237# 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.
4238law add_le_add_iff_left_sym:
4239 for k: Nat
4240 for -a: Nat
4241 for -b: Nat
4242 {Nat.is_le(Nat.add(k, a), Nat.add(k, b)) == Nat.is_le(a, b) : Bool}
4243
4244def add_le_add_iff_left_sym(k, a, b):
4245 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))
4246
4247# 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.
4248law le_and_le_sub_iff_add_le_sym:
4249 for a: Nat
4250 for -b: Nat
4251 for c: Nat
4252 {Nat.is_le(Nat.add(a, b), c) == Bool.and(Nat.is_le(a, c), Nat.is_le(b, Nat.sub(c, a))) : Bool}
4253
4254def le_and_le_sub_iff_add_le_sym(a, b, c):
4255 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))
4256
4257# 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.
4258law min_le_iff_sym:
4259 for a: Nat
4260 for b: Nat
4261 for c: Nat
4262 {Bool.or(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.min(a, b), c) : Bool}
4263
4264def min_le_iff_sym(a, b, c):
4265 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))
4266
4267# 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.
4268law lt_max_iff_sym:
4269 for a: Nat
4270 for b: Nat
4271 for c: Nat
4272 {Bool.or(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.max(b, c)) : Bool}
4273
4274def lt_max_iff_sym(a, b, c):
4275 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))
4276
4277# Comparing against a difference is comparing the sum: a < c - b tests as b + a < c, reversed to rewrite toward the simple side.
4278law lt_sub_iff_add_lt_sym:
4279 for a: Nat
4280 for b: Nat
4281 for c: Nat
4282 {Nat.is_lt(Nat.add(b, a), c) == Nat.is_lt(a, Nat.sub(c, b)) : Bool}
4283
4284def lt_sub_iff_add_lt_sym(a, b, c):
4285 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))
4286
4287# Zero divided by anything is zero: 0 / b = 0, reversed to rewrite toward the simple side.
4288law zero_div_sym:
4289 for b: Nat
4290 {0n == Nat.div(0n, b) : Nat}
4291
4292def zero_div_sym(b):
4293 Equal.sym(Nat, Nat.div(0n, b), 0n, zero_div(b))
4294
4295# Zero modulo anything is zero: 0 % b = 0, reversed to rewrite toward the simple side.
4296law zero_mod_sym:
4297 for b: Nat
4298 {0n == Nat.mod(0n, b) : Nat}
4299
4300def zero_mod_sym(b):
4301 Equal.sym(Nat, Nat.mod(0n, b), 0n, zero_mod(b))
4302
4303# Dividing by one changes nothing: a / 1 = a, reversed to rewrite toward the simple side.
4304law div_one_sym:
4305 for a: Nat
4306 {a == Nat.div(a, 1n) : Nat}
4307
4308def div_one_sym(a):
4309 Equal.sym(Nat, Nat.div(a, 1n), a, div_one(a))
4310
4311# Any natural modulo one is zero: a % 1 = 0, reversed to rewrite toward the simple side.
4312law mod_one_sym:
4313 for a: Nat
4314 {0n == Nat.mod(a, 1n) : Nat}
4315
4316def mod_one_sym(a):
4317 Equal.sym(Nat, Nat.mod(a, 1n), 0n, mod_one(a))
4318
4319# A natural modulo itself is zero: n % n = 0, reversed to rewrite toward the simple side.
4320law mod_self_sym:
4321 for n: Nat
4322 {0n == Nat.mod(n, n) : Nat}
4323
4324def mod_self_sym(n):
4325 Equal.sym(Nat, Nat.mod(n, n), 0n, mod_self(n))
4326
4327# A positive natural divided by itself is one: (1 + b) / (1 + b) = 1, reversed to rewrite toward the simple side.
4328law div_self_sym:
4329 for b: Nat
4330 {1n == Nat.div(1n+b, 1n+b) : Nat}
4331
4332def div_self_sym(b):
4333 Equal.sym(Nat, Nat.div(1n+b, 1n+b), 1n, div_self(b))
4334
4335# Taking a remainder twice is taking it once: (a % n) % n = a % n, reversed to rewrite toward the simple side.
4336law mod_mod_sym:
4337 for a: Nat
4338 for n: Nat
4339 {Nat.mod(a, n) == Nat.mod(Nat.mod(a, n), n) : Nat}
4340
4341def mod_mod_sym(a, n):
4342 Equal.sym(Nat, Nat.mod(Nat.mod(a, n), n), Nat.mod(a, n), mod_mod(a, n))
4343
4344# Adding the divisor does not change the remainder: (b + a) % b = a % b, reversed to rewrite toward the simple side.
4345law add_mod_left_sym:
4346 for a: Nat
4347 for b: Nat
4348 {Nat.mod(a, b) == Nat.mod(Nat.add(b, a), b) : Nat}
4349
4350def add_mod_left_sym(a, b):
4351 Equal.sym(Nat, Nat.mod(Nat.add(b, a), b), Nat.mod(a, b), add_mod_left(a, b))
4352
4353# Multiplying by a positive divisor then dividing by it cancels: (a * (1 + b)) / (1 + b) = a, reversed to rewrite toward the simple side.
4354law mul_div_cancel_sym:
4355 for a: Nat
4356 for b: Nat
4357 {a == Nat.div(Nat.mul(a, 1n+b), 1n+b) : Nat}
4358
4359def mul_div_cancel_sym(a, b):
4360 Equal.sym(Nat, Nat.div(Nat.mul(a, 1n+b), 1n+b), a, mul_div_cancel(a, b))
4361
4362# 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.
4363law mul_div_cancel_left_sym:
4364 for a: Nat
4365 for b: Nat
4366 {a == Nat.div(Nat.mul(1n+b, a), 1n+b) : Nat}
4367
4368def mul_div_cancel_left_sym(a, b):
4369 Equal.sym(Nat, Nat.div(Nat.mul(1n+b, a), 1n+b), a, mul_div_cancel_left(a, b))
4370
4371# A multiple of b leaves no remainder modulo b: (a * b) % b = 0, reversed to rewrite toward the simple side.
4372law mul_mod_left_sym:
4373 for a: Nat
4374 for b: Nat
4375 {0n == Nat.mod(Nat.mul(a, b), b) : Nat}
4376
4377def mul_mod_left_sym(a, b):
4378 Equal.sym(Nat, Nat.mod(Nat.mul(a, b), b), 0n, mul_mod_left(a, b))
4379
4380# A multiple of a leaves no remainder modulo a: (a * b) % a = 0, reversed to rewrite toward the simple side.
4381law mul_mod_right_sym:
4382 for a: Nat
4383 for b: Nat
4384 {0n == Nat.mod(Nat.mul(a, b), a) : Nat}
4385
4386def mul_mod_right_sym(a, b):
4387 Equal.sym(Nat, Nat.mod(Nat.mul(a, b), a), 0n, mul_mod_right(a, b))
4388
4389# The remainder plus the divisor times the quotient is the dividend: a % b + b * (a / b) = a, reversed to rewrite toward the simple side.
4390law mod_add_div_sym:
4391 for a: Nat
4392 for b: Nat
4393 {a == Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))) : Nat}
4394
4395def mod_add_div_sym(a, b):
4396 Equal.sym(Nat, Nat.add(Nat.mod(a, b), Nat.mul(b, Nat.div(a, b))), a, mod_add_div(a, b))
4397
4398# Left commutativity of multiplication: a * (b * c) = b * (a * c), reversed to rewrite toward the simple side.
4399law mul_left_comm_sym:
4400 for a: Nat
4401 for b: Nat
4402 for c: Nat
4403 {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
4404
4405def mul_left_comm_sym(a, b, c):
4406 Equal.sym(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)), mul_left_comm(a, b, c))
4407
4408# Right commutativity of multiplication: (a * b) * c = (a * c) * b, reversed to rewrite toward the simple side.
4409law mul_right_comm_sym:
4410 for a: Nat
4411 for b: Nat
4412 for c: Nat
4413 {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
4414
4415def mul_right_comm_sym(a, b, c):
4416 Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(Nat.mul(a, c), b), mul_right_comm(a, b, c))
4417
4418# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d), reversed to rewrite toward the simple side.
4419law mul_mul_mul_comm_sym:
4420 for a: Nat
4421 for b: Nat
4422 for c: Nat
4423 for d: Nat
4424 {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
4425
4426def mul_mul_mul_comm_sym(a, b, c, d):
4427 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))
4428
4429# Zero to a positive power is zero: 0^(n+1) = 0, reversed to rewrite toward the simple side.
4430law zero_pow_sym:
4431 for -n: Nat
4432 {0n == Nat.pow(0n, 1n+n) : Nat}
4433
4434def zero_pow_sym(n):
4435 Equal.sym(Nat, Nat.pow(0n, 1n+n), 0n, zero_pow(n))
4436
4437# 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.
4438law mul_pow_sym:
4439 for +a: Nat
4440 for +b: Nat
4441 for n: Nat
4442 {Nat.mul(Nat.pow(a, n), Nat.pow(b, n)) == Nat.pow(Nat.mul(a, b), n) : Nat}
4443
4444def mul_pow_sym(a, b, n):
4445 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))
4446
4447# Exponents multiply under repeated powers: a^(m * n) = (a^m)^n, reversed to rewrite toward the simple side.
4448law pow_mul_sym:
4449 for a: Nat
4450 for m: Nat
4451 for n: Nat
4452 {Nat.pow(Nat.pow(a, m), n) == Nat.pow(a, Nat.mul(m, n)) : Nat}
4453
4454def pow_mul_sym(a, m, n):
4455 Equal.sym(Nat, Nat.pow(a, Nat.mul(m, n)), Nat.pow(Nat.pow(a, m), n), pow_mul(a, m, n))
4456
4457# A common left summand cancels in a difference: (k + n) - (k + m) = n - m, reversed to rewrite toward the simple side.
4458law add_sub_add_left_sym:
4459 for k: Nat
4460 for -n: Nat
4461 for -m: Nat
4462 {Nat.sub(n, m) == Nat.sub(Nat.add(k, n), Nat.add(k, m)) : Nat}
4463
4464def add_sub_add_left_sym(k, n, m):
4465 Equal.sym(Nat, Nat.sub(Nat.add(k, n), Nat.add(k, m)), Nat.sub(n, m), add_sub_add_left(k, n, m))
4466
4467# A common right summand cancels in a difference: (n + k) - (m + k) = n - m, reversed to rewrite toward the simple side.
4468law add_sub_add_right_sym:
4469 for n: Nat
4470 for k: Nat
4471 for m: Nat
4472 {Nat.sub(n, m) == Nat.sub(Nat.add(n, k), Nat.add(m, k)) : Nat}
4473
4474def add_sub_add_right_sym(n, k, m):
4475 Equal.sym(Nat, Nat.sub(Nat.add(n, k), Nat.add(m, k)), Nat.sub(n, m), add_sub_add_right(n, k, m))
4476
4477# Multiplication distributes over subtraction on the right: (n - m) * k = n * k - m * k, reversed to rewrite toward the simple side.
4478law sub_mul_sym:
4479 for n: Nat
4480 for m: Nat
4481 for k: Nat
4482 {Nat.sub(Nat.mul(n, k), Nat.mul(m, k)) == Nat.mul(Nat.sub(n, m), k) : Nat}
4483
4484def sub_mul_sym(n, m, k):
4485 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))
4486
4487# Multiplication distributes over subtraction on the left: n * (m - k) = n * m - n * k, reversed to rewrite toward the simple side.
4488law mul_sub_sym:
4489 for n: Nat
4490 for m: Nat
4491 for k: Nat
4492 {Nat.sub(Nat.mul(n, m), Nat.mul(n, k)) == Nat.mul(n, Nat.sub(m, k)) : Nat}
4493
4494def mul_sub_sym(n, m, k):
4495 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))
4496
4497# 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.
4498law le_min_sym:
4499 for a: Nat
4500 for b: Nat
4501 for c: Nat
4502 {Bool.and(Nat.is_le(a, b), Nat.is_le(a, c)) == Nat.is_le(a, Nat.min(b, c)) : Bool}
4503
4504def le_min_sym(a, b, c):
4505 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))
4506
4507# 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.
4508law max_le_sym:
4509 for a: Nat
4510 for b: Nat
4511 for c: Nat
4512 {Bool.and(Nat.is_le(a, c), Nat.is_le(b, c)) == Nat.is_le(Nat.max(a, b), c) : Bool}
4513
4514def max_le_sym(a, b, c):
4515 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))
4516
4517# Below a successor means at most: m < n + 1 tests as m <= n, reversed to rewrite toward the simple side.
4518law lt_succ_iff_sym:
4519 for m: Nat
4520 for n: Nat
4521 {Nat.is_le(m, n) == Nat.is_lt(m, 1n+n) : Bool}
4522
4523def lt_succ_iff_sym(m, n):
4524 Equal.sym(Bool, Nat.is_lt(m, 1n+n), Nat.is_le(m, n), lt_succ_iff(m, n))
4525
4526# At most means below or equal: a <= b tests as a < b or a = b, reversed to rewrite toward the simple side.
4527law le_iff_lt_or_eq_sym:
4528 for a: Nat
4529 for b: Nat
4530 {Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)) == Nat.is_le(a, b) : Bool}
4531
4532def le_iff_lt_or_eq_sym(a, b):
4533 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))
4534
4535# Below means at most and different: a < b tests as a <= b and not a = b, reversed to rewrite toward the simple side.
4536law lt_iff_le_and_ne_sym:
4537 for a: Nat
4538 for b: Nat
4539 {Bool.and(Nat.is_le(a, b), Bool.not(Nat.is_eq(a, b))) == Nat.is_lt(a, b) : Bool}
4540
4541def lt_iff_le_and_ne_sym(a, b):
4542 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))
4543
4544# 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.
4545law add_lt_add_iff_left_sym:
4546 for k: Nat
4547 for -a: Nat
4548 for -b: Nat
4549 {Nat.is_lt(Nat.add(k, a), Nat.add(k, b)) == Nat.is_lt(a, b) : Bool}
4550
4551def add_lt_add_iff_left_sym(k, a, b):
4552 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))
4553
4554# 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.
4555law add_lt_add_iff_right_sym:
4556 for a: Nat
4557 for b: Nat
4558 for k: Nat
4559 {Nat.is_lt(Nat.add(a, k), Nat.add(b, k)) == Nat.is_lt(a, b) : Bool}
4560
4561def add_lt_add_iff_right_sym(a, b, k):
4562 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))
4563
4564# 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.
4565law min_max_distrib_left_sym:
4566 for a: Nat
4567 for b: Nat
4568 for c: Nat
4569 {Nat.max(Nat.min(a, b), Nat.min(a, c)) == Nat.min(a, Nat.max(b, c)) : Nat}
4570
4571def min_max_distrib_left_sym(a, b, c):
4572 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))
4573
4574# 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.
4575law max_min_distrib_left_sym:
4576 for a: Nat
4577 for b: Nat
4578 for c: Nat
4579 {Nat.min(Nat.max(a, b), Nat.max(a, c)) == Nat.max(a, Nat.min(b, c)) : Nat}
4580
4581def max_min_distrib_left_sym(a, b, c):
4582 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))
4583
4584# A common left summand leaves the minimum: min (a + b) (a + c) = a + min b c, reversed to rewrite toward the simple side.
4585law min_add_add_left_sym:
4586 for a: Nat
4587 for -b: Nat
4588 for -c: Nat
4589 {Nat.add(a, Nat.min(b, c)) == Nat.min(Nat.add(a, b), Nat.add(a, c)) : Nat}
4590
4591def min_add_add_left_sym(a, b, c):
4592 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))
4593
4594# A common right summand leaves the minimum: min (a + c) (b + c) = min a b + c, reversed to rewrite toward the simple side.
4595law min_add_add_right_sym:
4596 for a: Nat
4597 for b: Nat
4598 for c: Nat
4599 {Nat.add(Nat.min(a, b), c) == Nat.min(Nat.add(a, c), Nat.add(b, c)) : Nat}
4600
4601def min_add_add_right_sym(a, b, c):
4602 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))
4603
4604# A common left summand leaves the maximum: max (a + b) (a + c) = a + max b c, reversed to rewrite toward the simple side.
4605law max_add_add_left_sym:
4606 for a: Nat
4607 for -b: Nat
4608 for -c: Nat
4609 {Nat.add(a, Nat.max(b, c)) == Nat.max(Nat.add(a, b), Nat.add(a, c)) : Nat}
4610
4611def max_add_add_left_sym(a, b, c):
4612 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))
4613
4614# A common right summand leaves the maximum: max (a + c) (b + c) = max a b + c, reversed to rewrite toward the simple side.
4615law max_add_add_right_sym:
4616 for a: Nat
4617 for b: Nat
4618 for c: Nat
4619 {Nat.add(Nat.max(a, b), c) == Nat.max(Nat.add(a, c), Nat.add(b, c)) : Nat}
4620
4621def max_add_add_right_sym(a, b, c):
4622 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))
4623
4624# 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.
4625law min_lt_iff_sym:
4626 for a: Nat
4627 for b: Nat
4628 for c: Nat
4629 {Bool.or(Nat.is_lt(a, c), Nat.is_lt(b, c)) == Nat.is_lt(Nat.min(a, b), c) : Bool}
4630
4631def min_lt_iff_sym(a, b, c):
4632 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))
4633
4634# 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.
4635law lt_min_iff_sym:
4636 for a: Nat
4637 for b: Nat
4638 for c: Nat
4639 {Bool.and(Nat.is_lt(a, b), Nat.is_lt(a, c)) == Nat.is_lt(a, Nat.min(b, c)) : Bool}
4640
4641def lt_min_iff_sym(a, b, c):
4642 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))
4643
4644# 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.
4645law max_lt_iff_sym:
4646 for a: Nat
4647 for b: Nat
4648 for c: Nat
4649 {Bool.and(Nat.is_lt(a, c), Nat.is_lt(b, c)) == Nat.is_lt(Nat.max(a, b), c) : Bool}
4650
4651def max_lt_iff_sym(a, b, c):
4652 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))
4653
4654# 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.
4655law le_max_iff_sym:
4656 for a: Nat
4657 for b: Nat
4658 for c: Nat
4659 {Bool.or(Nat.is_le(a, b), Nat.is_le(a, c)) == Nat.is_le(a, Nat.max(b, c)) : Bool}
4660
4661def le_max_iff_sym(a, b, c):
4662 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))
4663
4664# 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.
4665law add_mul_div_right_sym:
4666 for x: Nat
4667 for z: Nat
4668 for b: Nat
4669 {Nat.add(Nat.div(x, 1n+b), z) == Nat.div(Nat.add(x, Nat.mul(z, 1n+b)), 1n+b) : Nat}
4670
4671def add_mul_div_right_sym(x, z, b):
4672 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))
4673
4674# 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.
4675law add_mul_div_left_sym:
4676 for x: Nat
4677 for z: Nat
4678 for b: Nat
4679 {Nat.add(Nat.div(x, 1n+b), z) == Nat.div(Nat.add(x, Nat.mul(1n+b, z)), 1n+b) : Nat}
4680
4681def add_mul_div_left_sym(x, z, b):
4682 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))
4683
4684# Adding a multiple of the divisor keeps the remainder: (a + c * b) % b = a % b, reversed to rewrite toward the simple side.
4685law add_mul_mod_self_right_sym:
4686 for a: Nat
4687 for b: Nat
4688 for c: Nat
4689 {Nat.mod(a, b) == Nat.mod(Nat.add(a, Nat.mul(c, b)), b) : Nat}
4690
4691def add_mul_mod_self_right_sym(a, b, c):
4692 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))
4693
4694# Adding a multiple of the divisor keeps the remainder: (a + b * c) % b = a % b, reversed to rewrite toward the simple side.
4695law add_mul_mod_self_left_sym:
4696 for a: Nat
4697 for b: Nat
4698 for c: Nat
4699 {Nat.mod(a, b) == Nat.mod(Nat.add(a, Nat.mul(b, c)), b) : Nat}
4700
4701def add_mul_mod_self_left_sym(a, b, c):
4702 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))
4703
4704# A remainder modulo two is zero or one, reversed to rewrite toward the simple side.
4705law mod_two_eq_zero_or_one_sym:
4706 for n: Nat
4707 {True{} == Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)) : Bool}
4708
4709def mod_two_eq_zero_or_one_sym(n):
4710 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))
4711
4712# The divisor times the quotient plus the remainder is the dividend: b * (a / b) + a % b = a, reversed to rewrite toward the simple side.
4713law div_add_mod_sym:
4714 for a: Nat
4715 for b: Nat
4716 {a == Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)) : Nat}
4717
4718def div_add_mod_sym(a, b):
4719 Equal.sym(Nat, Nat.add(Nat.mul(b, Nat.div(a, b)), Nat.mod(a, b)), a, div_add_mod(a, b))
4720
4721# Two times n is n + n, reversed to rewrite toward the simple side.
4722law two_mul_sym:
4723 for n: Nat
4724 {Nat.add(n, n) == Nat.mul(2n, n) : Nat}
4725
4726def two_mul_sym(n):
4727 Equal.sym(Nat, Nat.mul(2n, n), Nat.add(n, n), two_mul(n))
4728
4729# Doubling is multiplying by two: double n = 2 * n, reversed to rewrite toward the simple side.
4730law double_eq_two_mul_sym:
4731 for n: Nat
4732 {Nat.mul(2n, n) == Nat.double(n) : Nat}
4733
4734def double_eq_two_mul_sym(n):
4735 Equal.sym(Nat, Nat.double(n), Nat.mul(2n, n), double_eq_two_mul(n))
4736
4737# Doubling distributes over addition: double (a + b) = double a + double b, reversed to rewrite toward the simple side.
4738law double_add_sym:
4739 for a: Nat
4740 for b: Nat
4741 {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}
4742
4743def double_add_sym(a, b):
4744 Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(Nat.double(a), Nat.double(b)), double_add(a, b))
4745
4746# Doubling a product doubles its left factor: double (a * b) = double a * b, reversed to rewrite toward the simple side.
4747law double_mul_sym:
4748 for a: Nat
4749 for b: Nat
4750 {Nat.mul(Nat.double(a), b) == Nat.double(Nat.mul(a, b)) : Nat}
4751
4752def double_mul_sym(a, b):
4753 Equal.sym(Nat, Nat.double(Nat.mul(a, b)), Nat.mul(Nat.double(a), b), double_mul(a, b))
4754
4755# Multiplying by a doubled factor doubles the product: a * double b = double (a * b), reversed to rewrite toward the simple side.
4756law mul_double_sym:
4757 for a: Nat
4758 for b: Nat
4759 {Nat.double(Nat.mul(a, b)) == Nat.mul(a, Nat.double(b)) : Nat}
4760
4761def mul_double_sym(a, b):
4762 Equal.sym(Nat, Nat.mul(a, Nat.double(b)), Nat.double(Nat.mul(a, b)), mul_double(a, b))
4763
4764# Doubling distributes over truncated subtraction: double (a - b) = double a - double b, reversed to rewrite toward the simple side.
4765law double_sub_sym:
4766 for a: Nat
4767 for b: Nat
4768 {Nat.sub(Nat.double(a), Nat.double(b)) == Nat.double(Nat.sub(a, b)) : Nat}
4769
4770def double_sub_sym(a, b):
4771 Equal.sym(Nat, Nat.double(Nat.sub(a, b)), Nat.sub(Nat.double(a), Nat.double(b)), double_sub(a, b))
4772
4773# Twice the half plus the parity is the number: double (n / 2) + n % 2 = n, reversed to rewrite toward the simple side.
4774law double_div_two_add_mod_two_sym:
4775 for n: Nat
4776 {n == Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}
4777
4778def double_div_two_add_mod_two_sym(n):
4779 Equal.sym(Nat, Nat.add(Nat.double(Nat.div(n, 2n)), Nat.mod(n, 2n)), n, double_div_two_add_mod_two(n))
4780
4781# 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.
4782law add_le_add_iff_right_sym:
4783 for a: Nat
4784 for b: Nat
4785 for k: Nat
4786 {Nat.is_le(Nat.add(a, k), Nat.add(b, k)) == Nat.is_le(a, b) : Bool}
4787
4788def add_le_add_iff_right_sym(a, b, k):
4789 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))
4790
4791# 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.
4792law add_left_cancel_iff_sym:
4793 for k: Nat
4794 for -a: Nat
4795 for -b: Nat
4796 {Nat.is_eq(Nat.add(k, a), Nat.add(k, b)) == Nat.is_eq(a, b) : Bool}
4797
4798def add_left_cancel_iff_sym(k, a, b):
4799 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))
4800
4801# 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.
4802law add_right_cancel_iff_sym:
4803 for a: Nat
4804 for b: Nat
4805 for k: Nat
4806 {Nat.is_eq(Nat.add(a, k), Nat.add(b, k)) == Nat.is_eq(a, b) : Bool}
4807
4808def add_right_cancel_iff_sym(a, b, k):
4809 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))
4810
4811# Multiplying n by two gives n + n, reversed to rewrite toward the simple side.
4812law mul_two_sym:
4813 for n: Nat
4814 {Nat.add(n, n) == Nat.mul(n, 2n) : Nat}
4815
4816def mul_two_sym(n):
4817 Equal.sym(Nat, Nat.mul(n, 2n), Nat.add(n, n), mul_two(n))
4818
4819# Squaring n gives n times n, reversed to rewrite toward the simple side.
4820law pow_two_sym:
4821 for n: Nat
4822 {Nat.mul(n, n) == Nat.pow(n, 2n) : Nat}
4823
4824def pow_two_sym(n):
4825 Equal.sym(Nat, Nat.pow(n, 2n), Nat.mul(n, n), pow_two(n))
4826
4827# The minimum of two numbers is at most their maximum, reversed to rewrite toward the simple side.
4828law min_le_max_sym:
4829 for a: Nat
4830 for b: Nat
4831 {True{} == Nat.is_le(Nat.min(a, b), Nat.max(a, b)) : Bool}
4832
4833def min_le_max_sym(a, b):
4834 Equal.sym(Bool, Nat.is_le(Nat.min(a, b), Nat.max(a, b)), True{}, min_le_max(a, b))