def ru_self

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

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
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/f64exp.bend as EX

212# a significand of at most 52 bits at its own ulp u encodes as a subnormal;
213# u stays abstract, so pack's exponent arithmetic is never evaluated on a
214# literal (rt_sub instantiates u = 1926)
215def ru_self(+s: Bool, +Fr: Nat, +u: Nat, +hF: {C.fits(52n, Fr) == True{} : Bool}) -> {SF.round_u(s, Fr, u, u) == SF.encode(s, 0n, Fr) : F.F64}:
216  +f53 = SH.fits_mono(52n, 53n, Fr, {==}, hF)
217  +l1 = EX.ru(s, Fr, u, u)
218  +l2 = Equal.cong(Bool, F.F64, b => SF.pack(s, SF.pick(Nat, b, SF.rne(Fr, Nat.sub(u, u)), C.shift(Nat.sub(u, u), Fr)), u), Nat.is_le(u, u), True{}, N.le_refl(u))
219  +l3 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(Fr, t), u), Nat.sub(u, u), 0n, N.sub_self(u))
220  +l4 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.pack_n(s, Fr, u), SF.pack_e(s, Nat.sub(Nat.add(1n+u, 1075n), SF.zb()), 0n)), C.fits(53n, Fr), True{}, f53)
221  +l5 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.encode(s, 0n, Fr), SF.pack_e(s, Nat.sub(Nat.add(u, 1075n), SF.zb()), C.low(52n, Fr))), C.fits(52n, Fr), True{}, hF)
222  +p1 = SF.pack(s, SF.pick(Nat, Nat.is_le(u, u), SF.rne(Fr, Nat.sub(u, u)), C.shift(Nat.sub(u, u), Fr)), u)
223  +p2 = SF.pack(s, SF.rne(Fr, Nat.sub(u, u)), u)
224  +p3 = SF.pack(s, Fr, u)
225  +p4 = SF.pack_n(s, Fr, u)
226  +G = SF.encode(s, 0n, Fr)
227  Equal.trans(F.F64, SF.round_u(s, Fr, u, u), p1, G, l1, Equal.trans(F.F64, p1, p2, G, l2, Equal.trans(F.F64, p2, p3, G, l3, Equal.trans(F.F64, p3, p4, G, l4, l5))))