def inv_top

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

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/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

627def inv_top(+k: Nat, +hk: {k == 64n : Nat}, +a: WU.U64, +m: WU.U64, +c: Bool, +hc: {I.u64_is(NM.IsZero{m}) == c : Bool}, +nm: Nat, +hnm: {v(m) == nm : Nat}) -> {G.inv_ok(~WU.U64, ~I.u64_op, ~I.u64_is, a, m, c) == SG.lift(~WU.U64, ~SG.u64_of, M.mod_inverse(v(a), nm)) : Result<&2, &2, NM.NumError, WU.U64>}:
628  match c nm:
629    case True{} 0n:
630      {==}
631    case False{} 0n:
632      Empty.absurd({G.inv_ok(~WU.U64, ~I.u64_op, ~I.u64_is, a, m, False{}) == SG.lift(~WU.U64, ~SG.u64_of, M.mod_inverse(v(a), 0n)) : Result<&2, &2, NM.NumError, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, I.u64_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u64_is(NM.IsZero{m}), True{}, iz(m, 0n, hnm)), hc)))
633    case True{} 1n+ +mp:
634      Empty.absurd({G.inv_ok(~WU.U64, ~I.u64_op, ~I.u64_is, a, m, True{}) == SG.lift(~WU.U64, ~SG.u64_of, M.mod_inverse(v(a), 1n+mp)) : Result<&2, &2, NM.NumError, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, I.u64_is(NM.IsZero{m}), False{}, Equal.sym(Bool, I.u64_is(NM.IsZero{m}), True{}, hc), iz(m, 1n+mp, hnm))))
635    case False{} 1n+ +mp:
636      +r1 = I.u64_op(NM.Rem{a, m})
637      +ra = Nat.mod(v(a), 1n+mp)
638      +hk2 = L.subst(Nat, z => {Nat.is_le(1n+Nat.double(z), 140n) == True{} : Bool}, 64n, k, Equal.sym(Nat, k, 64n, hk), {==})
639      +s = invsim(140n, k, hk, m, mp, hnm, m, I.u64_op(NM.ZeroOp{}), I.u64_op(NM.One{}), r1, 1n+mp, 0n, 1n, hnm, zero_v(), one_v(), {==}, I.u64_is(NM.IsZero{r1}), ra, {==}, pm_rem(a, m, mp, hnm), hb_init(mp, v(a)))
640      +bz = M.inv_go(1n+mp, 1n+mp, 1n+mp, 0n, ra, 1n)
641      g = G.inv_go(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, m, m, I.u64_op(NM.ZeroOp{}), I.u64_op(NM.One{}), (r1, I.u64_is(NM.IsZero{r1})))
642      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))))