def nrp_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64nrp.bend:74

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/spec/math/w64.bend as SW
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/src/math/natural.bend as M
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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT

74# the rounding branch
75def nrp_r(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hz: {Nat.is_eq(SW.value(sig), 0n) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hx63: {Nat.is_le(63n, x) == True{} : Bool}) -> {F.round_pack(s, Nat.sub(e, Nat.sub(X.clz(sig), 1n)), X.shl(sig, Nat.sub(X.clz(sig), 1n))) == SF.round(s, SW.value(sig), x) : F.F64}:
76  +k = Nat.sub(X.clz(sig), 1n)
77  +ek = sdb(sig, h63)
78  +hk = N.le_lt_trans(k, 63n, 64n, sd_le(sig, h63), {==})
79  +ev = shl_v(sig, k, M.bit_length(SW.value(sig)), hk, L.subst(Nat, z => {Nat.is_le(z, 64n) == True{} : Bool}, 63n, Nat.add(k, M.bit_length(SW.value(sig))), Equal.sym(Nat, Nat.add(k, M.bit_length(SW.value(sig))), 63n, ek), {==}), RT.bl_fit(SW.value(sig)))
80  +f63 = tbf(k, SW.value(sig), 63n, ek)
81  +f62 = tbn(k, SW.value(sig), 62n, hz, ek)
82  +h62v = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, C.shift(k, SW.value(sig)), SW.value(X.shl(sig, k)), Equal.sym(Nat, SW.value(X.shl(sig, k)), C.shift(k, SW.value(sig)), ev), f62)
83  +h63v = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, C.shift(k, SW.value(sig)), SW.value(X.shl(sig, k)), Equal.sym(Nat, SW.value(X.shl(sig, k)), C.shift(k, SW.value(sig)), ev), f63)
84  +hkx = N.le_trans(k, 63n, x, sd_le(sig, h63), hx63)
85  +exk = Equal.sym(Nat, Nat.sub(e, k), Nat.add(Nat.sub(x, k), 2180n), Equal.trans(Nat, Nat.sub(e, k), Nat.sub(Nat.add(x, 2180n), k), Nat.add(Nat.sub(x, k), 2180n), Equal.cong(Nat, Nat, z => Nat.sub(z, k), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), FR.sub_add_r(x, 2180n, k, hkx)))
86  +r1 = FR.round_pack(s, Nat.sub(e, k), X.shl(sig, k), Nat.sub(x, k), exk, h62v, h63v)
87  +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(x, k)), SW.value(X.shl(sig, k)), C.shift(k, SW.value(sig)), ev)
88  +r3 = RT.round_shift(s, k, SW.value(sig), Nat.sub(x, k))
89  +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, SW.value(sig), z), Nat.add(Nat.sub(x, k), k), x, Equal.trans(Nat, Nat.add(Nat.sub(x, k), k), Nat.add(k, Nat.sub(x, k)), x, NA.add_comm(Nat.sub(x, k), k), N.sub_add(x, k, hkx)))
90  Equal.trans(F.F64, F.round_pack(s, Nat.sub(e, k), X.shl(sig, k)), SF.round(s, SW.value(X.shl(sig, k)), Nat.sub(x, k)), SF.round(s, SW.value(sig), x), r1, Equal.trans(F.F64, SF.round(s, SW.value(X.shl(sig, k)), Nat.sub(x, k)), SF.round(s, C.shift(k, SW.value(sig)), Nat.sub(x, k)), SF.round(s, SW.value(sig), x), r2, Equal.trans(F.F64, SF.round(s, C.shift(k, SW.value(sig)), Nat.sub(x, k)), SF.round(s, SW.value(sig), Nat.add(Nat.sub(x, k), k)), SF.round(s, SW.value(sig), x), r3, r4)))