proofs/lib/nat.bend

bend-collections-laws-crypto@1.0.0.0 · 576 lines · 75 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
4import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6
7# Natural-number order and arithmetic facts on Base Nat (Bool-valued
8# comparisons), proved by induction on the installed definitions.
9
10def pred(n: Nat) -> Nat:
11  match n:
12    case 0n:
13      0n
14    case 1n+p:
15      p
16
17def succ_inj(+a: Nat, +b: Nat, e: {1n+a == 1n+b : Nat}) -> {a == b : Nat}:
18  Equal.cong(Nat, Nat, pred, 1n+a, 1n+b, e)
19
20def succ_cong(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {1n+a == 1n+b : Nat}:
21  Equal.cong(Nat, Nat, x => 1n+x, a, b, e)
22
23def is_zero(n: Nat) -> Bool:
24  match n:
25    case 0n:
26      True{}
27    case 1n+p:
28      False{}
29
30def zero_succ(+n: Nat, e: {0n == 1n+n : Nat}) -> Empty:
31  %e : L.truth(is_zero(_))
32  Unit{}
33
34def succ_zero(+n: Nat, e: {1n+n == 0n : Nat}) -> Empty:
35  zero_succ(n, Equal.sym(Nat, 1n+n, 0n, e))
36
37def add_zero(+n: Nat) -> {Nat.add(n, 0n) == n : Nat}:
38  NA.add_zero(n)
39
40def add_succ(+a: Nat, +b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
41  NA.add_succ(a, b)
42
43def add_comm(+a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:
44  NA.add_comm(a, b)
45
46def add_assoc(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}:
47  NA.add_assoc(a, b, c)
48
49# ---- order ----
50
51def lt_irrefl(+n: Nat) -> {Nat.is_lt(n, n) == False{} : Bool}:
52  match n:
53    case 0n:
54      {==}
55    case 1n+p:
56      lt_irrefl(p)
57
58def le_refl(+n: Nat) -> {Nat.is_le(n, n) == True{} : Bool}:
59  match n:
60    case 0n:
61      {==}
62    case 1n+p:
63      le_refl(p)
64
65def lt_succ(+n: Nat) -> {Nat.is_lt(n, 1n+n) == True{} : Bool}:
66  match n:
67    case 0n:
68      {==}
69    case 1n+p:
70      lt_succ(p)
71
72def le_succ(+n: Nat) -> {Nat.is_le(n, 1n+n) == True{} : Bool}:
73  match n:
74    case 0n:
75      {==}
76    case 1n+p:
77      le_succ(p)
78
79def zero_le(+n: Nat) -> {Nat.is_le(0n, n) == True{} : Bool}:
80  match n:
81    case 0n:
82      {==}
83    case 1n+p:
84      {==}
85
86def not_lt_zero(+n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
87  match n:
88    case 0n:
89      {==}
90    case 1n+p:
91      {==}
92
93def lt_zero_absurd(+n: Nat, e: {Nat.is_lt(n, 0n) == True{} : Bool}) -> Empty:
94  L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(n, 0n), True{}, Equal.sym(Bool, Nat.is_lt(n, 0n), False{}, not_lt_zero(n)), e))
95
96def lt_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
97  match a b:
98    case 0n 0n:
99      {==}
100    case 0n 1n+q:
101      {==}
102    case 1n+p 0n:
103      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, L.false_true(e))
104    case 1n+p 1n+q:
105      lt_le(p, q, e)
106
107def le_lt_succ(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(a, 1n+b) == True{} : Bool}:
108  match a b:
109    case 0n _:
110      {==}
111    case 1n+p 0n:
112      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, L.false_true(e))
113    case 1n+p 1n+q:
114      le_lt_succ(p, q, e)
115
116def lt_succ_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, 1n+b) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
117  match a b:
118    case 0n _:
119      zero_le(b)
120    case 1n+p 0n:
121      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, lt_zero_absurd(p, e))
122    case 1n+p 1n+q:
123      lt_succ_le(p, q, e)
124
125def succ_le_lt(+a: Nat, +b: Nat, e: {Nat.is_le(1n+a, b) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
126  match a b:
127    case _ 0n:
128      Empty.absurd({Nat.is_lt(a, 0n) == True{} : Bool}, L.false_true(e))
129    case 0n 1n+q:
130      {==}
131    case 1n+p 1n+q:
132      succ_le_lt(p, q, e)
133
134def lt_succ_le_succ(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n+a, b) == True{} : Bool}:
135  match a b:
136    case _ 0n:
137      Empty.absurd({Nat.is_le(1n+a, 0n) == True{} : Bool}, lt_zero_absurd(a, e))
138    case 0n 1n+q:
139      zero_le(q)
140    case 1n+p 1n+q:
141      lt_succ_le_succ(p, q, e)
142
143def le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
144  match a b c:
145    case 0n _ _:
146      zero_le(c)
147    case 1n+p 0n _:
148      Empty.absurd({Nat.is_le(1n+p, c) == True{} : Bool}, L.false_true(ab))
149    case 1n+p 1n+q 0n:
150      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, L.false_true(bc))
151    case 1n+p 1n+q 1n+r:
152      le_trans(p, q, r, ab, bc)
153
154def lt_le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
155  succ_le_lt(a, c, le_trans(1n+a, b, c, lt_succ_le_succ(a, b, ab), bc))
156
157def le_lt_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, bc: {Nat.is_lt(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
158  succ_le_lt(a, c, le_trans(1n+a, 1n+b, c, ab, lt_succ_le_succ(b, c, bc)))
159
160def lt_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, bc: {Nat.is_lt(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
161  lt_le_trans(a, b, c, ab, lt_le(b, c, bc))
162
163# is_lt(a, b) == False gives b <= a.
164def not_lt_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_le(b, a) == True{} : Bool}:
165  match a b:
166    case _ 0n:
167      zero_le(a)
168    case 0n 1n+q:
169      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, L.true_false(e))
170    case 1n+p 1n+q:
171      not_lt_le(p, q, e)
172
173def le_not_lt(+a: Nat, +b: Nat, e: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.is_lt(a, b) == False{} : Bool}:
174  match a b:
175    case _ 0n:
176      not_lt_zero(a)
177    case 0n 1n+q:
178      Empty.absurd({Nat.is_lt(0n, 1n+q) == False{} : Bool}, L.false_true(e))
179    case 1n+p 1n+q:
180      le_not_lt(p, q, e)
181
182def lt_not_le(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(b, a) == False{} : Bool}:
183  match a b:
184    case _ 0n:
185      Empty.absurd({Nat.is_le(0n, a) == False{} : Bool}, lt_zero_absurd(a, e))
186    case 0n 1n+q:
187      {==}
188    case 1n+p 1n+q:
189      lt_not_le(p, q, e)
190
191def not_le_lt(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == False{} : Bool}) -> {Nat.is_lt(b, a) == True{} : Bool}:
192  match a b:
193    case 0n 0n:
194      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(e))
195    case 0n 1n+q:
196      Empty.absurd({Nat.is_lt(1n+q, 0n) == True{} : Bool}, L.true_false(e))
197    case 1n+p 0n:
198      {==}
199    case 1n+p 1n+q:
200      not_le_lt(p, q, e)
201
202def lt_asym(+a: Nat, +b: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool}, ba: {Nat.is_lt(b, a) == True{} : Bool}) -> Empty:
203  L.true_not_false(Nat.is_lt(a, a), lt_trans(a, b, a, ab, ba), lt_irrefl(a))
204
205def le_antisym(+a: Nat, +b: Nat, ab: {Nat.is_le(a, b) == True{} : Bool}, ba: {Nat.is_le(b, a) == True{} : Bool}) -> {a == b : Nat}:
206  match a b:
207    case 0n 0n:
208      {==}
209    case 0n 1n+q:
210      Empty.absurd({0n == 1n+q : Nat}, L.false_true(ba))
211    case 1n+p 0n:
212      Empty.absurd({1n+p == 0n : Nat}, L.false_true(ab))
213    case 1n+p 1n+q:
214      succ_cong(p, q, le_antisym(p, q, ab, ba))
215
216def eq_le(+a: Nat, +b: Nat, e: {a == b : Nat}) -> {Nat.is_le(a, b) == True{} : Bool}:
217  %e : {Nat.is_le(a, _) == True{} : Bool}
218  le_refl(a)
219
220def lt_ne(+a: Nat, +b: Nat, lt: {Nat.is_lt(a, b) == True{} : Bool}, e: {a == b : Nat}) -> Empty:
221  L.true_not_false(Nat.is_lt(a, a), Equal.trans(Bool, Nat.is_lt(a, a), Nat.is_lt(a, b), True{}, Equal.cong(Nat, Bool, x => Nat.is_lt(a, x), a, b, e), lt), lt_irrefl(a))
222
223def eq_from_is_eq(+a: Nat, +b: Nat, e: {Nat.is_eq(a, b) == True{} : Bool}) -> {a == b : Nat}:
224  match a b:
225    case 0n 0n:
226      {==}
227    case 0n 1n+q:
228      Empty.absurd({0n == 1n+q : Nat}, L.false_true(e))
229    case 1n+p 0n:
230      Empty.absurd({1n+p == 0n : Nat}, L.false_true(e))
231    case 1n+p 1n+q:
232      succ_cong(p, q, eq_from_is_eq(p, q, e))
233
234def is_eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
235  match a:
236    case 0n:
237      {==}
238    case 1n+p:
239      is_eq_refl(p)
240
241def is_eq_lt(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
242  match a b:
243    case _ 0n:
244      Empty.absurd({Nat.is_eq(a, 0n) == False{} : Bool}, lt_zero_absurd(a, e))
245    case 0n 1n+q:
246      {==}
247    case 1n+p 1n+q:
248      is_eq_lt(p, q, e)
249
250def lt_or_eq(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}, ne: {Nat.is_eq(a, b) == False{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
251  match a b:
252    case 0n 0n:
253      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, L.true_false(ne))
254    case 0n 1n+q:
255      {==}
256    case 1n+p 0n:
257      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, L.false_true(e))
258    case 1n+p 1n+q:
259      lt_or_eq(p, q, e, ne)
260
261# ---- addition and subtraction ----
262
263def add_sub_cancel(+a: Nat, +b: Nat) -> {Nat.sub(Nat.add(a, b), a) == b : Nat}:
264  match a b:
265    case 0n 0n:
266      {==}
267    case 0n 1n+q:
268      {==}
269    case 1n+p _:
270      add_sub_cancel(p, b)
271
272def sub_add(+a: Nat, +b: Nat, e: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.add(b, Nat.sub(a, b)) == a : Nat}:
273  match a b:
274    case 0n 0n:
275      {==}
276    case 1n+p 0n:
277      {==}
278    case 0n 1n+q:
279      Empty.absurd({Nat.add(1n+q, Nat.sub(0n, 1n+q)) == 0n : Nat}, L.false_true(e))
280    case 1n+p 1n+q:
281      succ_cong(Nat.add(q, Nat.sub(p, q)), p, sub_add(p, q, e))
282
283def sub_zero(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
284  match n:
285    case 0n:
286      {==}
287    case 1n+p:
288      {==}
289
290def sub_self(+n: Nat) -> {Nat.sub(n, n) == 0n : Nat}:
291  match n:
292    case 0n:
293      {==}
294    case 1n+p:
295      sub_self(p)
296
297def sub_succ_left(+a: Nat, +b: Nat, e: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.sub(1n+a, b) == 1n+Nat.sub(a, b) : Nat}:
298  match a b:
299    case _ 0n:
300      %Equal.sym(Nat, Nat.sub(a, 0n), a, sub_zero(a)) : {1n+a == 1n+_ : Nat}
301      {==}
302    case 0n 1n+q:
303      Empty.absurd({Nat.sub(1n, 1n+q) == 1n+Nat.sub(0n, 1n+q) : Nat}, L.false_true(e))
304    case 1n+p 1n+q:
305      sub_succ_left(p, q, e)
306
307def sub_lt(+a: Nat, +b: Nat, +c: Nat, le: {Nat.is_le(b, a) == True{} : Bool}, lt: {Nat.is_lt(a, Nat.add(b, c)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, b), c) == True{} : Bool}:
308  match a b:
309    case _ 0n:
310      %Equal.sym(Nat, Nat.sub(a, 0n), a, sub_zero(a)) : {Nat.is_lt(_, c) == True{} : Bool}
311      lt
312    case 0n 1n+q:
313      Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n+q), c) == True{} : Bool}, L.false_true(le))
314    case 1n+p 1n+q:
315      sub_lt(p, q, c, le, lt)
316
317def le_add_right(+a: Nat, +b: Nat) -> {Nat.is_le(a, Nat.add(a, b)) == True{} : Bool}:
318  match a:
319    case 0n:
320      zero_le(b)
321    case 1n+p:
322      le_add_right(p, b)
323
324def lt_add_left(+a: Nat, +b: Nat, +c: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}:
325  match c:
326    case 0n:
327      e
328    case 1n+r:
329      lt_add_left(a, b, r, e)
330
331def le_add_left(+a: Nat, +b: Nat, +c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}:
332  match c:
333    case 0n:
334      e
335    case 1n+r:
336      le_add_left(a, b, r, e)
337
338# ---- doubling and powers of two (spec/common.bend pow2) ----
339
340def double_inj(+a: Nat, +b: Nat, e: {Nat.double(a) == Nat.double(b) : Nat}) -> {a == b : Nat}:
341  match a b:
342    case 0n 0n:
343      {==}
344    case 0n 1n+q:
345      Empty.absurd({0n == 1n+q : Nat}, zero_succ(1n+Nat.double(q), e))
346    case 1n+p 0n:
347      Empty.absurd({1n+p == 0n : Nat}, succ_zero(1n+Nat.double(p), e))
348    case 1n+p 1n+q:
349      succ_cong(p, q, double_inj(p, q, succ_inj(Nat.double(p), Nat.double(q), succ_inj(1n+Nat.double(p), 1n+Nat.double(q), e))))
350
351def even_odd(+a: Nat, +b: Nat, e: {Nat.double(a) == 1n+Nat.double(b) : Nat}) -> Empty:
352  match a b:
353    case 0n _:
354      zero_succ(Nat.double(b), e)
355    case 1n+p 0n:
356      succ_zero(Nat.double(p), succ_inj(1n+Nat.double(p), 0n, e))
357    case 1n+p 1n+q:
358      even_odd(p, q, succ_inj(Nat.double(p), 1n+Nat.double(q), succ_inj(1n+Nat.double(p), 2n+Nat.double(q), e)))
359
360# bit + 2u == bit' + 2v determines both parts.
361def bit_split_bit(+b: Bool, +c: Bool, +u: Nat, +v: Nat, e: {Nat.add(S.bit_value(b), Nat.double(u)) == Nat.add(S.bit_value(c), Nat.double(v)) : Nat}) -> {b == c : Bool}:
362  match b c:
363    case False{} False{}:
364      {==}
365    case True{} True{}:
366      {==}
367    case False{} True{}:
368      Empty.absurd({False{} == True{} : Bool}, even_odd(u, v, e))
369    case True{} False{}:
370      Empty.absurd({True{} == False{} : Bool}, even_odd(v, u, Equal.sym(Nat, 1n+Nat.double(u), Nat.double(v), e)))
371
372def bit_split_val(+b: Bool, +c: Bool, +u: Nat, +v: Nat, e: {Nat.add(S.bit_value(b), Nat.double(u)) == Nat.add(S.bit_value(c), Nat.double(v)) : Nat}) -> {u == v : Nat}:
373  match b c:
374    case False{} False{}:
375      double_inj(u, v, e)
376    case True{} True{}:
377      double_inj(u, v, succ_inj(Nat.double(u), Nat.double(v), e))
378    case False{} True{}:
379      Empty.absurd({u == v : Nat}, even_odd(u, v, e))
380    case True{} False{}:
381      Empty.absurd({u == v : Nat}, even_odd(v, u, Equal.sym(Nat, 1n+Nat.double(u), Nat.double(v), e)))
382
383def double_lt(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.double(a), Nat.double(b)) == True{} : Bool}:
384  match a b:
385    case _ 0n:
386      Empty.absurd({Nat.is_lt(Nat.double(a), 0n) == True{} : Bool}, lt_zero_absurd(a, e))
387    case 0n 1n+q:
388      {==}
389    case 1n+p 1n+q:
390      double_lt(p, q, e)
391
392def double_le(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.double(a), Nat.double(b)) == True{} : Bool}:
393  match a b:
394    case 0n _:
395      zero_le(Nat.double(b))
396    case 1n+p 0n:
397      Empty.absurd({Nat.is_le(Nat.double(1n+p), 0n) == True{} : Bool}, L.false_true(e))
398    case 1n+p 1n+q:
399      double_le(p, q, e)
400
401# bit + 2u < 2v gives u < v.
402def bit_double_lt(+b: Bool, +u: Nat, +v: Nat, e: {Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}) -> {Nat.is_lt(u, v) == True{} : Bool}:
403  match b u v:
404    case _ _ 0n:
405      Empty.absurd({Nat.is_lt(u, 0n) == True{} : Bool}, lt_zero_absurd(Nat.add(S.bit_value(b), Nat.double(u)), e))
406    case _ 0n 1n+q:
407      {==}
408    case False{} 1n+p 1n+q:
409      bit_double_lt(False{}, p, q, e)
410    case True{} 1n+p 1n+q:
411      bit_double_lt(True{}, p, q, e)
412
413def double_lt_bit(+b: Bool, +u: Nat, +v: Nat, e: {Nat.is_lt(u, v) == True{} : Bool}) -> {Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}:
414  match b u v:
415    case _ _ 0n:
416      Empty.absurd({Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), 0n) == True{} : Bool}, lt_zero_absurd(u, e))
417    case False{} 0n 1n+q:
418      {==}
419    case True{} 0n 1n+q:
420      {==}
421    case False{} 1n+p 1n+q:
422      double_lt_bit(False{}, p, q, e)
423    case True{} 1n+p 1n+q:
424      double_lt_bit(True{}, p, q, e)
425
426def double_self_le(+n: Nat) -> {Nat.is_le(n, Nat.double(n)) == True{} : Bool}:
427  match n:
428    case 0n:
429      {==}
430    case 1n+p:
431      le_trans(p, Nat.double(p), 1n+Nat.double(p), double_self_le(p), le_succ(Nat.double(p)))
432
433def double_succ_le(+n: Nat, e: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_le(1n+n, Nat.double(n)) == True{} : Bool}:
434  match n:
435    case 0n:
436      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.false_true(e))
437    case 1n+p:
438      double_self_le(p)
439
440def pow2_pos(+k: Nat) -> {Nat.is_le(1n, SC.pow2(k)) == True{} : Bool}:
441  match k:
442    case 0n:
443      {==}
444    case 1n+p:
445      le_trans(1n, SC.pow2(p), Nat.double(SC.pow2(p)), pow2_pos(p), double_self_le(SC.pow2(p)))
446
447def pow2_lt_succ(+k: Nat) -> {Nat.is_lt(SC.pow2(k), SC.pow2(1n+k)) == True{} : Bool}:
448  succ_le_lt(SC.pow2(k), Nat.double(SC.pow2(k)), double_succ_le(SC.pow2(k), pow2_pos(k)))
449
450# 1 <= n gives 1 + n <= 2n.
451def pow2_mono(+a: Nat, +b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(SC.pow2(a), SC.pow2(b)) == True{} : Bool}:
452  match a b:
453    case 0n _:
454      pow2_pos(b)
455    case 1n+p 0n:
456      Empty.absurd({Nat.is_le(SC.pow2(1n+p), 1n) == True{} : Bool}, L.false_true(e))
457    case 1n+p 1n+q:
458      double_le(SC.pow2(p), SC.pow2(q), pow2_mono(p, q, e))
459
460def pow2_strict(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}:
461  match b:
462    case 0n:
463      Empty.absurd({Nat.is_lt(SC.pow2(a), 1n) == True{} : Bool}, lt_zero_absurd(a, e))
464    case 1n+q:
465      lt_le_trans(SC.pow2(a), SC.pow2(1n+a), SC.pow2(1n+q), pow2_lt_succ(a), pow2_mono(1n+a, 1n+q, lt_succ_le_succ(a, 1n+q, e)))
466
467# pred(2v) == 1 + 2 pred(v) for v >= 1.
468def pred_double(+v: Nat, e: {Nat.is_le(1n, v) == True{} : Bool}) -> {Nat.sub(Nat.double(v), 1n) == 1n+Nat.double(Nat.sub(v, 1n)) : Nat}:
469  match v:
470    case 0n:
471      Empty.absurd({Nat.sub(0n, 1n) == 1n+Nat.double(Nat.sub(0n, 1n)) : Nat}, L.false_true(e))
472    case 1n+p:
473      %Equal.sym(Nat, Nat.sub(p, 0n), p, sub_zero(p)) : {1n+Nat.double(p) == 1n+Nat.double(_) : Nat}
474      {==}
475
476def add_double(+a: Nat, +b: Nat) -> {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}:
477  match a:
478    case 0n:
479      {==}
480    case 1n+p:
481      succ_cong(1n+Nat.add(Nat.double(p), Nat.double(b)), 1n+Nat.double(Nat.add(p, b)), succ_cong(Nat.add(Nat.double(p), Nat.double(b)), Nat.double(Nat.add(p, b)), add_double(p, b)))
482
483# ---- halving ----
484#
485# `Nat.div(n, 2n)` is what the flat-array walks use to step from a block's
486# half size to the next one (the C references use `h >> 1`). Both facts below
487# come from Base's own `Nat.divmod.go`, which recurses structurally on the
488# dividend, so two unfoldings of `Nat.add(2n, i)` are a definitional step.
489
490def bump2(p: Nat & Nat) -> Nat & Nat:
491  (q, r) = p
492  (1n+q, r)
493
494def acc2(i: Nat, m: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(i, m, 1n+d, r) == bump2(Nat.divmod.go(i, m, d, r)) : Nat & Nat}:
495  match i m:
496    case 0n _:
497      {==}
498    case 1n+np 0n:
499      acc2(np, r, 1n+d, 0n)
500    case 1n+np 1n+mp:
501      acc2(np, mp, d, 1n+r)
502
503def peel2(+i: Nat, +d: Nat) -> {Nat.divmod.go(Nat.add(2n, i), 1n, d, 0n) == Nat.divmod.go(i, 1n, 1n+d, 0n) : Nat & Nat}:
504  {==}
505
506def fst_bump2(p: Nat & Nat) -> {Pair.fst(Nat, Nat, bump2(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}:
507  (q, r) = p
508  {==}
509
510def div2_step(+i: Nat) -> {Nat.div(Nat.add(2n, i), 2n) == 1n+Nat.div(i, 2n) : Nat}:
511  Equal.trans(Nat, Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n)), Pair.fst(Nat, Nat, bump2(Nat.divmod.go(i, 1n, 0n, 0n))), 1n+Pair.fst(Nat, Nat, Nat.divmod.go(i, 1n, 0n, 0n)),
512    Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n), bump2(Nat.divmod.go(i, 1n, 0n, 0n)),
513      Equal.trans(Nat & Nat, Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n), Nat.divmod.go(i, 1n, 1n, 0n), bump2(Nat.divmod.go(i, 1n, 0n, 0n)),
514        peel2(i, 0n), acc2(i, 1n, 0n, 0n))),
515    fst_bump2(Nat.divmod.go(i, 1n, 0n, 0n)))
516
517def double_succ(+y: Nat) -> {Nat.double(1n+y) == Nat.add(2n, Nat.double(y)) : Nat}:
518  %Equal.sym(Nat, Nat.double(y), Nat.add(y, y), NA.double_self(y)) : {Nat.double(1n+y) == Nat.add(2n, _) : Nat}
519  %Equal.sym(Nat, Nat.double(1n+y), Nat.add(1n+y, 1n+y), NA.double_self(1n+y)) : {_ == Nat.add(2n, Nat.add(y, y)) : Nat}
520  succ_cong(Nat.add(y, 1n+y), 1n+Nat.add(y, y), add_succ(y, y))
521
522def div2_double(x: Nat) -> {Nat.div(Nat.double(x), 2n) == x : Nat}:
523  match x:
524    case 0n:
525      {==}
526    case 1n+ +y:
527      %double_succ(y) : {Nat.div(_, 2n) == 1n+y : Nat}
528      %Equal.sym(Nat, Nat.div(Nat.add(2n, Nat.double(y)), 2n), 1n+Nat.div(Nat.double(y), 2n), div2_step(Nat.double(y))) : {_ == 1n+y : Nat}
529      succ_cong(Nat.div(Nat.double(y), 2n), y, div2_double(y))
530
531# 2^(1+r) / 2 = 2^r
532def div2_pow2(+r: Nat) -> {Nat.div(SC.pow2(1n+r), 2n) == SC.pow2(r) : Nat}:
533  div2_double(SC.pow2(r))
534
535def min_left(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
536  match a b:
537    case 0n _:
538      {==}
539    case 1n+ap 0n:
540      Empty.absurd({Nat.min(1n+ap, 0n) == 1n+ap : Nat}, lt_zero_absurd(1n+ap, h))
541    case 1n+ap 1n+bp:
542      succ_cong(Nat.min(ap, bp), ap, min_left(ap, bp, h))
543
544def min_right(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.min(a, b) == b : Nat}:
545  match a b:
546    case 0n 0n:
547      {==}
548    case 0n 1n+bp:
549      Empty.absurd({Nat.min(0n, 1n+bp) == 1n+bp : Nat}, zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
550    case 1n+ap 0n:
551      {==}
552    case 1n+ap 1n+bp:
553      succ_cong(Nat.min(ap, bp), bp, min_right(ap, bp, h))
554
555def is_eq_sym_false(+a: Nat, +b: Nat, +h: {Nat.is_eq(a, b) == False{} : Bool}) -> {Nat.is_eq(b, a) == False{} : Bool}:
556  match a b:
557    case 0n 0n:
558      h
559    case 0n 1n+q:
560      {==}
561    case 1n+p 0n:
562      {==}
563    case 1n+p 1n+q:
564      is_eq_sym_false(p, q, h)
565
566# a < b  ==>  a + c < b + c
567def lt_add_r2(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}:
568  match a b:
569    case 0n 0n:
570      Empty.absurd({Nat.is_lt(Nat.add(0n, c), Nat.add(0n, c)) == True{} : Bool}, lt_zero_absurd(0n, h))
571    case 0n 1n+q:
572      le_lt_succ(c, Nat.add(q, c), le_trans(c, Nat.add(c, q), Nat.add(q, c), le_add_right(c, q), eq_le(Nat.add(c, q), Nat.add(q, c), add_comm(c, q))))
573    case 1n+p 0n:
574      Empty.absurd({Nat.is_lt(Nat.add(1n+p, c), Nat.add(0n, c)) == True{} : Bool}, lt_zero_absurd(1n+p, h))
575    case 1n+p 1n+q:
576      lt_add_r2(p, q, c, h)