def qfit

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

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

766# a normal q with its exponent field below 2047 fits the 63-bit pattern
767def qfit(+one: Nat, +h1: {one == 1n : Nat}, +q: Nat, +EF: Nat, +hq: {Nat.is_le(q, C.shift(53n, one)) == True{} : Bool}, +h52: {C.fits(52n, q) == False{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n) == True{} : Bool}) -> {C.fits(63n, Nat.add(q, C.shift(52n, EF))) == True{} : Bool}:
768  +eH = hpick_c(one, h1, q, hq, h52, C.fits(53n, q), {==})
769  +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(EF, z), 2047n) == True{} : Bool}, SF.pick(Nat, C.fits(53n, q), 1n, 2n), C.high(52n, q), Equal.sym(Nat, C.high(52n, q), SF.pick(Nat, C.fits(53n, q), 1n, 2n), eH), hov)
770  +h3 = L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, Nat.add(EF, C.high(52n, q)), Nat.add(C.high(52n, q), EF), NA.add_comm(EF, C.high(52n, q)), h2)
771  +f11 = WW.fits_of_lt(11n, Nat.add(C.high(52n, q), EF), N.lt_trans(Nat.add(C.high(52n, q), EF), 2047n, 2048n, h3, {==}))
772  +f = WW.limbs_fit(52n, 11n, C.low(52n, q), Nat.add(C.high(52n, q), EF), WW.low_fits(52n, q), f11)
773  L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(C.low(52n, q), C.shift(52n, Nat.add(C.high(52n, q), EF))), Nat.add(q, C.shift(52n, EF)), qsplit(q, EF), f)