def sat_fit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:49

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/fixed.bend as F
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
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/math/typed/width.bend as WW

49def sat_fit(~T: Data, ~val: T -> Nat, +w: Nat, +n: Nat, +r: T, +top: T, +bad: Bool, +hb: {bad == Bool.not(C.fits(w, n)) : Bool}, +hv: {val(r) == C.low(w, n) : Nat}, +ht: {Bool.and(C.fits(w, val(top)), Bool.not(C.fits(w, 1n+val(top)))) == True{} : Bool}, +ok: Bool, +hok: {C.fits(w, n) == ok : Bool}) -> {SF.saturated(w, n, val(F.pick(T, bad, top, r)), ok) == True{} : Bool}:
50  match ok:
51    case True{}:
52      +eb = Equal.trans(Bool, bad, Bool.not(C.fits(w, n)), False{}, hb, bnot_eq(C.fits(w, n), True{}, hok))
53      %Equal.sym(Bool, bad, False{}, eb) : {SF.saturated(w, n, val(F.pick(T, _, top, r)), True{}) == True{} : Bool}
54      %Equal.sym(Nat, val(r), n, Equal.trans(Nat, val(r), C.low(w, n), n, hv, WW.low_fit(w, n, hok))) : {Nat.is_eq(_, n) == True{} : Bool}
55      N.is_eq_refl(n)
56    case False{}:
57      +eb = Equal.trans(Bool, bad, Bool.not(C.fits(w, n)), True{}, hb, bnot_eq(C.fits(w, n), False{}, hok))
58      %Equal.sym(Bool, bad, True{}, eb) : {SF.saturated(w, n, val(F.pick(T, _, top, r)), False{}) == True{} : Bool}
59      ht