The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

1. For (mostly) historical reasons we have three implementations of
real numbers:
IR (ascii art for blackboard R)
CR computable reals numbers in the directory reals/fast
Variants of AR, Reals based on the Approximate rationals.
e.g. Dyadics form an example of approximate rationals:
https://github.com/c-corn/corn/blob/master/reals/faster/ARbigD.v
These are the most modern, e.g. use type classes, and compute the fastest.
http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

2. Yes, by clever use of isomorphisms, you can actually compute with
Coq's axiomatic reals using corn.
http://jfr.cib.unibo.it/article/view/1411/932
Unfortunately, you still have to use CR for this. It is not been
(completely) ported to AR.

I think the paper above gives you the other information you are looking for.

On Fri, Dec 5, 2014 at 5:10 PM, CHAUVIN Barnabe
<barnabe.chauvin AT gmail.com>
 wrote:
> Hello club !
>
> Playing with the CoRN library, I have a few questions about how Reals work :
>  - I understood the structures from CSetoid to CReals, but I don't really
> understand the difference between IR and CR ? I know CR stand for
> Computational reals, but what does IR means ?
>  - What is exactly the aim of the RasIR and IRasR definitions ? Do they
> allow computation of coq reals (for example 4%R + 3%R ? )
>  - When to use CR or IR or R in a proof ? (And why rather this one). Of
> course, I guess it depends on the circumstances ..
>  - Let's assume I have a subgoal  2<3  (the type of the number depends on my
> previous question, but they are reals numbers), what is the best way to
> solve it ? Use CoRN computation (I'm talking of a simple inequality or
> equality) ?
>
> Thanks for your attention !
> These questions might seem weird or even destructured, but I'm a complete
> beginner ..
>
> Best regards.