Real to Float and computable numbers

Stream: new members

[Arthur Adjedj]

Hi, i've seen a few topics recently talking about possibly making code on reals runnable and give back floats, but as far as I understand, this is not possible in general, unless working on computable numbers, something that, to my knowledge, isn't yet present in mathlib. If one was to implement an API for computable numbers over reals (showing it's a subfield of R, stable through basic functions like exp and log,...), would this be enough to have "runnable" code for the most common equations we use day to day ?

[Alex J. Best]

Yes there are many nice subsets of computable real numbers which contain commonly used functions, see for instance https://fredrikj.net/math/ejcim2020_joh_en.pdf, having such a thing in lean would be really cool. The most similar things we have already are the linarith and norm_num tactics, which while tactics do normalize certain expressions in real fields, but are not runnable code in the sense of a definition of a type for which lean generates the code

[Patrick Johnstone]

It is possible to make code runnable on floats but prove things about it for reals. See bottom of

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Patrick.20Johnstone.20.28mathematical.20optimizer.29

where we figure out you can just define the function polymorphically to run on both real and float data types. If you run it with floats your proofs don't mean anything but it will run.

[Arthur Adjedj]

This is interesting, thanks for the link :smiley: . I was more interested in the subject of approximating reals themselves with an arbitrary precision, rather than interpreting functions over reals as functions over floats, sorry for the bad wording of my question. I'd be very interested on working on computable numbers in Lean, but i do not know if this would be of any interest for mathlib, hence this post.

[Arthur Adjedj]

Alex J. Best said:

Yes there are many nice subsets of computable real numbers which contain commonly used functions, see for instance https://fredrikj.net/math/ejcim2020_joh_en.pdf, having such a thing in lean would be really cool. The most similar things we have already are the linarith and norm_num tactics, which while tactics do normalize certain expressions in real fields, but are not runnable code in the sense of a definition of a type for which lean generates the code

I'll look into this document in more details in the following days, thanks a lot for the link :smile:

[Alex J. Best]

You might also be interested in work of Krebbers and Spitters who implemented exact reals in Coq, such as https://arxiv.org/abs/1106.3448, which is part of https://github.com/coq-community/corn

[Mario Carneiro]

We have also done a few abstract real computations in mathlib in ad-hoc fashion, for example to prove high precision estimates on e and pi. The method depends on the particular real number to approximate but it ultimately boils down to some computations on natural numbers that can be proven by norm_num