The Coq mailing list

[Micaela Mayero <mayero AT pauillac.inria.fr>]

Hi,

Sorry for this late answer.

> I have a question regarding the theory Reals from the standard library. I 
> would contact the author but I can't find out who it is, hence I send this 
> to 
> this list.

Some time ago, it was written in the CREDITS file but it seems this file has
changed (I don't know why?). Actually, I developped this library, which was
completed later by Olivier Desmettre.

> In the file Coq/Reals/Raxioms.v an injection is defined from nat to R, as 
> follows:
> 
> Fixpoint INR (n:nat) : R :=
>   match n with
>   | O => 0
>   | S O => 1
>   | S n => INR n + 1
>   end.  
> 
> It seems a bit strange to have a separate clause for S O - it can be proved 
> that a function inR, defined without this clause, is extensionally equal to 
> INR, and indeed "auto with real" cannot solve some subgoals that it /can/ 
> prove using inR.
> 
> So - is there a reason to define INR this way?

It is due to an historical reason (to use "simpl" in order to reduce (INR 1)
directly to 1, very useful in some cases).
I plan to clean this library significantly during this summer...

If it is a really a problem for you, as you said, for the moment, a simple
idea could be to define another INR, that you could use with an
extentionality lemma. This solution allows you to use all the properties of
INR after one step of rewriting.

Hope this helps,

Micaela.

----------------------------------------
Micaela.Mayero AT lipn.univ-paris13.fr
http://www-lipn.univ-paris13.fr/~mayero/