Interval arithmetic -- what approach?

Stream: metaprogramming / tactics

[Miroslav Olšák]

This topic is already discussed in maths and IMO streams, but I would like to ask here more about a possible implementation. Let's say I would like to automate proving things like $\pi \neq \sqrt2 + \sqrt3$ as Kevin did in the IMO stream.
To me, it sound reasonable to have a data structure representing two BigFloats (rationals with a denominator of the form $2^n$) $f_1, f_2$, one real number $x$, and a proof that $x\in[f_1, f_2]$ (interval, not a list :smile: ). With such intervals, I imagine performing arithmetic operations such as addition, multiplication, division, roots, etc. Every such operation could be performed with a certain precision -- it would be applied to the real number exactly, and the BigFloats could be rounded in a way that the proof could still be found. A tactic would then just follow a given calculation of a real number with a certain precision, and in the end returned the proof of the given inequality, if it is available from the calculation.
I could imagine doing all that on the meta level -- both $x$ and the proof that $x\in[f_1, f_2]$ could be just expressions, and only $f_1, f_2$ would be actually of a type BigFloat. The disadvantage of the approach is that it would require conversion of BigFloats into expressions, and second, it would be completely unverified, any bug would appear in the runtime of the appropriate tactic rather than during compilation of operations on intervals.
Other idea would be to really have a structure (f₁ f₂ : BigFloat) (x : ℝ) (x_lt : x ≤ f₂) (x_gt : x ≥ f₁) but we would need to somehow tell lean to actually calculate f₁, f₂ but not x, x_lt, x_gt.
What is the Lean way to do it? I am new to metaprogramming in lean (actually not even so experienced with lean in general), so maybe there is a suitable concept for that.

[Mario Carneiro]

I think Assia Mahboubi has a paper on how to do interval arithmetic in Coq, I would use that as the starting point

[Mario Carneiro]

Alternatively there is the approximation tactic in Isabelle although I don't know if there is a writeup of how it works

[Joseph Myers]

Given that some people would like to do program verification in Lean, and one area of program verification (with various existing practice) is verification of floating-point algorithms, if BigFloat can be implemented as a suitably general IEEE floating-point type (covering binary, decimal and maybe other radix, operating at IEEE level 3, covering decimal quantum exponents, covering exceptions and rounding modes, etc.) then you have infrastructure that can be used both for computation (via tactics) and verification of algorithms, which accords with mathlib principles of building up general infrastructure. You need rounding modes anyway to do properly rounded arithmetic on the endpoints of intervals to do interval arithmetic. (If someone wants to describe the operation of floating-point instructions on a given processor, they need a level 4 implementation, with all the implementation-specific rules about e.g. choice of NaN results. But that could certainly be built on top of a level 3 implementation.) Some key questions about this approach would be (a) does it make performance worse than something tuned purely for interval arithmetic? and (b) what would need generality from the start, and what could be implemented in a less general way that's still designed taking account of all the other IEEE features and so can be extended later without too much reimplementation?

[Mario Carneiro]

I would suggest using "abstract" interval arithmetic, rather than floats, unless you are actually compiling to float operations

[Mario Carneiro]

It's easier to deploy norm_num to work on rational arithmetic than float arithmetic

[Mario Carneiro]

floats are terrible in literally every possible way a spec can be

[Mario Carneiro]

For computation via tactics, it makes most sense to have the bounds of the interval be of type real

[Mario Carneiro]

but the tactic itself might be doing (unverified) float computations

[Mario Carneiro]

That said, IEEE verification is a thing, if you are specifically interested in that, and mathlib has some basic work on it in data.fp.basic

[Mario Carneiro]

(which BTW is a rare example of an unfinished proof in mathlib, cleverly worked around by using meta)

[Joseph Myers]

Also, if you prove error bounds for a particular algorithm, you can do just one set of (rounded) computations and extract an interval at the end (so half the number of computations compared to updating both endpoints at every step during the algorithm). But as interval arithmetic saves you from needing to do separate proofs about error propagation, it saves a lot of human time even if it involves more computations.

[Mario Carneiro]

Sure, but you don't need verified floats to do that

[Mario Carneiro]

You can do rounding with rational arithmetic too

[Mario Carneiro]

and you can use float computations under the hood to determine what to round to

[Joseph Myers]

(There's also the old issue #1038 "Implement computable real numbers" discussing various approaches in this area.)

[Yury G. Kudryashov]

Sometimes I want to forget that I opened this issue.

[Miroslav Olšák]

Oh, I floats are controversial, I see :smile: I didn't mean a standardized float numbers with all the +-inf, NaN, etc. Just that rationals seemed to me a bit less efficient for computation and unnecessary for approximate calculations.
But my main question was different -- if we define a structure (f₁ f₂ : BigFloat / ℚ) (x : ℝ) (x_lt : x ≤ f₂) (x_gt : x ≥ f₁), and some rounded operations on it, will it be usable by a tactic to actually proof inequalities using the defined computation?

[Miroslav Olšák]

Actually, +-inf would be likely necessary for the bounds of the interval but there could be also rationals with them in the library, right?

[Yury G. Kudryashov]

I don't know what's better: define a structure bundled_Icc, operations on this structure, and lemmas claiming correctness of these operations, or bundle x inside the structure. With the first approach it's clear that f₁ and f₂ in a + b don't depend on a.x and b.x.

[Yaël Dillies]

#14807 sounds relevant to this discussion. It implements intervals in preorders.