def tiny_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:86

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/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/f64round.bend as FR
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/f64rtools.bend as RT

86def tiny_c(+s: Bool, +m: Nat, +x: Nat, +hm: {C.fits(53n, m) == True{} : Bool}, +hx: {Nat.is_lt(x, 63n) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {SF.round(s, m, x) == SF.zero(s) : F.F64}:
87  match z:
88    case True{}:
89      Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, M.bit_length(m)), 53n), 1926n))), Nat.is_eq(m, 0n), True{}, hz)
90    case False{}:
91      +B = M.bit_length(m)
92      +A = Nat.sub(Nat.add(x, B), 53n)
93      +hB = BL.bl_le(53n, m, hm, Nat.is_le(B, 53n), {==})
94      +hx62 = N.lt_succ_le(x, 62n, hx)
95      +h1 = Equal.trans(Bool, Nat.is_le(Nat.add(x, B), Nat.add(62n, B)), Nat.is_le(x, 62n), True{}, FR.le_cancel_r(x, 62n, B), hx62)
96      +h2 = N.le_trans(B, 53n, 1864n, hB, {==})
97      +hA = N.le_trans(A, Nat.add(x, B), 1926n, sub_le_self(Nat.add(x, B), 53n), N.le_trans(Nat.add(x, B), Nat.add(62n, B), 1926n, h1, h2))
98      +emax = max_le(A, 1926n, hA)
99      +hxa = N.le_trans(x, 62n, 1926n, N.lt_succ_le(x, 62n, hx), {==})
100      +hxb = N.le_trans(x, 62n, 1925n, N.lt_succ_le(x, 62n, hx), {==})
101      +j = Nat.sub(1925n, x)
102      +hj = RT.le_sub(53n, x, 1925n, N.le_trans(x, 62n, 1872n, N.lt_succ_le(x, 62n, hx), {==}))
103      +P = SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m))
104      +e1 = Equal.cong(Bool, F.F64, b => SF.pick(F.F64, b, SF.zero(s), SF.round_u(s, m, x, Nat.max(A, 1926n))), Nat.is_eq(m, 0n), False{}, hz)
105      +e2 = Equal.cong(Nat, F.F64, u => SF.round_u(s, m, x, u), Nat.max(A, 1926n), 1926n, emax)
106      # the pick reduces under pack's argument, so the checker never unfolds pack
107      +e3p = Equal.cong(Bool, Nat, b => SF.pick(Nat, b, SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), Nat.is_le(x, 1926n), True{}, hxa)
108      +e3 = Equal.cong(Nat, F.F64, t => SF.pack(s, t, 1926n), SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), SF.rne(m, Nat.sub(1926n, x)), e3p)
109      +e4 = Equal.cong(Nat, F.F64, t => SF.pack(s, SF.rne(m, t), 1926n), Nat.sub(1926n, x), 1n+j, N.sub_succ_left(1925n, x, hxb))
110      +e5 = Equal.cong(Nat, F.F64, t => SF.pack(s, t, 1926n), SF.rne(m, 1n+j), 0n, rne_zero(m, j, hm, hj))
111      +e6 = FR.enc_bits(s, 0n, 0n)
112      +r1 = SF.round_u(s, m, x, Nat.max(A, 1926n))
113      +r2 = SF.round_u(s, m, x, 1926n)
114      +r3 = SF.pack(s, SF.rne(m, Nat.sub(1926n, x)), 1926n)
115      +r4 = SF.pack(s, SF.rne(m, 1n+j), 1926n)
116      +r5 = SF.pack(s, 0n, 1926n)
117      +r6 = FR.bits(s, 0n)
118      +r2p = SF.pack(s, SF.pick(Nat, Nat.is_le(x, 1926n), SF.rne(m, Nat.sub(1926n, x)), C.shift(Nat.sub(x, 1926n), m)), 1926n)
119      Equal.trans(F.F64, SF.round(s, m, x), r1, SF.zero(s), e1, Equal.trans(F.F64, r1, r2, SF.zero(s), e2, Equal.trans(F.F64, r2, r2p, SF.zero(s), ru(s, m, x, 1926n), Equal.trans(F.F64, r2p, r3, SF.zero(s), e3, Equal.trans(F.F64, r3, r4, SF.zero(s), e4, Equal.trans(F.F64, r4, r5, SF.zero(s), e5, Equal.trans(F.F64, r5, r6, SF.zero(s), e6, bz(s))))))))