~/jendhub

proofs/math/typed/f64close.bend

bend-collections-laws-math@1.0.0.0 · 94 lines · 14 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
3import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
4import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NE
5import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
6import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
7import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addv.bend as AV
8import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend as MV
9
10# isclose (python_style_math_stdlib_design.pdf 4.4; CPython's
11# math_isclose_impl): IsClose.value. The implementation is CPython's
12# algorithm on the proved operations, so each step is a proved clause:
13# Lt / Le / Eq (f64cmp), Sub and Mul (f64addv, f64mulv), Abs and IsInf
14# (f64bits).
15
16def fabs_v(+z: F.F64, +z2: F.F64, +h: {z == z2 : F.F64}) -> {F.abs(z) == SF.fabs(z2) : F.F64}:
17  Equal.trans(F.F64, F.abs(z), F.abs(z2), SF.fabs(z2), Equal.cong(F.F64, F.F64, t => F.abs(t), z, z2, h), FB.abs_value(z2))
18
19def D(+a: F.F64, +b: F.F64) -> F.F64:
20  SF.fabs(SF.add(b, SF.neg(a)))
21
22# three-way disjunction congruence over abstract Booleans (book-less: the
23# checker never unfolds the comparisons it is applied to)
24def or3(+x1: Bool, +x2: Bool, +x3: Bool, +y1: Bool, +y2: Bool, +y3: Bool, +h1: {x1 == y1 : Bool}, +h2: {x2 == y2 : Bool}, +h3: {x3 == y3 : Bool}) -> {Bool.or(Bool.or(x1, x2), x3) == Bool.or(Bool.or(y1, y2), y3) : Bool}:
25  +c1 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(t, x2), x3), x1, y1, h1)
26  +c2 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(y1, t), x3), x2, y2, h2)
27  +c3 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(y1, y2), t), x3, y3, h3)
28  Equal.trans(Bool, Bool.or(Bool.or(x1, x2), x3), Bool.or(Bool.or(y1, x2), x3), Bool.or(Bool.or(y1, y2), y3), c1, Equal.trans(Bool, Bool.or(Bool.or(y1, x2), x3), Bool.or(Bool.or(y1, y2), x3), Bool.or(Bool.or(y1, y2), y3), c2, c3))
29
30# d <= |r * x| on the implementation is le_s against the spec's |r * x|
31def lek(+d: F.F64, +r: F.F64, +x: F.F64) -> {F.le(d, F.abs(F.mul(r, x))) == SF.le_s(d, SF.fabs(SF.mul(r, x))) : Bool}:
32  +R = SF.fabs(SF.mul(r, x))
33  Equal.trans(Bool, F.le(d, F.abs(F.mul(r, x))), F.le(d, R), SF.le_s(d, R), Equal.cong(F.F64, Bool, t => F.le(d, t), F.abs(F.mul(r, x)), R, fabs_v(F.mul(r, x), SF.mul(r, x), MV.mul_value(r, x))), FC.le_value(d, R))
34
35def icd_t(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64, +d: F.F64) -> {F.ic_d(a, b, rel, at, d) == SF.ic_near(a, b, rel, at, d) : Bool}:
36  or3(F.le(d, F.abs(F.mul(rel, b))), F.le(d, F.abs(F.mul(rel, a))), F.le(d, at), SF.le_s(d, SF.fabs(SF.mul(rel, b))), SF.le_s(d, SF.fabs(SF.mul(rel, a))), SF.le_s(d, at), lek(d, rel, b), lek(d, rel, a), FC.le_value(d, at))
37
38def icd(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64) -> {F.ic_d(a, b, rel, at, F.abs(F.sub(b, a))) == SF.ic_near(a, b, rel, at, D(a, b)) : Bool}:
39  +d = D(a, b)
40  +e0 = Equal.cong(F.F64, Bool, t => F.ic_d(a, b, rel, at, t), F.abs(F.sub(b, a)), d, fabs_v(F.sub(b, a), SF.add(b, SF.neg(a)), AV.sub_value(b, a)))
41  Equal.trans(Bool, F.ic_d(a, b, rel, at, F.abs(F.sub(b, a))), F.ic_d(a, b, rel, at, d), SF.ic_near(a, b, rel, at, d), e0, icd_t(a, b, rel, at, d))
42
43# one unfolding step each, stated so the checker compares syntactically
44def ii_f(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64) -> {F.ic_inf(a, b, rel, at, False{}) == F.ic_d(a, b, rel, at, F.abs(F.sub(b, a))) : Bool}:
45  {==}
46
47def pk_f(+x: Bool, +y: Bool) -> {SF.pick(Bool, False{}, x, y) == y : Bool}:
48  {==}
49
50def iinf(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64, +big: Bool) -> {F.ic_inf(a, b, rel, at, big) == SF.pick(Bool, big, False{}, SF.ic_near(a, b, rel, at, D(a, b))) : Bool}:
51  match big:
52    case True{}:
53      {==}
54    case False{}:
55      +u = F.ic_d(a, b, rel, at, F.abs(F.sub(b, a)))
56      +n = SF.ic_near(a, b, rel, at, D(a, b))
57      Equal.trans(Bool, F.ic_inf(a, b, rel, at, False{}), u, SF.pick(Bool, False{}, False{}, n), ii_f(a, b, rel, at), Equal.trans(Bool, u, n, SF.pick(Bool, False{}, False{}, n), icd(a, b, rel, at), Equal.sym(Bool, SF.pick(Bool, False{}, False{}, n), n, pk_f(False{}, n))))
58
59def ie_f(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64) -> {F.ic_eq(a, b, rel, at, False{}) == F.ic_inf(a, b, rel, at, Bool.or(F.is_inf(a), F.is_inf(b))) : Bool}:
60  {==}
61
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))))))
75
76def NEAR(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64) -> Bool:
77  SF.pick(Bool, SF.eq_s(a, b), 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))))
78
79def itol(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64, +bad: Bool) -> {F.ic_tol(a, b, rel, at, bad) == SF.pick(Result<&2, &2, NE.NumError, Bool>, bad, Fail{NE.BadDomain{}}, Done{NEAR(a, b, rel, at)}) : Result<&2, &2, NE.NumError, Bool>}:
80  match bad:
81    case True{}:
82      {==}
83    case False{}:
84      +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => Done{F.ic_eq(a, b, rel, at, t)}, F.eq(a, b), SF.eq_s(a, b), FC.eq_value(a, b))
85      +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => Done{t}, F.ic_eq(a, b, rel, at, SF.eq_s(a, b)), NEAR(a, b, rel, at), ieq(a, b, rel, at, SF.eq_s(a, b)))
86      Equal.trans(Result<&2, &2, NE.NumError, Bool>, Done{F.ic_eq(a, b, rel, at, F.eq(a, b))}, Done{F.ic_eq(a, b, rel, at, SF.eq_s(a, b))}, Done{NEAR(a, b, rel, at)}, e1, e2)
87
88def isclose_value(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64) -> SF.IsClose.value(a, b, rel, at):
89  +z = F.zero(False{})
90  +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => F.ic_tol(a, b, rel, at, Bool.or(t, F.lt(at, z))), F.lt(rel, z), SF.lt_s(rel, z), FC.lt_value(rel, z))
91  +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => F.ic_tol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), t)), F.lt(at, z), SF.lt_s(at, z), FC.lt_value(at, z))
92  +r1 = F.ic_tol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), F.lt(at, z)))
93  +r2 = F.ic_tol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), SF.lt_s(at, z)))
94  Equal.trans(Result<&2, &2, NE.NumError, Bool>, F.isclose(a, b, rel, at), r1, SF.isclose(a, b, rel, at), e1, Equal.trans(Result<&2, &2, NE.NumError, Bool>, r1, r2, SF.isclose(a, b, rel, at), e2, itol(a, b, rel, at, Bool.or(SF.lt_s(rel, z), SF.lt_s(at, z)))))