def ieq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64close.bend:62

import Base
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/f64bits.bend as FB

62def ieq(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64, +e: Bool) -> {F.ic_eq(a, b, rel, at, e) == SF.pick(Bool, e, True{}, SF.pick(Bool, Bool.or(SF.is_inf(a), SF.is_inf(b)), False{}, SF.ic_near(a, b, rel, at, D(a, b)))) : Bool}:
63  match e:
64    case True{}:
65      {==}
66    case False{}:
67      +e1 = Equal.cong(Bool, Bool, t => F.ic_inf(a, b, rel, at, Bool.or(t, F.is_inf(b))), F.is_inf(a), SF.is_inf(a), FB.is_inf_value(a))
68      +e2 = Equal.cong(Bool, Bool, t => F.ic_inf(a, b, rel, at, Bool.or(SF.is_inf(a), t)), F.is_inf(b), SF.is_inf(b), FB.is_inf_value(b))
69      +b0 = F.ic_inf(a, b, rel, at, Bool.or(F.is_inf(a), F.is_inf(b)))
70      +b1 = F.ic_inf(a, b, rel, at, Bool.or(SF.is_inf(a), F.is_inf(b)))
71      +b2 = F.ic_inf(a, b, rel, at, Bool.or(SF.is_inf(a), SF.is_inf(b)))
72      +b3 = SF.pick(Bool, Bool.or(SF.is_inf(a), SF.is_inf(b)), False{}, SF.ic_near(a, b, rel, at, D(a, b)))
73      +g = SF.pick(Bool, False{}, True{}, b3)
74      Equal.trans(Bool, F.ic_eq(a, b, rel, at, False{}), b0, g, ie_f(a, b, rel, at), Equal.trans(Bool, b0, b1, g, e1, Equal.trans(Bool, b1, b2, g, e2, Equal.trans(Bool, b2, b3, g, iinf(a, b, rel, at, Bool.or(SF.is_inf(a), SF.is_inf(b))), Equal.sym(Bool, g, b3, pk_f(True{}, b3))))))