def mcf

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64cmp.bend:127

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/math/typed/natcmp.bend as NC

127# the finite branch of mag_cmp compares K
128def mcf(+one: Nat, +h1: {one == 1n : Nat}, +xl: U32, +xh: U32, +yl: U32, +yh: U32) -> {Nat.cmp(C.shift(Nat.sub(SF.xexp(F.Bits{xl, xh}), Nat.min(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.sub(SF.xexp(F.Bits{yl, yh}), Nat.min(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}))), SF.mant(F.Bits{yl, yh}))) == Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))) : Cmp}:
129  +hFx = hF(xl, xh)
130  +hFy = hF(yl, yh)
131  +e1 = NC.cmp_min(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh}))
132  +ex = xshx(F.Bits{xl, xh})
133  +ey = xshx(F.Bits{yl, yh})
134  +e2 = Equal.trans(Cmp, Nat.cmp(C.shift(SF.xexp(F.Bits{xl, xh}), SF.mant(F.Bits{xl, xh})), C.shift(SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{yl, yh}))), Nat.cmp(C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{yl, yh}))), Nat.cmp(C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh})))), Equal.cong(Nat, Cmp, z => Nat.cmp(z, C.shift(SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{yl, yh}))), C.shift(SF.xexp(F.Bits{xl, xh}), SF.mant(F.Bits{xl, xh})), C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), ex), Equal.cong(Nat, Cmp, z => Nat.cmp(C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), z), C.shift(SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{yl, yh})), C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}))), ey))
135  +e3 = NC.cmp_shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh})))
136  +e4 = gcmp(one, h1, SF.efield(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), {==}, SF.b2n(Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n))), {==}, SF.frac(F.Bits{xl, xh}), hFx, SF.efield(F.Bits{yl, yh}), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), {==}, SF.b2n(Bool.not(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n))), {==}, SF.frac(F.Bits{yl, yh}), hFy)
137  +e5 = Equal.sym(Cmp, Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))), NC.lex(Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})), Nat.cmp(SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}))), NC.cmp_limbs(52n, SF.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), hFx, hFy))
138  Equal.trans(Cmp, Nat.cmp(C.shift(Nat.sub(SF.xexp(F.Bits{xl, xh}), Nat.min(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}))), SF.mant(F.Bits{xl, xh})), C.shift(Nat.sub(SF.xexp(F.Bits{yl, yh}), Nat.min(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}))), SF.mant(F.Bits{yl, yh}))), Nat.cmp(C.shift(SF.xexp(F.Bits{xl, xh}), SF.mant(F.Bits{xl, xh})), C.shift(SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{yl, yh}))), Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))), e1, Equal.trans(Cmp, Nat.cmp(C.shift(SF.xexp(F.Bits{xl, xh}), SF.mant(F.Bits{xl, xh})), C.shift(SF.xexp(F.Bits{yl, yh}), SF.mant(F.Bits{yl, yh}))), Nat.cmp(C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh})))), Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))), e2, Equal.trans(Cmp, Nat.cmp(C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh}))), C.shift(1925n, C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh})))), Nat.cmp(C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}))), Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))), e3, Equal.trans(Cmp, Nat.cmp(C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 1n, SF.efield(F.Bits{xl, xh})), SF.mant(F.Bits{xl, xh})), C.shift(SF.pick(Nat, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), 1n, SF.efield(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}))), NC.lex(Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})), Nat.cmp(SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}))), Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh})))), e4, e5))))