def mf_c

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
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/proofs/math/typed/f64tools.bend as T

80def mf_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.mf_cls(x, t) == SF.pickt(F.F64 & F.F64, Bool.and(t, Bool.not(z)), (SF.qnan(), SF.qnan()), SF.pickt(F.F64 & F.F64, Bool.or(Bool.and(t, z), Nat.is_le(SF.zb(), SF.xexp(x))), (SF.zero(SF.sign(x)), x), (FRAC(x), SF.to_integral(F.Trunc{}, x)))) : F.F64 & F.F64}:
81  match t z:
82    case True{} True{}:
83      +e1 = Equal.cong(Bool, F.F64 & F.F64, b => (F.nan_or(F.zero(F.signbit(x)), Bool.not(b)), F.nan_or(x, Bool.not(b))), X.is_zero(F.frac(x)), True{}, hz)
84      Equal.trans(F.F64 & F.F64, (F.nan_or(F.zero(F.signbit(x)), Bool.not(X.is_zero(F.frac(x)))), F.nan_or(x, Bool.not(X.is_zero(F.frac(x))))), (F.zero(F.signbit(x)), x), (SF.zero(SF.sign(x)), x), e1, Equal.cong(F.F64, F.F64 & F.F64, u => (u, x), F.zero(F.signbit(x)), SF.zero(SF.sign(x)), zs(x)))
85    case True{} False{}:
86      Equal.cong(Bool, F.F64 & F.F64, b => (F.nan_or(F.zero(F.signbit(x)), Bool.not(b)), F.nan_or(x, Bool.not(b))), X.is_zero(F.frac(x)), False{}, hz)
87    case False{} _:
88      +e1 = Equal.cong(Nat, F.F64 & F.F64, u => F.mf_fin(x, Nat.is_le(3000n, u)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
89      Equal.trans(F.F64 & F.F64, F.mf_fin(x, Nat.is_le(3000n, F.dexp(x))), F.mf_fin(x, Nat.is_le(3000n, SF.xexp(x))), SF.pickt(F.F64 & F.F64, Nat.is_le(3000n, SF.xexp(x)), (SF.zero(SF.sign(x)), x), (FRAC(x), SF.to_integral(F.Trunc{}, x))), e1, mff_c(x, Nat.is_le(3000n, SF.xexp(x))))