def powsim

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

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/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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

1070def powsim(+f: Nat, +e: Nat, +b: U32, +bok: Bool, +a: U32, +aok: Bool, +nb: Nat, +na: Nat, +t0: Nat, +md: Bool, +ct: Bool, +he: {Nat.is_le(e, f) == True{} : Bool}, +hB: {C.fits(32n, nb) == bok : Bool}, +hb: {fv(bok, v(b), nb) == nb : Nat}, +hmb: {mode(md, nb) == True{} : Bool}, +hA: {C.fits(32n, na) == aok : Bool}, +ha: {fv(aok, v(a), na) == na : Nat}, +hma: {mode(md, na) == True{} : Bool}, +ht: {Nat.mul(na, Nat.pow(nb, e)) == t0 : Nat}, +hct: {C.fits(32n, t0) == ct : Bool}) -> {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, f, e, b, bok, (a, aok)) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}:
1071  match f e:
1072    case 0n 0n:
1073      pw_fin(a, aok, na, t0, ct, hA, ha, Equal.trans(Nat, na, Nat.mul(na, 1n), t0, Equal.sym(Nat, Nat.mul(na, 1n), na, NA.mul_one(na)), ht), hct)
1074    case 0n 1n+j:
1075      Empty.absurd({G.pow_go(~U32, ~I.u32_op, ~I.u32_is, 0n, 1n+j, b, bok, (a, aok)) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, he)))
1076    case 1n+g 0n:
1077      pw_fin(a, aok, na, t0, ct, hA, ha, Equal.trans(Nat, na, Nat.mul(na, 1n), t0, Equal.sym(Nat, Nat.mul(na, 1n), na, NA.mul_one(na)), ht), hct)
1078    case 1n+ +g 1n+ +j:
1079      +more = Nat.is_lt(1n, 1n+j)
1080      +bit = Nat.is_eq(Nat.mod(1n+j, 2n), 1n)
1081      +e2 = Nat.div(1n+j, 2n)
1082      +ht2 = Equal.trans(Nat, Nat.mul(NF.msn(bit, na, nb), Nat.pow(NF.sqn(more, nb), e2)), Nat.mul(na, Nat.pow(nb, 1n+j)), t0, NF.powstep(j, na, nb), ht)
1083      +he2 = N.le_trans(e2, j, g, NF.half_le(j), he)
1084      +ih = powsim(g, e2, G.sq_val(~U32, ~I.u32_op, more, b), G.sq_ok(~U32, ~I.u32_is, more, b, bok), ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok), NF.sqn(more, nb), NF.msn(bit, na, nb), t0, md, ct, he2, sq_fits(more, b, bok, nb, md, hB, hb, hmb), sq_fv(more, b, bok, nb, hb), sq_mode(more, nb, md, hmb), ms_fits(bit, a, aok, b, bok, na, nb, md, hA, ha, hma, hB, hb, hmb), ms_fv(bit, a, aok, b, bok, na, nb, ha, hb), ms_mode(bit, na, nb, md, hma, hmb), ht2, hct)
1085      L.subst(U32 & Bool, z => {G.pow_go(~U32, ~I.u32_op, ~I.u32_is, g, e2, G.sq_val(~U32, ~I.u32_op, more, b), G.sq_ok(~U32, ~I.u32_is, more, b, bok), z) == G.fits(U32, Bool.not(ct), of(t0)) : Maybe<&2, U32>}, (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)), G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)), Equal.sym(U32 & Bool, G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)), (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)), ms_eq(bit, b, bok, a, aok)), ih)