def bnz_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:129

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/src/math/f64.bend as F
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/f64bits.bend as FB
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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

129def bnz_c(+x: F.F64, +z: Bool, +hz: {Nat.is_eq(F.exp_field(x), 0n) == z : Bool}, +h: {Nat.is_le(3000n, F.dexp_z(F.exp_field(x), z)) == True{} : Bool}) -> {Nat.is_eq(SF.mant(x), 0n) == False{} : Bool}:
130  match z:
131    case True{}:
132      Empty.absurd({Nat.is_eq(SF.mant(x), 0n) == False{} : Bool}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
133    case False{}:
134      +hz2 = L.subst(Nat, t => {Nat.is_eq(t, 0n) == False{} : Bool}, F.exp_field(x), SF.efield(x), T.ea(x), hz)
135      +Fr = SF.frac(x)
136      +e1 = mz(x, False{}, hz2)
137      # the hidden bit stays b2n(not False): no closed 2^52
138      +H = SF.b2n(Bool.not(False{}))
139      +e2 = FB.z2(Fr, 52n, H)
140      +e3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Fr, 0n), t), Nat.is_eq(H, 0n), False{}, {==})
141      Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), Nat.is_eq(Nat.add(Fr, C.shift(52n, H)), 0n), False{}, e1, Equal.trans(Bool, Nat.is_eq(Nat.add(Fr, C.shift(52n, H)), 0n), Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(H, 0n)), False{}, e2, Equal.trans(Bool, Bool.and(Nat.is_eq(Fr, 0n), Nat.is_eq(H, 0n)), Bool.and(Nat.is_eq(Fr, 0n), False{}), False{}, e3, FR.and_f(Nat.is_eq(Fr, 0n)))))