def ilog_fin

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

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/spec/math/generic.bend as SG
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/lib/arith.bend as AR2

688def ilog_fin(+K: Nat, +hK: {K == 64n : Nat}, +n: WU.U64, +b: WU.U64, +nb: Nat, +hb: {v(b) == nb : Nat}, +hl: {Nat.is_lt(nb, 2n) == False{} : Bool}) -> {G.ilog_ok(~WU.U64, ~I.u64_op, ~I.u64_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), nb, False{})) : Result<&2, &2, NM.NumError, Nat>}:
689  match nb:
690    case 0n:
691      Empty.absurd({G.ilog_ok(~WU.U64, ~I.u64_op, ~I.u64_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 0n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl))
692    case 1n:
693      Empty.absurd({G.ilog_ok(~WU.U64, ~I.u64_op, ~I.u64_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 1n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl))
694    case 2n+ +bq:
695      +hnz = Equal.trans(Bool, Nat.is_eq(v(b), 0n), Nat.is_eq(2n+bq, 0n), False{}, Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(b), 2n+bq, hb), {==})
696      +q = I.u64_op(NM.Quot{n, b})
697      +dq = Nat.div(v(n), 2n+bq)
698      +eq = Equal.trans(Nat, v(q), Nat.div(v(n), v(b)), dq, LW.ops_quot(n, b, hnz), Equal.cong(Nat, Nat, t => Nat.div(v(n), t), v(b), 2n+bq, hb))
699      +one = I.u64_op(NM.One{})
700      +up = G.le(~WU.U64, ~I.u64_is, one, q)
701      +hup = lev(one, q, 1n, dq, one_v(), eq)
702      +hn = LW.val_lt(K, hK, n)
703      +hK2 = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 64n, K, Equal.sym(Nat, K, 64n, hK), {==})
704      +s = ilsim(140n, q, b, 0n, one, v(n), bq, 1n, eq, hb, one_v(), K, hK, hn, up, hup)
705      +c1 = Equal.cong(Bool, Nat, t => M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, t), up, Nat.is_le(1n, dq), hup)
706      +c2 = NF.il_140(K, v(n), bq, hK2, N.le_lt_trans(dq, v(n), C.pow2(K), AR2.div_le(v(n), 2n+bq), hn))
707      +r = M.ilog_go(v(n), v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq))
708      Equal.cong(Nat, Result<&2, &2, NM.NumError, Nat>, t => Done{t}, G.ilog_go(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, q, b, 0n, one, up), r, Equal.trans(Nat, G.ilog_go(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, q, b, 0n, one, up), M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, up), r, s, Equal.trans(Nat, M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, up), M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq)), r, c1, c2)))