Converting between formulations of reals in Coq

Question

While trying to answer more concretely a question on floating points, I tried proving a simple statement using the Flocq library of Coq. However, I got stuck before really exercising it because I am confused about the various notions of reals in Coq itself.

What are the differences between Dedekind reals (cuts of the rational line) and Cauchy reals (convergent sequences) as defined by Coq; which ones are constructive or not, and how can I convert from one to the other concretely? Are there other useful formulations of reals?

For instance, Rrepr : R -> ConstructiveCauchyReals.CReal seems to convert from Dedekind reals (I think) to Cauchy reals, but Compute Rrepr 3. simply yields = Rrepr (R1 + (R1 + R1)) : ConstructiveCauchyReals.CReal which means that 3 was interpreted as the real 1+1+1, but does not further evaluate to a concrete Cauchy real. According to Print ConstructiveCauchyReals.CReal., this should be a Record consisting of a sequence, a scale, and some convergence proofs.

Answer 1

I apologize, but the correct answer is “you do not want to convert between different formulations of reals”. As a rule of thumb, you should pick one formalization of reals and run with it. Trying to use several will just bring you pain and confusion.

The reals in the standard Coq library are a classical abomination that assumes a crazy form of choice and it axiomatizes the reals rather than constructs them. You can't compute a thing with those, don't use them unless you have to.

To give you at least something positive in my answer, here's a quick overview of the constructive theory of reals. If you'd like to know more, I recommend Chapter 11 of the HoTT book as a possible starting point. Another useful source is Auke Booij's PhD thesis.

A quick overview of real numbers constructions

The Dedekind reals are constructed as cuts of rationals.

The Cauchy reals are constructed as the metric completion of the rationals (with the euclidean metric).

Both the Dedekind and the Cauchy reals have constructive definitions. Here is a Coq formalization of dedekind reals and I see you already found the Cauchy reals in Coq.

The Dedekind reals require impredicativity to work well (although the HoTT book has some workarounds).

The Cauchy reals require the axiom of countable choice to work as expected. Alternatively, we can use setoids and avoid quotienting the Cauchy sequences, which is what Coq does.

Every Cauchy reals can be converted to a Dedekind real. For the reverse conversion we need countable choice again.