def rn_spec_far

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

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/nat.bend as N

641def rn_spec_far(+x: F.F64, +y: F.F64, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}) -> {RNs(x, y) == SF.rnear(SF.sign(x), SF.mant(x), C.shift(Nat.sub(SF.xexp(y), SF.xexp(x)), SF.mant(y)), 0n, SF.xexp(x)) : F.F64}:
642  +s = SF.sign(x)
643  +xx = SF.xexp(x)
644  +xy = SF.xexp(y)
645  +mx = SF.mant(x)
646  +my = SF.mant(y)
647  +S = C.shift(Nat.sub(xy, xx), my)
648  +e1 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), C.shift(Nat.sub(xy, t), my), Nat.div(C.shift(Nat.sub(xx, t), mx), C.shift(Nat.sub(xy, t), my)), t), Nat.min(xx, xy), xx, N.min_left(xx, xy, hlt))
649  +e2 = Equal.cong(Nat, F.F64, t => SF.rnear(s, Nat.mod(C.shift(t, mx), S), S, Nat.div(C.shift(t, mx), S), xx), Nat.sub(xx, xx), 0n, N.sub_self(xx))
650  +e3 = Equal.cong(Nat, F.F64, t => SF.rnear(s, t, S, Nat.div(mx, S), xx), Nat.mod(mx, S), mx, mod_small(mx, S, far_lt(x, y, hlt, 1n, {==})))
651  +e4 = Equal.cong(Nat, F.F64, t => SF.rnear(s, mx, S, t, xx), Nat.div(mx, S), 0n, div_small(mx, S, far_lt(x, y, hlt, 1n, {==})))
652  +r1 = SF.rnear(s, Nat.mod(C.shift(Nat.sub(xx, xx), mx), S), S, Nat.div(C.shift(Nat.sub(xx, xx), mx), S), xx)
653  +r2 = SF.rnear(s, Nat.mod(mx, S), S, Nat.div(mx, S), xx)
654  +r3 = SF.rnear(s, mx, S, Nat.div(mx, S), xx)
655  +G = SF.rnear(s, mx, S, 0n, xx)
656  Equal.trans(F.F64, RNs(x, y), r1, G, e1, Equal.trans(F.F64, r1, r2, G, e2, Equal.trans(F.F64, r2, r3, G, e3, e4)))