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.