def perm_top

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

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

884def perm_top(+K: Nat, +hK: {K == 32n : Nat}, +n: U32, +k: U32, +big: Bool, +hbig: {I.u32_is(NM.Lt{n, k}) == big : Bool}) -> {G.perm_big(~U32, ~I.u32_op, ~I.u32_is, n, k, big) == SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))) : Result<&2, &2, NM.NumError, U32>}:
885  match big:
886    case True{}:
887      +dz = NF.desc_zero(v(n), v(k), lt_of(n, k, True{}, hbig))
888      Equal.trans(Result<&2, &2, NM.NumError, U32>, Done{I.u32_op(NM.ZeroOp{})}, SG.checked(~U32, ~SG.u32_of, 32n, 0n), SG.checked(~U32, ~SG.u32_of, 32n, S.desc(v(n), v(k))), Equal.cong(U32, Result<&2, &2, NM.NumError, U32>, t => Done{t}, I.u32_op(NM.ZeroOp{}), of(0n), as_of(I.u32_op(NM.ZeroOp{}), 0n, zero_v())), Equal.cong(Nat, Result<&2, &2, NM.NumError, U32>, t => SG.checked(~U32, ~SG.u32_of, 32n, t), 0n, S.desc(v(n), v(k)), Equal.sym(Nat, S.desc(v(n), v(k)), 0n, dz)))
889    case False{}:
890      +one = I.u32_op(NM.One{})
891      +D = S.desc(v(n), v(k))
892      +hge = N.not_lt_le(v(n), v(k), lt_of(n, k, False{}, hbig))
893      +hf0 = L.subst(Nat, z => {Nat.is_le(1n+z, 140n) == True{} : Bool}, 32n, K, Equal.sym(Nat, K, 32n, hK), {==})
894      +hm0 = Equal.sym(Nat, Nat.sub(v(n), 0n), v(n), N.sub_zero(v(n)))
895      +more = Bool.not(I.u32_is(NM.IsZero{k}))
896      +hmore = Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.IsZero{k}), Nat.is_eq(v(k), 0n), iz(k, v(k), {==}))
897      +s = permsim(140n, k, n, one, v(n), 0n, v(k), v(k), K, True{}, more, C.fits(32n, D), hK, {==}, hm0, {==}, hge, hf0, {==}, one_v(), hmore, {==})
898      +g = G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 140n, k, n, (one, True{}), more)
899      Equal.trans(Result<&2, &2, NM.NumError, U32>, G.ok(U32, g), G.ok(U32, G.fits(U32, Bool.not(C.fits(32n, D)), of(D))), SG.checked(~U32, ~SG.u32_of, 32n, D), Equal.cong(Maybe<&2, U32>, Result<&2, &2, NM.NumError, U32>, t => G.ok(U32, t), g, G.fits(U32, Bool.not(C.fits(32n, D)), of(D)), s), okfits(D, C.fits(32n, D)))