def rp_norm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:893

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/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

893def rp_norm(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +hb: {Nat.is_lt(x, 1916n) == False{} : Bool}, +u: Nat, +hu: {Nat.max(Nat.add(10n, x), 1926n) == u : Nat}) -> {F.rp_neg(s, e, sig, False{}) == SF.round_u(s, SW.value(sig), x, u) : F.F64}:
894  +hge = N.not_lt_le(x, 1916n, hb)
895  +hu1 = Equal.trans(Nat, u, Nat.max(Nat.add(10n, x), 1926n), Nat.add(10n, x), Equal.sym(Nat, Nat.max(Nat.add(10n, x), 1926n), u, hu), max_l(Nat.add(10n, x), 1926n, hge))
896  +eEF = Equal.trans(Nat, Nat.sub(e, F.off()), Nat.sub(Nat.add(x, 2180n), F.off()), Nat.sub(x, 1916n), Equal.cong(Nat, Nat, z => Nat.sub(z, F.off()), e, Nat.add(x, 2180n), Equal.sym(Nat, Nat.add(x, 2180n), e, hx)), sub_cancel_r(x, 1916n, 2180n))
897  +y = Nat.sub(x, 1916n)
898  +ex = Equal.trans(Nat, Nat.add(y, 1926n), Nat.add(Nat.add(y, 1916n), 10n), u, Equal.sym(Nat, Nat.add(Nat.add(y, 1916n), 10n), Nat.add(y, 1926n), NA.add_assoc(y, 1916n, 10n)), Equal.trans(Nat, Nat.add(Nat.add(y, 1916n), 10n), Nat.add(x, 10n), u, Equal.cong(Nat, Nat, z => Nat.add(z, 10n), Nat.add(y, 1916n), x, Equal.trans(Nat, Nat.add(y, 1916n), Nat.add(1916n, y), x, NA.add_comm(y, 1916n), N.sub_add(x, 1916n, hge))), Equal.trans(Nat, Nat.add(x, 10n), Nat.add(10n, x), u, NA.add_comm(x, 10n), Equal.sym(Nat, u, Nat.add(10n, x), hu1))))
899  +hEF = Equal.trans(Nat, Nat.add(Nat.sub(e, F.off()), 1926n), Nat.add(y, 1926n), u, Equal.cong(Nat, Nat, z => Nat.add(z, 1926n), Nat.sub(e, F.off()), y, eEF), ex)
900  +hle = L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.add(10n, x), u, Equal.sym(Nat, u, Nat.add(10n, x), hu1), L.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.add(x, 10n), Nat.add(10n, x), NA.add_comm(x, 10n), N.le_add_right(x, 10n)))
901  +ku = Equal.trans(Nat, Nat.sub(u, x), Nat.sub(Nat.add(10n, x), x), 10n, Equal.cong(Nat, Nat, z => Nat.sub(z, x), u, Nat.add(10n, x), hu1), sub_add_l(10n, x))
902  +s1 = Equal.cong(Bool, F.F64, t => SF.pack(s, SF.pick(Nat, t, SF.rne(SW.value(sig), Nat.sub(u, x)), C.shift(Nat.sub(x, u), SW.value(sig))), u), Nat.is_le(x, u), True{}, hle)
903  +s2 = Equal.cong(Nat, F.F64, z => SF.pack(s, SF.rne(SW.value(sig), z), u), Nat.sub(u, x), 10n, ku)
904  +sp = Equal.trans(F.F64, SF.round_u(s, SW.value(sig), x, u), SF.pack(s, SF.rne(SW.value(sig), Nat.sub(u, x)), u), SF.pack(s, SF.rne(SW.value(sig), 10n), u), s1, s2)
905  +eo = ov_eq(one, h1, e, sig, x, hx, hge, h63)
906  +i1 = Equal.cong(Bool, F.F64, t => F.rp_over(s, e, sig, t), Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0})))), Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), eo)
907  +i2 = rp_nc(one, h1, s, e, sig, x, h62, h63, u, hEF, Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n)), {==})
908  Equal.trans(F.F64, F.rp_over(s, e, sig, Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0}))))), SF.pack(s, SF.rne(SW.value(sig), 10n), u), SF.round_u(s, SW.value(sig), x, u), Equal.trans(F.F64, F.rp_over(s, e, sig, Bool.or(Nat.is_lt(Nat.add(F.off(), 2045n), e), Bool.and(Nat.is_eq(e, Nat.add(F.off(), 2045n)), X.le(WU.U64{0, 2147483648}, X.add(sig, WU.U64{512, 0}))))), F.rp_over(s, e, sig, Bool.not(Nat.is_lt(Nat.add(Nat.sub(e, F.off()), SF.pick(Nat, C.fits(53n, SF.rne(SW.value(sig), 10n)), 1n, 2n)), 2047n))), SF.pack(s, SF.rne(SW.value(sig), 10n), u), i1, i2), Equal.sym(F.F64, SF.round_u(s, SW.value(sig), x, u), SF.pack(s, SF.rne(SW.value(sig), 10n), u), sp))