1 import Base 2 import ../../lib/nat.bend as N 3 import ../../lib/logic.bend as L 4 import ../../../spec/lib/common.bend as SC 5 import ../../lib/lemmas/proofs/nat_algebra.bend as A 6 import ../../lib/lemmas/proofs/natural_products.bend as PR 7 import ../../../src/math/natural.bend as M 8 import ../../../src/math/pow2.bend as P2 9 import ../pow2/pow2.bend as PP 10 import ./arith.bend as R 11 import ./lcm.bend as LC 12 import ./fact.bend as F 13 import ./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 23 def 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 31 def 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 40 def 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 55 def 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 69 def 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 73 def 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 81 def 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 89 def 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 109 def 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 125 def 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 137 def 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 140 def 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) 144 def 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 149 def 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 152 def 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 177 def 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 183 def 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) 193 def 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) 203 def 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 213 def 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 222 def 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 226 def 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 231 def 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 235 def 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 239 def 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 248 def 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 251 def iroot_zero(+n: Nat) -> {M.iroot(n, 0n) == Fail{M.Domain{}} : Result<&2, &2, M.MathError, Nat>}: 252 {==} 253 254 def 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 257 def 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))