proofs/math/natural/sqrtn.bend
bend-collections-laws-containers@1.0.0.0 · 152 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
5import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as M
6import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P2
7import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/arith.bend as R
8import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/bits.bend as B
9import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/roots.bend as RT
10import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/logs.bend as LG
11
12# isqrt(n) by Heron's iteration is the integer square root: r^2 <= n <
13# (r + 1)^2. The proof follows Lean 4 Mathlib's Nat.sqrt (Mathlib/Data/Nat/
14# Defs: Nat.sqrt.iter_sq_le, Nat.sqrt.lt_iter_succ_sq): at a fixed point g
15# <= n / g, so g^2 <= n; and every step keeps n < (g + 1)^2. For the step,
16# Mathlib goes through AM-GM, 4 g n <= (g^2 + n)^2; here the same bound is
17# the product lemma u + v <= 2 w => u v <= w^2 (joint induction), applied to
18# u = g, v = n / g + 1, w = next + 1.
19
20# ---- products ----
21
22# (1 + u)(1 + v) == 1 + ((u + v) + u v)
23def succ_mul_succ(+u: Nat, +v: Nat) -> {Nat.mul(1n+u, 1n+v) == 1n+Nat.add(Nat.add(u, v), Nat.mul(u, v)) : Nat}:
24 %Equal.sym(Nat, Nat.mul(u, 1n+v), Nat.add(u, Nat.mul(u, v)), A.mul_succ(u, v)) : {Nat.add(1n+v, _) == 1n+Nat.add(Nat.add(u, v), Nat.mul(u, v)) : Nat}
25 N.succ_cong(Nat.add(v, Nat.add(u, Nat.mul(u, v))), Nat.add(Nat.add(u, v), Nat.mul(u, v)), Equal.trans(Nat, Nat.add(v, Nat.add(u, Nat.mul(u, v))), Nat.add(u, Nat.add(v, Nat.mul(u, v))), Nat.add(Nat.add(u, v), Nat.mul(u, v)), A.add_swap(v, u, Nat.mul(u, v)), Equal.sym(Nat, Nat.add(Nat.add(u, v), Nat.mul(u, v)), Nat.add(u, Nat.add(v, Nat.mul(u, v))), A.add_assoc(u, v, Nat.mul(u, v)))))
26
27# a <= b and c <= d give a + c <= b + d
28def le_add2(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +h1: {Nat.is_le(a, b) == True{} : Bool}, +h2: {Nat.is_le(c, d) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, d)) == True{} : Bool}:
29 N.le_trans(Nat.add(a, c), Nat.add(b, c), Nat.add(b, d), LG.le_add_r(a, b, c, h1), N.le_add_left(c, d, b, h2))
30
31# (1 + x) + (1 + y) == 2 + (x + y)
32def add_two(+x: Nat, +y: Nat) -> {Nat.add(1n+x, 1n+y) == 2n+Nat.add(x, y) : Nat}:
33 N.succ_cong(Nat.add(x, 1n+y), 1n+Nat.add(x, y), A.add_succ(x, y))
34
35# u + v <= 2 w gives u v <= w w
36def prod_le(+u: Nat, +v: Nat, +w: Nat, +h: {Nat.is_le(Nat.add(u, v), Nat.add(w, w)) == True{} : Bool}) -> {Nat.is_le(Nat.mul(u, v), Nat.mul(w, w)) == True{} : Bool}:
37 match u v w:
38 case 0n v0 w0:
39 N.zero_le(Nat.mul(w0, w0))
40 case 1n+ +up 0n w0:
41 %Equal.sym(Nat, Nat.mul(1n+up, 0n), 0n, A.mul_zero(1n+up)) : {Nat.is_le(_, Nat.mul(w0, w0)) == True{} : Bool}
42 N.zero_le(Nat.mul(w0, w0))
43 case 1n+ +up 1n+ +vp 0n:
44 Empty.absurd({Nat.is_le(Nat.mul(1n+up, 1n+vp), 0n) == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_le(Nat.add(1n+up, 1n+vp), 0n), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, 0n), 2n+Nat.add(up, vp), Nat.add(1n+up, 1n+vp), Equal.sym(Nat, Nat.add(1n+up, 1n+vp), 2n+Nat.add(up, vp), add_two(up, vp))), h)))
45 case 1n+ +up 1n+ +vp 1n+ +wp:
46 +h2 = Equal.trans(Bool, Nat.is_le(Nat.add(up, vp), Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), Nat.add(1n+wp, 1n+wp)), True{},
47 Equal.trans(Bool, Nat.is_le(Nat.add(up, vp), Nat.add(wp, wp)), Nat.is_le(2n+Nat.add(up, vp), 2n+Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), Nat.add(1n+wp, 1n+wp)), {==},
48 Equal.trans(Bool, Nat.is_le(2n+Nat.add(up, vp), 2n+Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), 2n+Nat.add(wp, wp)), Nat.is_le(Nat.add(1n+up, 1n+vp), Nat.add(1n+wp, 1n+wp)), Equal.cong(Nat, Bool, z => Nat.is_le(z, 2n+Nat.add(wp, wp)), 2n+Nat.add(up, vp), Nat.add(1n+up, 1n+vp), Equal.sym(Nat, Nat.add(1n+up, 1n+vp), 2n+Nat.add(up, vp), add_two(up, vp))), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(1n+up, 1n+vp), z), 2n+Nat.add(wp, wp), Nat.add(1n+wp, 1n+wp), Equal.sym(Nat, Nat.add(1n+wp, 1n+wp), 2n+Nat.add(wp, wp), add_two(wp, wp))))), h)
49 %Equal.sym(Nat, Nat.mul(1n+up, 1n+vp), 1n+Nat.add(Nat.add(up, vp), Nat.mul(up, vp)), succ_mul_succ(up, vp)) : {Nat.is_le(_, Nat.mul(1n+wp, 1n+wp)) == True{} : Bool}
50 %Equal.sym(Nat, Nat.mul(1n+wp, 1n+wp), 1n+Nat.add(Nat.add(wp, wp), Nat.mul(wp, wp)), succ_mul_succ(wp, wp)) : {Nat.is_le(1n+Nat.add(Nat.add(up, vp), Nat.mul(up, vp)), _) == True{} : Bool}
51 le_add2(Nat.add(up, vp), Nat.add(wp, wp), Nat.mul(up, vp), Nat.mul(wp, wp), h2, prod_le(up, vp, wp, h2))
52
53# ---- the fixed point: next >= g gives g^2 <= n (Mathlib Nat.sqrt.iter_sq_le) ----
54
55def stop_sq(+n: Nat, +g: Nat, +h: {Nat.is_lt(M.sqrt_next(n, g), g) == False{} : Bool}) -> {Nat.is_le(Nat.mul(g, g), n) == True{} : Bool}:
56 match g:
57 case 0n:
58 N.zero_le(n)
59 case 1n+ +gp:
60 +q = Nat.div(n, 1n+gp)
61 +hge = N.not_lt_le(M.sqrt_next(n, 1n+gp), 1n+gp, h)
62 +h2 = Equal.trans(Bool, Nat.is_le(1n+gp, q), Nat.is_le(Nat.add(1n+gp, 1n+gp), Nat.add(1n+gp, q)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(1n+gp, 1n+gp), Nat.add(1n+gp, q)), Nat.is_le(1n+gp, q), R.le_add_cancel(1n+gp, 1n+gp, q)),
63 Equal.trans(Bool, Nat.is_le(Nat.add(1n+gp, 1n+gp), Nat.add(1n+gp, q)), Nat.is_le(Nat.mul(1n+gp, 2n), Nat.add(1n+gp, q)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(1n+gp, q)), Nat.add(1n+gp, 1n+gp), Nat.mul(1n+gp, 2n), Equal.sym(Nat, Nat.mul(1n+gp, 2n), Nat.add(1n+gp, 1n+gp), RT.two_mul(1n+gp))),
64 Equal.trans(Bool, Nat.is_le(Nat.mul(1n+gp, 2n), Nat.add(1n+gp, q)), Nat.is_le(1n+gp, M.sqrt_next(n, 1n+gp)), True{}, Equal.sym(Bool, Nat.is_le(1n+gp, Nat.div(Nat.add(1n+gp, q), 2n)), Nat.is_le(Nat.mul(1n+gp, 2n), Nat.add(1n+gp, q)), R.le_div(1n, 1n+gp, Nat.add(1n+gp, q))), hge)))
65 Equal.trans(Bool, Nat.is_le(Nat.mul(1n+gp, 1n+gp), n), Nat.is_le(1n+gp, q), True{}, Equal.sym(Bool, Nat.is_le(1n+gp, Nat.div(n, 1n+gp)), Nat.is_le(Nat.mul(1n+gp, 1n+gp), n), R.le_div(gp, 1n+gp, n)), h2)
66
67def le_zero(+g: Nat, +h: {Nat.is_le(g, 0n) == True{} : Bool}) -> {g == 0n : Nat}:
68 match g:
69 case 0n:
70 {==}
71 case 1n+gp:
72 Empty.absurd({1n+gp == 0n : Nat}, L.false_true(h))
73
74def iter_sq(fuel: Nat, +n: Nat, +g: Nat, +m: Nat, +down: Bool, +hm: {m == M.sqrt_next(n, g) : Nat}, +hd: {down == Nat.is_lt(m, g) : Bool}, +hf: {Nat.is_le(g, fuel) == True{} : Bool}) -> {Nat.is_le(Nat.mul(M.sqrt_iter(fuel, n, g, m, down), M.sqrt_iter(fuel, n, g, m, down)), n) == True{} : Bool}:
75 match fuel down:
76 case 0n False{}:
77 %Equal.sym(Nat, g, 0n, le_zero(g, hf)) : {Nat.is_le(Nat.mul(_, _), n) == True{} : Bool}
78 N.zero_le(n)
79 case 0n True{}:
80 %Equal.sym(Nat, g, 0n, le_zero(g, hf)) : {Nat.is_le(Nat.mul(_, _), n) == True{} : Bool}
81 N.zero_le(n)
82 case 1n+f False{}:
83 stop_sq(n, g, Equal.trans(Bool, Nat.is_lt(M.sqrt_next(n, g), g), Nat.is_lt(m, g), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, g), M.sqrt_next(n, g), m, Equal.sym(Nat, m, M.sqrt_next(n, g), hm)), Equal.sym(Bool, False{}, Nat.is_lt(m, g), hd)))
84 case 1n+ +f True{}:
85 iter_sq(f, n, m, M.sqrt_next(n, m), Nat.is_lt(M.sqrt_next(n, m), m), {==}, {==}, RT.shrink(m, g, f, Equal.sym(Bool, True{}, Nat.is_lt(m, g), hd), hf))
86
87# ---- a step keeps n < (g + 1)^2 (Mathlib Nat.sqrt.lt_iter_succ_sq) ----
88
89def step_lt(+n: Nat, +gp: Nat, +m: Nat, +hm: {m == M.sqrt_next(n, 1n+gp) : Nat}) -> {Nat.is_lt(n, Nat.mul(1n+m, 1n+m)) == True{} : Bool}:
90 +g = {1n+gp : Nat}
91 +q = Nat.div(n, g)
92 +r = Nat.mod(n, g)
93 +s = Nat.add(g, q)
94 # n < g (q + 1)
95 +ha = Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.add(Nat.mul(q, g), g)), True{},
96 Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.add(Nat.mul(q, g), g)),
97 Equal.cong(Nat, Bool, z => Nat.is_lt(z, Nat.mul(g, 1n+q)), n, Nat.add(Nat.mul(q, g), r), R.dm_eq(gp, n)),
98 Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(Nat.mul(q, g), r), z), Nat.mul(g, 1n+q), Nat.add(Nat.mul(q, g), g), Equal.trans(Nat, Nat.mul(g, 1n+q), Nat.mul(1n+q, g), Nat.add(Nat.mul(q, g), g), A.mul_comm(g, 1n+q), A.add_comm(g, Nat.mul(q, g))))),
99 N.lt_add_left(r, g, Nat.mul(q, g), R.dm_lt(gp, n)))
100 # g + (q + 1) <= 2 (m + 1): s == 2 m + (s mod 2)
101 +es = Equal.trans(Nat, s, Nat.add(Nat.double(m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), Nat.mod(s, 2n)),
102 Equal.trans(Nat, s, Nat.add(Nat.double(Nat.div(s, 2n)), Nat.mod(s, 2n)), Nat.add(Nat.double(m), Nat.mod(s, 2n)), B.half_eq(s), Equal.cong(Nat, Nat, z => Nat.add(Nat.double(z), Nat.mod(s, 2n)), Nat.div(s, 2n), m, Equal.sym(Nat, m, Nat.div(s, 2n), hm))),
103 Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(s, 2n)), Nat.double(m), Nat.add(m, m), A.double_self(m)))
104 +hs = Equal.trans(Bool, Nat.is_le(s, 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), 1n)), True{},
105 Equal.trans(Bool, Nat.is_le(s, 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), 1n)),
106 Equal.cong(Nat, Bool, z => Nat.is_le(z, 1n+Nat.add(m, m)), s, Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), es),
107 Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), z), 1n+Nat.add(m, m), Nat.add(Nat.add(m, m), 1n), A.add_comm(1n, Nat.add(m, m)))),
108 N.le_add_left(Nat.mod(s, 2n), 1n, Nat.add(m, m), N.lt_succ_le(Nat.mod(s, 2n), 1n, B.half_rem(s))))
109 +hb = Equal.trans(Bool, Nat.is_le(Nat.add(g, 1n+q), Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, 2n+Nat.add(m, m)), True{},
110 Equal.trans(Bool, Nat.is_le(Nat.add(g, 1n+q), Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, 2n+Nat.add(m, m)),
111 Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(1n+m, 1n+m)), Nat.add(g, 1n+q), 1n+s, A.add_succ(g, q)),
112 Equal.cong(Nat, Bool, z => Nat.is_le(1n+s, z), Nat.add(1n+m, 1n+m), 2n+Nat.add(m, m), add_two(m, m))),
113 hs)
114 N.lt_le_trans(n, Nat.mul(g, 1n+q), Nat.mul(1n+m, 1n+m), ha, prod_le(g, 1n+q, 1n+m, hb))
115
116def step_any(+n: Nat, +g: Nat, +m: Nat, +hm: {m == M.sqrt_next(n, g) : Nat}, +hlt: {Nat.is_lt(m, g) == True{} : Bool}) -> {Nat.is_lt(n, Nat.mul(1n+m, 1n+m)) == True{} : Bool}:
117 match g:
118 case 0n:
119 Empty.absurd({Nat.is_lt(n, Nat.mul(1n+m, 1n+m)) == True{} : Bool}, N.lt_zero_absurd(m, hlt))
120 case 1n+ +gp:
121 step_lt(n, gp, m, hm)
122
123def iter_lt(fuel: Nat, +n: Nat, +g: Nat, +m: Nat, +down: Bool, +hm: {m == M.sqrt_next(n, g) : Nat}, +hd: {down == Nat.is_lt(m, g) : Bool}, +hn: {Nat.is_lt(n, Nat.mul(1n+g, 1n+g)) == True{} : Bool}) -> {Nat.is_lt(n, Nat.mul(1n+M.sqrt_iter(fuel, n, g, m, down), 1n+M.sqrt_iter(fuel, n, g, m, down))) == True{} : Bool}:
124 match fuel down:
125 case 0n False{}:
126 hn
127 case 0n True{}:
128 hn
129 case 1n+f False{}:
130 hn
131 case 1n+ +f True{}:
132 iter_lt(f, n, m, M.sqrt_next(n, m), Nat.is_lt(M.sqrt_next(n, m), m), {==}, {==}, step_any(n, g, m, hm, Equal.sym(Bool, True{}, Nat.is_lt(m, g), hd)))
133
134# ---- the theorems ----
135
136def g0_bound(+n: Nat) -> {Nat.is_lt(n, Nat.mul(1n+P2.pow2t(1n+Nat.div(M.bit_length(n), 2n)), 1n+P2.pow2t(1n+Nat.div(M.bit_length(n), 2n)))) == True{} : Bool}:
137 +g = P2.pow2t(1n+Nat.div(M.bit_length(n), 2n))
138 +lt = N.not_le_lt(Nat.pow(g, 2n), n, Equal.trans(Bool, Nat.is_le(Nat.pow(g, 2n), n), M.root_le(n, 2n, g), False{}, Equal.sym(Bool, M.root_le(n, 2n, g), Nat.is_le(Nat.pow(g, 2n), n), RT.root_le_ok(n, 2n, g)), RT.hi_bound(n, 1n)))
139 +lt2 = Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, g)), Nat.is_lt(n, Nat.pow(g, 2n)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(n, Nat.mul(g, z)), g, Nat.mul(g, 1n), Equal.sym(Nat, Nat.mul(g, 1n), g, A.mul_one(g))), lt)
140 N.lt_le_trans(n, Nat.mul(g, g), Nat.mul(1n+g, 1n+g), lt2, prod_le(g, g, 1n+g, le_add2(g, 1n+g, g, 1n+g, N.le_succ(g), N.le_succ(g))))
141
142# isqrt(n)^2 <= n (Mathlib Nat.sqrt_le')
143def isqrt_le(+n: Nat) -> {Nat.is_le(Nat.pow(M.isqrt(n), 2n), n) == True{} : Bool}:
144 +g = P2.pow2t(1n+Nat.div(M.bit_length(n), 2n))
145 %Equal.sym(Nat, Nat.pow(M.isqrt(n), 2n), Nat.mul(M.isqrt(n), M.isqrt(n)), Equal.cong(Nat, Nat, z => Nat.mul(M.isqrt(n), z), Nat.mul(M.isqrt(n), 1n), M.isqrt(n), A.mul_one(M.isqrt(n)))) : {Nat.is_le(_, n) == True{} : Bool}
146 iter_sq(g, n, g, M.sqrt_next(n, g), Nat.is_lt(M.sqrt_next(n, g), g), {==}, {==}, N.le_refl(g))
147
148# n < (isqrt(n) + 1)^2 (Mathlib Nat.lt_succ_sqrt')
149def lt_succ_isqrt(+n: Nat) -> {Nat.is_lt(n, Nat.pow(1n+M.isqrt(n), 2n)) == True{} : Bool}:
150 +g = P2.pow2t(1n+Nat.div(M.bit_length(n), 2n))
151 %Equal.sym(Nat, Nat.pow(1n+M.isqrt(n), 2n), Nat.mul(1n+M.isqrt(n), 1n+M.isqrt(n)), Equal.cong(Nat, Nat, z => Nat.mul(1n+M.isqrt(n), z), Nat.mul(1n+M.isqrt(n), 1n), 1n+M.isqrt(n), A.mul_one(1n+M.isqrt(n)))) : {Nat.is_lt(n, _) == True{} : Bool}
152 iter_lt(g, n, g, M.sqrt_next(n, g), Nat.is_lt(M.sqrt_next(n, g), g), {==}, {==}, g0_bound(n))