src/storage/arith.bend
bendtorch-core@0.1.0.0 · 487 lines · 41 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3
4def falsity(value: Bool) -> Data:
5 match value:
6 case True{}:
7 Empty
8 case False{}:
9 Unit
10
11def clash(equal: {False{} == True{} : Bool}) -> Empty:
12 %equal : falsity(_)
13 Unit{}
14
15def bit(b: Bool, x: Nat) -> Nat:
16 match b:
17 case False{}:
18 Nat.double(x)
19 case True{}:
20 1n+Nat.double(x)
21
22def borrow(c: Bool) -> Nat:
23 match c:
24 case False{}:
25 1n
26 case True{}:
27 0n
28
29def add_succ(a: Nat, -b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
30 match a:
31 case 0n:
32 {==}
33 case 1n+p:
34 %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
35 {==}
36
37def double_add(a: Nat, -b: Nat) -> {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}:
38 match a:
39 case 0n:
40 {==}
41 case 1n+p:
42 %double_add(p, b) : {2n+Nat.add(Nat.double(p), Nat.double(b)) == 2n+_ : Nat}
43 {==}
44
45def double_self(+a: Nat) -> {Nat.add(a, a) == Nat.double(a) : Nat}:
46 match a:
47 case 0n:
48 {==}
49 case 1n+p:
50 %double_self(p) : {1n+Nat.add(p, 1n+p) == 2n+_ : Nat}
51 %add_succ(p, p) : {1n+Nat.add(p, 1n+p) == 1n+_ : Nat}
52 {==}
53
54def eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
55 match a:
56 case 0n:
57 {==}
58 case 1n+p:
59 eq_refl(p)
60
61def eq_true(+a: Nat, +b: Nat, decided: {Nat.is_eq(a, b) == True{} : Bool}) -> {a == b : Nat}:
62 match a b:
63 case 0n 0n:
64 {==}
65 case 0n 1n+q:
66 Empty.absurd({0n == 1n+q : Nat}, clash(decided))
67 case 1n+p 0n:
68 Empty.absurd({1n+p == 0n : Nat}, clash(decided))
69 case 1n+p 1n+q:
70 %eq_true(p, q, decided) : {1n+p == 1n+_ : Nat}
71 {==}
72
73def cmp_bits(+x: Nat, +y: Nat, +a: Bool, +b: Bool) ->
74 {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(bit(a, x), bit(b, y)) : Cmp}:
75 match x y:
76 case 0n 0n:
77 match a b:
78 case False{} False{}:
79 {==}
80 case False{} True{}:
81 {==}
82 case True{} False{}:
83 {==}
84 case True{} True{}:
85 {==}
86 case 0n 1n+q:
87 match a b:
88 case False{} False{}:
89 {==}
90 case False{} True{}:
91 {==}
92 case True{} False{}:
93 {==}
94 case True{} True{}:
95 {==}
96 case 1n+p 0n:
97 match a b:
98 case False{} False{}:
99 {==}
100 case False{} True{}:
101 {==}
102 case True{} False{}:
103 {==}
104 case True{} True{}:
105 {==}
106 case 1n+p 1n+q:
107 match a b:
108 case False{} False{}:
109 cmp_bits(p, q, False{}, False{})
110 case False{} True{}:
111 cmp_bits(p, q, False{}, True{})
112 case True{} False{}:
113 cmp_bits(p, q, True{}, False{})
114 case True{} True{}:
115 cmp_bits(p, q, True{}, True{})
116
117def word_bit(-p: Nat, +b: Bool, -t: Word(p)) -> {bit(b, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
118 match b:
119 case False{}:
120 {==}
121 case True{}:
122 {==}
123
124def word_cmp(+n: Nat, +a: Word(n), +b: Word(n)) ->
125 {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}:
126 match n:
127 case 0n:
128 {==}
129 case 1n+p:
130 match a b:
131 case WCon{+x, +xs} WCon{+y, +ys}:
132 %word_bit(p, x, xs) : {Nat.cmp(_, Word.to_nat(1n+p, WCon{y, ys})) == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
133 %word_bit(p, y, ys) : {Nat.cmp(bit(x, Word.to_nat(p, xs)), _) == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
134 %cmp_bits(Word.to_nat(p, xs), Word.to_nat(p, ys), x, y) : {_ == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
135 %word_cmp(p, xs, ys) : {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, xs), Word.to_nat(p, ys))) == Word.cmp.fin(x, y, _) : Cmp}
136 {==}
137
138def u32_lt(+a: U32, +b: U32) -> {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}:
139 match a b:
140 case U32{x} U32{y}:
141 %word_cmp(32n, x, y) : {Cmp.is_lt(Nat.cmp(Word.to_nat(32n, x), Word.to_nat(32n, y))) == Cmp.is_lt(_) : Bool}
142 {==}
143
144def u32_le(+a: U32, +b: U32) -> {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}:
145 match a b:
146 case U32{x} U32{y}:
147 %word_cmp(32n, x, y) : {Cmp.is_le(Nat.cmp(Word.to_nat(32n, x), Word.to_nat(32n, y))) == Cmp.is_le(_) : Bool}
148 {==}
149
150def le_zero(+q: Nat) -> {Nat.is_le(0n, q) == True{} : Bool}:
151 match q:
152 case 0n:
153 {==}
154 case 1n+r:
155 {==}
156
157def le_dd(+u: Nat, +v: Nat, h: {Nat.is_le(Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(u, v) == True{} : Bool}:
158 match u v:
159 case 0n 0n:
160 {==}
161 case 0n 1n+q:
162 {==}
163 case 1n+p 0n:
164 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, clash(h))
165 case 1n+p 1n+q:
166 le_dd(p, q, h)
167
168def le_sd(+u: Nat, +v: Nat, h: {Nat.is_le(1n+Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(1n+u, v) == True{} : Bool}:
169 match u v:
170 case 0n 0n:
171 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, clash(h))
172 case 0n 1n+q:
173 le_zero(q)
174 case 1n+p 0n:
175 Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, clash(h))
176 case 1n+p 1n+q:
177 le_sd(p, q, h)
178
179def le_ds(+u: Nat, +v: Nat, h: {Nat.is_le(Nat.double(u), 1n+Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(u, v) == True{} : Bool}:
180 match u v:
181 case 0n v:
182 le_zero(v)
183 case 1n+p 0n:
184 Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, clash(h))
185 case 1n+p 1n+q:
186 le_ds(p, q, h)
187
188
189
190def sub_word(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool,
191 h: {Nat.is_le(Nat.add(borrow(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) ->
192 {Nat.add(borrow(c), Nat.add(Word.to_nat(n, b), Word.to_nat(n, Word.adc(n, a, b, True{}, c)))) == Word.to_nat(n, a) : Nat}:
193 match n:
194 case 0n:
195 match c:
196 case False{}:
197 Empty.absurd({1n == 0n : Nat}, clash(h))
198 case True{}:
199 {==}
200 case 1n+p:
201 match a:
202 case WCon{+x, +xs}:
203 match x:
204 case False{}:
205 match b:
206 case WCon{+y, +ys}:
207 match y:
208 case False{}:
209 match c:
210 case False{}:
211 %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
212 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
213 %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
214 {==}
215 case True{}:
216 %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == Nat.double(_) : Nat}
217 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
218 {==}
219 case True{}:
220 match c:
221 case False{}:
222 %sub_word(p, xs, ys, False{}, le_dd(1n+Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
223 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
224 {==}
225 case True{}:
226 %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
227 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
228 %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
229 {==}
230 case True{}:
231 match b:
232 case WCon{+y, +ys}:
233 match y:
234 case False{}:
235 match c:
236 case False{}:
237 %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
238 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
239 {==}
240 case True{}:
241 %sub_word(p, xs, ys, True{}, le_ds(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
242 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
243 %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
244 {==}
245 case True{}:
246 match c:
247 case False{}:
248 %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+Nat.double(_) : Nat}
249 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 3n+_ : Nat}
250 %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
251 {==}
252 case True{}:
253 %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
254 %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
255 {==}
256
257def lt_le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool},
258 bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
259 match a:
260 case 0n:
261 match b:
262 case 0n:
263 Empty.absurd({Nat.is_lt(0n, c) == True{} : Bool}, clash(ab))
264 case 1n+q:
265 match c:
266 case 0n:
267 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(bc))
268 case 1n+r:
269 {==}
270 case 1n+p:
271 match b:
272 case 0n:
273 Empty.absurd({Nat.is_lt(1n+p, c) == True{} : Bool}, clash(ab))
274 case 1n+q:
275 match c:
276 case 0n:
277 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(bc))
278 case 1n+r:
279 lt_le_trans(p, q, r, ab, bc)
280
281def lt_succ(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(a, 1n+b) == True{} : Bool}:
282 match a:
283 case 0n:
284 {==}
285 case 1n+p:
286 match b:
287 case 0n:
288 Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, clash(h))
289 case 1n+q:
290 lt_succ(p, q, h)
291
292def lt_dd(+x: Nat, +c: Nat, h: {Nat.is_lt(Nat.double(x), Nat.double(c)) == True{} : Bool}) -> {Nat.is_lt(x, c) == True{} : Bool}:
293 match x c:
294 case 0n 0n:
295 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(h))
296 case 0n 1n+q:
297 {==}
298 case 1n+p 0n:
299 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(h))
300 case 1n+p 1n+q:
301 lt_dd(p, q, h)
302
303def lt_sd(+x: Nat, +c: Nat, h: {Nat.is_lt(1n+Nat.double(x), Nat.double(c)) == True{} : Bool}) -> {Nat.is_lt(x, c) == True{} : Bool}:
304 match x c:
305 case 0n 0n:
306 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(h))
307 case 0n 1n+q:
308 {==}
309 case 1n+p 0n:
310 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(h))
311 case 1n+p 1n+q:
312 lt_sd(p, q, h)
313
314def lt_doubled(+x: Nat, +c: Nat, h: {Nat.is_lt(x, Nat.add(c, c)) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(c)) == True{} : Bool}:
315 %double_self(c) : {Nat.is_lt(x, _) == True{} : Bool}
316 h
317
318def lt_half(+b: Bool, +x: Nat, +c: Nat, h: {Nat.is_lt(bit(b, x), Model.capacity(1n+c)) == True{} : Bool}) ->
319 {Nat.is_lt(x, Model.capacity(c)) == True{} : Bool}:
320 match b:
321 case False{}:
322 lt_dd(x, Model.capacity(c), lt_doubled(Nat.double(x), Model.capacity(c), h))
323 case True{}:
324 lt_sd(x, Model.capacity(c), lt_doubled(1n+Nat.double(x), Model.capacity(c), h))
325
326def lt_zero(+x: Nat, h: {Nat.is_lt(x, 0n) == True{} : Bool}) -> Empty:
327 match x:
328 case 0n:
329 clash(h)
330 case 1n+p:
331 clash(h)
332
333def lt_one(+x: Nat, h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {0n == x : Nat}:
334 match x:
335 case 0n:
336 {==}
337 case 1n+p:
338 Empty.absurd({0n == 1n+p : Nat}, lt_zero(p, h))
339
340def lt_d1(+x: Nat, h: {Nat.is_lt(Nat.double(x), 1n) == True{} : Bool}) -> {Nat.is_lt(x, 1n) == True{} : Bool}:
341 match x:
342 case 0n:
343 {==}
344 case 1n+p:
345 Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, clash(h))
346
347def low(m: Nat, +k: Nat) -> Word(m):
348 match m:
349 case 0n:
350 WNil{}
351 case 1n+q:
352 match k:
353 case 0n:
354 WCon{False{}, low(q, 0n)}
355 case 1n+r:
356 WCon{True{}, low(q, r)}
357
358def mask_word(+m: Nat, +k: Nat, +w: Word(m), h: {Nat.is_lt(Word.to_nat(m, w), Model.capacity(k)) == True{} : Bool}) ->
359 {w == Word.and(m, w, low(m, k)) : Word(m)}:
360 match m:
361 case 0n:
362 match w:
363 case WNil{}:
364 {==}
365 case 1n+q:
366 match k:
367 case 0n:
368 match w:
369 case WCon{+b, +t}:
370 match b:
371 case False{}:
372 %mask_word(q, 0n, t, lt_d1(Word.to_nat(q, t), h)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+q)}
373 {==}
374 case True{}:
375 Empty.absurd({WCon{True{}, t} == Word.and(1n+q, WCon{True{}, t}, low(1n+q, 0n)) : Word(1n+q)}, lt_zero(Nat.double(Word.to_nat(q, t)), h))
376 case 1n+r:
377 match w:
378 case WCon{+b, +t}:
379 match b:
380 case False{}:
381 %mask_word(q, r, t, lt_half(False{}, Word.to_nat(q, t), r, h)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+q)}
382 {==}
383 case True{}:
384 %mask_word(q, r, t, lt_half(True{}, Word.to_nat(q, t), r, h)) : {WCon{True{}, t} == WCon{True{}, _} : Word(1n+q)}
385 {==}
386
387def unit(m: Nat, +k: Nat) -> Word(m):
388 match m:
389 case 0n:
390 WNil{}
391 case 1n+q:
392 match k:
393 case 0n:
394 WCon{True{}, Word.zero(q)}
395 case 1n+r:
396 WCon{False{}, unit(q, r)}
397
398def zero_nat(+q: Nat) -> {0n == Word.to_nat(q, Word.zero(q)) : Nat}:
399 match q:
400 case 0n:
401 {==}
402 case 1n+p:
403 %zero_nat(p) : {0n == Nat.double(_) : Nat}
404 {==}
405
406def unit_nat(+m: Nat, +k: Nat, h: {Nat.is_lt(k, m) == True{} : Bool}) -> {Model.capacity(k) == Word.to_nat(m, unit(m, k)) : Nat}:
407 match m:
408 case 0n:
409 match k:
410 case 0n:
411 Empty.absurd({1n == 0n : Nat}, clash(h))
412 case 1n+r:
413 Empty.absurd({Model.capacity(1n+r) == 0n : Nat}, clash(h))
414 case 1n+q:
415 match k:
416 case 0n:
417 %zero_nat(q) : {1n == 1n+Nat.double(_) : Nat}
418 {==}
419 case 1n+r:
420 %unit_nat(q, r, h) : {Model.capacity(1n+r) == Nat.double(_) : Nat}
421 double_self(Model.capacity(r))
422
423def truth(value: Bool) -> Data:
424 match value:
425 case True{}:
426 Unit
427 case False{}:
428 Empty
429
430def clash_true(equal: {True{} == False{} : Bool}) -> Empty:
431 %equal : truth(_)
432 Unit{}
433
434def le_succ(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
435 match a:
436 case 0n:
437 {==}
438 case 1n+p:
439 match b:
440 case 0n:
441 Empty.absurd({Nat.is_le(1n+p, 1n) == True{} : Bool}, clash(h))
442 case 1n+q:
443 le_succ(p, q, h)
444
445def not_lt_le(+a: Nat, +b: Nat, h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_le(b, a) == True{} : Bool}:
446 match a:
447 case 0n:
448 match b:
449 case 0n:
450 {==}
451 case 1n+q:
452 Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, clash_true(h))
453 case 1n+p:
454 match b:
455 case 0n:
456 {==}
457 case 1n+q:
458 not_lt_le(p, q, h)
459
460def lt_add_cancel(+c: Nat, +j: Nat, +k: Nat, h: {Nat.is_lt(Nat.add(c, j), Nat.add(c, k)) == True{} : Bool}) ->
461 {Nat.is_lt(j, k) == True{} : Bool}:
462 match c:
463 case 0n:
464 h
465 case 1n+r:
466 lt_add_cancel(r, j, k, h)
467
468def and_left(+a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
469 match a:
470 case False{}:
471 Empty.absurd({False{} == True{} : Bool}, clash(h))
472 case True{}:
473 {==}
474
475def and_right(+a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
476 match a:
477 case False{}:
478 Empty.absurd({b == True{} : Bool}, clash(h))
479 case True{}:
480 h
481
482def sub_u32(+i: U32, +c: U32, h: {Nat.is_le(U32.to_nat(c), U32.to_nat(i)) == True{} : Bool}) ->
483 {U32.to_nat(i) == Nat.add(U32.to_nat(c), U32.to_nat(U32.sub(i, c))) : Nat}:
484 match i c:
485 case U32{x} U32{y}:
486 Equal.sym(Nat, Nat.add(Word.to_nat(32n, y), Word.to_nat(32n, Word.adc(32n, x, y, True{}, True{}))), Word.to_nat(32n, x),
487 sub_word(32n, x, y, True{}, h))