14
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ I am not an expert on Coq reals, but checking the library definitions it seems that the properties of the reals R that you obtain when you do Require Import Reals rely on the limited principle of omniscience, an non-constructive principle. You can see this by typing Print Assumptions R1. So there is no hope to compute with these in general, and they even made the definitions opaque to reflect this. $\endgroup$
    – Loïc
    Feb 11, 2022 at 13:15
  • $\begingroup$ As for Dedekind vs Cauchy reals, both can be defined constructively, but they will lack some properties of classical reals -- for instance, < is not constructively anti-symmetric on either of them. Moreover, the two sets are not constructively isomorphic (as they differ in some models, such as sheaf toposes). $\endgroup$
    – Loïc
    Feb 11, 2022 at 13:20
  • 1
    $\begingroup$ $<$ is antisymmetric! This is a favorite trick question of mine which I asked students in exams. $\endgroup$ Mar 15, 2022 at 20:46
  • 2
    $\begingroup$ Surely, you both meant . $\endgroup$ Mar 15, 2022 at 23:37
  • 1
    $\begingroup$ I'm not sure Andrej did ;-) $\endgroup$ Mar 22, 2022 at 22:30

1 Answer 1

5
$\begingroup$

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.

$\endgroup$
3
  • 2
    $\begingroup$ In recent versions of Coq, reals are defined through an abstract interface and at least two implementations are provided, one based on Cauchy reals and one based on Dedekind cuts. This allows implementing the exported API via some mix of both, relying on classical logic, but you can also just use the constructive flavour. $\endgroup$ Mar 15, 2022 at 21:45
  • 1
    $\begingroup$ Excellent! I should remember to look at the standard library every decade, to see what's new. $\endgroup$ Mar 16, 2022 at 13:44
  • 1
    $\begingroup$ Wait, what?! The standard library contains stuff inspired by my formalization of Dedekind reals (which other people helped complete)? Why didn't anyone tell me? I am honored :-) $\endgroup$ Mar 16, 2022 at 13:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.