With @Vincent Semeria @MSoegtropIMC @Hugo Herbelin we're exploring how to proceed on Vincent's work on the constructive reals in the stdlib, from which the classical reals are derived.

Any opinions on whether/how this could interact with math-comp analysis?

Hi @Bas Spitters . I believe the project is very committed to classical analysis. Adding a constructive layer to MathComp analysis would definitively not be easy, and might interfere with the objective of concise proofs accessible to non-logicians.

I've been told that some discussions can be found here : https://github.com/coq/coq/wiki/CoqWG-2019-10#reals-vincent-semeria

Thanks @mkerjean Those notes are from half a year ago. Meanwhile, @Vincent Semeria has integrated the constructive reals within the existing classical reals while maintaining the old interface. Showing that this could be done quite smoothly.

To quote Andrej Bauer, 90% of the proofs in maths are constructive, the rest is just bad mathematical hygiene.

@MSoegtropIMC would like to compute with real numbers for very practical reasons.

Which non-logicians do you have in mind? One needs a certain logical background to understand how to formalize maths.

I would say that constructive proofs (or at least with a weak version of choice) in everyday analysis might come as a second step but do not provide the most direct nor well-known proofs. Formalizing everything by going towards constructive proofs clearly breaks the objective of short proofs alike that taught at university.

While to formalize maths one might one to know a bit about type theory, there is a huge gap between using Coq and saying that non-constructive proofs are bad hygiene don't you think ?

To say something more specific, even when dealing with limits, MathComp analysis uses the constructive indefinite description axiom. I don't think constructive proofs are easy to find in this library.

Andrej called *unnecessary* use of classical logic "bad logical hygiene", not non-constructive proofs in general.

One could build on the classical shell/API if one is inclined to write classical proofs.

How does one currently compute with real numbers in math-comp? E.g. how to prove e<3 ?

Constructive indefinite description is constructive :-) At least, it holds under propositions as types, not under propositions as ||Types|| (the default in HoTT). Also, I perhaps often a countable version might be enough, which is provable in HoTT.

Let me explain what I am up to. I am using Coq to verify electrical RF engineering work. This contains a lot of proofs, but also a lot of straight forward computations, say 3dB * 5dB <= 7 (x dB is defined as 10^(x/10). Usually the computations are of cause a bit longer but from a Coq complexity point of view that is what it is - one needs to compute with irrational numbers. I can prove such things with classical reals using e.g. CoqInterval reasonably well, but after working with classical reals in engineering for a few years now I cannot get the thought out of my mind that numbers which are abstract elements of a set which only exist because we have axioms which say so, somehow defeats the original purpose of numbers : to compute. With classical reals one cannot even know that 1<2 without applying several lemmas. Constructive reals are in a sense much more tangible than classical reals. I am also working a lot with CAS tools like Mathematica or Maxima and looking at all the types of numbers which are available in such tools, say floats, arbitrary precision floats, exact rationals, interval arithmetic and symbolic irrationals like sqrt(2) and thinking about their advantages and shortcomings I came up with a sort of wish list for numbers:

1.) numbers are easy to use in proofs, e.g. they build exactly a field
(not just approximately as floats do)

2.) rational numbers can be embedded exactly, e.g. 1/3 is not 0.3333 but 1/3

3.) irrational numbers can be represented numerically to arbitrary precision

4.) numerical computations are reasonably efficient (not more than 10x slower than equivalent precision arithmetic in Maxima (lisp) would be ideal)

5.) the numbers are in the physically relevant area (that is roughly ￼10^+-100) scale invariant, that is performance does not depend (substantially) on scale

6.) computations can be trusted

Nothing which exists in a CAS fulfils more than half of these requirements. I would say that the classical reals in the Coq standard library don't fulfil requirements 3 and 4 and likely also not 5. The point is, that with some tweaking constructive reals fulfil all 6 requirements. For me this is a very convincing argument to look into them. In the end I think I live in a world where simplicity of "low level" analysis proofs is much less important than the touch and feel of the numbers in practical computations. Analysis needs to be proven once and thats it. But computation is ubiquitous in engineering and natural sciences.

I know that constructive reals have a downside - it is not possible to have total functions and this can make it a pain to even just write down terms, but there might be ways around this - e.g. work with abstract terms rather than terms of type constructive real and interpret such terms with numbers when it comes to it. This is anyway common practice in the natural sciences, and also what CAS and Coq tools like ring, lra or CoqInterval do. So why not work with such terms in the first place?

I must admit I don't know what is better. I am quite successful with Coquelicot, CoqInterval, Gappa, Flocq, ... all tools based on classical reals and total functions. But as I said initially, I don't get this nagging doubt out of my mind that there might be something better.

What are constructive reals ? I though that due to R being uncountable it was not possible to "catch" all reals with a computable définition.

@vlj I think your message appears in the wrong topic, I guess you want to contribute to the constructive reals stdlib reals.

Assia Mahboubi said:

vlj I think your message appears in the wrong topic, I guess you want to contribute to the constructive reals stdlib reals.

@Assia Mahboubi feel free to reclassify messages in the appropriate topics...

Dear @Michael Soegtrop, having constructive reals and algorithms on them (in order to make computations) does not force one to do constructive analysis.

vlj said:

What are constructive reals ? I though that due to R being uncountable it was not possible to "catch" all reals with a computable définition.

This is a classic paradox in model theory (https://en.wikipedia.org/wiki/Skolem%27s_paradox). One will be able to prove uncountability within the model, even though the model could be countable.

Cyril Cohen said:

Assia Mahboubi feel free to reclassify messages in the appropriate topics...

I do not see how: may be just admins can?

@Cyril Cohen thans for the link. What is a countable axiomatisation ? It means a countable séquence of axiom ?

@Cyril Cohen do you have a coq development in mind that combines classical logic with computation on constructive real numbers?

There's the work by Russell and Cezary of course...

@Cyril Cohen : sure I can combine proofs and tools for classical reals with constructive reals. But this is not terribly convenient. Say I have a differential equation and I compute the generic solution using analysis proofs / tools based on classical reals. Then I want to put some concrete numbers into the generic solution and compute the result. This is what physicists and engineers do all day long. What I do today then is to compute an approximate result somewhere else (in a CAS) and use CoqInterval to show that this approximation is within certain limits of the true result. Alternatively I use proven correct interval arithmetic, but I didn't find a convenient way to do this as yet. Yes this is absolutely doable, but after doing this a few 1000 times I started to look for something a bit more convenient. With constructive reals I could just say "Compute the expression to this and that precision" and it would just do it. Of cause I can do the same with proven correct interval arithmetic, with the only difference that I have to estimate the required precision upfront. Well and of cause interval arithmetic does not form a field, while constructive reals do, so I have to do symbolic transformations with something else and then use some reinterpretation lemma to move from the symbolic world to the interval world and back. On the other hand I might have to do this also for constructive reals cause of the partial function issue, as explained in my above.

My post was more about: where do I want to be in the future and does it make sense to investigate such paths. I think for the overall acceptance of Coq in engineering, such nit picking details do make a difference. I do believe that constructive reals have a potential to be good "just do it and forget about all the details engineers are not interested in and which don't really matter here anyway" numbers - something like a fool proof proven correct pocket calculator. This could of cause also work with classical reals, but as far as I can tell only in a much less direct way using complicated tactics generating proofs. Constructive reals could just compute many interesting proofs. Well not really interesting proofs, but the kind of proofs I do for a living ;-)

Last updated: Feb 22 2024 at 04:02 UTC