def rp62_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mulp.bend:49

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
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/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT

49def rp62_c(+s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +hx1: {Nat.is_le(1n, x) == True{} : Bool}, +h61: {C.fits(61n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +f: Bool, +hf: {C.fits(62n, SW.value(sig)) == f : Bool}) -> {F.rp62_pick(s, e, sig, f) == SF.round(s, SW.value(sig), x) : F.F64}:
50  match f:
51    case True{}:
52      +Vs = SW.value(sig)
53      +d = X.add(sig, sig)
54      a1 = WA.add_value(sig, sig)
55      +f63 = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(0n, C.shift(1n, Vs)), Nat.double(Vs), {==}, WW.limbs_fit(1n, 62n, 0n, Vs, FR.fz(1n), hf))
56      +eVV = Equal.sym(Nat, Nat.double(Vs), Nat.add(Vs, Vs), NA.double_self(Vs))
57      +ed = Equal.trans(Nat, SW.value(d), C.low(64n, Nat.add(Vs, Vs)), Nat.double(Vs), a1, Equal.trans(Nat, C.low(64n, Nat.add(Vs, Vs)), C.low(64n, Nat.double(Vs)), Nat.double(Vs), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(Vs, Vs), Nat.double(Vs), eVV), WW.low_fit(64n, Nat.double(Vs), SH.fits_mono(63n, 64n, Nat.double(Vs), {==}, f63))))
58      +f62 = Equal.trans(Bool, C.fits(62n, Nat.double(Vs)), C.fits(61n, Vs), False{}, RT.fit_td(61n, 0n, Vs, {==}), h61)
59      +h62d = L.subst(Nat, z => {C.fits(62n, z) == False{} : Bool}, Nat.double(Vs), SW.value(d), Equal.sym(Nat, SW.value(d), Nat.double(Vs), ed), f62)
60      +h63d = L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.double(Vs), SW.value(d), Equal.sym(Nat, SW.value(d), Nat.double(Vs), ed), f63)
61      +ex = Equal.trans(Nat, Nat.add(Nat.sub(x, 1n), 2180n), Nat.sub(Nat.add(x, 2180n), 1n), Nat.sub(e, 1n), Equal.sym(Nat, Nat.sub(Nat.add(x, 2180n), 1n), Nat.add(Nat.sub(x, 1n), 2180n), FR.sub_add_r(x, 2180n, 1n, hx1)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(x, 2180n), e, hx))
62      +r1 = FR.round_pack(s, Nat.sub(e, 1n), d, Nat.sub(x, 1n), ex, h62d, h63d)
63      +r2 = Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(x, 1n)), SW.value(d), C.shift(1n, Vs), ed)
64      +r3 = RT.round_shift(s, 1n, Vs, Nat.sub(x, 1n))
65      +r4 = Equal.cong(Nat, F.F64, z => SF.round(s, Vs, z), Nat.add(Nat.sub(x, 1n), 1n), x, Equal.trans(Nat, Nat.add(Nat.sub(x, 1n), 1n), Nat.add(1n, Nat.sub(x, 1n)), x, NA.add_comm(Nat.sub(x, 1n), 1n), N.sub_add(x, 1n, hx1)))
66      Equal.trans(F.F64, F.round_pack(s, Nat.sub(e, 1n), d), SF.round(s, SW.value(d), Nat.sub(x, 1n)), SF.round(s, Vs, x), r1, Equal.trans(F.F64, SF.round(s, SW.value(d), Nat.sub(x, 1n)), SF.round(s, C.shift(1n, Vs), Nat.sub(x, 1n)), SF.round(s, Vs, x), r2, Equal.trans(F.F64, SF.round(s, C.shift(1n, Vs), Nat.sub(x, 1n)), SF.round(s, Vs, Nat.add(Nat.sub(x, 1n), 1n)), SF.round(s, Vs, x), r3, r4)))
67    case False{}:
68      FR.round_pack(s, e, sig, x, hx, hf, h63)