proof_base.bend
minebender-game@1.0.0.0 · 736 lines · 58 definitions
1import Base
2
3
4
5
6
7
8def Bool.disc_ft(b: Bool) -> Type:
9 match b:
10 case False{}:
11 Unit
12 case True{}:
13 Empty
14
15law false_ne_true:
16 for e: {False{} == True{} : Bool}
17 Empty
18
19def false_ne_true(e):
20 %e : Bool.disc_ft(_)
21 Unit{}
22
23law true_ne_false:
24 for e: {True{} == False{} : Bool}
25 Empty
26
27def true_ne_false(e):
28 false_ne_true(Equal.sym(Bool, True{}, False{}, e))
29
30law and_true_l:
31 for +a: Bool
32 for +b: Bool
33 for e: {Bool.and(a, b) == True{} : Bool}
34 {a == True{} : Bool}
35
36def and_true_l(a, b, e):
37 match a:
38 case True{}:
39 {==}
40 case False{}:
41 Empty.absurd({False{} == True{} : Bool}, false_ne_true(e))
42
43law and_true_r:
44 for +a: Bool
45 for +b: Bool
46 for e: {Bool.and(a, b) == True{} : Bool}
47 {b == True{} : Bool}
48
49def and_true_r(a, b, e):
50 match a:
51 case True{}:
52 e
53 case False{}:
54 Empty.absurd({b == True{} : Bool}, false_ne_true(e))
55
56law not_not:
57 for +b: Bool
58 {Bool.not(Bool.not(b)) == b : Bool}
59
60def not_not(b):
61 match b:
62 case True{}:
63 {==}
64 case False{}:
65 {==}
66
67
68
69
70def Nat.disc_z(n: Nat) -> Type:
71 match n:
72 case 0n:
73 Empty
74 case 1n+p:
75 Unit
76
77law succ_ne_zero:
78 for -n: Nat
79 for e: {1n+n == 0n : Nat}
80 Empty
81
82def succ_ne_zero(n, e):
83 %e : Nat.disc_z(_)
84 Unit{}
85
86law eq_refl:
87 for +n: Nat
88 {Nat.is_eq(n, n) == True{} : Bool}
89
90def eq_refl(n):
91 match n:
92 case 0n:
93 {==}
94 case 1n+p:
95 eq_refl(p)
96
97law lt_irrefl:
98 for +n: Nat
99 {Nat.is_lt(n, n) == False{} : Bool}
100
101def lt_irrefl(n):
102 match n:
103 case 0n:
104 {==}
105 case 1n+p:
106 lt_irrefl(p)
107
108law eq_sound:
109 for +a: Nat
110 for +b: Nat
111 for e: {Nat.is_eq(a, b) == True{} : Bool}
112 {a == b : Nat}
113
114def eq_sound(a, b, e):
115 match a b:
116 case 0n 0n:
117 {==}
118 case 0n 1n+q:
119 Empty.absurd({0n == 1n+q : Nat}, false_ne_true(e))
120 case 1n+p 0n:
121 Empty.absurd({1n+p == 0n : Nat}, false_ne_true(e))
122 case 1n+p 1n+q:
123 %eq_sound(p, q, e) : {1n+p == 1n+_ : Nat}
124 {==}
125
126law lt_zero:
127 for +i: Nat
128 {Nat.is_lt(i, 0n) == False{} : Bool}
129
130def lt_zero(i):
131 match i:
132 case 0n:
133 {==}
134 case 1n+k:
135 {==}
136
137law sub_zero:
138 for +i: Nat
139 {Nat.sub(i, 0n) == i : Nat}
140
141def sub_zero(i):
142 match i:
143 case 0n:
144 {==}
145 case 1n+k:
146 {==}
147
148law add_one:
149 for +n: Nat
150 {Nat.add(n, 1n) == 1n+n : Nat}
151
152def add_one(n):
153 match n:
154 case 0n:
155 {==}
156 case 1n+p:
157 %add_one(p) : {1n+Nat.add(p, 1n) == 1n+_ : Nat}
158 {==}
159
160law add_zero:
161 for +n: Nat
162 {Nat.add(n, 0n) == n : Nat}
163
164def add_zero(n):
165 match n:
166 case 0n:
167 {==}
168 case 1n+p:
169 %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
170 {==}
171
172law add_succ:
173 for +a: Nat
174 for +b: Nat
175 {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
176
177def add_succ(a, b):
178 match a:
179 case 0n:
180 {==}
181 case 1n+p:
182 %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
183 {==}
184
185def lt_succ.zero(+j: Nat, e: {Nat.is_lt(1n+j, 1n) == True{} : Bool}) -> Empty:
186 false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(j, 0n), True{},
187 Equal.sym(Bool, Nat.is_lt(j, 0n), False{}, lt_zero(j)), e))
188
189def lt_succ.lift(+j: Nat, +q: Nat,
190 r: Or({Nat.is_lt(j, q) == True{} : Bool}, {j == q : Nat})) ->
191 Or({Nat.is_lt(1n+j, 1n+q) == True{} : Bool}, {1n+j == 1n+q : Nat}):
192 match r:
193 case Inl{lt}:
194 Inl{lt}
195 case Inr{eq}:
196 %eq : Or({Nat.is_lt(1n+j, 1n+q) == True{} : Bool}, {1n+j == 1n+_ : Nat})
197 Inr{{==}}
198
199
200law lt_succ:
201 for +i: Nat
202 for +p: Nat
203 for e: {Nat.is_lt(i, 1n+p) == True{} : Bool}
204 Or({Nat.is_lt(i, p) == True{} : Bool}, {i == p : Nat})
205
206def lt_succ(i, p, e):
207 match i p:
208 case 0n 0n:
209 Inr{{==}}
210 case 0n 1n+q:
211 Inl{{==}}
212 case 1n+j 0n:
213 Empty.absurd(Or({Nat.is_lt(1n+j, 0n) == True{} : Bool}, {1n+j == 0n : Nat}),
214 lt_succ.zero(j, e))
215 case 1n+j 1n+q:
216 lt_succ.lift(j, q, lt_succ(j, q, e))
217
218
219
220
221
222law append_nil:
223 for -A: Data
224 for +xs: List<&2, A>
225 {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}
226
227def append_nil(A, xs):
228 match xs:
229 case Nil{}:
230 {==}
231 case h <> t:
232 %append_nil(A, t) : {h <> List.append(&2, A, t, Nil{}) == h <> _ : List<&2, A>}
233 {==}
234
235law append_assoc:
236 for -A: Data
237 for +xs: List<&2, A>
238 for +ys: List<&2, A>
239 for +zs: List<&2, A>
240 {List.append(&2, A, List.append(&2, A, xs, ys), zs)
241 == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}
242
243def append_assoc(A, xs, ys, zs):
244 match xs:
245 case Nil{}:
246 {==}
247 case h <> t:
248 %append_assoc(A, t, ys, zs) :
249 {h <> List.append(&2, A, List.append(&2, A, t, ys), zs) == h <> _ : List<&2, A>}
250 {==}
251
252law length_append:
253 for -A: Data
254 for +xs: List<&2, A>
255 for +ys: List<&2, A>
256 {List.length(&2, A, List.append(&2, A, xs, ys))
257 == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}
258
259def length_append(A, xs, ys):
260 match xs:
261 case Nil{}:
262 {==}
263 case h <> t:
264 %length_append(A, t, ys) :
265 {1n+List.length(&2, A, List.append(&2, A, t, ys)) == 1n+_ : Nat}
266 {==}
267
268
269law get_append_l:
270 for -A: Data
271 for +xs: List<&2, A>
272 for +ys: List<&2, A>
273 for +i: Nat
274 for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
275 {List.get(&2, A, List.append(&2, A, xs, ys), i) == List.get(&2, A, xs, i) : Maybe<&2, A>}
276
277def get_append_l(A, xs, ys, i, e):
278 match xs i:
279 case Nil{} _:
280 Empty.absurd({List.get(&2, A, ys, i) == None{} : Maybe<&2, A>},
281 false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(i, 0n), True{},
282 Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, lt_zero(i)), e)))
283 case h <> t 0n:
284 {==}
285 case h <> t 1n+k:
286 get_append_l(A, t, ys, k, e)
287
288law get_append_len:
289 for -A: Data
290 for +xs: List<&2, A>
291 for +v: A
292 for +ys: List<&2, A>
293 {List.get(&2, A, List.append(&2, A, xs, v <> ys), List.length(&2, A, xs)) == Some{v}
294 : Maybe<&2, A>}
295
296def get_append_len(A, xs, v, ys):
297 match xs:
298 case Nil{}:
299 {==}
300 case h <> t:
301 get_append_len(A, t, v, ys)
302
303
304
305
306law range_acc:
307 for +n: Nat
308 for +acc: List<&2, Nat>
309 {List.range.go(n, acc) == List.append(&2, Nat, List.range.go(n, Nil{}), acc) : List<&2, Nat>}
310
311def range_acc(n, acc):
312 match n:
313 case 0n:
314 {==}
315 case 1n+p:
316 +r = List.range.go(p, Nil{})
317 %Equal.sym(List<&2, Nat>, List.range.go(p, [p]), List.append(&2, Nat, r, [p]),
318 range_acc(p, [p])) :
319 {List.range.go(p, p <> acc) == List.append(&2, Nat, _, acc) : List<&2, Nat>}
320 %Equal.sym(List<&2, Nat>, List.append(&2, Nat, List.append(&2, Nat, r, [p]), acc),
321 List.append(&2, Nat, r, p <> acc), append_assoc(Nat, r, [p], acc)) :
322 {List.range.go(p, p <> acc) == _ : List<&2, Nat>}
323 range_acc(p, p <> acc)
324
325law range_snoc:
326 for +p: Nat
327 {List.range(1n+p) == List.append(&2, Nat, List.range(p), [p]) : List<&2, Nat>}
328
329def range_snoc(p):
330 range_acc(p, [p])
331
332law range_length:
333 for +n: Nat
334 {List.length(&2, Nat, List.range(n)) == n : Nat}
335
336def range_length(n):
337 match n:
338 case 0n:
339 {==}
340 case 1n+p:
341 %Equal.sym(List<&2, Nat>, List.range(1n+p), List.append(&2, Nat, List.range(p), [p]),
342 range_snoc(p)) : {List.length(&2, Nat, _) == 1n+p : Nat}
343 %Equal.sym(Nat, List.length(&2, Nat, List.append(&2, Nat, List.range(p), [p])),
344 Nat.add(List.length(&2, Nat, List.range(p)), 1n), length_append(Nat, List.range(p), [p])) :
345 {_ == 1n+p : Nat}
346 %Equal.sym(Nat, List.length(&2, Nat, List.range(p)), p, range_length(p)) :
347 {Nat.add(_, 1n) == 1n+p : Nat}
348 add_one(p)
349
350law range_get:
351 for +n: Nat
352 for +i: Nat
353 for e: {Nat.is_lt(i, n) == True{} : Bool}
354 {List.get(&2, Nat, List.range(n), i) == Some{i} : Maybe<&2, Nat>}
355
356def range_get.cases(+p: Nat, +i: Nat,
357 r: Or({Nat.is_lt(i, p) == True{} : Bool}, {i == p : Nat}),
358 ih: {Nat.is_lt(i, p) == True{} : Bool} -> {List.get(&2, Nat, List.range(p), i) == Some{i} : Maybe<&2, Nat>}) ->
359 {List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), i) == Some{i} : Maybe<&2, Nat>}:
360 match r:
361 case Inl{+lt}:
362 +lt2 = {%Equal.sym(Nat, List.length(&2, Nat, List.range(p)), p, range_length(p)) :
363 {Nat.is_lt(i, _) == True{} : Bool}; lt : {Nat.is_lt(i, List.length(&2, Nat, List.range(p))) == True{} : Bool}}
364 %Equal.sym(Maybe<&2, Nat>, List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), i),
365 List.get(&2, Nat, List.range(p), i), get_append_l(Nat, List.range(p), [p], i, lt2)) :
366 {_ == Some{i} : Maybe<&2, Nat>}
367 ih(lt)
368 case Inr{eq}:
369 %Equal.sym(Nat, i, p, eq) :
370 {List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), _) == Some{_} : Maybe<&2, Nat>}
371 %range_length(p) :
372 {List.get(&2, Nat, List.append(&2, Nat, List.range(p), [p]), _) == Some{p} : Maybe<&2, Nat>}
373 get_append_len(Nat, List.range(p), p, Nil{})
374
375def range_get(n, i, e):
376 match n:
377 case 0n:
378 Empty.absurd({List.get(&2, Nat, List.range(0n), i) == Some{i} : Maybe<&2, Nat>},
379 false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(i, 0n), True{},
380 Equal.sym(Bool, Nat.is_lt(i, 0n), False{}, lt_zero(i)), e)))
381 case 1n+p:
382 %Equal.sym(List<&2, Nat>, List.range(1n+p), List.append(&2, Nat, List.range(p), [p]),
383 range_snoc(p)) : {List.get(&2, Nat, _, i) == Some{i} : Maybe<&2, Nat>}
384 range_get.cases(p, i, lt_succ(i, p, e), lt => range_get(p, i, lt))
385
386law and_false_r:
387 for +a: Bool
388 {Bool.and(a, False{}) == False{} : Bool}
389
390def and_false_r(a):
391 match a:
392 case True{}:
393 {==}
394 case False{}:
395 {==}
396
397law or_false_l:
398 for +b: Bool
399 {Bool.or(False{}, b) == b : Bool}
400
401def or_false_l(b):
402 {==}
403
404
405law get_out:
406 for -A: Data
407 for +xs: List<&2, A>
408 for +i: Nat
409 for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool}
410 {List.get(&2, A, xs, i) == None{} : Maybe<&2, A>}
411
412def get_out(A, xs, i, e):
413 match xs i:
414 case Nil{} _:
415 {==}
416 case h <> t 0n:
417 Empty.absurd({List.get(&2, A, h <> t, 0n) == None{} : Maybe<&2, A>}, true_ne_false(e))
418 case h <> t 1n+k:
419 get_out(A, t, k, e)
420
421law range_get_out:
422 for +n: Nat
423 for +i: Nat
424 for e: {Nat.is_lt(i, n) == False{} : Bool}
425 {List.get(&2, Nat, List.range(n), i) == None{} : Maybe<&2, Nat>}
426
427def range_get_out(n, i, e):
428 get_out(Nat, List.range(n), i,
429 %Equal.sym(Nat, List.length(&2, Nat, List.range(n)), n, range_length(n)) :
430 {Nat.is_lt(i, _) == False{} : Bool}; e)
431
432
433
434
435law add_comm:
436 for +a: Nat
437 for +b: Nat
438 {Nat.add(a, b) == Nat.add(b, a) : Nat}
439
440def add_comm(a, b):
441 match a:
442 case 0n:
443 Equal.sym(Nat, Nat.add(b, 0n), b, add_zero(b))
444 case 1n+p:
445 %Equal.sym(Nat, Nat.add(p, b), Nat.add(b, p), add_comm(p, b)) :
446 {1n+_ == Nat.add(b, 1n+p) : Nat}
447 Equal.sym(Nat, Nat.add(b, 1n+p), 1n+Nat.add(b, p), add_succ(b, p))
448
449law add_assoc:
450 for +a: Nat
451 for +b: Nat
452 for +c: Nat
453 {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}
454
455def add_assoc(a, b, c):
456 match a:
457 case 0n:
458 {==}
459 case 1n+p:
460 %add_assoc(p, b, c) : {1n+Nat.add(Nat.add(p, b), c) == 1n+_ : Nat}
461 {==}
462
463law add_left_comm:
464 for +a: Nat
465 for +b: Nat
466 for +c: Nat
467 {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
468
469def add_left_comm(a, b, c):
470 %add_assoc(a, b, c) : {_ == Nat.add(b, Nat.add(a, c)) : Nat}
471 %Equal.sym(Nat, Nat.add(a, b), Nat.add(b, a), add_comm(a, b)) :
472 {Nat.add(_, c) == Nat.add(b, Nat.add(a, c)) : Nat}
473 add_assoc(b, a, c)
474
475law mul_zero_r:
476 for +a: Nat
477 {Nat.mul(a, 0n) == 0n : Nat}
478
479def mul_zero_r(a):
480 match a:
481 case 0n:
482 {==}
483 case 1n+p:
484 mul_zero_r(p)
485
486law mul_succ_r:
487 for +a: Nat
488 for +b: Nat
489 {Nat.mul(a, 1n+b) == Nat.add(a, Nat.mul(a, b)) : Nat}
490
491def mul_succ_r(a, b):
492 match a:
493 case 0n:
494 {==}
495 case 1n+p:
496 +x = Nat.mul(p, b)
497 %Equal.sym(Nat, Nat.mul(p, 1n+b), Nat.add(p, x), mul_succ_r(p, b)) :
498 {1n+Nat.add(b, _) == 1n+Nat.add(p, Nat.add(b, x)) : Nat}
499 %Equal.sym(Nat, Nat.add(b, Nat.add(p, x)), Nat.add(p, Nat.add(b, x)), add_left_comm(b, p, x)) :
500 {1n+_ == 1n+Nat.add(p, Nat.add(b, x)) : Nat}
501 {==}
502
503law mul_comm:
504 for +a: Nat
505 for +b: Nat
506 {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
507
508def mul_comm(a, b):
509 match a:
510 case 0n:
511 Equal.sym(Nat, Nat.mul(b, 0n), 0n, mul_zero_r(b))
512 case 1n+p:
513 %Equal.sym(Nat, Nat.mul(p, b), Nat.mul(b, p), mul_comm(p, b)) :
514 {Nat.add(b, _) == Nat.mul(b, 1n+p) : Nat}
515 Equal.sym(Nat, Nat.mul(b, 1n+p), Nat.add(b, Nat.mul(b, p)), mul_succ_r(b, p))
516
517law le_zero:
518 for +n: Nat
519 for e: {Nat.is_le(n, 0n) == True{} : Bool}
520 {n == 0n : Nat}
521
522def le_zero(n, e):
523 match n:
524 case 0n:
525 {==}
526 case 1n+p:
527 Empty.absurd({1n+p == 0n : Nat}, false_ne_true(e))
528
529law le_zero_l:
530 for +n: Nat
531 {Nat.is_le(0n, n) == True{} : Bool}
532
533def le_zero_l(n):
534 match n:
535 case 0n:
536 {==}
537 case 1n+p:
538 {==}
539
540
541law le_ne:
542 for +a: Nat
543 for +b: Nat
544 for le: {Nat.is_le(a, b) == True{} : Bool}
545 for ne: {Nat.is_eq(a, b) == False{} : Bool}
546 {Nat.is_le(1n+a, b) == True{} : Bool}
547
548def le_ne(a, b, le, ne):
549 match a b:
550 case 0n 0n:
551 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, true_ne_false(ne))
552 case 0n 1n+q:
553 le_zero_l(q)
554 case 1n+p 0n:
555 Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, false_ne_true(le))
556 case 1n+p 1n+q:
557 le_ne(p, q, le, ne)
558
559
560law lt_succ_le:
561 for +n: Nat
562 for +k: Nat
563 for e: {Nat.is_lt(n, 1n+k) == True{} : Bool}
564 {Nat.is_le(n, k) == True{} : Bool}
565
566def lt_succ_le(n, k, e):
567 match n k:
568 case 0n _:
569 le_zero_l(k)
570 case 1n+p 0n:
571 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool},
572 false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(p, 0n), True{},
573 Equal.sym(Bool, Nat.is_lt(p, 0n), False{}, lt_zero(p)), e)))
574 case 1n+p 1n+q:
575 lt_succ_le(p, q, e)
576
577law or_false_inv:
578 for +a: Bool
579 for +b: Bool
580 for e: {Bool.or(a, b) == False{} : Bool}
581 {a == False{} : Bool}
582
583def or_false_inv(a, b, e):
584 match a:
585 case False{}:
586 {==}
587 case True{}:
588 Empty.absurd({True{} == False{} : Bool}, true_ne_false(e))
589
590law and_true_r_id:
591 for +a: Bool
592 {Bool.and(a, True{}) == a : Bool}
593
594def and_true_r_id(a):
595 match a:
596 case True{}:
597 {==}
598 case False{}:
599 {==}
600
601law not_true:
602 for +b: Bool
603 for e: {Bool.not(b) == True{} : Bool}
604 {b == False{} : Bool}
605
606def not_true(b, e):
607 match b:
608 case False{}:
609 {==}
610 case True{}:
611 Empty.absurd({True{} == False{} : Bool}, false_ne_true(e))
612
613law not_false:
614 for +b: Bool
615 for e: {Bool.not(b) == False{} : Bool}
616 {b == True{} : Bool}
617
618def not_false(b, e):
619 match b:
620 case True{}:
621 {==}
622 case False{}:
623 Empty.absurd({False{} == True{} : Bool}, true_ne_false(e))
624
625law succ_inj:
626 for +a: Nat
627 for +b: Nat
628 for e: {1n+a == 1n+b : Nat}
629 {a == b : Nat}
630
631def pred(n: Nat) -> Nat:
632 match n:
633 case 0n:
634 0n
635 case 1n+p:
636 p
637
638def succ_inj(a, b, e):
639 Equal.cong(Nat, Nat, n => pred(n), 1n+a, 1n+b, e)
640
641
642
643
644law le_of_add:
645 for +a: Nat
646 for +k: Nat
647 {Nat.is_le(a, Nat.add(a, k)) == True{} : Bool}
648
649def le_of_add(a, k):
650 match a:
651 case 0n:
652 le_zero_l(k)
653 case 1n+p:
654 le_of_add(p, k)
655
656def LeW(+a: Nat, +b: Nat) -> Type:
657 Exists(Nat, k => {b == Nat.add(a, k) : Nat})
658
659def le_witness.lift(+p: Nat, +q: Nat, r: LeW(p, q)) -> LeW(1n+p, 1n+q):
660 match r:
661 case (k, e):
662 (k, %Equal.sym(Nat, q, Nat.add(p, k), e) : {1n+_ == 1n+Nat.add(p, k) : Nat}; {==})
663
664law le_witness:
665 for +a: Nat
666 for +b: Nat
667 for e: {Nat.is_le(a, b) == True{} : Bool}
668 LeW(a, b)
669
670def le_witness(a, b, e):
671 match a b:
672 case 0n _:
673 (b, {==})
674 case 1n+p 0n:
675 Empty.absurd(LeW(1n+p, 0n), false_ne_true(e))
676 case 1n+p 1n+q:
677 le_witness.lift(p, q, le_witness(p, q, e))
678
679law add_swap:
680 for +a: Nat
681 for +b: Nat
682 for +c: Nat
683 for +d: Nat
684 {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
685
686def add_swap(a, b, c, d):
687 %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))) :
688 {_ == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
689 %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))) :
690 {Nat.add(a, Nat.add(b, Nat.add(c, d))) == _ : Nat}
691 %Equal.sym(Nat, Nat.add(b, Nat.add(c, d)), Nat.add(c, Nat.add(b, d)), add_left_comm(b, c, d)) :
692 {Nat.add(a, _) == Nat.add(a, Nat.add(c, Nat.add(b, d))) : Nat}
693 {==}
694
695def le_add.k(+a: Nat, +b: Nat, +c: Nat, +d: Nat, r1: LeW(a, b), r2: LeW(c, d)) ->
696 {Nat.is_le(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}:
697 match r1:
698 case (+k1, e1):
699 match r2:
700 case (+k2, e2):
701 %Equal.sym(Nat, b, Nat.add(a, k1), e1) : {Nat.is_le(Nat.add(a, c), Nat.add(_, d)) == True{} : Bool}
702 %Equal.sym(Nat, d, Nat.add(c, k2), e2) : {Nat.is_le(Nat.add(a, c), Nat.add(Nat.add(a, k1), _)) == True{} : Bool}
703 %Equal.sym(Nat, Nat.add(Nat.add(a, k1), Nat.add(c, k2)), Nat.add(Nat.add(a, c), Nat.add(k1, k2)), add_swap(a, k1, c, k2)) :
704 {Nat.is_le(Nat.add(a, c), _) == True{} : Bool}
705 le_of_add(Nat.add(a, c), Nat.add(k1, k2))
706
707law le_add:
708 for +a: Nat
709 for +b: Nat
710 for +c: Nat
711 for +d: Nat
712 for e1: {Nat.is_le(a, b) == True{} : Bool}
713 for e2: {Nat.is_le(c, d) == True{} : Bool}
714 {Nat.is_le(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}
715
716def le_add(a, b, c, d, e1, e2):
717 le_add.k(a, b, c, d, le_witness(a, b, e1), le_witness(c, d, e2))
718
719law le_refl:
720 for +a: Nat
721 {Nat.is_le(a, a) == True{} : Bool}
722
723def le_refl(a):
724 %add_zero(a) : {Nat.is_le(a, _) == True{} : Bool}
725 le_of_add(a, 0n)
726
727law or_false_r:
728 for +a: Bool
729 {Bool.or(a, False{}) == a : Bool}
730
731def or_false_r(a):
732 match a:
733 case True{}:
734 {==}
735 case False{}:
736 {==}