def ulp_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64misc.bend:36

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/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

36def ulp_c(+x: F.F64, +t: Bool, +z: Bool, +hz: {X.is_zero(F.frac(x)) == z : Bool}) -> {F.ulp_cls(x, t) == SF.pick(F.F64, Bool.and(t, Bool.not(z)), SF.qnan(), SF.pick(F.F64, Bool.and(t, z), SF.inf(False{}), SF.round(False{}, 1n, SF.xexp(x)))) : F.F64}:
37  match t z:
38    case True{} True{}:
39      Equal.cong(Bool, F.F64, b => F.nan_or(F.inf(False{}), Bool.not(b)), X.is_zero(F.frac(x)), True{}, hz)
40    case True{} False{}:
41      Equal.cong(Bool, F.F64, b => F.nan_or(F.inf(False{}), Bool.not(b)), X.is_zero(F.frac(x)), False{}, hz)
42    case False{} _:
43      +e1 = T.rw_value(False{}, F.dexp(x), WU.U64{1, 0}, T.dexp_ge(x))
44      +e2 = Equal.cong(Nat, F.F64, t => SF.round(False{}, 1n, t), F.dexp(x), SF.xexp(x), T.dexp_value(x))
45      Equal.trans(F.F64, F.round_w(False{}, F.dexp(x), WU.U64{1, 0}), SF.round(False{}, 1n, F.dexp(x)), SF.round(False{}, 1n, SF.xexp(x)), e1, e2)