def magc_c

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

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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

182def magc_c(+one: Nat, +h1: {one == 1n : Nat}, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +nx: {SF.is_nan(F.Bits{xl, xh}) == False{} : Bool}, +ny: {SF.is_nan(F.Bits{yl, yh}) == False{} : Bool}, +ix: Bool, +hix: {SF.is_inf(F.Bits{xl, xh}) == ix : Bool}, +iy: Bool, +hiy: {SF.is_inf(F.Bits{yl, yh}) == iy : Bool}) -> {SF.pick(Cmp, ix, SF.pick(Cmp, iy, EQ{}, GT{}), SF.pick(Cmp, iy, LT{}, 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}:
183  match ix iy:
184    case True{} True{}:
185      +ex = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, and_l(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), hix))
186      +ey = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, and_l(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), hiy))
187      +fx = N.eq_from_is_eq(SF.frac(F.Bits{xl, xh}), 0n, and_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), hix))
188      +fy = N.eq_from_is_eq(SF.frac(F.Bits{yl, yh}), 0n, and_r(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), hiy))
189      +eE = Equal.trans(Nat, SF.efield(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), ex, Equal.sym(Nat, SF.efield(F.Bits{yl, yh}), 2047n, ey))
190      +eF = Equal.trans(Nat, SF.frac(F.Bits{xl, xh}), 0n, SF.frac(F.Bits{yl, yh}), fx, Equal.sym(Nat, SF.frac(F.Bits{yl, yh}), 0n, fy))
191      +eK = Equal.trans(Nat, 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{xl, xh}))), Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, SF.efield(F.Bits{yl, yh}))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(52n, SF.efield(F.Bits{xl, xh}))), SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}), eF), Equal.cong(Nat, Nat, z => Nat.add(SF.frac(F.Bits{yl, yh}), C.shift(52n, z)), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), eE))
192      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})))), EQ{}, L.subst(Nat, z => {Nat.cmp(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))), z) == EQ{} : 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}))), eK, NC.cmp_refl(Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.efield(F.Bits{xl, xh}))))))
193    case True{} False{}:
194      +ex = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, and_l(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), hix))
195      +hy = lt2047(yl, yh, hiy, ny)
196      +h = L.subst(Nat, z => {Nat.is_lt(SF.efield(F.Bits{yl, yh}), z) == True{} : Bool}, 2047n, SF.efield(F.Bits{xl, xh}), Equal.sym(Nat, SF.efield(F.Bits{xl, xh}), 2047n, ex), hy)
197      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})))), GT{}, Equal.trans(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}))), GT{}, 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}), hF(xl, xh), hF(yl, yh)), Equal.cong(Cmp, Cmp, t => NC.lex(t, Nat.cmp(SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}))), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})), GT{}, NC.cmp_gt(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), h))))
198    case False{} True{}:
199      +ey = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, and_l(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), hiy))
200      +hx = lt2047(xl, xh, hix, nx)
201      +h = L.subst(Nat, z => {Nat.is_lt(SF.efield(F.Bits{xl, xh}), z) == True{} : Bool}, 2047n, SF.efield(F.Bits{yl, yh}), Equal.sym(Nat, SF.efield(F.Bits{yl, yh}), 2047n, ey), hx)
202      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})))), LT{}, Equal.trans(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}))), LT{}, 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}), hF(xl, xh), hF(yl, yh)), Equal.cong(Cmp, Cmp, t => NC.lex(t, Nat.cmp(SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}))), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})), LT{}, NC.cmp_lt(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), h))))
203    case False{} False{}:
204      mcf(one, h1, xl, xh, yl, yh)