def rt_c

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

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/f64cmp.bend as FC

283def rt_c(+x: F.F64, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +z: Bool, +hz: {Nat.is_eq(SF.efield(x), 0n) == z : Bool}) -> {SF.round(SF.sign(x), SF.mant(x), SF.xexp(x)) == x : F.F64}:
284  match z:
285    case True{}:
286      +s = SF.sign(x)
287      +E = SF.efield(x)
288      +Fr = SF.frac(x)
289      +e1 = Equal.cong(Bool, F.F64, b => SF.round(s, Nat.add(Fr, C.shift(52n, SF.b2n(Bool.not(b)))), SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))), Nat.is_eq(E, 0n), True{}, hz)
290      +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, t, 1926n), Nat.add(Fr, 0n), Fr, N.add_zero(Fr))
291      +e3 = rt_sub(s, Fr, frac52(x), Nat.is_eq(Fr, 0n), {==})
292      +e4 = Equal.cong(Nat, F.F64, t => SF.encode(s, t, Fr), 0n, E, Equal.sym(Nat, E, 0n, N.eq_from_is_eq(E, 0n, hz)))
293      +e5 = Equal.sym(F.F64, x, SF.encode(s, E, Fr), dec(x))
294      Equal.trans(F.F64, SF.round(s, SF.mant(x), SF.xexp(x)), SF.round(s, Nat.add(Fr, 0n), 1926n), x, e1, Equal.trans(F.F64, SF.round(s, Nat.add(Fr, 0n), 1926n), SF.round(s, Fr, 1926n), x, e2, Equal.trans(F.F64, SF.round(s, Fr, 1926n), SF.encode(s, 0n, Fr), x, e3, Equal.trans(F.F64, SF.encode(s, 0n, Fr), SF.encode(s, E, Fr), x, e4, e5))))
295    case False{}:
296      +s = SF.sign(x)
297      +E = SF.efield(x)
298      +Fr = SF.frac(x)
299      +eb = Equal.trans(Nat, SF.b2n(Bool.not(Nat.is_eq(E, 0n))), 1n, one, Equal.cong(Bool, Nat, b => SF.b2n(Bool.not(b)), Nat.is_eq(E, 0n), False{}, hz), Equal.sym(Nat, one, 1n, h1))
300      +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.add(Fr, C.shift(52n, t)), SF.xexp(x)), SF.b2n(Bool.not(Nat.is_eq(E, 0n))), one, eb)
301      +e2 = Equal.cong(Bool, F.F64, b => SF.round(s, Nat.add(Fr, C.shift(52n, one)), SF.pick(Nat, b, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))), Nat.is_eq(E, 0n), False{}, hz)
302      +e3 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.add(Fr, C.shift(52n, one)), t), Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E))
303      +e4 = rt_norm(s, E, Fr, one, h1, hz, hfin, frac52(x))
304      +e5 = Equal.sym(F.F64, x, SF.encode(s, E, Fr), dec(x))
305      +r1 = SF.round(s, Nat.add(Fr, C.shift(52n, one)), SF.xexp(x))
306      +r2 = SF.round(s, Nat.add(Fr, C.shift(52n, one)), Nat.sub(Nat.add(E, SF.zb()), 1075n))
307      +r3 = SF.round(s, Nat.add(Fr, C.shift(52n, one)), Nat.add(1925n, E))
308      Equal.trans(F.F64, SF.round(s, SF.mant(x), SF.xexp(x)), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, r3, x, e3, Equal.trans(F.F64, r3, SF.encode(s, E, Fr), x, e4, e5))))