def combsim

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

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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LW
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/combnat.bend as CN
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

1242def combsim(+f: Nat, +n: WU.U64, +i: WU.U64, +k: WU.U64, +r: WU.U64, +nn: Nat, +ni: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 64n : Nat}, +hn: {v(n) == nn : Nat}, +hi: {v(i) == ni : Nat}, +hk: {v(k) == k0 : Nat}, +h2: {Nat.is_le(Nat.double(k0), nn) == True{} : Bool}, +hle: {Nat.is_le(ni, k0) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, ni)) == True{} : Bool}, +hok: {C.fits(64n, S.choose(nn, ni)) == ok : Bool}, +ha: {fv(ok, v(r), S.choose(nn, ni)) == S.choose(nn, ni) : Nat}, +hmore: {more == Nat.is_lt(ni, k0) : Bool}, +hcn: {C.fits(64n, S.choose(nn, k0)) == cn : Bool}) -> {G.comb_go(~WU.U64, ~I.u64_op, ~I.u64_is, f, n, i, k, (r, ok), more) == G.fits(WU.U64, Bool.not(cn), of(S.choose(nn, k0))) : Maybe<&2, WU.U64>}:
1243  match f ok more cn:
1244    case 0n True{} _ _:
1245      +h2i = N.le_trans(Nat.double(ni), Nat.double(k0), nn, N.double_le(ni, k0, hle), h2)
1246      +big = CN.cbig(K, nn, ni, N.le_trans(K, 1n+K, ni, N.le_succ(K), hf), h2i)
1247      Empty.absurd({G.comb_go(~WU.U64, ~I.u64_op, ~I.u64_is, 0n, n, i, k, (r, True{}), more) == G.fits(WU.U64, Bool.not(cn), of(S.choose(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.choose(nn, ni), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.choose(nn, ni), C.pow2(K)), True{}, fk(K, hK, S.choose(nn, ni), hok)), N.le_not_lt(S.choose(nn, ni), C.pow2(K), big))))
1248    case 0n False{} _ True{}:
1249      Empty.absurd({G.comb_go(~WU.U64, ~I.u64_op, ~I.u64_is, 0n, n, i, k, (r, False{}), more) == G.fits(WU.U64, Bool.not(True{}), of(S.choose(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, S.choose(nn, k0)), False{}, Equal.sym(Bool, C.fits(64n, S.choose(nn, k0)), True{}, hcn), unfit_mono(64n, S.choose(nn, ni), S.choose(nn, k0), CN.cmono(nn, ni, k0, hle, h2), hok))))
1250    case 0n False{} _ False{}:
1251      {==}
1252    case 1n+g False{} _ True{}:
1253      Empty.absurd({G.comb_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, n, i, k, (r, False{}), more) == G.fits(WU.U64, Bool.not(True{}), of(S.choose(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, S.choose(nn, k0)), False{}, Equal.sym(Bool, C.fits(64n, S.choose(nn, k0)), True{}, hcn), unfit_mono(64n, S.choose(nn, ni), S.choose(nn, k0), CN.cmono(nn, ni, k0, hle, h2), hok))))
1254    case 1n+g False{} _ False{}:
1255      {==}
1256    case 1n+g True{} False{} True{}:
1257      +eik = N.le_antisym(ni, k0, hle, N.not_lt_le(ni, k0, Equal.sym(Bool, False{}, Nat.is_lt(ni, k0), hmore)))
1258      Equal.cong(WU.U64, Maybe<&2, WU.U64>, t => Some{t}, r, of(S.choose(nn, k0)), as_of(r, S.choose(nn, k0), Equal.trans(Nat, v(r), S.choose(nn, ni), S.choose(nn, k0), ha, Equal.cong(Nat, Nat, t => S.choose(nn, t), ni, k0, eik))))
1259    case 1n+g True{} False{} False{}:
1260      +eik = N.le_antisym(ni, k0, hle, N.not_lt_le(ni, k0, Equal.sym(Bool, False{}, Nat.is_lt(ni, k0), hmore)))
1261      Empty.absurd({G.comb_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, n, i, k, (r, True{}), False{}) == G.fits(WU.U64, Bool.not(False{}), of(S.choose(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, S.choose(nn, ni)), False{}, Equal.sym(Bool, C.fits(64n, S.choose(nn, ni)), True{}, hok), Equal.trans(Bool, C.fits(64n, S.choose(nn, ni)), C.fits(64n, S.choose(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(64n, S.choose(nn, t)), ni, k0, eik), hcn))))
1262    case 1n+ +g True{} True{} _:
1263      +hlt = Equal.sym(Bool, True{}, Nat.is_lt(ni, k0), hmore)
1264      +hin = N.le_trans(ni, k0, nn, N.lt_le(ni, k0, hlt), N.le_trans(k0, Nat.double(k0), nn, N.double_self_le(k0), h2))
1265      +x = G.inc(~WU.U64, ~I.u64_op, i)
1266      +ex = inc_v(K, hK, i, k, ni, k0, hi, hk, hlt)
1267      +t = I.u64_op(NM.Sub{n, i})
1268      +tn = Nat.sub(nn, ni)
1269      +et = Equal.trans(Nat, v(t), Nat.sub(v(n), v(i)), tn, LW.ops_sub(n, i, le_v(i, n, ni, nn, hi, hn, hin)), nsub(v(n), v(i), nn, ni, hn, hi))
1270      +c = S.choose(nn, ni)
1271      +c1 = S.choose(nn, 1n+ni)
1272      +ce = FA.choose_succ_right(nn, ni)
1273      +gu = G.gcd(~WU.U64, ~I.u64_op, ~I.u64_is, r, x)
1274      +eg = Equal.trans(Nat, v(gu), M.gcd(v(r), v(x)), CN.gg(c, ni), gcd_val(r, x), Equal.trans(Nat, M.gcd(v(r), v(x)), M.gcd(c, v(x)), M.gcd(c, 1n+ni), Equal.cong(Nat, Nat, z => M.gcd(z, v(x)), v(r), c, ha), Equal.cong(Nat, Nat, z => M.gcd(c, z), v(x), 1n+ni, ex)))
1275      +au = I.u64_op(NM.Quot{r, gu})
1276      +ea = Equal.trans(Nat, v(au), Nat.div(c, CN.gg(c, ni)), CN.wl(c, ni), quot_v(r, gu, c, CN.gg(c, ni), ha, eg, CN.g_pos(c, ni)), CN.div_c(c, ni))
1277      +ju = I.u64_op(NM.Quot{x, gu})
1278      +ej = Equal.trans(Nat, v(ju), Nat.div(1n+ni, CN.gg(c, ni)), CN.wr(c, ni), quot_v(x, gu, 1n+ni, CN.gg(c, ni), ex, eg, CN.g_pos(c, ni)), CN.div_j(c, ni))
1279      +bu = I.u64_op(NM.Quot{t, ju})
1280      +eb = Equal.trans(Nat, v(bu), Nat.div(tn, CN.wr(c, ni)), CN.sq(c, ni, tn, c1), quot_v(t, ju, tn, CN.wr(c, ni), et, ej, CN.wr_pos(c, ni)), CN.div_t(c, ni, tn, c1, ce))
1281      +hpn = Equal.trans(Nat, Nat.mul(v(au), v(bu)), Nat.mul(CN.wl(c, ni), CN.sq(c, ni, tn, c1)), c1, nmul(v(au), v(bu), CN.wl(c, ni), CN.sq(c, ni, tn, c1), ea, eb), CN.prod_eq(c, ni, tn, c1, ce))
1282      +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, ni), Nat.add(g, 1n+ni), Equal.sym(Nat, Nat.add(g, 1n+ni), 1n+Nat.add(g, ni), NA.add_succ(g, ni)), hf)
1283      combsim(g, n, x, k, I.u64_op(NM.Mul{au, bu}), nn, 1n+ni, k0, K, Bool.not(I.u64_is(NM.MulOver{au, bu})), I.u64_is(NM.Lt{x, k}), cn, hK, hn, ex, hk, h2, succ_le(ni, k0, hlt), hf2, ok_mul(au, bu, c1, hpn), fv_mul(au, bu, c1, hpn, C.fits(64n, c1), {==}), ltv(x, k, 1n+ni, k0, ex, hk), hcn)