def mfr_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64modf.bend:43

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

43def mfr_c(+s: Bool, +w: WU.U64, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}, +k: Nat, +b: Bool, +hb: {Nat.is_lt(k, 64n) == b : Bool}) -> {F.mf_frac(s, w, u, k, b) == SF.round(s, C.low(k, SW.value(w)), u) : F.F64}:
44  match b:
45    case True{}:
46      +r = X.sub(w, X.shl(X.shr(w, k), k))
47      Equal.trans(F.F64, F.round_w(s, u, r), SF.round(s, SW.value(r), u), SF.round(s, C.low(k, SW.value(w)), u), T.rw_value(s, u, r, hu), Equal.cong(Nat, F.F64, t => SF.round(s, t, u), SW.value(r), C.low(k, SW.value(w)), rem_v(w, k, hb)))
48    case False{}:
49      +V = SW.value(w)
50      +el = WW.low_fit(k, V, SH.fits_mono(64n, k, V, N.not_lt_le(k, 64n, hb), FL.vb64(w)))
51      Equal.trans(F.F64, F.round_w(s, u, w), SF.round(s, V, u), SF.round(s, C.low(k, V), u), T.rw_value(s, u, w, hu), Equal.cong(Nat, F.F64, t => SF.round(s, t, u), V, C.low(k, V), Equal.sym(Nat, C.low(k, V), V, el)))