proofs/u32_successor.bend
stelliferous@0.0.2.0 · 150 lines · 11 definitions
1import Base
2import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
3import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
4import stelliferous@0.0.2.0/proofs/word_width.bend as WordWidth
5
6law pad_nat:
7 for +n: Nat
8 for +w: Word(n)
9 {Word.to_nat(1n+n,Word.shr.pad(n,w)) == Word.to_nat(n,w) : Nat}
10def pad_nat(n,w):
11 match n:
12 case 0n:
13 match w:
14 case WNil{}: {==}
15 case 1n+ +p:
16 match w:
17 case WCon{False{},+t}:
18 %pad_nat(p,t) : {Nat.double(Word.to_nat(1n+p,Word.shr.pad(p,t))) == Nat.double(_) : Nat}
19 {==}
20 case WCon{True{},+t}:
21 %pad_nat(p,t) : {1n+Nat.double(Word.to_nat(1n+p,Word.shr.pad(p,t))) == 1n+Nat.double(_) : Nat}
22 {==}
23
24law inc_nat:
25 for +n: Nat
26 for +w: Word(n)
27 {Word.to_nat(1n+n,Word.inc(1n+n,Word.shr.pad(n,w))) == 1n+Word.to_nat(n,w) : Nat}
28def inc_nat(n,w):
29 match n:
30 case 0n:
31 match w:
32 case WNil{}: {==}
33 case 1n+ +p:
34 match w:
35 case WCon{False{},+t}:
36 %pad_nat(p,t) : {1n+Nat.double(Word.to_nat(1n+p,Word.shr.pad(p,t))) == 1n+Nat.double(_) : Nat}
37 {==}
38 case WCon{True{},+t}:
39 %inc_nat(p,t) : {Nat.double(Word.to_nat(1n+p,Word.inc(1n+p,Word.shr.pad(p,t)))) == Nat.double(_) : Nat}
40 {==}
41
42law adc_zero:
43 for +n: Nat
44 for +w: Word(n)
45 {Word.adc(n,w,Word.zero(n),False{},False{}) == w : Word(n)}
46def adc_zero(n,w):
47 match n:
48 case 0n:
49 WNil{} = w
50 {==}
51 case 1n+ +p:
52 match w:
53 case WCon{False{},+t}:
54 %adc_zero(p,t) : {WCon{False{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{False{},_} : Word(1n+p)}
55 {==}
56 case WCon{True{},+t}:
57 %adc_zero(p,t) : {WCon{True{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{True{},_} : Word(1n+p)}
58 {==}
59
60law adc_one:
61 for +n: Nat
62 for +w: Word(n)
63 {Word.adc(n,w,Word.zero(n),False{},True{}) == Word.inc(n,w) : Word(n)}
64def adc_one(n,w):
65 match n:
66 case 0n:
67 WNil{} = w
68 {==}
69 case 1n+ +p:
70 match w:
71 case WCon{False{},+t}:
72 %adc_zero(p,t) : {WCon{True{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{True{},_} : Word(1n+p)}
73 {==}
74 case WCon{True{},+t}:
75 %adc_one(p,t) : {WCon{False{},Word.adc(p,t,Word.zero(p),False{},True{})} == WCon{False{},_} : Word(1n+p)}
76 {==}
77
78law add_one:
79 for +n: Nat
80 for +w: Word(n)
81 {Word.add(n,w,Word.inc(n,Word.zero(n))) == Word.inc(n,w) : Word(n)}
82def add_one(n,w):
83 match n:
84 case 0n:
85 {==}
86 case 1n+ +p:
87 match w:
88 case WCon{False{},+t}:
89 %adc_zero(p,t) : {WCon{True{},Word.adc(p,t,Word.zero(p),False{},False{})} == WCon{True{},_} : Word(1n+p)}
90 {==}
91 case WCon{True{},+t}:
92 %adc_one(p,t) : {WCon{False{},Word.adc(p,t,Word.zero(p),False{},True{})} == WCon{False{},_} : Word(1n+p)}
93 {==}
94
95law concat_pad:
96 for +width: Nat
97 for +word: Word(width)
98 {WordWidth.transport(Nat.add(width,1n),1n+width,WordEncoding.concat(width,1n,word,Word.zero(1n)),
99 Addition.successor_width(width)) == Word.shr.pad(width,word) : Word(1n+width)}
100
101def concat_pad(width,word):
102 match width:
103 case 0n:
104 match word:
105 case WNil{}:
106 {==}
107 case 1n+ +rest:
108 match word:
109 case WCon{+bit,+tail}:
110 Equal.trans(Word(2n+rest),
111 WordWidth.transport(1n+Nat.add(rest,1n),2n+rest,WCon{bit,WordEncoding.concat(rest,1n,tail,Word.zero(1n))},
112 Addition.successor_width(1n+rest)),
113 WCon{bit,WordWidth.transport(Nat.add(rest,1n),1n+rest,WordEncoding.concat(rest,1n,tail,Word.zero(1n)),
114 Addition.successor_width(rest))},
115 WCon{bit,Word.shr.pad(rest,tail)},
116 WordWidth.transport_cons(Nat.add(rest,1n),1n+rest,bit,WordEncoding.concat(rest,1n,tail,Word.zero(1n)),
117 Addition.successor_width(rest)),
118 Equal.cong(Word(1n+rest),Word(2n+rest),w => WCon{bit,w},WordWidth.transport(Nat.add(rest,1n),1n+rest,WordEncoding.concat(rest,1n,
119 tail,Word.zero(1n)),Addition.successor_width(rest)),Word.shr.pad(rest,tail),concat_pad(rest,tail)))
120
121def padded_successor(+low: Word(31n)) -> {U32.to_nat(U32.add(U32{Word.shr.pad(31n,low)},1)) == 1n+U32.to_nat(U32{Word.shr.pad(31n,low)}) : Nat}:
122 %Equal.sym(Word(32n),Word.add(32n,Word.shr.pad(31n,low),Word.inc(32n,Word.zero(32n))),Word.inc(32n,Word.shr.pad(31n,low)),add_one(32n,
123 Word.shr.pad(31n,low))) : {Word.to_nat(32n,_) == 1n+Word.to_nat(32n,Word.shr.pad(31n,low)) : Nat}
124 %Equal.sym(Nat,Word.to_nat(32n,Word.shr.pad(31n,low)),Word.to_nat(31n,low),pad_nat(31n,low)) : {Word.to_nat(32n,Word.inc(32n,Word.shr.pad(31n,
125 low))) == 1n+_ : Nat}
126 inc_nat(31n,low)
127
128def Goal(+i: U32) -> Type:
129 {U32.is_lt(i,2147483648) == True{} : Bool} -> {U32.to_nat((i + 1 : U32)) == 1n+U32.to_nat(i) : Nat}
130
131def parts(+parts: WordEncoding.Split<31n,1n>) -> Goal(U32{WordEncoding.join(31n,1n,parts)}):
132 WordEncoding.Parts{+low,+high} = parts
133 bound =>
134 %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {U32.to_nat(U32.add(U32{WordEncoding.concat(31n,1n,
135 low,_)},1)) == 1n+U32.to_nat(U32{WordEncoding.concat(31n,1n,low,_)}) : Nat}
136 %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),concat_pad(31n,low)) : {U32.to_nat(U32.add(U32{_},
137 1)) == 1n+U32.to_nat(U32{_}) : Nat}
138 padded_successor(low)
139
140def word(+w: Word(32n)) -> Goal(U32{w}):
141 %WordEncoding.recover(31n,1n,w) : Goal(U32{_})
142 parts(WordEncoding.split(31n,1n,w))
143
144law successor:
145 for +i: U32
146 Goal(i)
147def successor(i):
148 match i:
149 case U32{w}:
150 word(w)