The Coq mailing list

[Bruno Barras <barras AT lix.polytechnique.fr>]

Thery Laurent wrote:

> 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?
Yes, because equality over Z is decidable (this is also provable in 
classical logic, see lemma eq_proofs_unicity):

Require Eqdep_dec.
Open Scope Z_scope.
Lemma eq_rat_intro:
(t1,t2:Z) (b1,b2:positive)
(H1:(Zgcd t1 (POS b1))==1) (H2: (Zgcd t2 (POS b2))==1)
t1 = t2 -> b1 = b2 -> (mkRat t1 b1 H1) = (mkRat t2 b2 H2).
Intros.
Subst t1 b1.
Rewrite -> [H](eq_proofs_unicity H H1 H2).
Trivial.

Intros x y.
Elim (Z_eq_dec x y); Intros H.
Subst x; Auto.

Right; Intro b.
Apply H.
Elim b; Trivial.
Save.

--
Bruno Barras