New `by_approx` tactic for proving real inequalities

Stream: mathlib4

[Sebastian Zimmer]

Work in progress new tactic: https://github.com/leanprover-community/mathlib4/pull/8949

It proves goals like

example : |sqrt 2 - 1.414| < 0.001 := by by_approx

example : exp (sqrt 10) > 23.6243 := by by_approx

by searching for successively precise rational approximations of both sides.

Currently it is really inefficient. This is for the following reasons:

• It has a global precision value which gets increased each iteration across the entire expression. For example, if you have an expression like 1000 * sqrt 2 + exp 0.5 it will might expend loads of effort coming up with accurate approximations for exp 0.5, even though the accuracy of the sqrt term is much more important.

• It throws away lots of information after each iteration. This doesn't matter as much as it sounds because only on the final iteration does it actually produce a proof term, and this is often the majority of the runtime of the tactic.

• It does no rounding on the rational numbers which appear as intermediate terms. This means that really big integers show up in calculations when they don't really need to.

• It uses the norm_num tactic many times to produce the final proof. Previously I was doing as much as I could with reduce which was much faster for Nat expressions but didn't work at all for rational ones.

• I have not put any effort into making sure the computed approximations are actually reasonable. I think the exp one is probably fine, but sqrt is more questionable

[Sebastian Zimmer]

My vision for the tactic is that it should build a tree of approximations for each side of the expression. Then on each iteration it should only work on the section of the tree that is responsible for the largest share of the error.

I think I want to implement more extensions (especially log, which was the reason I made this in the first place) before I change the approach though. That way I can measure what works best, and the tactic is already fast enough for some usecases.

[Michael Stoll]

A long tim ago, I have written an implementation of "lazy computable reals" in Common Lisp; see "reals.lsp" near the bottom of this page. This could perhaps provide some inspriration on how evaluation with the necessary precision can be implemented.