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?
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.
Rthat you obtain when you do
Require Import Realsrely 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$
<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$