## Stream: metaprogramming / tactics

### Topic: Interval arithmetic -- what approach?

#### Miroslav Olšák (Oct 02 2020 at 13:55):

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 (Oct 02 2020 at 15:05):

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 (Oct 02 2020 at 15:05):

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

#### Joseph Myers (Oct 02 2020 at 19:26):

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 (Oct 02 2020 at 19:28):

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

#### Mario Carneiro (Oct 02 2020 at 19:28):

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

#### Mario Carneiro (Oct 02 2020 at 19:29):

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

#### Mario Carneiro (Oct 02 2020 at 19:30):

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

#### Mario Carneiro (Oct 02 2020 at 19:31):

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

#### Mario Carneiro (Oct 02 2020 at 19:32):

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 (Oct 02 2020 at 19:34):

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

#### Joseph Myers (Oct 02 2020 at 19:35):

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 (Oct 02 2020 at 19:35):

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

#### Mario Carneiro (Oct 02 2020 at 19:36):

You can do rounding with rational arithmetic too

#### Mario Carneiro (Oct 02 2020 at 19:36):

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

#### Joseph Myers (Oct 02 2020 at 19:40):

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

#### Yury G. Kudryashov (Oct 02 2020 at 19:55):

Sometimes I want to forget that I opened this issue.

#### Miroslav Olšák (Oct 03 2020 at 07:47):

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 (Oct 03 2020 at 07:51):

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 (Oct 03 2020 at 08:30):

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.

Last updated: May 09 2021 at 22:13 UTC