proof_nat.bend
lawful-words@0.1.0.0 · 1,572 lines · 114 definitions
1import Base
2
3
4
5
6
7
8
9
10def Bool.disc_ft(b: Bool) -> Type:
11 match b:
12 case False{}:
13 Unit
14 case True{}:
15 Empty
16
17law false_ne_true:
18 for e: {False{} == True{} : Bool}
19 Empty
20
21def false_ne_true(e):
22 %e : Bool.disc_ft(_)
23 Unit{}
24
25law true_ne_false:
26 for e: {True{} == False{} : Bool}
27 Empty
28
29def true_ne_false(e):
30 false_ne_true(Equal.sym(Bool, True{}, False{}, e))
31
32law and_true_r_id:
33 for +a: Bool
34 {Bool.and(a, True{}) == a : Bool}
35
36def and_true_r_id(a):
37 match a:
38 case True{}:
39 {==}
40 case False{}:
41 {==}
42
43law and_false_r:
44 for +a: Bool
45 {Bool.and(a, False{}) == False{} : Bool}
46
47def and_false_r(a):
48 match a:
49 case True{}:
50 {==}
51 case False{}:
52 {==}
53
54law or_false_r:
55 for +a: Bool
56 {Bool.or(a, False{}) == a : Bool}
57
58def or_false_r(a):
59 match a:
60 case True{}:
61 {==}
62 case False{}:
63 {==}
64
65law and_true_l:
66 for +a: Bool
67 for +b: Bool
68 for e: {Bool.and(a, b) == True{} : Bool}
69 {a == True{} : Bool}
70
71def and_true_l(a, b, e):
72 match a:
73 case True{}:
74 {==}
75 case False{}:
76 Empty.absurd({False{} == True{} : Bool}, false_ne_true(e))
77
78law and_true_r:
79 for +a: Bool
80 for +b: Bool
81 for e: {Bool.and(a, b) == True{} : Bool}
82 {b == True{} : Bool}
83
84def and_true_r(a, b, e):
85 match a:
86 case True{}:
87 e
88 case False{}:
89 Empty.absurd({b == True{} : Bool}, false_ne_true(e))
90
91
92def bn(b: Bool) -> Nat:
93 match b:
94 case False{}:
95 0n
96 case True{}:
97 1n
98
99
100
101
102def Nat.disc_z(n: Nat) -> Type:
103 match n:
104 case 0n:
105 Empty
106 case 1n+p:
107 Unit
108
109law succ_ne_zero:
110 for -n: Nat
111 for e: {1n+n == 0n : Nat}
112 Empty
113
114def succ_ne_zero(n, e):
115 %e : Nat.disc_z(_)
116 Unit{}
117
118law zero_ne_succ:
119 for -n: Nat
120 for e: {0n == 1n+n : Nat}
121 Empty
122
123def zero_ne_succ(n, e):
124 succ_ne_zero(n, Equal.sym(Nat, 0n, 1n+n, e))
125
126def pred(n: Nat) -> Nat:
127 match n:
128 case 0n:
129 0n
130 case 1n+p:
131 p
132
133law succ_inj:
134 for +a: Nat
135 for +b: Nat
136 for e: {1n+a == 1n+b : Nat}
137 {a == b : Nat}
138
139def succ_inj(a, b, e):
140 Equal.cong(Nat, Nat, n => pred(n), 1n+a, 1n+b, e)
141
142law eq_refl:
143 for +n: Nat
144 {Nat.is_eq(n, n) == True{} : Bool}
145
146def eq_refl(n):
147 match n:
148 case 0n:
149 {==}
150 case 1n+p:
151 eq_refl(p)
152
153law cmp_refl:
154 for +n: Nat
155 {Nat.cmp(n, n) == EQ{} : Cmp}
156
157def cmp_refl(n):
158 match n:
159 case 0n:
160 {==}
161 case 1n+p:
162 cmp_refl(p)
163
164law eq_sound:
165 for +a: Nat
166 for +b: Nat
167 for e: {Nat.is_eq(a, b) == True{} : Bool}
168 {a == b : Nat}
169
170def eq_sound(a, b, e):
171 match a b:
172 case 0n 0n:
173 {==}
174 case 0n 1n+q:
175 Empty.absurd({0n == 1n+q : Nat}, false_ne_true(e))
176 case 1n+p 0n:
177 Empty.absurd({1n+p == 0n : Nat}, false_ne_true(e))
178 case 1n+p 1n+q:
179 %eq_sound(p, q, e) : {1n+p == 1n+_ : Nat}
180 {==}
181
182
183
184
185law add_zero:
186 for +n: Nat
187 {Nat.add(n, 0n) == n : Nat}
188
189def add_zero(n):
190 match n:
191 case 0n:
192 {==}
193 case 1n+p:
194 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
195 {==}
196
197law add_succ:
198 for +a: Nat
199 for +b: Nat
200 {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
201
202def add_succ(a, b):
203 match a:
204 case 0n:
205 {==}
206 case 1n+p:
207 %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
208 {==}
209
210law add_one:
211 for +n: Nat
212 {Nat.add(n, 1n) == 1n+n : Nat}
213
214def add_one(n):
215 %add_zero(n) : {Nat.add(n, 1n) == 1n+_ : Nat}
216 add_succ(n, 0n)
217
218law add_comm:
219 for +a: Nat
220 for +b: Nat
221 {Nat.add(a, b) == Nat.add(b, a) : Nat}
222
223def add_comm(a, b):
224 match a:
225 case 0n:
226 Equal.sym(Nat, Nat.add(b, 0n), b, add_zero(b))
227 case 1n+p:
228 %Equal.sym(Nat, Nat.add(p, b), Nat.add(b, p), add_comm(p, b)) :
229 {1n+_ == Nat.add(b, 1n+p) : Nat}
230 Equal.sym(Nat, Nat.add(b, 1n+p), 1n+Nat.add(b, p), add_succ(b, p))
231
232law add_assoc:
233 for +a: Nat
234 for +b: Nat
235 for +c: Nat
236 {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
237
238def add_assoc(a, b, c):
239 match a:
240 case 0n:
241 {==}
242 case 1n+p:
243 %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
244 {==}
245
246law add_left_comm:
247 for +a: Nat
248 for +b: Nat
249 for +c: Nat
250 {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
251
252def add_left_comm(a, b, c):
253 %add_assoc(a, b, c) : {_ == Nat.add(b, Nat.add(a, c)) : Nat}
254 %Equal.sym(Nat, Nat.add(a, b), Nat.add(b, a), add_comm(a, b)) :
255 {Nat.add(_, c) == Nat.add(b, Nat.add(a, c)) : Nat}
256 add_assoc(b, a, c)
257
258law add_swap:
259 for +a: Nat
260 for +b: Nat
261 for +c: Nat
262 for +d: Nat
263 {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
264
265def add_swap(a, b, c, d):
266 %Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(a, Nat.add(b, Nat.add(c, d))), add_assoc(a, b, Nat.add(c, d))) :
267 {_ == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
268 %Equal.sym(Nat, Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(a, Nat.add(c, Nat.add(b, d))), add_assoc(a, c, Nat.add(b, d))) :
269 {Nat.add(a, Nat.add(b, Nat.add(c, d))) == _ : Nat}
270 %Equal.sym(Nat, Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), add_left_comm(b, c, d)) :
271 {Nat.add(a, _) == Nat.add(a, Nat.add(c, Nat.add(b, d))) : Nat}
272 {==}
273
274
275law add_cancel_l:
276 for +a: Nat
277 for +x: Nat
278 for +y: Nat
279 for e: {Nat.add(a, x) == Nat.add(a, y) : Nat}
280 {x == y : Nat}
281
282def add_cancel_l(a, x, y, e):
283 match a:
284 case 0n:
285 e
286 case 1n+p:
287 add_cancel_l(p, x, y, succ_inj(Nat.add(p, x), Nat.add(p, y), e))
288
289
290law add_cancel_r:
291 for +a: Nat
292 for +x: Nat
293 for +y: Nat
294 for e: {Nat.add(x, a) == Nat.add(y, a) : Nat}
295 {x == y : Nat}
296
297def add_cancel_r(a, x, y, e):
298 add_cancel_l(a, x, y,
299 %add_comm(x, a) : {_ == Nat.add(a, y) : Nat}
300 %add_comm(y, a) : {Nat.add(x, a) == _ : Nat}
301 e)
302
303
304law add_self_r:
305 for +x: Nat
306 for +y: Nat
307 for e: {Nat.add(x, y) == x : Nat}
308 {y == 0n : Nat}
309
310def add_self_r(x, y, e):
311 add_cancel_l(x, y, 0n,
312 %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.add(x, y) == _ : Nat}
313 e)
314
315
316law add_eq_zero_l:
317 for +x: Nat
318 for +y: Nat
319 for e: {Nat.add(x, y) == 0n : Nat}
320 {x == 0n : Nat}
321
322def add_eq_zero_l(x, y, e):
323 match x:
324 case 0n:
325 {==}
326 case 1n+p:
327 Empty.absurd({1n+p == 0n : Nat}, succ_ne_zero(Nat.add(p, y), e))
328
329law add_eq_zero_r:
330 for +x: Nat
331 for +y: Nat
332 for e: {Nat.add(x, y) == 0n : Nat}
333 {y == 0n : Nat}
334
335def add_eq_zero_r(x, y, e):
336 match x:
337 case 0n:
338 e
339 case 1n+p:
340 Empty.absurd({y == 0n : Nat}, succ_ne_zero(Nat.add(p, y), e))
341
342
343
344
345law sub_zero:
346 for +i: Nat
347 {Nat.sub(i, 0n) == i : Nat}
348
349def sub_zero(i):
350 match i:
351 case 0n:
352 {==}
353 case 1n+k:
354 {==}
355
356
357law sub_add:
358 for +x: Nat
359 for +y: Nat
360 {Nat.sub(Nat.add(x, y), y) == x : Nat}
361
362def sub_add(x, y):
363 match y:
364 case 0n:
365 %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.sub(_, 0n) == x : Nat}
366 sub_zero(x)
367 case 1n+q:
368 %Equal.sym(Nat, Nat.add(x, 1n+q), 1n+Nat.add(x, q), add_succ(x, q)) :
369 {Nat.sub(_, 1n+q) == x : Nat}
370 sub_add(x, q)
371
372
373law sub_add_l:
374 for +y: Nat
375 for +x: Nat
376 {Nat.sub(Nat.add(y, x), y) == x : Nat}
377
378def sub_add_l(y, x):
379 %add_comm(x, y) : {Nat.sub(_, y) == x : Nat}
380 sub_add(x, y)
381
382
383
384
385law mul_zero_r:
386 for +a: Nat
387 {Nat.mul(a, 0n) == 0n : Nat}
388
389def mul_zero_r(a):
390 match a:
391 case 0n:
392 {==}
393 case 1n+p:
394 mul_zero_r(p)
395
396law mul_succ_r:
397 for +a: Nat
398 for +b: Nat
399 {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}
400
401def mul_succ_r(a, b):
402 match a:
403 case 0n:
404 {==}
405 case 1n+p:
406 +x = Nat.mul(p, b)
407 %Equal.sym(Nat, Nat.mul(p, 1n+b), Nat.add(p, x), mul_succ_r(p, b)) :
408 {1n+Nat.add(b, _) == 1n+Nat.add(p, Nat.add(b, x)) : Nat}
409 %Equal.sym(Nat, Nat.add(b, Nat.add(p, x)), Nat.add(p, Nat.add(b, x)), add_left_comm(b, p, x)) :
410 {1n+_ == 1n+Nat.add(p, Nat.add(b, x)) : Nat}
411 {==}
412
413law mul_comm:
414 for +a: Nat
415 for +b: Nat
416 {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
417
418def mul_comm(a, b):
419 match a:
420 case 0n:
421 Equal.sym(Nat, Nat.mul(b, 0n), 0n, mul_zero_r(b))
422 case 1n+p:
423 %Equal.sym(Nat, Nat.mul(p, b), Nat.mul(b, p), mul_comm(p, b)) :
424 {Nat.add(b, _) == Nat.mul(b, 1n+p) : Nat}
425 Equal.sym(Nat, Nat.mul(b, 1n+p), Nat.add(b, Nat.mul(b, p)), mul_succ_r(b, p))
426
427law mul_one:
428 for +a: Nat
429 {Nat.mul(a, 1n) == a : Nat}
430
431def mul_one(a):
432 match a:
433 case 0n:
434 {==}
435 case 1n+p:
436 %mul_one(p) : {1n+Nat.mul(p, 1n) == 1n+_ : Nat}
437 {==}
438
439law mul_add:
440 for +a: Nat
441 for +b: Nat
442 for +c: Nat
443 {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}
444
445def mul_add(a, b, c):
446 match a:
447 case 0n:
448 {==}
449 case 1n+p:
450 %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}
451 add_swap(b, c, Nat.mul(p, b), Nat.mul(p, c))
452
453law mul_add_r:
454 for +a: Nat
455 for +b: Nat
456 for +c: Nat
457 {Nat.mul(Nat.add(a, b), c) == Nat.add(Nat.mul(a, c), Nat.mul(b, c)) : Nat}
458
459def mul_add_r(a, b, c):
460 match a:
461 case 0n:
462 {==}
463 case 1n+p:
464 %Equal.sym(Nat, Nat.mul(Nat.add(p, b), c), Nat.add(Nat.mul(p, c), Nat.mul(b, c)), mul_add_r(p, b, c)) :
465 {Nat.add(c, _) == Nat.add(Nat.add(c, Nat.mul(p, c)), Nat.mul(b, c)) : Nat}
466 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))),
467 add_assoc(c, Nat.mul(p, c), Nat.mul(b, c)))
468
469law mul_assoc:
470 for +a: Nat
471 for +b: Nat
472 for +c: Nat
473 {Nat.mul(Nat.mul(a, b), c) == Nat.mul(a, Nat.mul(b, c)) : Nat}
474
475def mul_assoc(a, b, c):
476 match a:
477 case 0n:
478 {==}
479 case 1n+p:
480 %Equal.sym(Nat, Nat.mul(Nat.add(b, Nat.mul(p, b)), c), Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p, b), c)), mul_add_r(b, Nat.mul(p, b), c)) :
481 {_ == Nat.add(Nat.mul(b, c), Nat.mul(p, Nat.mul(b, c))) : Nat}
482 %mul_assoc(p, b, c) : {Nat.add(Nat.mul(b, c), Nat.mul(Nat.mul(p, b), c)) == Nat.add(Nat.mul(b, c), _) : Nat}
483 {==}
484
485
486
487
488law dbl_add:
489 for +x: Nat
490 {Nat.double(x) == Nat.add(x, x) : Nat}
491
492def dbl_add(x):
493 match x:
494 case 0n:
495 {==}
496 case 1n+p:
497 %Equal.sym(Nat, Nat.add(p, 1n+p), 1n+Nat.add(p, p), add_succ(p, p)) : {2n+Nat.double(p) == 1n+_ : Nat}
498 %dbl_add(p) : {2n+Nat.double(p) == 2n+_ : Nat}
499 {==}
500
501law dbl_dist:
502 for +x: Nat
503 for +y: Nat
504 {Nat.double(Nat.add(x, y)) == Nat.add(Nat.double(x), Nat.double(y)) : Nat}
505
506def dbl_dist(x, y):
507 match x:
508 case 0n:
509 {==}
510 case 1n+p:
511 %dbl_dist(p, y) : {2n+Nat.double(Nat.add(p, y)) == 2n+_ : Nat}
512 {==}
513
514law mul2:
515 for +x: Nat
516 {Nat.mul(2n, x) == Nat.double(x) : Nat}
517
518def mul2(x):
519 %Equal.sym(Nat, Nat.add(x, 0n), x, add_zero(x)) : {Nat.add(x, _) == Nat.double(x) : Nat}
520 Equal.sym(Nat, Nat.double(x), Nat.add(x, x), dbl_add(x))
521
522law mul2_r:
523 for +x: Nat
524 {Nat.mul(x, 2n) == Nat.double(x) : Nat}
525
526def mul2_r(x):
527 %mul_comm(2n, x) : {_ == Nat.double(x) : Nat}
528 mul2(x)
529
530law mul_dbl_r:
531 for +a: Nat
532 for +x: Nat
533 {Nat.mul(a, Nat.double(x)) == Nat.double(Nat.mul(a, x)) : Nat}
534
535def mul_dbl_r(a, x):
536 match a:
537 case 0n:
538 {==}
539 case 1n+p:
540 %Equal.sym(Nat, Nat.mul(p, Nat.double(x)), Nat.double(Nat.mul(p, x)), mul_dbl_r(p, x)) : {Nat.add(Nat.double(x), _) == Nat.double(Nat.add(x, Nat.mul(p, x))) : Nat}
541 Equal.sym(Nat, Nat.double(Nat.add(x, Nat.mul(p, x))), Nat.add(Nat.double(x), Nat.double(Nat.mul(p, x))), dbl_dist(x, Nat.mul(p, x)))
542
543law mul_dbl_l:
544 for +a: Nat
545 for +x: Nat
546 {Nat.mul(Nat.double(a), x) == Nat.double(Nat.mul(a, x)) : Nat}
547
548def mul_dbl_l(a, x):
549 %mul_comm(x, Nat.double(a)) : {_ == Nat.double(Nat.mul(a, x)) : Nat}
550 %mul_comm(x, a) : {Nat.mul(x, Nat.double(a)) == Nat.double(_) : Nat}
551 mul_dbl_r(x, a)
552
553law dbl_inj:
554 for +x: Nat
555 for +y: Nat
556 for e: {Nat.double(x) == Nat.double(y) : Nat}
557 {x == y : Nat}
558
559def dbl_inj(x, y, e):
560 match x y:
561 case 0n 0n:
562 {==}
563 case 0n 1n+q:
564 Empty.absurd({0n == 1n+q : Nat}, zero_ne_succ(1n+Nat.double(q), e))
565 case 1n+p 0n:
566 Empty.absurd({1n+p == 0n : Nat}, succ_ne_zero(1n+Nat.double(p), e))
567 case 1n+p 1n+q:
568 %dbl_inj(p, q, succ_inj(Nat.double(p), Nat.double(q), succ_inj(1n+Nat.double(p), 1n+Nat.double(q), e))) : {1n+p == 1n+_ : Nat}
569 {==}
570
571law dbl_ne_odd:
572 for +x: Nat
573 for +y: Nat
574 for e: {Nat.double(x) == 1n+Nat.double(y) : Nat}
575 Empty
576
577def dbl_ne_odd(x, y, e):
578 match x y:
579 case 0n _:
580 zero_ne_succ(Nat.double(y), e)
581 case 1n+p 0n:
582 succ_ne_zero(Nat.double(p), succ_inj(1n+Nat.double(p), 0n, e))
583 case 1n+p 1n+q:
584 dbl_ne_odd(p, q, succ_inj(Nat.double(p), 1n+Nat.double(q), succ_inj(1n+Nat.double(p), 2n+Nat.double(q), e)))
585
586law dbl_zero:
587 for +x: Nat
588 for e: {Nat.double(x) == 0n : Nat}
589 {x == 0n : Nat}
590
591def dbl_zero(x, e):
592 match x:
593 case 0n:
594 {==}
595 case 1n+p:
596 Empty.absurd({1n+p == 0n : Nat}, succ_ne_zero(1n+Nat.double(p), e))
597
598
599
600
601law lt_zero:
602 for +i: Nat
603 {Nat.is_lt(i, 0n) == False{} : Bool}
604
605def lt_zero(i):
606 match i:
607 case 0n:
608 {==}
609 case 1n+k:
610 {==}
611
612law lt_irrefl:
613 for +n: Nat
614 {Nat.is_lt(n, n) == False{} : Bool}
615
616def lt_irrefl(n):
617 match n:
618 case 0n:
619 {==}
620 case 1n+p:
621 lt_irrefl(p)
622
623law le_zero_l:
624 for +n: Nat
625 {Nat.is_le(0n, n) == True{} : Bool}
626
627def le_zero_l(n):
628 match n:
629 case 0n:
630 {==}
631 case 1n+p:
632 {==}
633
634law le_refl:
635 for +a: Nat
636 {Nat.is_le(a, a) == True{} : Bool}
637
638def le_refl(a):
639 match a:
640 case 0n:
641 {==}
642 case 1n+p:
643 le_refl(p)
644
645
646law lt_succ_iff:
647 for +a: Nat
648 for +b: Nat
649 {Nat.is_lt(a, 1n+b) == Nat.is_le(a, b) : Bool}
650
651def lt_succ_iff(a, b):
652 match a b:
653 case 0n 0n:
654 {==}
655 case 0n 1n+q:
656 {==}
657 case 1n+p 0n:
658 lt_zero(p)
659 case 1n+p 1n+q:
660 lt_succ_iff(p, q)
661
662
663law le_succ_lt:
664 for +a: Nat
665 for +b: Nat
666 {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}
667
668def le_succ_lt(a, b):
669 match b:
670 case 0n:
671 Equal.sym(Bool, Nat.is_lt(a, 0n), False{}, lt_zero(a))
672 case 1n+q:
673 Equal.sym(Bool, Nat.is_lt(a, 1n+q), Nat.is_le(a, q), lt_succ_iff(a, q))
674
675
676law not_lt_le:
677 for +a: Nat
678 for +b: Nat
679 for e: {Nat.is_lt(a, b) == False{} : Bool}
680 {Nat.is_le(b, a) == True{} : Bool}
681
682def not_lt_le(a, b, e):
683 match a b:
684 case 0n 0n:
685 {==}
686 case 0n 1n+q:
687 Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, true_ne_false(e))
688 case 1n+p 0n:
689 {==}
690 case 1n+p 1n+q:
691 not_lt_le(p, q, e)
692
693
694law not_le_lt:
695 for +a: Nat
696 for +b: Nat
697 for e: {Nat.is_le(a, b) == False{} : Bool}
698 {Nat.is_lt(b, a) == True{} : Bool}
699
700def not_le_lt(a, b, e):
701 match a b:
702 case 0n _:
703 Empty.absurd({Nat.is_lt(b, 0n) == True{} : Bool}, true_ne_false(
704 Equal.trans(Bool, True{}, Nat.is_le(0n, b), False{}, Equal.sym(Bool, Nat.is_le(0n, b), True{}, le_zero_l(b)), e)))
705 case 1n+p 0n:
706 {==}
707 case 1n+p 1n+q:
708 not_le_lt(p, q, e)
709
710law lt_to_le:
711 for +a: Nat
712 for +b: Nat
713 for e: {Nat.is_lt(a, b) == True{} : Bool}
714 {Nat.is_le(a, b) == True{} : Bool}
715
716def lt_to_le(a, b, e):
717 match a b:
718 case 0n _:
719 le_zero_l(b)
720 case 1n+p 0n:
721 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, false_ne_true(e))
722 case 1n+p 1n+q:
723 lt_to_le(p, q, e)
724
725law le_trans:
726 for +a: Nat
727 for +b: Nat
728 for +c: Nat
729 for ab: {Nat.is_le(a, b) == True{} : Bool}
730 for bc: {Nat.is_le(b, c) == True{} : Bool}
731 {Nat.is_le(a, c) == True{} : Bool}
732
733def le_trans(a, b, c, ab, bc):
734 match a b c:
735 case 0n _ _:
736 le_zero_l(c)
737 case 1n+p 0n _:
738 Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, false_ne_true(ab))
739 case 1n+p 1n+q 0n:
740 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, false_ne_true(bc))
741 case 1n+p 1n+q 1n+r:
742 le_trans(p, q, r, ab, bc)
743
744law lt_le_trans:
745 for +a: Nat
746 for +b: Nat
747 for +c: Nat
748 for ab: {Nat.is_lt(a, b) == True{} : Bool}
749 for bc: {Nat.is_le(b, c) == True{} : Bool}
750 {Nat.is_lt(a, c) == True{} : Bool}
751
752def lt_le_trans(a, b, c, ab, bc):
753 %le_succ_lt(a, c) : {_ == True{} : Bool}
754 le_trans(1n+a, b, c, %Equal.sym(Bool, Nat.is_le(1n+a, b), Nat.is_lt(a, b), le_succ_lt(a, b)) : {_ == True{} : Bool}; ab, bc)
755
756law le_lt_trans:
757 for +a: Nat
758 for +b: Nat
759 for +c: Nat
760 for ab: {Nat.is_le(a, b) == True{} : Bool}
761 for bc: {Nat.is_lt(b, c) == True{} : Bool}
762 {Nat.is_lt(a, c) == True{} : Bool}
763
764def le_lt_trans(a, b, c, ab, bc):
765 %le_succ_lt(a, c) : {_ == True{} : Bool}
766 le_trans(1n+a, 1n+b, c, ab, %Equal.sym(Bool, Nat.is_le(1n+b, c), Nat.is_lt(b, c), le_succ_lt(b, c)) : {_ == True{} : Bool}; bc)
767
768law lt_trans:
769 for +a: Nat
770 for +b: Nat
771 for +c: Nat
772 for ab: {Nat.is_lt(a, b) == True{} : Bool}
773 for bc: {Nat.is_lt(b, c) == True{} : Bool}
774 {Nat.is_lt(a, c) == True{} : Bool}
775
776def lt_trans(a, b, c, ab, bc):
777 lt_le_trans(a, b, c, ab, lt_to_le(b, c, bc))
778
779
780law le_add_r:
781 for +a: Nat
782 for +k: Nat
783 {Nat.is_le(a, Nat.add(a, k)) == True{} : Bool}
784
785def le_add_r(a, k):
786 match a:
787 case 0n:
788 le_zero_l(k)
789 case 1n+p:
790 le_add_r(p, k)
791
792law le_add_l:
793 for +a: Nat
794 for +k: Nat
795 {Nat.is_le(a, Nat.add(k, a)) == True{} : Bool}
796
797def le_add_l(a, k):
798 %add_comm(a, k) : {Nat.is_le(a, _) == True{} : Bool}
799 le_add_r(a, k)
800
801
802law lt_add_self:
803 for +b: Nat
804 for +x: Nat
805 {Nat.is_lt(Nat.add(b, x), b) == False{} : Bool}
806
807def lt_add_self(b, x):
808 match b:
809 case 0n:
810 lt_zero(x)
811 case 1n+p:
812 lt_add_self(p, x)
813
814law lt_pos:
815 for +r: Nat
816 for +b: Nat
817 for h: {Nat.is_lt(r, b) == True{} : Bool}
818 {Nat.is_lt(0n, b) == True{} : Bool}
819
820def lt_pos(r, b, h):
821 match b:
822 case 0n:
823 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, false_ne_true(
824 Equal.trans(Bool, False{}, Nat.is_lt(r, 0n), True{}, Equal.sym(Bool, Nat.is_lt(r, 0n), False{}, lt_zero(r)), h)))
825 case 1n+q:
826 {==}
827
828law pos_add_l:
829 for +x: Nat
830 for +y: Nat
831 for h: {Nat.is_lt(0n, x) == True{} : Bool}
832 {Nat.is_lt(0n, Nat.add(x, y)) == True{} : Bool}
833
834def pos_add_l(x, y, h):
835 match x:
836 case 0n:
837 Empty.absurd({Nat.is_lt(0n, y) == True{} : Bool}, false_ne_true(h))
838 case 1n+p:
839 {==}
840
841
842law lt_add_l:
843 for +c: Nat
844 for +a: Nat
845 for +b: Nat
846 for h: {Nat.is_lt(a, b) == True{} : Bool}
847 {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
848
849def lt_add_l(c, a, b, h):
850 match c:
851 case 0n:
852 h
853 case 1n+p:
854 lt_add_l(p, a, b, h)
855
856law le_add_mono_l:
857 for +c: Nat
858 for +a: Nat
859 for +b: Nat
860 for h: {Nat.is_le(a, b) == True{} : Bool}
861 {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
862
863def le_add_mono_l(c, a, b, h):
864 match c:
865 case 0n:
866 h
867 case 1n+p:
868 le_add_mono_l(p, a, b, h)
869
870law le_add_mono_r:
871 for +c: Nat
872 for +a: Nat
873 for +b: Nat
874 for h: {Nat.is_le(a, b) == True{} : Bool}
875 {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}
876
877def le_add_mono_r(c, a, b, h):
878 %add_comm(c, a) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool}
879 %add_comm(c, b) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool}
880 le_add_mono_l(c, a, b, h)
881
882law lt_add_mono_r:
883 for +c: Nat
884 for +a: Nat
885 for +b: Nat
886 for h: {Nat.is_lt(a, b) == True{} : Bool}
887 {Nat.is_lt(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}
888
889def lt_add_mono_r(c, a, b, h):
890 %add_comm(c, a) : {Nat.is_lt(_, Nat.add(b, c)) == True{} : Bool}
891 %add_comm(c, b) : {Nat.is_lt(Nat.add(c, a), _) == True{} : Bool}
892 lt_add_l(c, a, b, h)
893
894
895law le_mul_r:
896 for +a: Nat
897 for +b: Nat
898 for +c: Nat
899 for e: {Nat.is_le(a, b) == True{} : Bool}
900 {Nat.is_le(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}
901
902def le_mul_r(a, b, c, e):
903 match a b:
904 case 0n _:
905 le_zero_l(Nat.mul(b, c))
906 case 1n+p 0n:
907 Empty.absurd({Nat.is_le(Nat.mul(1n+p, c), 0n) == True{} : Bool}, false_ne_true(e))
908 case 1n+p 1n+q:
909 le_add_mono_l(c, Nat.mul(p, c), Nat.mul(q, c), le_mul_r(p, q, c, e))
910
911law le_mul_l:
912 for +c: Nat
913 for +a: Nat
914 for +b: Nat
915 for e: {Nat.is_le(a, b) == True{} : Bool}
916 {Nat.is_le(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool}
917
918def le_mul_l(c, a, b, e):
919 %mul_comm(a, c) : {Nat.is_le(_, Nat.mul(c, b)) == True{} : Bool}
920 %mul_comm(b, c) : {Nat.is_le(Nat.mul(a, c), _) == True{} : Bool}
921 le_mul_r(a, b, c, e)
922
923
924law le_sub_add:
925 for +k: Nat
926 for +m: Nat
927 for h: {Nat.is_le(k, m) == True{} : Bool}
928 {Nat.add(k, Nat.sub(m, k)) == m : Nat}
929
930def le_sub_add(k, m, h):
931 match k m:
932 case 0n _:
933 sub_zero(m)
934 case 1n+p 0n:
935 Empty.absurd({Nat.add(1n+p, Nat.sub(0n, 1n+p)) == 0n : Nat}, false_ne_true(h))
936 case 1n+p 1n+q:
937 %le_sub_add(p, q, h) : {1n+Nat.add(p, Nat.sub(q, p)) == 1n+_ : Nat}
938 {==}
939
940
941
942
943
944law go_eq:
945 for +n: Nat
946 for +m: Nat
947 for +d: Nat
948 for +r: Nat
949 for +bp: Nat
950 for +h: {Nat.add(m, r) == bp : Nat}
951 {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)))
952 == Nat.add(Nat.mul(d, 1n+bp), Nat.add(r, n)) : Nat}
953
954def go_eq(n, m, d, r, bp, h):
955 match n:
956 case 0n:
957 %Equal.sym(Nat, Nat.add(r, 0n), r, add_zero(r)) : {Nat.add(Nat.mul(d, 1n+bp), r) == Nat.add(Nat.mul(d, 1n+bp), _) : Nat}
958 {==}
959 case 1n+np:
960 match m:
961 case 0n:
962 -g = Nat.divmod.go(np, r, 1n+d, 0n)
963 +db = Nat.mul(d, 1n+bp)
964 Equal.trans(Nat, Nat.add(Nat.mul(Pair.fst(Nat, Nat, g), 1n+bp), Pair.snd(Nat, Nat, g)),
965 Nat.add(Nat.mul(1n+d, 1n+bp), Nat.add(0n, np)), Nat.add(db, Nat.add(r, 1n+np)),
966 go_eq(np, r, 1n+d, 0n, bp, %Equal.sym(Nat, Nat.add(r, 0n), r, add_zero(r)) : {_ == bp : Nat}; h),
967 %Equal.sym(Nat, r, bp, h) : {Nat.add(Nat.add(1n+bp, db), np) == Nat.add(db, Nat.add(_, 1n+np)) : Nat}
968 %Equal.sym(Nat, Nat.add(bp, 1n+np), 1n+Nat.add(bp, np), add_succ(bp, np)) :
969 {Nat.add(Nat.add(1n+bp, db), np) == Nat.add(db, _) : Nat}
970 %Equal.sym(Nat, Nat.add(db, 1n+Nat.add(bp, np)), 1n+Nat.add(db, Nat.add(bp, np)), add_succ(db, Nat.add(bp, np))) :
971 {Nat.add(Nat.add(1n+bp, db), np) == _ : Nat}
972 %Equal.sym(Nat, Nat.add(Nat.add(bp, db), np), Nat.add(bp, Nat.add(db, np)), add_assoc(bp, db, np)) :
973 {1n+_ == 1n+Nat.add(db, Nat.add(bp, np)) : Nat}
974 %add_left_comm(bp, db, np) : {1n+Nat.add(bp, Nat.add(db, np)) == 1n+_ : Nat}
975 {==})
976 case 1n+mp:
977 -g = Nat.divmod.go(np, mp, d, 1n+r)
978 +db = Nat.mul(d, 1n+bp)
979 Equal.trans(Nat, Nat.add(Nat.mul(Pair.fst(Nat, Nat, g), 1n+bp), Pair.snd(Nat, Nat, g)),
980 Nat.add(db, Nat.add(1n+r, np)), Nat.add(db, Nat.add(r, 1n+np)),
981 go_eq(np, mp, d, 1n+r, bp, %Equal.sym(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), add_succ(mp, r)) : {_ == bp : Nat}; h),
982 %Equal.sym(Nat, Nat.add(r, 1n+np), 1n+Nat.add(r, np), add_succ(r, np)) : {Nat.add(db, 1n+Nat.add(r, np)) == Nat.add(db, _) : Nat}
983 {==})
984
985law go_lt:
986 for +n: Nat
987 for +m: Nat
988 for +d: Nat
989 for +r: Nat
990 for +bp: Nat
991 for +h: {Nat.add(m, r) == bp : Nat}
992 {Nat.is_lt(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp) == True{} : Bool}
993
994def go_lt(n, m, d, r, bp, h):
995 match n:
996 case 0n:
997 %h : {Nat.is_lt(r, 1n+_) == True{} : Bool}
998 %Equal.sym(Bool, Nat.is_lt(r, 1n+Nat.add(m, r)), Nat.is_le(r, Nat.add(m, r)), lt_succ_iff(r, Nat.add(m, r))) : {_ == True{} : Bool}
999 le_add_l(r, m)
1000 case 1n+np:
1001 match m:
1002 case 0n:
1003 go_lt(np, r, 1n+d, 0n, bp, %Equal.sym(Nat, Nat.add(r, 0n), r, add_zero(r)) : {_ == bp : Nat}; h)
1004 case 1n+mp:
1005 go_lt(np, mp, d, 1n+r, bp, %Equal.sym(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), add_succ(mp, r)) : {_ == bp : Nat}; h)
1006
1007
1008law div_mod:
1009 for +a: Nat
1010 for +b: Nat
1011 {Nat.add(Nat.mul(Nat.div(a, b), b), Nat.mod(a, b)) == a : Nat}
1012
1013def div_mod(a, b):
1014 match b:
1015 case 0n:
1016 {==}
1017 case 1n+bp:
1018 go_eq(a, bp, 0n, 0n, bp, add_zero(bp))
1019
1020law mod_lt:
1021 for +a: Nat
1022 for +b: Nat
1023 for h: {Nat.is_lt(0n, b) == True{} : Bool}
1024 {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}
1025
1026def mod_lt(a, b, h):
1027 match b:
1028 case 0n:
1029 Empty.absurd({Nat.is_lt(Nat.mod(a, 0n), 0n) == True{} : Bool}, false_ne_true(h))
1030 case 1n+bp:
1031 go_lt(a, bp, 0n, 0n, bp, add_zero(bp))
1032
1033
1034law div_uniq:
1035 for +q1: Nat
1036 for +q2: Nat
1037 for +b: Nat
1038 for +r1: Nat
1039 for +r2: Nat
1040 for h1: {Nat.is_lt(r1, b) == True{} : Bool}
1041 for h2: {Nat.is_lt(r2, b) == True{} : Bool}
1042 for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
1043 {q1 == q2 : Nat}
1044
1045def div_uniq(q1, q2, b, r1, r2, h1, h2, e):
1046 match q1 q2:
1047 case 0n 0n:
1048 {==}
1049 case 0n 1n+q:
1050 +x = Nat.mul(q, b)
1051 Empty.absurd({0n == 1n+q : Nat}, false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(b, Nat.add(x, r2)), b), True{},
1052 Equal.sym(Bool, Nat.is_lt(Nat.add(b, Nat.add(x, r2)), b), False{}, lt_add_self(b, Nat.add(x, r2))),
1053 %add_assoc(b, x, r2) : {Nat.is_lt(_, b) == True{} : Bool}
1054 %e : {Nat.is_lt(_, b) == True{} : Bool}
1055 h1)))
1056 case 1n+p 0n:
1057 +x = Nat.mul(p, b)
1058 Empty.absurd({1n+p == 0n : Nat}, false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(b, Nat.add(x, r1)), b), True{},
1059 Equal.sym(Bool, Nat.is_lt(Nat.add(b, Nat.add(x, r1)), b), False{}, lt_add_self(b, Nat.add(x, r1))),
1060 %add_assoc(b, x, r1) : {Nat.is_lt(_, b) == True{} : Bool}
1061 %Equal.sym(Nat, Nat.add(Nat.add(b, x), r1), r2, e) : {Nat.is_lt(_, b) == True{} : Bool}
1062 h2)))
1063 case 1n+p 1n+q:
1064 +x = Nat.mul(p, b)
1065 +y = Nat.mul(q, b)
1066 %div_uniq(p, q, b, r1, r2, h1, h2, add_cancel_l(b, Nat.add(x, r1), Nat.add(y, r2),
1067 %add_assoc(b, x, r1) : {_ == Nat.add(b, Nat.add(y, r2)) : Nat}
1068 %add_assoc(b, y, r2) : {Nat.add(Nat.add(b, x), r1) == _ : Nat}
1069 e)) : {1n+p == 1n+_ : Nat}
1070 {==}
1071
1072law div_mul_add:
1073 for +q: Nat
1074 for +b: Nat
1075 for +r: Nat
1076 for +h: {Nat.is_lt(r, b) == True{} : Bool}
1077 {Nat.div(Nat.add(Nat.mul(q, b), r), b) == q : Nat}
1078
1079def div_mul_add(q, b, r, h):
1080 +n = Nat.add(Nat.mul(q, b), r)
1081 div_uniq(Nat.div(n, b), q, b, Nat.mod(n, b), r, mod_lt(n, b, lt_pos(r, b, h)), h, div_mod(n, b))
1082
1083law mod_mul_add:
1084 for +q: Nat
1085 for +b: Nat
1086 for +r: Nat
1087 for +h: {Nat.is_lt(r, b) == True{} : Bool}
1088 {Nat.mod(Nat.add(Nat.mul(q, b), r), b) == r : Nat}
1089
1090def mod_mul_add(q, b, r, h):
1091 +n = Nat.add(Nat.mul(q, b), r)
1092 add_cancel_l(Nat.mul(q, b), Nat.mod(n, b), r,
1093 %div_mul_add(q, b, r, h) : {Nat.add(Nat.mul(_, b), Nat.mod(n, b)) == n : Nat}
1094 div_mod(n, b))
1095
1096law mod_small:
1097 for +a: Nat
1098 for +b: Nat
1099 for +h: {Nat.is_lt(a, b) == True{} : Bool}
1100 {Nat.mod(a, b) == a : Nat}
1101
1102def mod_small(a, b, h):
1103 mod_mul_add(0n, b, a, h)
1104
1105law div_small:
1106 for +a: Nat
1107 for +b: Nat
1108 for +h: {Nat.is_lt(a, b) == True{} : Bool}
1109 {Nat.div(a, b) == 0n : Nat}
1110
1111def div_small(a, b, h):
1112 div_mul_add(0n, b, a, h)
1113
1114law mul_mod:
1115 for +a: Nat
1116 for +b: Nat
1117 {Nat.mod(Nat.mul(a, b), b) == 0n : Nat}
1118
1119def mul_mod(a, b):
1120 match b:
1121 case 0n:
1122 mul_zero_r(a)
1123 case 1n+bp:
1124 %add_zero(Nat.mul(a, 1n+bp)) : {Nat.mod(_, 1n+bp) == 0n : Nat}
1125 mod_mul_add(a, 1n+bp, 0n, {==})
1126
1127law div_mul:
1128 for +a: Nat
1129 for +b: Nat
1130 for +h: {Nat.is_lt(0n, b) == True{} : Bool}
1131 {Nat.div(Nat.mul(a, b), b) == a : Nat}
1132
1133def div_mul(a, b, h):
1134 %add_zero(Nat.mul(a, b)) : {Nat.div(_, b) == a : Nat}
1135 div_mul_add(a, b, 0n, h)
1136
1137law mod_one:
1138 for +a: Nat
1139 {Nat.mod(a, 1n) == 0n : Nat}
1140
1141def mod_one(a):
1142 %mul_one(a) : {Nat.mod(_, 1n) == 0n : Nat}
1143 mul_mod(a, 1n)
1144
1145law div_one:
1146 for +a: Nat
1147 {Nat.div(a, 1n) == a : Nat}
1148
1149def div_one(a):
1150 %mul_one(a) : {Nat.div(_, 1n) == a : Nat}
1151 div_mul(a, 1n, {==})
1152
1153law mod_zero_l:
1154 for +b: Nat
1155 {Nat.mod(0n, b) == 0n : Nat}
1156
1157def mod_zero_l(b):
1158 match b:
1159 case 0n:
1160 {==}
1161 case 1n+bp:
1162 {==}
1163
1164law div_zero_l:
1165 for +b: Nat
1166 {Nat.div(0n, b) == 0n : Nat}
1167
1168def div_zero_l(b):
1169 match b:
1170 case 0n:
1171 {==}
1172 case 1n+bp:
1173 {==}
1174
1175
1176law mod_add_mul:
1177 for +j: Nat
1178 for +x: Nat
1179 for +z: Nat
1180 {Nat.mod(Nat.add(Nat.mul(j, x), z), x) == Nat.mod(z, x) : Nat}
1181
1182def mod_add_mul(j, x, z):
1183 match x:
1184 case 0n:
1185 %Equal.sym(Nat, Nat.mul(j, 0n), 0n, mul_zero_r(j)) : {Nat.add(_, z) == z : Nat}
1186 {==}
1187 case 1n+xp:
1188 +q = Nat.div(z, 1n+xp)
1189 +r = Nat.mod(z, 1n+xp)
1190 %div_mod(z, 1n+xp) : {Nat.mod(Nat.add(Nat.mul(j, 1n+xp), _), 1n+xp) == r : Nat}
1191 %Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(j, q), 1n+xp), r), Nat.add(Nat.add(Nat.mul(j, 1n+xp), Nat.mul(q, 1n+xp)), r),
1192 Nat.add(Nat.mul(j, 1n+xp), Nat.add(Nat.mul(q, 1n+xp), r)),
1193 Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(Nat.add(j, q), 1n+xp), Nat.add(Nat.mul(j, 1n+xp), Nat.mul(q, 1n+xp)), mul_add_r(j, q, 1n+xp)),
1194 add_assoc(Nat.mul(j, 1n+xp), Nat.mul(q, 1n+xp), r)) :
1195 {Nat.mod(_, 1n+xp) == r : Nat}
1196 mod_mul_add(Nat.add(j, q), 1n+xp, r, mod_lt(z, 1n+xp, {==}))
1197
1198law div_add_mul:
1199 for +j: Nat
1200 for +x: Nat
1201 for +z: Nat
1202 for +h: {Nat.is_lt(0n, x) == True{} : Bool}
1203 {Nat.div(Nat.add(Nat.mul(j, x), z), x) == Nat.add(j, Nat.div(z, x)) : Nat}
1204
1205def div_add_mul(j, x, z, h):
1206 +q = Nat.div(z, x)
1207 +r = Nat.mod(z, x)
1208 %div_mod(z, x) : {Nat.div(Nat.add(Nat.mul(j, x), _), x) == Nat.add(j, q) : Nat}
1209 %Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(j, q), x), r), Nat.add(Nat.add(Nat.mul(j, x), Nat.mul(q, x)), r),
1210 Nat.add(Nat.mul(j, x), Nat.add(Nat.mul(q, x), r)),
1211 Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(Nat.add(j, q), x), Nat.add(Nat.mul(j, x), Nat.mul(q, x)), mul_add_r(j, q, x)),
1212 add_assoc(Nat.mul(j, x), Nat.mul(q, x), r)) :
1213 {Nat.div(_, x) == Nat.add(j, q) : Nat}
1214 div_mul_add(Nat.add(j, q), x, r, mod_lt(z, x, h))
1215
1216
1217law mod_add_mod_l:
1218 for +u: Nat
1219 for +v: Nat
1220 for +m: Nat
1221 {Nat.mod(Nat.add(Nat.mod(u, m), v), m) == Nat.mod(Nat.add(u, v), m) : Nat}
1222
1223def mod_add_mod_l(u, v, m):
1224 +q = Nat.div(u, m)
1225 +r = Nat.mod(u, m)
1226 %div_mod(u, m) : {Nat.mod(Nat.add(r, v), m) == Nat.mod(Nat.add(_, v), m) : Nat}
1227 %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, m), r), v), Nat.add(Nat.mul(q, m), Nat.add(r, v)), add_assoc(Nat.mul(q, m), r, v)) :
1228 {Nat.mod(Nat.add(r, v), m) == Nat.mod(_, m) : Nat}
1229 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, m), Nat.add(r, v)), m), Nat.mod(Nat.add(r, v), m), mod_add_mul(q, m, Nat.add(r, v)))
1230
1231law mod_add_mod_r:
1232 for +v: Nat
1233 for +u: Nat
1234 for +m: Nat
1235 {Nat.mod(Nat.add(v, Nat.mod(u, m)), m) == Nat.mod(Nat.add(v, u), m) : Nat}
1236
1237def mod_add_mod_r(v, u, m):
1238 %add_comm(Nat.mod(u, m), v) : {Nat.mod(_, m) == Nat.mod(Nat.add(v, u), m) : Nat}
1239 %add_comm(u, v) : {Nat.mod(Nat.add(Nat.mod(u, m), v), m) == Nat.mod(_, m) : Nat}
1240 mod_add_mod_l(u, v, m)
1241
1242law mod_mul_mod_l:
1243 for +u: Nat
1244 for +y: Nat
1245 for +m: Nat
1246 {Nat.mod(Nat.mul(Nat.mod(u, m), y), m) == Nat.mod(Nat.mul(u, y), m) : Nat}
1247
1248def mod_mul_mod_l(u, y, m):
1249 +q = Nat.div(u, m)
1250 +r = Nat.mod(u, m)
1251 %div_mod(u, m) : {Nat.mod(Nat.mul(r, y), m) == Nat.mod(Nat.mul(_, y), m) : Nat}
1252 %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q, m), r), y), Nat.add(Nat.mul(Nat.mul(q, m), y), Nat.mul(r, y)), mul_add_r(Nat.mul(q, m), r, y)) :
1253 {Nat.mod(Nat.mul(r, y), m) == Nat.mod(_, m) : Nat}
1254 %Equal.trans(Nat, Nat.mul(Nat.mul(q, y), m), Nat.mul(q, Nat.mul(y, m)), Nat.mul(Nat.mul(q, m), y),
1255 mul_assoc(q, y, m),
1256 %mul_comm(m, y) : {Nat.mul(q, _) == Nat.mul(Nat.mul(q, m), y) : Nat}
1257 Equal.sym(Nat, Nat.mul(Nat.mul(q, m), y), Nat.mul(q, Nat.mul(m, y)), mul_assoc(q, m, y))) :
1258 {Nat.mod(Nat.mul(r, y), m) == Nat.mod(Nat.add(_, Nat.mul(r, y)), m) : Nat}
1259 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Nat.mul(q, y), m), Nat.mul(r, y)), m), Nat.mod(Nat.mul(r, y), m), mod_add_mul(Nat.mul(q, y), m, Nat.mul(r, y)))
1260
1261law mod_mul_mod_r:
1262 for +y: Nat
1263 for +u: Nat
1264 for +m: Nat
1265 {Nat.mod(Nat.mul(y, Nat.mod(u, m)), m) == Nat.mod(Nat.mul(y, u), m) : Nat}
1266
1267def mod_mul_mod_r(y, u, m):
1268 %mul_comm(Nat.mod(u, m), y) : {Nat.mod(_, m) == Nat.mod(Nat.mul(y, u), m) : Nat}
1269 %mul_comm(u, y) : {Nat.mod(Nat.mul(Nat.mod(u, m), y), m) == Nat.mod(_, m) : Nat}
1270 mod_mul_mod_l(u, y, m)
1271
1272law mod_mod:
1273 for +u: Nat
1274 for +m: Nat
1275 {Nat.mod(Nat.mod(u, m), m) == Nat.mod(u, m) : Nat}
1276
1277def mod_mod(u, m):
1278 %add_zero(Nat.mod(u, m)) : {Nat.mod(_, m) == Nat.mod(u, m) : Nat}
1279 %add_zero(u) : {Nat.mod(Nat.add(Nat.mod(u, m), 0n), m) == Nat.mod(_, m) : Nat}
1280 mod_add_mod_l(u, 0n, m)
1281
1282
1283law mod_mod_mul:
1284 for +a: Nat
1285 for +x: Nat
1286 for +y: Nat
1287 {Nat.mod(Nat.mod(a, Nat.mul(x, y)), x) == Nat.mod(a, x) : Nat}
1288
1289def mod_mod_mul(a, x, y):
1290 +q = Nat.div(a, Nat.mul(x, y))
1291 +r = Nat.mod(a, Nat.mul(x, y))
1292 %div_mod(a, Nat.mul(x, y)) : {Nat.mod(r, x) == Nat.mod(_, x) : Nat}
1293 %Equal.trans(Nat, Nat.mul(Nat.mul(q, y), x), Nat.mul(q, Nat.mul(y, x)), Nat.mul(q, Nat.mul(x, y)),
1294 mul_assoc(q, y, x), %mul_comm(x, y) : {Nat.mul(q, _) == Nat.mul(q, Nat.mul(x, y)) : Nat}; {==}) :
1295 {Nat.mod(r, x) == Nat.mod(Nat.add(_, r), x) : Nat}
1296 Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Nat.mul(q, y), x), r), x), Nat.mod(r, x), mod_add_mul(Nat.mul(q, y), x, r))
1297
1298
1299law div_div:
1300 for +a: Nat
1301 for +x: Nat
1302 for +y: Nat
1303 {Nat.div(Nat.div(a, x), y) == Nat.div(a, Nat.mul(x, y)) : Nat}
1304
1305def div_div(a, x, y):
1306 match x y:
1307 case 0n 0n:
1308 {==}
1309 case 0n 1n+yp:
1310 {==}
1311 case 1n+xp 0n:
1312 %Equal.sym(Nat, Nat.mul(1n+xp, 0n), 0n, mul_zero_r(1n+xp)) : {0n == Nat.div(a, _) : Nat}
1313 {==}
1314 case 1n+xp 1n+yp:
1315 +x1 = {1n+xp : Nat}
1316 +y1 = {1n+yp : Nat}
1317 +q1 = Nat.div(a, x1)
1318 +r1 = Nat.mod(a, x1)
1319 +q2 = Nat.div(q1, y1)
1320 +r2 = Nat.mod(q1, y1)
1321 +xy = Nat.mul(x1, y1)
1322 +s = Nat.add(Nat.mul(r2, x1), r1)
1323
1324 +ea = Equal.trans(Nat, Nat.add(Nat.mul(q2, xy), s), Nat.add(Nat.mul(q1, x1), r1), a,
1325 %div_mod(q1, y1) : {Nat.add(Nat.mul(q2, xy), s) == Nat.add(Nat.mul(_, x1), r1) : Nat}
1326 %Equal.sym(Nat, Nat.mul(Nat.add(Nat.mul(q2, y1), r2), x1), Nat.add(Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(r2, x1)), mul_add_r(Nat.mul(q2, y1), r2, x1)) :
1327 {Nat.add(Nat.mul(q2, xy), s) == Nat.add(_, r1) : Nat}
1328 %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(r2, x1)), r1), Nat.add(Nat.mul(Nat.mul(q2, y1), x1), s),
1329 add_assoc(Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(r2, x1), r1)) : {Nat.add(Nat.mul(q2, xy), s) == _ : Nat}
1330 %Equal.trans(Nat, Nat.mul(q2, xy), Nat.mul(q2, Nat.mul(y1, x1)), Nat.mul(Nat.mul(q2, y1), x1),
1331 %mul_comm(x1, y1) : {Nat.mul(q2, xy) == Nat.mul(q2, _) : Nat}; {==},
1332 Equal.sym(Nat, Nat.mul(Nat.mul(q2, y1), x1), Nat.mul(q2, Nat.mul(y1, x1)), mul_assoc(q2, y1, x1))) :
1333 {Nat.add(Nat.mul(q2, xy), s) == Nat.add(_, s) : Nat}
1334 {==},
1335 div_mod(a, x1))
1336
1337 +hs = lt_le_trans(s, Nat.add(Nat.mul(r2, x1), x1), xy,
1338 lt_add_l(Nat.mul(r2, x1), r1, x1, mod_lt(a, x1, {==})),
1339 %add_comm(x1, Nat.mul(r2, x1)) : {Nat.is_le(_, xy) == True{} : Bool}
1340 %mul_comm(y1, x1) : {Nat.is_le(Nat.mul(1n+r2, x1), _) == True{} : Bool}
1341 le_mul_r(1n+r2, y1, x1, %Equal.sym(Bool, Nat.is_le(1n+r2, y1), Nat.is_lt(r2, y1), le_succ_lt(r2, y1)) : {_ == True{} : Bool}; mod_lt(q1, y1, {==})))
1342 %ea : {q2 == Nat.div(_, xy) : Nat}
1343 Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(q2, xy), s), xy), q2, div_mul_add(q2, xy, s, hs))
1344
1345
1346def div_lt.go(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool},
1347 t: Bool, et: {Nat.is_lt(Nat.div(a, b), c) == t : Bool}) -> {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}:
1348 match t:
1349 case True{}:
1350 et
1351 case False{}:
1352 +q = Nat.div(a, b)
1353 +hcq = not_lt_le(q, c, et)
1354 +hle = le_trans(Nat.mul(c, b), Nat.mul(q, b), a, le_mul_r(c, q, b, hcq),
1355 %div_mod(a, b) : {Nat.is_le(Nat.mul(q, b), _) == True{} : Bool}
1356 le_add_r(Nat.mul(q, b), Nat.mod(a, b)))
1357 +hlt = lt_le_trans(a, Nat.mul(b, c), a, h, %mul_comm(c, b) : {Nat.is_le(_, a) == True{} : Bool}; hle)
1358 Empty.absurd({Nat.is_lt(q, c) == True{} : Bool}, false_ne_true(
1359 Equal.trans(Bool, False{}, Nat.is_lt(a, a), True{}, Equal.sym(Bool, Nat.is_lt(a, a), False{}, lt_irrefl(a)), hlt)))
1360
1361law div_lt:
1362 for +a: Nat
1363 for +b: Nat
1364 for +c: Nat
1365 for +hb: {Nat.is_lt(0n, b) == True{} : Bool}
1366 for +h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool}
1367 {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}
1368
1369def div_lt(a, b, c, hb, h):
1370 div_lt.go(a, b, c, h, Nat.is_lt(Nat.div(a, b), c), {==})
1371
1372
1373
1374
1375law pow_add:
1376 for +b: Nat
1377 for +j: Nat
1378 for +k: Nat
1379 {Nat.pow(b, Nat.add(j, k)) == Nat.mul(Nat.pow(b, j), Nat.pow(b, k)) : Nat}
1380
1381def pow_add(b, j, k):
1382 match j:
1383 case 0n:
1384 Equal.sym(Nat, Nat.add(Nat.pow(b, k), 0n), Nat.pow(b, k), add_zero(Nat.pow(b, k)))
1385 case 1n+p:
1386 %Equal.sym(Nat, Nat.pow(b, Nat.add(p, k)), Nat.mul(Nat.pow(b, p), Nat.pow(b, k)), pow_add(b, p, k)) :
1387 {Nat.mul(b, _) == Nat.mul(Nat.mul(b, Nat.pow(b, p)), Nat.pow(b, k)) : Nat}
1388 Equal.sym(Nat, Nat.mul(Nat.mul(b, Nat.pow(b, p)), Nat.pow(b, k)), Nat.mul(b, Nat.mul(Nat.pow(b, p), Nat.pow(b, k))),
1389 mul_assoc(b, Nat.pow(b, p), Nat.pow(b, k)))
1390
1391law pow_pos:
1392 for +k: Nat
1393 {Nat.is_lt(0n, Nat.pow(2n, k)) == True{} : Bool}
1394
1395def pow_pos(k):
1396 match k:
1397 case 0n:
1398 {==}
1399 case 1n+j:
1400 pos_add_l(Nat.pow(2n, j), Nat.mul(1n, Nat.pow(2n, j)), pow_pos(j))
1401
1402law pow2s:
1403 for +p: Nat
1404 {Nat.pow(2n, 1n+p) == Nat.double(Nat.pow(2n, p)) : Nat}
1405
1406def pow2s(p):
1407 mul2(Nat.pow(2n, p))
1408
1409
1410law pow_sub1:
1411 for +j: Nat
1412 {Nat.sub(Nat.pow(2n, 1n+j), 1n) == 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)) : Nat}
1413
1414def pow_sub1.go(+u: Nat) -> {Nat.sub(Nat.double(1n+u), 1n) == 1n+Nat.double(Nat.sub(1n+u, 1n)) : Nat}:
1415 %Equal.sym(Nat, Nat.sub(u, 0n), u, sub_zero(u)) : {Nat.sub(Nat.double(1n+u), 1n) == 1n+Nat.double(_) : Nat}
1416 {==}
1417
1418law pow_one_plus:
1419 for +k: Nat
1420 {1n+Nat.sub(Nat.pow(2n, k), 1n) == Nat.pow(2n, k) : Nat}
1421
1422def pow_one_plus(k):
1423 match k:
1424 case 0n:
1425 {==}
1426 case 1n+j:
1427 %Equal.sym(Nat, Nat.mul(2n, Nat.pow(2n, j)), Nat.double(Nat.pow(2n, j)), mul2(Nat.pow(2n, j))) :
1428 {1n+Nat.sub(_, 1n) == _ : Nat}
1429 %pow_one_plus(j) : {1n+Nat.sub(Nat.double(_), 1n) == Nat.double(_) : Nat}
1430 {==}
1431
1432def pow_sub1(j):
1433 %Equal.sym(Nat, Nat.mul(2n, Nat.pow(2n, j)), Nat.double(Nat.pow(2n, j)), mul2(Nat.pow(2n, j))) :
1434 {Nat.sub(_, 1n) == 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)) : Nat}
1435 %pow_one_plus(j) : {Nat.sub(Nat.double(_), 1n) == 1n+Nat.double(Nat.sub(_, 1n)) : Nat}
1436 pow_sub1.go(Nat.sub(Nat.pow(2n, j), 1n))
1437
1438
1439law pow_le:
1440 for +m: Nat
1441 for +k: Nat
1442 for +h: {Nat.is_le(m, k) == True{} : Bool}
1443 {Nat.is_le(Nat.pow(2n, m), Nat.pow(2n, k)) == True{} : Bool}
1444
1445def pow_le(m, k, h):
1446 %le_sub_add(m, k, h) : {Nat.is_le(Nat.pow(2n, m), Nat.pow(2n, _)) == True{} : Bool}
1447 %Equal.sym(Nat, Nat.pow(2n, Nat.add(m, Nat.sub(k, m))), Nat.mul(Nat.pow(2n, m), Nat.pow(2n, Nat.sub(k, m))), pow_add(2n, m, Nat.sub(k, m))) :
1448 {Nat.is_le(Nat.pow(2n, m), _) == True{} : Bool}
1449 %mul_one(Nat.pow(2n, m)) :
1450 {Nat.is_le(_, Nat.mul(Nat.pow(2n, m), Nat.pow(2n, Nat.sub(k, m)))) == True{} : Bool}
1451 le_mul_l(Nat.pow(2n, m), 1n, Nat.pow(2n, Nat.sub(k, m)),
1452 %Equal.sym(Bool, Nat.is_le(1n, Nat.pow(2n, Nat.sub(k, m))), Nat.is_lt(0n, Nat.pow(2n, Nat.sub(k, m))), le_succ_lt(0n, Nat.pow(2n, Nat.sub(k, m)))) : {_ == True{} : Bool}
1453 pow_pos(Nat.sub(k, m)))
1454
1455
1456law mod_mod_pow:
1457 for +a: Nat
1458 for +k: Nat
1459 for +m: Nat
1460 for +h: {Nat.is_le(k, m) == True{} : Bool}
1461 {Nat.mod(Nat.mod(a, Nat.pow(2n, m)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}
1462
1463def mod_mod_pow(a, k, m, h):
1464 %le_sub_add(k, m, h) : {Nat.mod(Nat.mod(a, Nat.pow(2n, _)), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}
1465 %Equal.sym(Nat, Nat.pow(2n, Nat.add(k, Nat.sub(m, k))), Nat.mul(Nat.pow(2n, k), Nat.pow(2n, Nat.sub(m, k))), pow_add(2n, k, Nat.sub(m, k))) :
1466 {Nat.mod(Nat.mod(a, _), Nat.pow(2n, k)) == Nat.mod(a, Nat.pow(2n, k)) : Nat}
1467 mod_mod_mul(a, Nat.pow(2n, k), Nat.pow(2n, Nat.sub(m, k)))
1468
1469
1470law le_add_sub:
1471 for +m: Nat
1472 for +k: Nat
1473 {Nat.is_le(m, Nat.add(k, Nat.sub(m, k))) == True{} : Bool}
1474
1475def le_add_sub(m, k):
1476 match m k:
1477 case 0n _:
1478 le_zero_l(Nat.add(k, Nat.sub(0n, k)))
1479 case 1n+p 0n:
1480 le_refl(1n+p)
1481 case 1n+p 1n+q:
1482 le_add_sub(p, q)
1483
1484law eq_comm:
1485 for +a: Nat
1486 for +b: Nat
1487 {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}
1488
1489def eq_comm(a, b):
1490 match a b:
1491 case 0n 0n:
1492 {==}
1493 case 0n 1n+q:
1494 {==}
1495 case 1n+p 0n:
1496 {==}
1497 case 1n+p 1n+q:
1498 eq_comm(p, q)
1499
1500
1501law le_ne:
1502 for +a: Nat
1503 for +b: Nat
1504 for +le: {Nat.is_le(a, b) == True{} : Bool}
1505 for +ne: {Nat.is_eq(a, b) == False{} : Bool}
1506 {Nat.is_le(1n+a, b) == True{} : Bool}
1507
1508def le_ne(a, b, le, ne):
1509 match a b:
1510 case 0n 0n:
1511 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, true_ne_false(ne))
1512 case 0n 1n+q:
1513 le_zero_l(q)
1514 case 1n+p 0n:
1515 Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, false_ne_true(le))
1516 case 1n+p 1n+q:
1517 le_ne(p, q, le, ne)
1518
1519
1520law le_not_lt:
1521 for +a: Nat
1522 for +b: Nat
1523 for +h: {Nat.is_le(a, b) == True{} : Bool}
1524 {Nat.is_lt(b, a) == False{} : Bool}
1525
1526def le_not_lt(a, b, h):
1527 match a b:
1528 case 0n _:
1529 lt_zero(b)
1530 case 1n+p 0n:
1531 Empty.absurd({Nat.is_lt(0n, 1n+p) == False{} : Bool}, false_ne_true(h))
1532 case 1n+p 1n+q:
1533 le_not_lt(p, q, h)
1534
1535
1536law le_sub_r:
1537 for +a: Nat
1538 for +c: Nat
1539 for +x: Nat
1540 for +h: {Nat.is_le(Nat.add(a, c), x) == True{} : Bool}
1541 {Nat.is_le(c, Nat.sub(x, a)) == True{} : Bool}
1542
1543def le_sub_r(a, c, x, h):
1544 match a x:
1545 case 0n _:
1546 %Equal.sym(Nat, Nat.sub(x, 0n), x, sub_zero(x)) : {Nat.is_le(c, _) == True{} : Bool}
1547 h
1548 case 1n+p 0n:
1549 Empty.absurd({Nat.is_le(c, Nat.sub(0n, 1n+p)) == True{} : Bool}, false_ne_true(h))
1550 case 1n+p 1n+y:
1551 le_sub_r(p, c, y, h)
1552
1553
1554def lt_mul_cancel.go(+c: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool},
1555 t: Bool, et: {Nat.is_lt(a, b) == t : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
1556 match t:
1557 case True{}:
1558 et
1559 case False{}:
1560 Empty.absurd({Nat.is_lt(a, b) == True{} : Bool}, false_ne_true(
1561 Equal.trans(Bool, False{}, Nat.is_lt(Nat.mul(c, a), Nat.mul(c, a)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.mul(c, a), Nat.mul(c, a)), False{}, lt_irrefl(Nat.mul(c, a))),
1562 lt_le_trans(Nat.mul(c, a), Nat.mul(c, b), Nat.mul(c, a), h, le_mul_l(c, b, a, not_lt_le(a, b, et))))))
1563
1564law lt_mul_cancel:
1565 for +c: Nat
1566 for +a: Nat
1567 for +b: Nat
1568 for +h: {Nat.is_lt(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool}
1569 {Nat.is_lt(a, b) == True{} : Bool}
1570
1571def lt_mul_cancel(c, a, b, h):
1572 lt_mul_cancel.go(c, a, b, h, Nat.is_lt(a, b), {==})