def fm_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:388

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/proofs/lib/nat.bend as N
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/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

388# a zero x
389def fm_zero(+x: F.F64, +y: F.F64, +hzx: {SF.is_zero(x) == True{} : Bool}, +hzy: {SF.is_zero(y) == False{} : Bool}, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {FM(x, y) == x : F.F64}:
390  +s = SF.sign(x)
391  +em = N.eq_from_is_eq(SF.mant(x), 0n, Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), SF.is_zero(x), True{}, T.mant_z(x), hzx))
392  +a = Nat.sub(SF.xexp(x), SF.rsc(x, y))
393  +rb = SF.rb(x, y)
394  +hmy = FL.nz_le(SF.mant(y), Equal.trans(Bool, Nat.is_eq(SF.mant(y), 0n), SF.is_zero(y), False{}, T.mant_z(y), hzy))
395  +hrb = N.succ_le_lt(0n, rb, N.le_trans(1n, SF.mant(y), rb, hmy, WW.shift_ge(Nat.sub(SF.xexp(y), SF.rsc(x, y)), SF.mant(y))))
396  +e1 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(C.shift(a, t), rb), SF.rsc(x, y)), SF.mant(x), 0n, em)
397  +e2 = Equal.cong(Nat, F.F64, t => SF.round(s, Nat.mod(t, rb), SF.rsc(x, y)), C.shift(a, 0n), 0n, WW.shift_zero(a))
398  +e3 = Equal.cong(Nat, F.F64, t => SF.round(s, t, SF.rsc(x, y)), Nat.mod(0n, rb), 0n, mod_small(0n, rb, hrb))
399  +e4 = Equal.cong(Nat, F.F64, t => SF.round(s, t, SF.xexp(x)), 0n, SF.mant(x), Equal.sym(Nat, SF.mant(x), 0n, N.eq_from_is_eq(SF.mant(x), 0n, Equal.trans(Bool, Nat.is_eq(SF.mant(x), 0n), SF.is_zero(x), True{}, T.mant_z(x), hzx))))
400  +r1 = SF.round(s, Nat.mod(C.shift(a, 0n), rb), SF.rsc(x, y))
401  +r2 = SF.round(s, Nat.mod(0n, rb), SF.rsc(x, y))
402  +r3 = SF.round(s, 0n, SF.rsc(x, y))
403  +r4 = SF.round(s, 0n, SF.xexp(x))
404  Equal.trans(F.F64, FM(x, y), r1, x, e1, Equal.trans(F.F64, r1, r2, x, e2, Equal.trans(F.F64, r2, r3, x, e3, Equal.trans(F.F64, r3, r4, x, {==}, Equal.trans(F.F64, r4, SF.round(s, SF.mant(x), SF.xexp(x)), x, e4, rt(x, hfin))))))