The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Thu, 27 Nov 2003, Thery Laurent wrote:

>
> Hi,
>

Salut Laurent!

> A pity there is not in these three choices the usual representation
> of rational number as a pair of irreducible numerator/denominator.
>

You're right, I forgot this fourth representation with logical
annotations. Shame on me.

>
> This representation seems perfect. It is canonical and
> relatively efficient.
>

The only drawback is the obligation of carrying the logical statements.
That may become quite painful in some case.


> I've only one doubt, since there is only one proof of equality,
> it should be possible to prove
>
> (t1,t2:Z) (b1,b2:positive) (H1:(Zgcd t1 (POS b1))) (H2: (Zgcd t2 (POS b2))
>   t1 = t2 -> b1 = b2 -> (mkRat t1 b1 H1) = (mkRat t2 b2 H2).
>
> Is this true in Coq?

That sounds to me like proof irrelevance ... which is not there by
default. So you end with sereral representation of 1/2, after all, unless
you add a logical axiom.

>
> Second remark, why do we need the rationals when we already have
> the reals :-)
>

... for people who dislike *axiomatized* reals. A typical example is the
building of constructive reals via Cauchy sequence, like in FTA/C-CoRN or
in a small work I was doing with H. Schwichtenberg. More generally, coq
reals aren't well suited for computation and in particular extraction.

Pierre Letouzey