The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

On 5/12/14 5:10 PM, CHAUVIN Barnabe 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.

I hope that specialists of CCorn will answer to your questions, but 
while waiting, here are a few hints.

1- real numbers are hard to compute with.  Of course, you think that 
there should be no problem computing 4%R + 3%R, but what about computing 
PI + cos 1, what does it mean to compute it?  In some sense, computing a 
number only means "find a more natural way to express the same number".  
So 7%R is a more natural way to represent 4%R + 3%R, but I am afraid 
that deciding what is the most natural way to express (PI + cos 1) is 
rather subjective...

Now, another point of view around real numbers, is that they can be 
computed up to some precision: this is the "Cauchy" point of view: you 
give me a precision, I give you a value within that precision (in fact 
Cauchy is more about sequences of values, but in my mind the spirit is 
the same).

The value that I give can be taken in another type, where computation 
has a more "concrete" meaning, like rational numbers.

With this approach, it is easy to show that 3 < PI (by taking a 
sufficiently close approximation of PI), but there is no general 
algorithm that takes two real numbers a and b as arguments and returns 
true exactly when a < b.  Because, when a and b are the same (but I 
don't know it), every question I ask will return approximations of a and 
b that are very close to each other, but these approximations never give 
enough information to conclude that a < b is indeed not satisfied.  For 
instance, let's call v1 the first positive value where the sine function 
vanishes and let's call v2 the number (4 * (1 - 1/3 + 1/5 + ...)).  We 
know mathematically that v1 and v2 are the same.  Algorithmically, we 
can compute arbitrarily close approximations of these two values showing
that they must be very close to each other, but we will never have, just 
by computation, a certitude that one cannot be higher than the other (we 
will always conclude that we need more precision).

Note that, for rational numbers, there exists an algorithm that takes 
two rational numbers a and b as arguments and returns true exactly when 
a < b.  So the type of real numbers is, in a sense, a weaker type than 
the type of rational numbers.

Yves