proofs/math/natural/roots.bend
bend-collections-laws-containers@1.0.0.0 · 258 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as PR
7import bend-collections-laws-containers@1.0.0.0/src/math/natural.bend as M
8import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P2
9import bend-collections-laws-containers@1.0.0.0/proofs/math/pow2/pow2.bend as PP
10import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/arith.bend as R
11import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/lcm.bend as LC
12import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/fact.bend as F
13import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/bits.bend as B
14
15# iroot is the exact integer root: r^k <= n < (r + 1)^k for
16# r = iroot(n, k), k >= 1, so r is the floor of the k-th root. Statement
17# shape of Lean 4 Mathlib Mathlib/Data/Nat/Sqrt (Nat.sqrt_le',
18# Nat.lt_succ_sqrt'), for every k; the binary-search proof follows the Why3 gallery's
19# isqrt (loop invariant lo^2 <= n < hi^2 with a shrinking interval).
20
21# ---- the power test r^k <= n ----
22
23def pow_pos(+rp: Nat, +j: Nat) -> {Nat.is_lt(0n, Nat.pow(1n+rp, j)) == True{} : Bool}:
24 match j:
25 case 0n:
26 {==}
27 case 1n+ +jp:
28 F.pos_mul(rp, Nat.pow(1n+rp, jp), pow_pos(rp, jp))
29
30# x <= x y for y > 0
31def le_mul_pos(+x: Nat, +y: Nat, +hy: {Nat.is_lt(0n, y) == True{} : Bool}) -> {Nat.is_le(x, Nat.mul(x, y)) == True{} : Bool}:
32 match y:
33 case 0n:
34 Empty.absurd({Nat.is_le(x, Nat.mul(x, 0n)) == True{} : Bool}, L.false_true(hy))
35 case 1n+ +yp:
36 %Equal.sym(Nat, Nat.mul(x, 1n+yp), Nat.add(x, Nat.mul(x, yp)), A.mul_succ(x, yp)) : {Nat.is_le(x, _) == True{} : Bool}
37 N.le_add_right(x, Nat.mul(x, yp))
38
39# the division-guarded loop computes (acc r) r^j <= n
40def pow_le_case(+j: Nat, +rp: Nat, +acc: Nat, +n: Nat, +ok: Bool, +hk: {ok == Nat.is_le(Nat.mul(acc, 1n+rp), n) : Bool}) -> {M.pow_le_go(1n+j, 1n+rp, acc, n, ok) == Nat.is_le(Nat.mul(Nat.mul(acc, 1n+rp), Nat.pow(1n+rp, j)), n) : Bool}:
41 match j ok:
42 case 0n False{}:
43 Equal.sym(Bool, Nat.is_le(Nat.mul(Nat.mul(acc, 1n+rp), 1n), n), False{}, Equal.trans(Bool, Nat.is_le(Nat.mul(Nat.mul(acc, 1n+rp), 1n), n), Nat.is_le(Nat.mul(acc, 1n+rp), n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(Nat.mul(acc, 1n+rp), 1n), Nat.mul(acc, 1n+rp), A.mul_one(Nat.mul(acc, 1n+rp))), Equal.sym(Bool, False{}, Nat.is_le(Nat.mul(acc, 1n+rp), n), hk)))
44 case 1n+ +jp False{}:
45 +big = N.not_le_lt(Nat.mul(acc, 1n+rp), n, Equal.sym(Bool, False{}, Nat.is_le(Nat.mul(acc, 1n+rp), n), hk))
46 Equal.sym(Bool, Nat.is_le(Nat.mul(Nat.mul(acc, 1n+rp), Nat.pow(1n+rp, 1n+jp)), n), False{}, N.lt_not_le(n, Nat.mul(Nat.mul(acc, 1n+rp), Nat.pow(1n+rp, 1n+jp)), N.lt_le_trans(n, Nat.mul(acc, 1n+rp), Nat.mul(Nat.mul(acc, 1n+rp), Nat.pow(1n+rp, 1n+jp)), big, le_mul_pos(Nat.mul(acc, 1n+rp), Nat.pow(1n+rp, 1n+jp), pow_pos(rp, 1n+jp)))))
47 case 0n True{}:
48 Equal.trans(Bool, True{}, Nat.is_le(Nat.mul(acc, 1n+rp), n), Nat.is_le(Nat.mul(Nat.mul(acc, 1n+rp), 1n), n), hk, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(acc, 1n+rp), Nat.mul(Nat.mul(acc, 1n+rp), 1n), Equal.sym(Nat, Nat.mul(Nat.mul(acc, 1n+rp), 1n), Nat.mul(acc, 1n+rp), A.mul_one(Nat.mul(acc, 1n+rp)))))
49 case 1n+ +jp True{}:
50 +ar = Nat.mul(acc, 1n+rp)
51 %Equal.sym(Nat, Nat.mul(ar, Nat.mul(1n+rp, Nat.pow(1n+rp, jp))), Nat.mul(Nat.mul(ar, 1n+rp), Nat.pow(1n+rp, jp)), Equal.sym(Nat, Nat.mul(Nat.mul(ar, 1n+rp), Nat.pow(1n+rp, jp)), Nat.mul(ar, Nat.mul(1n+rp, Nat.pow(1n+rp, jp))), A.mul_assoc(ar, 1n+rp, Nat.pow(1n+rp, jp)))) : {M.pow_le_go(1n+jp, 1n+rp, ar, n, Nat.is_le(ar, Nat.div(n, 1n+rp))) == Nat.is_le(_, n) : Bool}
52 pow_le_case(jp, rp, ar, n, Nat.is_le(ar, Nat.div(n, 1n+rp)), R.le_div(rp, ar, n))
53
54# root_le(n, k, r) is r^k <= n
55def root_le_ok(+n: Nat, +k: Nat, +r: Nat) -> {M.root_le(n, k, r) == Nat.is_le(Nat.pow(r, k), n) : Bool}:
56 match k r:
57 case 0n r0:
58 {==}
59 case 1n+ +kp 0n:
60 Equal.sym(Bool, Nat.is_le(0n, n), True{}, N.zero_le(n))
61 case 1n+ +kp 1n+ +rp:
62 +c = pow_le_case(kp, rp, 1n, n, Nat.is_le(1n, Nat.div(n, 1n+rp)), R.le_div(rp, 1n, n))
63 %Equal.sym(Nat, Nat.pow(1n+rp, 1n+kp), Nat.mul(Nat.mul(1n, 1n+rp), Nat.pow(1n+rp, kp)), Equal.cong(Nat, Nat, z => Nat.mul(z, Nat.pow(1n+rp, kp)), 1n+rp, Nat.mul(1n, 1n+rp), Equal.sym(Nat, Nat.mul(1n, 1n+rp), 1n+rp, LC.one_mul(1n+rp)))) : {M.root_le(n, 1n+kp, 1n+rp) == Nat.is_le(_, n) : Bool}
64 c
65
66# ---- the search interval ----
67
68# x 2 == x + x
69def two_mul(+x: Nat) -> {Nat.mul(x, 2n) == Nat.add(x, x) : Nat}:
70 Equal.trans(Nat, Nat.mul(x, 2n), Nat.mul(2n, x), Nat.add(x, x), A.mul_comm(x, 2n), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(x, 0n), x, A.add_zero(x)))
71
72# lo + 1 < hi gives lo < (lo + hi) / 2
73def lo_lt_mid(+lo: Nat, +hi: Nat, +h: {Nat.is_lt(1n+lo, hi) == True{} : Bool}) -> {Nat.is_lt(lo, M.mid(lo, hi)) == True{} : Bool}:
74 +e = Equal.trans(Bool, Nat.is_le(1n+lo, M.mid(lo, hi)), Nat.is_le(Nat.mul(1n+lo, 2n), Nat.add(lo, hi)), Nat.is_le(Nat.add(2n, lo), hi), R.le_div(1n, 1n+lo, Nat.add(lo, hi)),
75 Equal.trans(Bool, Nat.is_le(Nat.mul(1n+lo, 2n), Nat.add(lo, hi)), Nat.is_le(Nat.add(lo, Nat.add(2n, lo)), Nat.add(lo, hi)), Nat.is_le(Nat.add(2n, lo), hi),
76 Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(lo, hi)), Nat.mul(1n+lo, 2n), Nat.add(lo, Nat.add(2n, lo)), Equal.trans(Nat, Nat.mul(1n+lo, 2n), Nat.add(2n, Nat.add(lo, lo)), Nat.add(lo, Nat.add(2n, lo)), Equal.cong(Nat, Nat, z => Nat.add(2n, z), Nat.mul(lo, 2n), Nat.add(lo, lo), two_mul(lo)), A.add_swap(2n, lo, lo))),
77 R.le_add_cancel(lo, Nat.add(2n, lo), hi)))
78 N.succ_le_lt(lo, M.mid(lo, hi), Equal.trans(Bool, Nat.is_le(1n+lo, M.mid(lo, hi)), Nat.is_le(Nat.add(2n, lo), hi), True{}, e, N.lt_succ_le_succ(1n+lo, hi, h)))
79
80# lo < hi gives (lo + hi) / 2 < hi
81def mid_lt_hi(+lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}) -> {Nat.is_lt(M.mid(lo, hi), hi) == True{} : Bool}:
82 +e = Equal.trans(Bool, Nat.is_le(hi, M.mid(lo, hi)), Nat.is_le(Nat.mul(hi, 2n), Nat.add(lo, hi)), False{}, R.le_div(1n, hi, Nat.add(lo, hi)),
83 Equal.trans(Bool, Nat.is_le(Nat.mul(hi, 2n), Nat.add(lo, hi)), Nat.is_le(Nat.add(hi, hi), Nat.add(hi, lo)), False{},
84 Equal.trans(Bool, Nat.is_le(Nat.mul(hi, 2n), Nat.add(lo, hi)), Nat.is_le(Nat.add(hi, hi), Nat.add(lo, hi)), Nat.is_le(Nat.add(hi, hi), Nat.add(hi, lo)), Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(lo, hi)), Nat.mul(hi, 2n), Nat.add(hi, hi), two_mul(hi)), Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(hi, hi), z), Nat.add(lo, hi), Nat.add(hi, lo), A.add_comm(lo, hi))),
85 Equal.trans(Bool, Nat.is_le(Nat.add(hi, hi), Nat.add(hi, lo)), Nat.is_le(hi, lo), False{}, R.le_add_cancel(hi, hi, lo), N.lt_not_le(lo, hi, h))))
86 N.not_le_lt(hi, M.mid(lo, hi), e)
87
88# b < c <= a gives a - c < a - b
89def lt_sub(+a: Nat, +b: Nat, +c: Nat, +h1: {Nat.is_lt(b, c) == True{} : Bool}, +h2: {Nat.is_le(c, a) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, c), Nat.sub(a, b)) == True{} : Bool}:
90 match a b c:
91 case 0n 0n 0n:
92 Empty.absurd({Nat.is_lt(Nat.sub(0n, 0n), Nat.sub(0n, 0n)) == True{} : Bool}, L.false_true(h1))
93 case 0n 0n 1n+cp:
94 Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n+cp), Nat.sub(0n, 0n)) == True{} : Bool}, L.false_true(h2))
95 case 0n 1n+bp 0n:
96 Empty.absurd({Nat.is_lt(Nat.sub(0n, 0n), Nat.sub(0n, 1n+bp)) == True{} : Bool}, L.false_true(h1))
97 case 0n 1n+bp 1n+cp:
98 Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n+cp), Nat.sub(0n, 1n+bp)) == True{} : Bool}, L.false_true(h2))
99 case 1n+ap 0n 0n:
100 Empty.absurd({Nat.is_lt(Nat.sub(1n+ap, 0n), Nat.sub(1n+ap, 0n)) == True{} : Bool}, L.false_true(h1))
101 case 1n+ +ap 0n 1n+ +cp:
102 N.le_lt_succ(Nat.sub(ap, cp), ap, F.sub_le_self(ap, cp))
103 case 1n+ap 1n+bp 0n:
104 Empty.absurd({Nat.is_lt(Nat.sub(1n+ap, 0n), Nat.sub(1n+ap, 1n+bp)) == True{} : Bool}, L.false_true(h1))
105 case 1n+ +ap 1n+ +bp 1n+ +cp:
106 lt_sub(ap, bp, cp, h1, h2)
107
108# a < b and c <= a give a - c < b - c
109def lt_sub2(+a: Nat, +b: Nat, +c: Nat, +h1: {Nat.is_lt(a, b) == True{} : Bool}, +h2: {Nat.is_le(c, a) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}:
110 match a b c:
111 case 0n 0n c0:
112 Empty.absurd({Nat.is_lt(Nat.sub(0n, c0), Nat.sub(0n, c0)) == True{} : Bool}, L.false_true(h1))
113 case 0n 1n+bp 0n:
114 {==}
115 case 0n 1n+bp 1n+cp:
116 Empty.absurd({Nat.is_lt(Nat.sub(0n, 1n+cp), Nat.sub(1n+bp, 1n+cp)) == True{} : Bool}, L.false_true(h2))
117 case 1n+ap 0n c0:
118 Empty.absurd({Nat.is_lt(Nat.sub(1n+ap, c0), Nat.sub(0n, c0)) == True{} : Bool}, L.false_true(h1))
119 case 1n+ap 1n+bp 0n:
120 h1
121 case 1n+ +ap 1n+ +bp 1n+ +cp:
122 lt_sub2(ap, bp, cp, h1, h2)
123
124# lo < hi gives 0 < hi - lo
125def sub_pos(+lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(hi, lo)) == True{} : Bool}:
126 match lo hi:
127 case lo0 0n:
128 Empty.absurd({Nat.is_lt(0n, Nat.sub(0n, lo0)) == True{} : Bool}, N.lt_zero_absurd(lo0, h))
129 case 0n 1n+hp:
130 {==}
131 case 1n+ +lp 1n+ +hp:
132 sub_pos(lp, hp, h)
133
134# ---- the search ----
135
136# the answer r: r^k <= n < (r + 1)^k, through root_le
137def root_ok(+n: Nat, +k: Nat, +r: Nat) -> Type:
138 {M.root_le(n, k, r) == True{} : Bool} & {M.root_le(n, k, 1n+r) == False{} : Bool}
139
140def no_fuel(+lo: Nat, +hi: Nat, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}, +hf: {Nat.is_le(Nat.sub(hi, lo), 0n) == True{} : Bool}) -> Empty:
141 N.lt_zero_absurd(0n, N.lt_le_trans(0n, Nat.sub(hi, lo), 0n, sub_pos(lo, hi, hlt), hf))
142
143# lo + 1 >= hi with lo < hi: the interval is [lo, lo + 1)
144def done_ok(+n: Nat, +k: Nat, +lo: Nat, +hi: Nat, +hlo: {M.root_le(n, k, lo) == True{} : Bool}, +hhi: {M.root_le(n, k, hi) == False{} : Bool}, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}, +hm: {False{} == Nat.is_lt(1n+lo, hi) : Bool}) -> root_ok(n, k, lo):
145 +e = N.le_antisym(hi, 1n+lo, N.not_lt_le(1n+lo, hi, Equal.sym(Bool, False{}, Nat.is_lt(1n+lo, hi), hm)), N.lt_succ_le_succ(lo, hi, hlt))
146 (hlo, Equal.trans(Bool, M.root_le(n, k, 1n+lo), M.root_le(n, k, hi), False{}, Equal.cong(Nat, Bool, z => M.root_le(n, k, z), 1n+lo, hi, Equal.sym(Nat, hi, 1n+lo, e)), hhi))
147
148# the interval shrinks: a step fits in the remaining fuel
149def shrink(+x: Nat, +y: Nat, +f: Nat, +h: {Nat.is_lt(x, y) == True{} : Bool}, +hf: {Nat.is_le(y, 1n+f) == True{} : Bool}) -> {Nat.is_le(x, f) == True{} : Bool}:
150 N.lt_succ_le(x, f, N.lt_le_trans(x, y, 1n+f, h, hf))
151
152def search_ok(fuel: Nat, +n: Nat, +k: Nat, +lo: Nat, +hi: Nat, +more: Bool, +ok: Bool, +hlo: {M.root_le(n, k, lo) == True{} : Bool}, +hhi: {M.root_le(n, k, hi) == False{} : Bool}, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}, +hf: {Nat.is_le(Nat.sub(hi, lo), fuel) == True{} : Bool}, +hm: {more == Nat.is_lt(1n+lo, hi) : Bool}, +hok: {ok == M.root_le(n, k, M.mid(lo, hi)) : Bool}) -> root_ok(n, k, M.search_go(fuel, n, k, lo, hi, more, ok)):
153 match fuel more ok:
154 case 0n False{} False{}:
155 Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, False{}, False{})), no_fuel(lo, hi, hlt, hf))
156 case 0n False{} True{}:
157 Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, False{}, True{})), no_fuel(lo, hi, hlt, hf))
158 case 0n True{} False{}:
159 Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, True{}, False{})), no_fuel(lo, hi, hlt, hf))
160 case 0n True{} True{}:
161 Empty.absurd(root_ok(n, k, M.search_go(0n, n, k, lo, hi, True{}, True{})), no_fuel(lo, hi, hlt, hf))
162 case 1n+f False{} False{}:
163 done_ok(n, k, lo, hi, hlo, hhi, hlt, hm)
164 case 1n+f False{} True{}:
165 done_ok(n, k, lo, hi, hlo, hhi, hlt, hm)
166 case 1n+ +f True{} True{}:
167 +m = M.mid(lo, hi)
168 +hml = lo_lt_mid(lo, hi, Equal.sym(Bool, True{}, Nat.is_lt(1n+lo, hi), hm))
169 +hmh = mid_lt_hi(lo, hi, hlt)
170 search_ok(f, n, k, m, hi, Nat.is_lt(1n+m, hi), M.root_le(n, k, M.mid(m, hi)), Equal.sym(Bool, True{}, M.root_le(n, k, m), hok), hhi, hmh, shrink(Nat.sub(hi, m), Nat.sub(hi, lo), f, lt_sub(hi, lo, m, hml, N.lt_le(m, hi, hmh)), hf), {==}, {==})
171 case 1n+ +f True{} False{}:
172 +m = M.mid(lo, hi)
173 +hml = lo_lt_mid(lo, hi, Equal.sym(Bool, True{}, Nat.is_lt(1n+lo, hi), hm))
174 +hmh = mid_lt_hi(lo, hi, hlt)
175 search_ok(f, n, k, lo, m, Nat.is_lt(1n+lo, m), M.root_le(n, k, M.mid(lo, m)), hlo, Equal.sym(Bool, False{}, M.root_le(n, k, m), hok), hml, shrink(Nat.sub(m, lo), Nat.sub(hi, lo), f, lt_sub2(m, hi, lo, hmh, N.lt_le(lo, m, hml)), hf), {==}, {==})
176
177def search_top(+n: Nat, +k: Nat, +lo: Nat, +hi: Nat, +hlo: {M.root_le(n, k, lo) == True{} : Bool}, +hhi: {M.root_le(n, k, hi) == False{} : Bool}, +hlt: {Nat.is_lt(lo, hi) == True{} : Bool}) -> root_ok(n, k, M.search(n, k, lo, hi)):
178 search_ok(Nat.sub(hi, lo), n, k, lo, hi, Nat.is_lt(1n+lo, hi), M.root_le(n, k, M.mid(lo, hi)), hlo, hhi, hlt, N.le_refl(Nat.sub(hi, lo)), {==}, {==})
179
180# ---- the initial bound hi = 2^(1 + L/k), L = bit_length(n) ----
181
182# 2^(x + y) == 2^x 2^y
183def pow2_add(+x: Nat, +y: Nat) -> {SC.pow2(Nat.add(x, y)) == Nat.mul(SC.pow2(x), SC.pow2(y)) : Nat}:
184 match x:
185 case 0n:
186 Equal.sym(Nat, Nat.mul(1n, SC.pow2(y)), SC.pow2(y), LC.one_mul(SC.pow2(y)))
187 case 1n+ +xp:
188 Equal.trans(Nat, Nat.double(SC.pow2(Nat.add(xp, y))), Nat.double(Nat.mul(SC.pow2(xp), SC.pow2(y))), Nat.mul(Nat.double(SC.pow2(xp)), SC.pow2(y)),
189 Equal.cong(Nat, Nat, z => Nat.double(z), SC.pow2(Nat.add(xp, y)), Nat.mul(SC.pow2(xp), SC.pow2(y)), pow2_add(xp, y)),
190 Equal.sym(Nat, Nat.mul(Nat.double(SC.pow2(xp)), SC.pow2(y)), Nat.double(Nat.mul(SC.pow2(xp), SC.pow2(y))), PR.double_product(SC.pow2(xp), SC.pow2(y))))
191
192# (2^a)^k == 2^(k a)
193def pow_pow2(+a: Nat, +k: Nat) -> {Nat.pow(SC.pow2(a), k) == SC.pow2(Nat.mul(k, a)) : Nat}:
194 match k:
195 case 0n:
196 {==}
197 case 1n+ +kp:
198 Equal.trans(Nat, Nat.mul(SC.pow2(a), Nat.pow(SC.pow2(a), kp)), Nat.mul(SC.pow2(a), SC.pow2(Nat.mul(kp, a))), SC.pow2(Nat.add(a, Nat.mul(kp, a))),
199 Equal.cong(Nat, Nat, z => Nat.mul(SC.pow2(a), z), Nat.pow(SC.pow2(a), kp), SC.pow2(Nat.mul(kp, a)), pow_pow2(a, kp)),
200 Equal.sym(Nat, SC.pow2(Nat.add(a, Nat.mul(kp, a))), Nat.mul(SC.pow2(a), SC.pow2(Nat.mul(kp, a))), pow2_add(a, Nat.mul(kp, a))))
201
202# L <= k (1 + L / k)
203def bl_le(+kp: Nat, +bl: Nat) -> {Nat.is_le(bl, Nat.mul(1n+kp, 1n+Nat.div(bl, 1n+kp))) == True{} : Bool}:
204 +k = {1n+kp : Nat}
205 +q = Nat.div(bl, k)
206 +r = Nat.mod(bl, k)
207 %Equal.sym(Nat, bl, Nat.add(Nat.mul(q, k), r), R.dm_eq(kp, bl)) : {Nat.is_le(_, Nat.mul(k, 1n+q)) == True{} : Bool}
208 %Equal.sym(Nat, Nat.mul(k, 1n+q), Nat.add(k, Nat.mul(k, q)), A.mul_succ(k, q)) : {Nat.is_le(Nat.add(Nat.mul(q, k), r), _) == True{} : Bool}
209 %Equal.sym(Nat, Nat.add(k, Nat.mul(k, q)), Nat.add(Nat.mul(q, k), k), Equal.trans(Nat, Nat.add(k, Nat.mul(k, q)), Nat.add(Nat.mul(k, q), k), Nat.add(Nat.mul(q, k), k), A.add_comm(k, Nat.mul(k, q)), Equal.cong(Nat, Nat, z => Nat.add(z, k), Nat.mul(k, q), Nat.mul(q, k), A.mul_comm(k, q)))) : {Nat.is_le(Nat.add(Nat.mul(q, k), r), _) == True{} : Bool}
210 N.lt_le(Nat.add(Nat.mul(q, k), r), Nat.add(Nat.mul(q, k), k), N.lt_add_left(r, k, Nat.mul(q, k), R.dm_lt(kp, bl)))
211
212# n < (2^(1 + L/k))^k
213def hi_bound(+n: Nat, +kp: Nat) -> {M.root_le(n, 1n+kp, P2.pow2t(1n+Nat.div(M.bit_length(n), 1n+kp))) == False{} : Bool}:
214 +k = {1n+kp : Nat}
215 +a = {1n+Nat.div(M.bit_length(n), k) : Nat}
216 +big = N.lt_le_trans(n, SC.pow2(M.bit_length(n)), SC.pow2(Nat.mul(k, a)), B.bit_length_lt(n), N.pow2_mono(M.bit_length(n), Nat.mul(k, a), bl_le(kp, M.bit_length(n))))
217 %Equal.sym(Nat, P2.pow2t(a), SC.pow2(a), PP.same(a)) : {M.root_le(n, k, _) == False{} : Bool}
218 %Equal.sym(Bool, M.root_le(n, k, SC.pow2(a)), Nat.is_le(Nat.pow(SC.pow2(a), k), n), root_le_ok(n, k, SC.pow2(a))) : {_ == False{} : Bool}
219 %Equal.sym(Nat, Nat.pow(SC.pow2(a), k), SC.pow2(Nat.mul(k, a)), pow_pow2(a, k)) : {Nat.is_le(_, n) == False{} : Bool}
220 N.lt_not_le(n, SC.pow2(Nat.mul(k, a)), big)
221
222def hi_pos(+a: Nat) -> {Nat.is_lt(0n, P2.pow2t(a)) == True{} : Bool}:
223 %Equal.sym(Nat, P2.pow2t(a), SC.pow2(a), PP.same(a)) : {Nat.is_lt(0n, _) == True{} : Bool}
224 N.succ_le_lt(0n, SC.pow2(a), N.pow2_pos(a))
225
226def root_top(+n: Nat, +kp: Nat) -> root_ok(n, 1n+kp, M.search(n, 1n+kp, 0n, P2.pow2t(1n+Nat.div(M.bit_length(n), 1n+kp)))):
227 search_top(n, 1n+kp, 0n, P2.pow2t(1n+Nat.div(M.bit_length(n), 1n+kp)), {==}, hi_bound(n, kp), hi_pos(1n+Nat.div(M.bit_length(n), 1n+kp)))
228
229# ---- the theorems ----
230
231def ok_le(+n: Nat, +k: Nat, +r: Nat, p: root_ok(n, k, r)) -> {Nat.is_le(Nat.pow(r, k), n) == True{} : Bool}:
232 (a, b) = p
233 Equal.trans(Bool, Nat.is_le(Nat.pow(r, k), n), M.root_le(n, k, r), True{}, Equal.sym(Bool, M.root_le(n, k, r), Nat.is_le(Nat.pow(r, k), n), root_le_ok(n, k, r)), a)
234
235def ok_lt(+n: Nat, +k: Nat, +r: Nat, p: root_ok(n, k, r)) -> {Nat.is_lt(n, Nat.pow(1n+r, k)) == True{} : Bool}:
236 (a, b) = p
237 N.not_le_lt(Nat.pow(1n+r, k), n, Equal.trans(Bool, Nat.is_le(Nat.pow(1n+r, k), n), M.root_le(n, k, 1n+r), False{}, Equal.sym(Bool, M.root_le(n, k, 1n+r), Nat.is_le(Nat.pow(1n+r, k), n), root_le_ok(n, k, 1n+r)), b))
238
239def iroot_k_ok(+n: Nat, +kp: Nat) -> root_ok(n, 1n+kp, M.iroot_k(n, 1n+kp)):
240 match kp:
241 case 0n:
242 (Equal.trans(Bool, M.root_le(n, 1n, n), Nat.is_le(Nat.mul(n, 1n), n), True{}, root_le_ok(n, 1n, n), Equal.trans(Bool, Nat.is_le(Nat.mul(n, 1n), n), Nat.is_le(n, n), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(n, 1n), n, A.mul_one(n)), N.le_refl(n))),
243 Equal.trans(Bool, M.root_le(n, 1n, 1n+n), Nat.is_le(Nat.mul(1n+n, 1n), n), False{}, root_le_ok(n, 1n, 1n+n), Equal.trans(Bool, Nat.is_le(Nat.mul(1n+n, 1n), n), Nat.is_le(1n+n, n), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, n), Nat.mul(1n+n, 1n), 1n+n, A.mul_one(1n+n)), N.lt_not_le(n, 1n+n, N.lt_succ(n)))))
244 case 1n+ +kq:
245 root_top(n, 1n+kq)
246
247# iroot(n, k) == Done{r} with r^k <= n < (r + 1)^k for k >= 1, Domain for k == 0
248def iroot_done(+n: Nat, +kp: Nat) -> {M.iroot(n, 1n+kp) == Done{M.iroot_k(n, 1n+kp)} : Result<&2, &2, M.MathError, Nat>}:
249 {==}
250
251def iroot_zero(+n: Nat) -> {M.iroot(n, 0n) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}:
252 {==}
253
254def iroot_le(+n: Nat, +kp: Nat) -> {Nat.is_le(Nat.pow(M.iroot_k(n, 1n+kp), 1n+kp), n) == True{} : Bool}:
255 ok_le(n, 1n+kp, M.iroot_k(n, 1n+kp), iroot_k_ok(n, kp))
256
257def lt_succ_iroot(+n: Nat, +kp: Nat) -> {Nat.is_lt(n, Nat.pow(1n+M.iroot_k(n, 1n+kp), 1n+kp)) == True{} : Bool}:
258 ok_lt(n, 1n+kp, M.iroot_k(n, 1n+kp), iroot_k_ok(n, kp))