def big_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64ratio.bend:106

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/num.bend as NE
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
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/w64clz.bend as CZ
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bl.bend as BL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64conv.bend as CV

106def big_v(+x: F.F64, +hc: {Nat.is_le(3000n, F.dexp(x)) == True{} : Bool}) -> {SF.rtriple(F.ar_big(F.signbit(x), F.dmant(x), Nat.sub(F.dexp(x), 3000n), Nat.is_le(Nat.add(Nat.sub(F.dexp(x), 3000n), Nat.sub(64n, X.clz(F.dmant(x)))), 64n))) == BIGR(SF.sign(x), C.shift(Nat.sub(SF.xexp(x), SF.zb()), SF.mant(x))) : Result<&2, &2, NE.NumError, SF.Rat>}:
107  +w = F.dmant(x)
108  +V = SW.value(w)
109  +B = M.bit_length(V)
110  +k = Nat.sub(F.dexp(x), 3000n)
111  +hB = N.le_trans(B, 53n, 64n, BL.bl_le(53n, V, T.mw53(x), Nat.is_le(B, 53n), {==}), {==})
112  +eb = Equal.trans(Nat, Nat.sub(64n, X.clz(w)), Nat.sub(64n, Nat.sub(64n, B)), B, Equal.cong(Nat, Nat, t => Nat.sub(64n, t), X.clz(w), Nat.sub(64n, B), CZ.clz_value(w)), T.subsub(64n, B, hB))
113  +e0 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => SF.rtriple(F.ar_big(F.signbit(x), w, k, Nat.is_le(Nat.add(k, t), 64n))), Nat.sub(64n, X.clz(w)), B, eb)
114  +e1 = ab_c(F.signbit(x), w, k, CV.big_nz(x, hc), Nat.is_le(Nat.add(k, B), 64n), {==})
115  +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, SF.Rat>, t => BIGR(t, C.shift(k, V)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
116  +e3 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => BIGR(SF.sign(x), C.shift(k, t)), V, SF.mant(x), T.dmant_value(x))
117  +e4 = Equal.cong(Nat, Result<&2, &2, NE.NumError, SF.Rat>, t => BIGR(SF.sign(x), C.shift(Nat.sub(t, 3000n), SF.mant(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
118  +r0 = SF.rtriple(F.ar_big(F.signbit(x), w, k, Nat.is_le(Nat.add(k, Nat.sub(64n, X.clz(w))), 64n)))
119  +r1 = SF.rtriple(F.ar_big(F.signbit(x), w, k, Nat.is_le(Nat.add(k, B), 64n)))
120  +r2 = BIGR(F.signbit(x), C.shift(k, V))
121  +r3 = BIGR(SF.sign(x), C.shift(k, V))
122  +r4 = BIGR(SF.sign(x), C.shift(k, SF.mant(x)))
123  +r5 = BIGR(SF.sign(x), C.shift(Nat.sub(SF.xexp(x), SF.zb()), SF.mant(x)))
124  Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r0, r1, r5, e0, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r1, r2, r5, e1, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r2, r3, r5, e2, Equal.trans(Result<&2, &2, NE.NumError, SF.Rat>, r3, r4, r5, e3, e4))))