def iroot_big

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:1194

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT
import bend-collections-laws-math@1.0.0.0/src/math/pow2.bend as P2
import bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend as PP

1194def iroot_big(+K: Nat, +hK: {K == 64n : Nat}, +n: WU.U64, +kp: Nat) -> {v(G.iroot_k(~WU.U64, ~I.u64_op, ~I.u64_is, n, 2n+kp)) == M.iroot_k(v(n), 2n+kp) : Nat}:
1195  +bg = G.bit_length(~WU.U64, ~I.u64_op, ~I.u64_is, n)
1196  +bl = M.bit_length(v(n))
1197  +ebl = bit_length_k(K, hK, n)
1198  +hn = LW.val_lt(K, hK, n)
1199  +hbl = L.subst(Nat, z => {Nat.is_le(bl, z) == True{} : Bool}, K, 64n, hK, NF.bl_le_n(K, v(n), hn))
1200  +E2 = {1n+Nat.div(bl, 2n+kp) : Nat}
1201  +E = {1n+Nat.div(bg, 2n+kp) : Nat}
1202  +eE = Equal.cong(Nat, Nat, t => 1n+Nat.div(t, 2n+kp), bg, bl, ebl)
1203  +hE2 = NF.e_lt64(kp, bl, hbl)
1204  +hE = L.subst(Nat, z => {Nat.is_lt(z, 64n) == True{} : Bool}, E2, E, Equal.sym(Nat, E, E2, eE), hE2)
1205  +hi = I.u64_op(NM.Pow2{E})
1206  +W = C.pow2(E2)
1207  ehi0 = LW.ops_pow2(E, hE)
1208  +ehi = Equal.trans(Nat, v(hi), C.pow2(E), W, ehi0, Equal.cong(Nat, Nat, t => C.pow2(t), E, E2, eE))
1209  +zero = I.u64_op(NM.ZeroOp{})
1210  +m = G.imid(~WU.U64, ~I.u64_op, zero, hi)
1211  +hm = imid_v(K, hK, zero, hi, 0n, W, zero_v(), ehi)
1212  +hmore = ltv(I.u64_op(NM.One{}), hi, 1n, W, one_v(), ehi)
1213  +hhit = Equal.trans(Bool, G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, 2n+kp, m), Nat.is_le(Nat.pow(v(m), 2n+kp), v(n)), Nat.is_le(Nat.pow(Nat.div(W, 2n), 2n+kp), v(n)), rl_v(K, hK, n, 2n+kp, m), Equal.cong(Nat, Bool, t => Nat.is_le(Nat.pow(t, 2n+kp), v(n)), v(m), Nat.div(W, 2n), hm))
1214  +R = M.iroot_k(v(n), 2n+kp)
1215  +hb = Equal.trans(Bool, Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), M.root_le(v(n), 2n+kp, P2.pow2t(E2)), False{}, Equal.sym(Bool, M.root_le(v(n), 2n+kp, P2.pow2t(E2)), Nat.is_le(Nat.pow(P2.pow2t(E2), 2n+kp), v(n)), RT.root_le_ok(v(n), 2n+kp, P2.pow2t(E2))), RT.hi_bound(v(n), 1n+kp))
1216  +hb2 = L.subst(Nat, z => {Nat.is_le(Nat.pow(z, 2n+kp), v(n)) == False{} : Bool}, P2.pow2t(E2), W, PP.same(E2), hb)
1217  +hR1 = RT.iroot_le(v(n), 1n+kp)
1218  +hr = NF.root_above(R, W, 2n+kp, v(n), hb2, hR1)
1219  +hf = N.le_trans(1n+E2, 64n, 140n, N.lt_succ_le_succ(E2, 64n, hE2), {==})
1220  srch(140n, n, 2n+kp, zero, hi, m, I.u64_is(NM.Lt{I.u64_op(NM.One{}), hi}), G.root_le(~WU.U64, ~I.u64_op, ~I.u64_is, n, 2n+kp, m), E2, 0n, W, R, K, hK, zero_v(), ehi, hm, hR1, RT.lt_succ_iroot(v(n), 1n+kp), N.zero_le(R), hr, hmore, hhit, N.le_refl(W), hf)