def inv_top

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

import Base
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/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

626def inv_top(+k: Nat, +hk: {k == 32n : Nat}, +a: U32, +m: U32, +c: Bool, +hc: {I.u32_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, c) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), nm)) : Result<&2, &2, NM.NumError, U32>}:
627  match c nm:
628    case True{} 0n:
629      {==}
630    case False{} 0n:
631      Empty.absurd({G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, False{}) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), 0n)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc)))
632    case True{} 1n+ +mp:
633      Empty.absurd({G.inv_ok(~U32, ~I.u32_op, ~I.u32_is, a, m, True{}) == SG.lift(~U32, ~SG.u32_of, M.mod_inverse(v(a), 1n+mp)) : Result<&2, &2, NM.NumError, U32>}, true_ne_false(Equal.trans(Bool, True{}, I.u32_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u32_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm))))
634    case False{} 1n+ +mp:
635      +r1 = I.u32_op(NM.Rem{a, m})
636      +ra = Nat.mod(v(a), 1n+mp)
637      +hk2 = L.subst(Nat, z => {Nat.is_le(1n+Nat.double(z), 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
638      +s = invsim(140n, k, hk, m, mp, hnm, m, I.u32_op(NM.ZeroOp{}), I.u32_op(NM.One{}), r1, 1n+mp, 0n, 1n, hnm, zero_v(), one_v(), {==}, I.u32_is(NM.IsZero{r1}), ra, {==}, pm_rem(a, m, mp, hnm), hb_init(mp, v(a)))
639      +bz = M.inv_go(1n+mp, 1n+mp, 1n+mp, 0n, ra, 1n)
640      g = G.inv_go(~U32, ~I.u32_op, ~I.u32_is, 140n, m, m, I.u32_op(NM.ZeroOp{}), I.u32_op(NM.One{}), (r1, I.u32_is(NM.IsZero{r1})))
641      finsim(m, mp, hnm, g, bz, Equal.trans(M.Bezout, pv(g), M.inv_go(140n, 1n+mp, 1n+mp, 0n, ra, 1n), bz, s, NF.inv_140(k, mp, v(a), hk2, mv(k, hk, m, mp, hnm))))