def comb_top

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

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/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/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/natural/fact.bend as FA
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

1303def comb_top(+K: Nat, +hK: {K == 64n : Nat}, +n: WU.U64, +k: WU.U64, +big: Bool, +hbig: {I.u64_is(NM.Lt{n, k}) == big : Bool}) -> {G.comb_big(~WU.U64, ~I.u64_op, ~I.u64_is, n, k, big) == SG.checked(~WU.U64, ~SG.u64_of, 64n, S.choose(v(n), v(k))) : Result<&2, &2, NM.NumError, WU.U64>}:
1304  match big:
1305    case True{}:
1306      +cz = FA.choose_eq_zero(v(n), v(k), lt_of(n, k, True{}, hbig))
1307      Equal.trans(Result<&2, &2, NM.NumError, WU.U64>, Done{I.u64_op(NM.ZeroOp{})}, SG.checked(~WU.U64, ~SG.u64_of, 64n, 0n), SG.checked(~WU.U64, ~SG.u64_of, 64n, S.choose(v(n), v(k))), Equal.cong(WU.U64, Result<&2, &2, NM.NumError, WU.U64>, t => Done{t}, I.u64_op(NM.ZeroOp{}), of(0n), as_of(I.u64_op(NM.ZeroOp{}), 0n, zero_v())), Equal.cong(Nat, Result<&2, &2, NM.NumError, WU.U64>, t => SG.checked(~WU.U64, ~SG.u64_of, 64n, t), 0n, S.choose(v(n), v(k)), Equal.sym(Nat, S.choose(v(n), v(k)), 0n, cz)))
1308    case False{}:
1309      +hkn = N.not_lt_le(v(n), v(k), lt_of(n, k, False{}, hbig))
1310      +s = I.u64_op(NM.Sub{n, k})
1311      +sn = Nat.sub(v(n), v(k))
1312      +es = Equal.trans(Nat, v(s), Nat.sub(v(n), v(k)), sn, LW.ops_sub(n, k, hkn), {==})
1313      +k0 = Nat.min(v(k), sn)
1314      +kk = G.min(~WU.U64, ~I.u64_op, ~I.u64_is, k, s)
1315      +hk0a = min_le_a(v(k), sn, Nat.is_lt(v(k), sn), {==})
1316      +hk0b = min_le_b(v(k), sn, Nat.is_lt(v(k), sn), {==})
1317      +hkK = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(K)) == True{} : Bool}, v(k), v(k), {==}, LW.val_lt(K, hK, k))
1318      +ekk0 = min_c(k, s, I.u64_is(NM.Lt{s, k}), {==})
1319      +ekk1 = Equal.cong(WU.U64, Nat, t => v(t), kk, of(Nat.min(v(k), v(s))), ekk0)
1320      +ekk2 = Equal.cong(Nat, Nat, t => Nat.min(v(k), t), v(s), sn, es)
1321      +hfk = fits32(K, hK, k0, N.le_lt_trans(k0, v(k), C.pow2(K), hk0a, hkK))
1322      +ekk = Equal.trans(Nat, v(kk), v(of(Nat.min(v(k), v(s)))), k0, ekk1, Equal.trans(Nat, v(of(Nat.min(v(k), v(s)))), v(of(k0)), k0, Equal.cong(Nat, Nat, t => v(of(t)), Nat.min(v(k), v(s)), k0, ekk2), LW.vo(k0, hfk)))
1323      +hsum = N.le_trans(Nat.add(k0, k0), Nat.add(v(k), k0), v(n), le_add_rr(k0, v(k), k0, hk0a), L.subst(Nat, z => {Nat.is_le(Nat.add(v(k), k0), z) == True{} : Bool}, Nat.add(v(k), sn), v(n), N.sub_add(v(n), v(k), hkn), N.le_add_left(k0, sn, v(k), hk0b)))
1324      +h2 = L.subst(Nat, z => {Nat.is_le(z, v(n)) == True{} : Bool}, Nat.add(k0, k0), Nat.double(k0), Equal.sym(Nat, Nat.double(k0), Nat.add(k0, k0), NA.double_self(k0)), hsum)
1325      +one = I.u64_op(NM.One{})
1326      +zero = I.u64_op(NM.ZeroOp{})
1327      +c0 = FA.choose_zero_right(v(n))
1328      +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 140n) == True{} : Bool}, 64n, K, Equal.sym(Nat, K, 64n, hK), {==})
1329      +hok = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, 1n, S.choose(v(n), 0n), Equal.sym(Nat, S.choose(v(n), 0n), 1n, c0), {==})
1330      +ha = Equal.trans(Nat, v(one), 1n, S.choose(v(n), 0n), one_v(), Equal.sym(Nat, S.choose(v(n), 0n), 1n, c0))
1331      +D = S.choose(v(n), k0)
1332      +sm = combsim(140n, n, zero, kk, one, v(n), 0n, k0, K, True{}, I.u64_is(NM.Lt{zero, kk}), C.fits(64n, D), hK, {==}, zero_v(), ekk, h2, N.zero_le(k0), hf0, hok, ha, ltv(zero, kk, 0n, k0, zero_v(), ekk), {==})
1333      +g = G.comb_go(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, n, zero, kk, (one, True{}), I.u64_is(NM.Lt{zero, kk}))
1334      +em = FA.comb_min(v(n), v(k), hkn, Nat.is_lt(v(k), sn), {==})
1335      Equal.trans(Result<&2, &2, NM.NumError, WU.U64>, G.ok(WU.U64, g), SG.checked(~WU.U64, ~SG.u64_of, 64n, D), SG.checked(~WU.U64, ~SG.u64_of, 64n, S.choose(v(n), v(k))), Equal.trans(Result<&2, &2, NM.NumError, WU.U64>, G.ok(WU.U64, g), G.ok(WU.U64, G.fits(WU.U64, Bool.not(C.fits(64n, D)), of(D))), SG.checked(~WU.U64, ~SG.u64_of, 64n, D), Equal.cong(Maybe<&2, WU.U64>, Result<&2, &2, NM.NumError, WU.U64>, t => G.ok(WU.U64, t), g, G.fits(WU.U64, Bool.not(C.fits(64n, D)), of(D)), sm), okfits(D, C.fits(64n, D))), Equal.cong(Nat, Result<&2, &2, NM.NumError, WU.U64>, t => SG.checked(~WU.U64, ~SG.u64_of, 64n, t), D, S.choose(v(n), v(k)), em))