proofs/natural_addition.bend
stelliferous@0.0.2.0 · 65 lines · 5 definitions
1
2import Base
3
4law successor_right:
5 for +a: Nat
6 for +b: Nat
7 {Nat.add(a,1n+b) == 1n+Nat.add(a,b) : Nat}
8
9def successor_right(a,b):
10 match a:
11 case 0n:
12 {==}
13 case 1n+ +p:
14 %successor_right(p,b) : {1n+Nat.add(p,1n+b) == 1n+_ : Nat}
15 {==}
16
17law double:
18 for +n: Nat
19 {Nat.add(n,n) == Nat.double(n) : Nat}
20
21def double(n):
22 match n:
23 case 0n:
24 {==}
25 case 1n+ +p:
26 %double(p) : {1n+Nat.add(p,1n+p) == 2n+_ : Nat}
27 %successor_right(p,p) : {1n+Nat.add(p,1n+p) == 1n+_ : Nat}
28 {==}
29
30law zero_right:
31 for +n: Nat
32 {Nat.add(n,0n) == n : Nat}
33
34def zero_right(n):
35 match n:
36 case 0n:
37 {==}
38 case 1n+ +p:
39 %zero_right(p) : {1n+Nat.add(p,0n) == 1n+_ : Nat}
40 {==}
41
42law successor_width:
43 for +width: Nat
44 {Nat.add(width,1n) == 1n+width : Nat}
45
46def successor_width(width):
47 match width:
48 case 0n:
49 {==}
50 case 1n+ +rest:
51 Equal.cong(Nat,Nat,n => 1n+n,Nat.add(rest,1n),1n+rest,successor_width(rest))
52
53law associative:
54 for +first: Nat
55 for +second: Nat
56 for +third: Nat
57 {Nat.add(Nat.add(first,second),third) == Nat.add(first,Nat.add(second,third)) : Nat}
58
59def associative(first,second,third):
60 match first:
61 case 0n:
62 {==}
63 case 1n+ +rest:
64 Equal.cong(Nat,Nat,n => 1n+n,Nat.add(Nat.add(rest,second),third),Nat.add(rest,Nat.add(second,third)),associative(rest,second,third))
65