def tu_fin_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:152

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/num.bend as NE
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/f64tools.bend as T

152def tu_fin_c(+x: F.F64, +c: Bool, +hc: {Nat.is_le(3000n, F.dexp(x)) == c : Bool}) -> {SF.rv64(F.tu_fin(x, c)) == TN(SF.sign(x), IPc(x, c)) : Result<&2, &2, NE.NumError, Nat>}:
153  match c:
154    case True{}:
155      +k = Nat.sub(F.dexp(x), 3000n)
156      +e0 = big_nat(F.signbit(x), F.dmant(x), k, big_nz(x, hc), hw53(x))
157      +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, t => TN(t, C.shift(k, SW.value(F.dmant(x)))), F.signbit(x), SF.sign(x), FB.signbit_value(x))
158      +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.shift(k, t)), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
159      +e3 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.shift(Nat.sub(t, 3000n), SF.mant(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
160      +r0 = TN(F.signbit(x), C.shift(k, SW.value(F.dmant(x))))
161      +r1 = TN(SF.sign(x), C.shift(k, SW.value(F.dmant(x))))
162      +r2 = TN(SF.sign(x), C.shift(k, SF.mant(x)))
163      Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_fin(x, True{})), r0, TN(SF.sign(x), IPc(x, True{})), e0, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r0, r1, TN(SF.sign(x), IPc(x, True{})), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r1, r2, TN(SF.sign(x), IPc(x, True{})), e2, e3)))
164    case False{}:
165      +k = Nat.sub(3000n, F.dexp(x))
166      +e0 = small_nat(F.signbit(x), F.dmant(x), k)
167      +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, t => TN(t, C.high(k, SW.value(F.dmant(x)))), F.signbit(x), SF.sign(x), FB.signbit_value(x))
168      +e2 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.high(k, t)), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
169      +e3 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, t => TN(SF.sign(x), C.high(Nat.sub(3000n, t), SF.mant(x))), F.dexp(x), SF.xexp(x), T.dexp_value(x))
170      +r0 = TN(F.signbit(x), C.high(k, SW.value(F.dmant(x))))
171      +r1 = TN(SF.sign(x), C.high(k, SW.value(F.dmant(x))))
172      +r2 = TN(SF.sign(x), C.high(k, SF.mant(x)))
173      Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.tu_fin(x, False{})), r0, TN(SF.sign(x), IPc(x, False{})), e0, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r0, r1, TN(SF.sign(x), IPc(x, False{})), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, r1, r2, TN(SF.sign(x), IPc(x, False{})), e2, e3)))