The Coq mailing list

[Jasper Stein <jasper AT cs.ru.nl>]

Dear Coq-club,

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.

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?

Groeten,
-- 
Jasper Stein