def ilsim

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

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

662def ilsim(+f: Nat, +q: U32, +b: U32, +k: Nat, +p: U32, +nn: Nat, +bq: Nat, +np: Nat, +hq: {v(q) == Nat.div(nn, 2n+bq) : Nat}, +hb: {v(b) == 2n+bq : Nat}, +hp: {v(p) == np : Nat}, +K: Nat, +hK: {K == 32n : Nat}, +hn: {Nat.is_lt(nn, C.pow2(K)) == True{} : Bool}, +up: Bool, +hup: {up == Nat.is_le(np, Nat.div(nn, 2n+bq)) : Bool}) -> {G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, f, q, b, k, p, up) == M.ilog_go(f, nn, 2n+bq, k, np, up) : Nat}:
663  match f up:
664    case 0n _:
665      {==}
666    case 1n+g False{}:
667      {==}
668    case 1n+ +g True{}:
669      +hle = Equal.sym(Bool, True{}, Nat.is_le(np, Nat.div(nn, 2n+bq)), hup)
670      +hmn = Equal.trans(Bool, Nat.is_le(Nat.mul(np, 2n+bq), nn), Nat.is_le(np, Nat.div(nn, 2n+bq)), True{}, Equal.sym(Bool, Nat.is_le(np, Nat.div(nn, 2n+bq)), Nat.is_le(Nat.mul(np, 2n+bq), nn), NR.le_div(1n+bq, np, nn)), hle)
671      +emul = nmul(v(p), v(b), np, 2n+bq, hp, hb)
672      +hfit = fits32(K, hK, Nat.mul(v(p), v(b)), L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, Nat.mul(np, 2n+bq), Nat.mul(v(p), v(b)), Equal.sym(Nat, Nat.mul(v(p), v(b)), Nat.mul(np, 2n+bq), emul), N.le_lt_trans(Nat.mul(np, 2n+bq), nn, C.pow2(K), hmn, hn)))
673      +hmo = Equal.trans(Bool, I.u32_is(NM.MulOver{p, b}), Bool.not(C.fits(32n, Nat.mul(v(p), v(b)))), False{}, LW.tests_mul_over(p, b), Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(32n, Nat.mul(v(p), v(b))), True{}, hfit))
674      +pb = I.u32_op(NM.Mul{p, b})
675      +epb = Equal.trans(Nat, v(pb), Nat.mul(v(p), v(b)), Nat.mul(np, 2n+bq), LW.ops_mul(p, b, hmo), emul)
676      +u2 = G.le(~U32, ~I.u32_is, pb, q)
677      +hu2 = lev(pb, q, Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq), epb, hq)
678      Equal.trans(Nat, G.ilog_go(~U32, ~I.u32_op, ~I.u32_is, g, q, b, 1n+k, pb, u2), M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), u2), M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), Nat.is_le(Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq))), ilsim(g, q, b, 1n+k, pb, nn, bq, Nat.mul(np, 2n+bq), hq, hb, epb, K, hK, hn, u2, hu2), Equal.cong(Bool, Nat, t => M.ilog_go(g, nn, 2n+bq, 1n+k, Nat.mul(np, 2n+bq), t), u2, Nat.is_le(Nat.mul(np, 2n+bq), Nat.div(nn, 2n+bq)), hu2))