def rne_zero

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

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/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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend as RI

44# m < 2^53 divided by 2^(1+j) >= 2^54 rounds to 0
45def rne_zero(+m: Nat, +j: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hj: {Nat.is_le(53n, j) == True{} : Bool}) -> {SF.rne(m, 1n+j) == 0n : Nat}:
46  +hj1 = N.le_trans(53n, j, 1n+j, hj, N.le_succ(j))
47  +f1 = SH.fits_mono(53n, 1n+j, m, hj1, hm)
48  +eh = N.eq_from_is_eq(C.high(1n+j, m), 0n, f1)
49  +el = WW.low_fit(1n+j, m, SH.fits_mono(53n, 1n+j, m, N.le_trans(53n, j, 1n+j, hj, N.le_succ(j)), hm))
50  +fj = SH.fits_mono(53n, j, m, hj, hm)
51  +hl = Equal.trans(Bool, Nat.is_lt(m, C.shift(j, 1n)), C.fits(j, m), True{}, FR.lt_fit(j, 1n, {==}, m), fj)
52  +la = RI.nlt(j, 1n, {==}, m, SH.fits_mono(53n, j, m, hj, hm))
53  +le = N.is_eq_lt(m, C.shift(j, 1n), hl)
54  +H = C.shift(j, 1n)
55  +e1 = Equal.cong(Nat, Nat, t => SF.rne_up(t, C.low(1n+j, m), H), C.high(1n+j, m), 0n, eh)
56  +e2 = Equal.cong(Nat, Nat, t => SF.rne_up(0n, t, H), C.low(1n+j, m), m, el)
57  +e3 = Equal.cong(Bool, Nat, b => Nat.add(0n, SF.b2n(Bool.or(b, Bool.and(Nat.is_eq(m, H), False{})))), Nat.is_lt(H, m), False{}, la)
58  +e4 = Equal.cong(Bool, Nat, b => SF.b2n(Bool.and(b, False{})), Nat.is_eq(m, H), False{}, le)
59  Equal.trans(Nat, SF.rne(m, 1n+j), SF.rne_up(0n, C.low(1n+j, m), H), 0n, e1, Equal.trans(Nat, SF.rne_up(0n, C.low(1n+j, m), H), SF.rne_up(0n, m, H), 0n, e2, Equal.trans(Nat, SF.rne_up(0n, m, H), SF.b2n(Bool.and(Nat.is_eq(m, H), False{})), 0n, e3, e4)))