def ilog_fin

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:687

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/u32.bend as U32P
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
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

687def ilog_fin(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +b: U32, +nb: Nat, +hb: {v(b) == nb : Nat}, +hl: {Nat.is_lt(nb, 2n) == False{} : Bool}) -> {G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), nb, False{})) : Result<&2, &2, NM.NumError, Nat>}:
688  match nb:
689    case 0n:
690      Empty.absurd({G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 0n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl))
691    case 1n:
692      Empty.absurd({G.ilog_ok(~U32, ~I.u32_op, ~I.u32_is, n, b, False{}) == SG.lift_nat(M.ilog_ok(v(n), 1n, False{})) : Result<&2, &2, NM.NumError, Nat>}, true_ne_false(hl))
693    case 2n+ +bq:
694      +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), {==})
695      +q = I.u32_op(NM.Quot{n, b})
696      +dq = Nat.div(v(n), 2n+bq)
697      +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))
698      +one = I.u32_op(NM.One{})
699      +up = G.le(~U32, ~I.u32_is, one, q)
700      +hup = lev(one, q, 1n, dq, one_v(), eq)
701      +hn = U32P.val_lt(1n, {==}, K, hK, n)
702      +hK2 = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==})
703      +s = ilsim(140n, q, b, 0n, one, v(n), bq, 1n, eq, hb, one_v(), K, hK, hn, up, hup)
704      +c1 = Equal.cong(Bool, Nat, t => M.ilog_go(140n, v(n), 2n+bq, 0n, 1n, t), up, Nat.is_le(1n, dq), hup)
705      +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))
706      +r = M.ilog_go(v(n), v(n), 2n+bq, 0n, 1n, Nat.is_le(1n, dq))
707      Equal.cong(Nat, Result<&2, &2, NM.NumError, Nat>, t => Done{t}, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, 140n, q, b, 0n, one, up), r, Equal.trans(Nat, G.ilog_go(~U32, ~I.u32_op, ~I.u32_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)))