def ldn_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:212

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/proofs/lib/nat.bend as N
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/lib/lemmas/proofs/nat_algebra.bend as NA
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/f64rtools.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

212def ldn_c(+x: F.F64, +k: Nat, +c: Bool, +hc: {Nat.is_lt(F.dexp(x), Nat.add(k, 63n)) == c : Bool}) -> {F.ld_neg(x, k, c) == LD(x, True{}, k) : F.F64}:
213  match c:
214    case True{}:
215      +h1 = L.subst(Nat, t => {Nat.is_lt(t, Nat.add(k, 63n)) == True{} : Bool}, F.dexp(x), SF.xexp(x), T.dexp_value(x), hc)
216      +et = tiny(SF.sign(x), SF.mant(x), Nat.sub(SF.xexp(x), k), T.mant_fits(x), slt(SF.xexp(x), k, h1))
217      +ez = Equal.trans(F.F64, F.zero(F.signbit(x)), SF.zero(F.signbit(x)), SF.zero(SF.sign(x)), T.zero_v(F.signbit(x)), Equal.cong(Bool, F.F64, t => SF.zero(t), F.signbit(x), SF.sign(x), FB.signbit_value(x)))
218      Equal.trans(F.F64, F.zero(F.signbit(x)), SF.zero(SF.sign(x)), LD(x, True{}, k), ez, Equal.sym(F.F64, LD(x, True{}, k), SF.zero(SF.sign(x)), et))
219    case False{}:
220      +h0 = N.not_lt_le(F.dexp(x), Nat.add(k, 63n), hc)
221      +h1 = L.subst(Nat, t => {Nat.is_le(t, F.dexp(x)) == True{} : Bool}, Nat.add(k, 63n), Nat.add(63n, k), NA.add_comm(k, 63n), h0)
222      +hu = RT.le_sub(63n, k, F.dexp(x), h1)
223      +e1 = rwx(x, Nat.sub(F.dexp(x), k), hu)
224      +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.mant(x), Nat.sub(t, k)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
225      Equal.trans(F.F64, F.round_w(F.signbit(x), Nat.sub(F.dexp(x), k), F.dmant(x)), SF.round(SF.sign(x), SF.mant(x), Nat.sub(F.dexp(x), k)), LD(x, True{}, k), e1, e2)