def rm_one

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:661

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/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/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/f64tools.bend as T

661# exactly one scale step below y
662def rm_one(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +hk: {Nat.sub(F.dexp(y), F.dexp(x)) == 1n : Nat}) -> {F.rm_fix(F.signbit(x), F.dexp(x), X.add(F.dmant(y), F.dmant(y)), F.dmant(x), WU.U64{0, 0}) == RNs(x, y) : F.F64}:
663  +s = SF.sign(x)
664  +xx = SF.xexp(x)
665  +mx = SF.mant(x)
666  +my = SF.mant(y)
667  +my2 = Nat.add(my, my)
668  +ek = Equal.trans(Nat, Nat.sub(SF.xexp(y), xx), Nat.sub(F.dexp(y), F.dexp(x)), 1n, Equal.sym(Nat, Nat.sub(F.dexp(y), F.dexp(x)), Nat.sub(SF.xexp(y), xx), xsub(x, y)), hk)
669  +h0 = L.subst(Nat, t => {Nat.is_lt(mx, C.shift(t, my)) == True{} : Bool}, Nat.sub(SF.xexp(y), xx), 1n, ek, far_lt(x, y, hlt, 1n, {==}))
670  +h2 = L.subst(Nat, t => {Nat.is_lt(mx, t) == True{} : Bool}, Nat.double(my), my2, NA.double_self(my), h0)
671  +e1 = rmfix_v(F.signbit(x), F.dexp(x), T.dexp_ge(x), X.add(F.dmant(y), F.dmant(y)), F.dmant(x), WU.U64{0, 0}, my2, mx, 0n, addrr(F.dmant(y), my, T.dmant_value(y), T.mant_fits(y)), T.dmant_value(x), {==}, N.lt_le(mx, my2, h2), T.mant_fits(x))
672  +e2 = Equal.cong(Bool, F.F64, t => SF.rnear(t, mx, my2, 0n, F.dexp(x)), F.signbit(x), s, FB.signbit_value(x))
673  +e3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, my2, 0n, t), F.dexp(x), xx, T.dexp_value(x))
674  +S = C.shift(Nat.sub(SF.xexp(y), xx), my)
675  +f1 = rn_spec_far(x, y, hlt)
676  +f2 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, C.shift(t, my), 0n, xx), Nat.sub(SF.xexp(y), xx), 1n, ek)
677  +f3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, t, 0n, xx), Nat.double(my), my2, NA.double_self(my))
678  +G = SF.rnear(s, mx, my2, 0n, xx)
679  +eR = Equal.trans(F.F64, RNs(x, y), SF.rnear(s, mx, S, 0n, xx), G, f1, Equal.trans(F.F64, SF.rnear(s, mx, S, 0n, xx), SF.rnear(s, mx, Nat.double(my), 0n, xx), G, f2, f3))
680  +a1 = SF.rnear(F.signbit(x), mx, my2, 0n, F.dexp(x))
681  +a2 = SF.rnear(s, mx, my2, 0n, F.dexp(x))
682  Equal.trans(F.F64, F.rm_fix(F.signbit(x), F.dexp(x), X.add(F.dmant(y), F.dmant(y)), F.dmant(x), WU.U64{0, 0}), a1, RNs(x, y), e1, Equal.trans(F.F64, a1, a2, RNs(x, y), e2, Equal.trans(F.F64, a2, G, RNs(x, y), e3, Equal.sym(F.F64, RNs(x, y), G, eR))))