The Coq mailing list

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

On Thu, 27 Nov 2003, Bruno Barras wrote:


> >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):

If I understand well what the lemma eq_proofs_unicity says:

1)
If I want to define a subtype {x: A | (P a)} where P is decidable

P_dec: (a:A) {(P a)} + {~(P a)}

I'd better define it as {x: A | (Case (P_dec a) true false) = true} like 
this I get proof irrelevance

2) 
If I have a relation R on a set A such that equality is decidable

eqA_dec:(a:A)(b:A) {a=b}+{~(a=b)}

and R is such that I can build a function cano that returns me a canonical
element

(a,b:A) (R a (cano a)) /\ ((R a b) <-> (cano a) = (cano b))


{x: A | (Case (eqA_dec a (cano A)) true false) = true} gives a nice way to
build the quotient A/R.

Am I right?

If 1) and 2) are true this means that we could get the canonical
representation of the rational simply by taking the quotient of the 
Nijmegen
contribution with cano:

 m/p  -> (m/(Zgcd m n))/(n/(Zgcd m n))

But if efficency really matters maybe it would be better to start from 
scratch
since operations like multiplication can take benefit of the canonicity

a/b * c/d could be computed as 

((a/(gcd a d)) * (c/(gcd c b)))/ ((b/(gcd c  b)) * (d / (gcd a d)))


--
Laurent Thery