proofs/lib/nat.bend
bend-collections-laws-containers@1.0.0.0 · 576 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@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)