The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

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

This is given only as an example in the documentation of the record

Record Rat : Set := mkRat {
  sign     : bool;
  top      : nat;
  bottom   : nat;
  Rat_bottom_cond : ~O=bottom;
  Rat_irred_cond:(x,y,z:nat)(mult x y)=top/\(mult x z)=bottom->x=(S O)
}.

Rewriting it using ZArith it should look something like

Record Rat : Set = mkRat {
  top : Z;
  bottom : positive;
  Rat_irred_cond: (Zgcd top (POS bottom)) = 1
}.

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

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?

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

--

Laurent Thery