proofs/math/typed/float.bend

bend-collections-laws-math@1.0.0.0 · 211 lines · 41 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
3import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
4import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N
5import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
6import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
7
8# The float clauses of spec/math/generic.bend (FMin.select, FMax.select,
9# FClamp.select, FAbs.value, FSign.select, FSum.fold, FProd.fold,
10# FPow.binary), proved once for every instance whose over-tests are False
11# and then read at F32 (Base's primitives) and F64 (src/math/f64.bend).
12#
13# The clauses say how each generic function combines the instance's own
14# operations (which operation, on which arguments, in which order); they do
15# not depend on what the operations compute, so they hold for any
16# operations, IEEE's included. This is the parametric style of Mathlib's
17# lemmas over a structure (Mathlib.Algebra.Order.*: statements over any
18# LinearOrder / ring, instantiated per type), and of the "free theorems"
19# of parametric polymorphism (Wadler, Theorems for free!, 1989).
20
21# the instance never reports an overflow (floats round instead)
22def NoAddOver(~T: Data, ~test: N.Test<T> -> Bool) -> Type:
23  @+a: T -> @+b: T -> {test(N.AddOver{a, b}) == False{} : Bool}
24
25def NoMulOver(~T: Data, ~test: N.Test<T> -> Bool) -> Type:
26  @+a: T -> @+b: T -> {test(N.MulOver{a, b}) == False{} : Bool}
27
28# ---- selections: the two picks agree ----
29
30def pick_eq(-T: Data, +c: Bool, +a: T, +b: T) -> {G.pick(T, c, a, b) == SG.pick(T, c, a, b) : T}:
31  match c:
32    case True{}:
33      {==}
34    case False{}:
35      {==}
36
37def fmin_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +a: T, +b: T) -> SG.FMin.select(~T, ~op, ~test, a, b):
38  pick_eq(T, test(N.Lt{b, a}), b, a)
39
40def fmax_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +a: T, +b: T) -> SG.FMax.select(~T, ~op, ~test, a, b):
41  pick_eq(T, test(N.Lt{a, b}), b, a)
42
43def fclamp_c(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +lo: T, +hi: T, +c: Bool) -> {G.clamp_ok(~T, ~op, ~test, x, lo, hi, c) == SG.fclamp_pick(~T, ~test, x, lo, hi, c) : Result<&2, &2, N.NumError, T>}:
44  match c:
45    case True{}:
46      {==}
47    case False{}:
48      %Equal.sym(T, G.pick(T, test(N.Lt{x, lo}), lo, x), SG.pick(T, test(N.Lt{x, lo}), lo, x), pick_eq(T, test(N.Lt{x, lo}), lo, x)) : {Done{G.pick(T, test(N.Lt{hi, _}), hi, _)} == Done{SG.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x))} : Result<&2, &2, N.NumError, T>}
49      %Equal.sym(T, G.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)), SG.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)), pick_eq(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x))) : {Done{_} == Done{SG.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x))} : Result<&2, &2, N.NumError, T>}
50      {==}
51
52def fclamp_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +lo: T, +hi: T) -> SG.FClamp.select(~T, ~op, ~test, x, lo, hi):
53  fclamp_c(~T, ~op, ~test, x, lo, hi, test(N.Lt{hi, lo}))
54
55def fabs_value(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> SG.FAbs.value(~T, ~op, ~test, x):
56  {==}
57
58def sign_b(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +c: Bool) -> {G.sign_below(~T, ~op, ~test, x, c) == SG.pick(T, c, op(N.Neg{op(N.One{})}), x) : T}:
59  match c:
60    case True{}:
61      {==}
62    case False{}:
63      {==}
64
65def sign_a(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +c: Bool) -> {G.sign_above(~T, ~op, ~test, x, c) == SG.pick(T, c, op(N.One{}), SG.pick(T, test(N.Lt{x, op(N.ZeroOp{})}), op(N.Neg{op(N.One{})}), x)) : T}:
66  match c:
67    case True{}:
68      {==}
69    case False{}:
70      sign_b(~T, ~op, ~test, x, test(N.Lt{x, op(N.ZeroOp{})}))
71
72def fsign_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> SG.FSign.select(~T, ~op, ~test, x):
73  sign_a(~T, ~op, ~test, x, test(N.Lt{op(N.ZeroOp{}), x}))
74
75# ---- folds: with no overflow the checked fold is the plain fold ----
76
77def sum_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~ao: NoAddOver(~T, ~test), xs: List<&2, T>, +acc: T) -> {G.sum_go(~T, ~op, ~test, xs, Some{acc}) == Some{SG.fold_add(~T, ~op, xs, acc)} : Maybe<&2, T>}:
78  match xs:
79    case Nil{}:
80      {==}
81    case Con{+x, t}:
82      %Equal.sym(Bool, test(N.AddOver{acc, x}), False{}, ao(acc, x)) : {G.sum_go(~T, ~op, ~test, t, G.fits(T, _, op(N.Add{acc, x}))) == Some{SG.fold_add(~T, ~op, t, op(N.Add{acc, x}))} : Maybe<&2, T>}
83      sum_fold(~T, ~op, ~test, ~ao, t, op(N.Add{acc, x}))
84
85def fsum_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~ao: NoAddOver(~T, ~test), xs: List<&2, T>) -> SG.FSum.fold(~T, ~op, ~test, xs):
86  %Equal.sym(Maybe<&2, T>, G.sum_go(~T, ~op, ~test, xs, Some{op(N.ZeroOp{})}), Some{SG.fold_add(~T, ~op, xs, op(N.ZeroOp{}))}, sum_fold(~T, ~op, ~test, ~ao, xs, op(N.ZeroOp{}))) : {G.ok(T, _) == Done{SG.fold_add(~T, ~op, xs, op(N.ZeroOp{}))} : Result<&2, &2, N.NumError, T>}
87  {==}
88
89def prod_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), xs: List<&2, T>, +acc: T) -> {G.prod_go(~T, ~op, ~test, xs, Some{acc}) == Some{SG.fold_mul(~T, ~op, xs, acc)} : Maybe<&2, T>}:
90  match xs:
91    case Nil{}:
92      {==}
93    case Con{+x, t}:
94      %Equal.sym(Bool, test(N.MulOver{acc, x}), False{}, mo(acc, x)) : {G.prod_go(~T, ~op, ~test, t, G.fits(T, _, op(N.Mul{acc, x}))) == Some{SG.fold_mul(~T, ~op, t, op(N.Mul{acc, x}))} : Maybe<&2, T>}
95      prod_fold(~T, ~op, ~test, ~mo, t, op(N.Mul{acc, x}))
96
97def fprod_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), xs: List<&2, T>) -> SG.FProd.fold(~T, ~op, ~test, xs):
98  %Equal.sym(Maybe<&2, T>, G.prod_go(~T, ~op, ~test, xs, Some{op(N.One{})}), Some{SG.fold_mul(~T, ~op, xs, op(N.One{}))}, prod_fold(~T, ~op, ~test, ~mo, xs, op(N.One{}))) : {G.ok(T, _) == Done{SG.fold_mul(~T, ~op, xs, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
99  {==}
100
101# ---- pow: square-and-multiply is the specification's binary exponentiation ----
102
103# k = 0 is a fixed point of the specification's loop
104def binpow_zero(~T: Data, ~op: N.Op<T> -> T, fuel: Nat, +b: T, +a: T) -> {SG.binpow(~T, ~op, fuel, 0n, b, a) == a : T}:
105  match fuel:
106    case 0n:
107      {==}
108    case 1n+f:
109      binpow_zero(~T, ~op, f, b, a)
110
111def sq_val_eq(~T: Data, ~op: N.Op<T> -> T, +c: Bool, +b: T) -> {G.sq_val(~T, ~op, c, b) == SG.pick(T, c, op(N.Mul{b, b}), b) : T}:
112  match c:
113    case True{}:
114      {==}
115    case False{}:
116      {==}
117
118def sq_ok_eq(~T: Data, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +c: Bool, +b: T) -> {G.sq_ok(~T, ~test, c, b, True{}) == True{} : Bool}:
119  match c:
120    case True{}:
121      %Equal.sym(Bool, test(N.MulOver{b, b}), False{}, mo(b, b)) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
122      {==}
123    case False{}:
124      {==}
125
126def mul_st_eq(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +d: Bool, +b: T, +a: T) -> {G.mul_st(~T, ~op, ~test, d, b, True{}, (a, True{})) == (SG.pick(T, d, op(N.Mul{a, b}), a), True{}) : T & Bool}:
127  match d:
128    case True{}:
129      %Equal.sym(Bool, test(N.MulOver{a, b}), False{}, mo(a, b)) : {(op(N.Mul{a, b}), Bool.and(Bool.and(True{}, True{}), Bool.not(_))) == (op(N.Mul{a, b}), True{}) : T & Bool}
130      {==}
131    case False{}:
132      {==}
133
134def pow_bin(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +fuel: Nat, +k: Nat, +b: T, +a: T) -> {G.pow_go(~T, ~op, ~test, fuel, k, b, True{}, (a, True{})) == Some{SG.binpow(~T, ~op, fuel, k, b, a)} : Maybe<&2, T>}:
135  match fuel k:
136    case 0n _:
137      {==}
138    case 1n+ +f 0n:
139      %Equal.sym(T, SG.binpow(~T, ~op, f, 0n, b, a), a, binpow_zero(~T, ~op, f, b, a)) : {Some{a} == Some{_} : Maybe<&2, T>}
140      {==}
141    case 1n+ +f 1n+ +j:
142      %Equal.sym(T & Bool, G.mul_st(~T, ~op, ~test, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), b, True{}, (a, True{})), (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{}), mul_st_eq(~T, ~op, ~test, ~mo, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), b, a)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), G.sq_ok(~T, ~test, Nat.is_lt(1n, 1n+j), b, True{}), _) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
143      %Equal.sym(Bool, G.sq_ok(~T, ~test, Nat.is_lt(1n, 1n+j), b, True{}), True{}, sq_ok_eq(~T, ~test, ~mo, Nat.is_lt(1n, 1n+j), b)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), _, (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{})) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
144      %Equal.sym(T, G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), sq_val_eq(~T, ~op, Nat.is_lt(1n, 1n+j), b)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), _, True{}, (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{})) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
145      pow_bin(~T, ~op, ~test, ~mo, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))
146
147def fpow_binary(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +x: T, +k: Nat) -> SG.FPow.binary(~T, ~op, ~test, x, k):
148  %Equal.sym(Maybe<&2, T>, G.pow_go(~T, ~op, ~test, 1n+k, k, x, True{}, (op(N.One{}), True{})), Some{SG.binpow(~T, ~op, 1n+k, k, x, op(N.One{}))}, pow_bin(~T, ~op, ~test, ~mo, 1n+k, k, x, op(N.One{}))) : {G.ok(T, _) == Done{SG.binpow(~T, ~op, 1n+k, k, x, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
149  {==}
150
151# ---- F32 and F64: the over-tests are False ----
152
153def f32_ao(+a: F32, +b: F32) -> {I.f32_is(N.AddOver{a, b}) == False{} : Bool}:
154  {==}
155
156def f32_mo(+a: F32, +b: F32) -> {I.f32_is(N.MulOver{a, b}) == False{} : Bool}:
157  {==}
158
159def f64_ao(+a: F.F64, +b: F.F64) -> {F.f64_is(N.AddOver{a, b}) == False{} : Bool}:
160  {==}
161
162def f64_mo(+a: F.F64, +b: F.F64) -> {F.f64_is(N.MulOver{a, b}) == False{} : Bool}:
163  {==}
164
165def f32_min(+a: F32, +b: F32) -> SG.FMin.select(~F32, ~I.f32_op, ~I.f32_is, a, b):
166  fmin_select(~F32, ~I.f32_op, ~I.f32_is, a, b)
167
168def f32_max(+a: F32, +b: F32) -> SG.FMax.select(~F32, ~I.f32_op, ~I.f32_is, a, b):
169  fmax_select(~F32, ~I.f32_op, ~I.f32_is, a, b)
170
171def f32_clamp(+x: F32, +lo: F32, +hi: F32) -> SG.FClamp.select(~F32, ~I.f32_op, ~I.f32_is, x, lo, hi):
172  fclamp_select(~F32, ~I.f32_op, ~I.f32_is, x, lo, hi)
173
174def f32_abs(+x: F32) -> SG.FAbs.value(~F32, ~I.f32_op, ~I.f32_is, x):
175  fabs_value(~F32, ~I.f32_op, ~I.f32_is, x)
176
177def f32_sign(+x: F32) -> SG.FSign.select(~F32, ~I.f32_op, ~I.f32_is, x):
178  fsign_select(~F32, ~I.f32_op, ~I.f32_is, x)
179
180def f32_sum(xs: List<&2, F32>) -> SG.FSum.fold(~F32, ~I.f32_op, ~I.f32_is, xs):
181  fsum_fold(~F32, ~I.f32_op, ~I.f32_is, ~(a => b => f32_ao(a, b)), xs)
182
183def f32_prod(xs: List<&2, F32>) -> SG.FProd.fold(~F32, ~I.f32_op, ~I.f32_is, xs):
184  fprod_fold(~F32, ~I.f32_op, ~I.f32_is, ~(a => b => f32_mo(a, b)), xs)
185
186def f32_pow(+x: F32, +k: Nat) -> SG.FPow.binary(~F32, ~I.f32_op, ~I.f32_is, x, k):
187  fpow_binary(~F32, ~I.f32_op, ~I.f32_is, ~(a => b => f32_mo(a, b)), x, k)
188
189def f64_min(+a: F.F64, +b: F.F64) -> SG.FMin.select(~F.F64, ~F.f64_op, ~F.f64_is, a, b):
190  fmin_select(~F.F64, ~F.f64_op, ~F.f64_is, a, b)
191
192def f64_max(+a: F.F64, +b: F.F64) -> SG.FMax.select(~F.F64, ~F.f64_op, ~F.f64_is, a, b):
193  fmax_select(~F.F64, ~F.f64_op, ~F.f64_is, a, b)
194
195def f64_clamp(+x: F.F64, +lo: F.F64, +hi: F.F64) -> SG.FClamp.select(~F.F64, ~F.f64_op, ~F.f64_is, x, lo, hi):
196  fclamp_select(~F.F64, ~F.f64_op, ~F.f64_is, x, lo, hi)
197
198def f64_abs(+x: F.F64) -> SG.FAbs.value(~F.F64, ~F.f64_op, ~F.f64_is, x):
199  fabs_value(~F.F64, ~F.f64_op, ~F.f64_is, x)
200
201def f64_sign(+x: F.F64) -> SG.FSign.select(~F.F64, ~F.f64_op, ~F.f64_is, x):
202  fsign_select(~F.F64, ~F.f64_op, ~F.f64_is, x)
203
204def f64_sum(xs: List<&2, F.F64>) -> SG.FSum.fold(~F.F64, ~F.f64_op, ~F.f64_is, xs):
205  fsum_fold(~F.F64, ~F.f64_op, ~F.f64_is, ~(a => b => f64_ao(a, b)), xs)
206
207def f64_prod(xs: List<&2, F.F64>) -> SG.FProd.fold(~F.F64, ~F.f64_op, ~F.f64_is, xs):
208  fprod_fold(~F.F64, ~F.f64_op, ~F.f64_is, ~(a => b => f64_mo(a, b)), xs)
209
210def f64_pow(+x: F.F64, +k: Nat) -> SG.FPow.binary(~F.F64, ~F.f64_op, ~F.f64_is, x, k):
211  fpow_binary(~F.F64, ~F.f64_op, ~F.f64_is, ~(a => b => f64_mo(a, b)), x, k)