The Coq mailing list

[Milad Niqui <milad AT cs.kun.nl>]

Thery Laurent wrote:
> 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):

Here is a proof:

Require Eqdep_dec.
Require ZArith.

Variable Zgcd:Z->Z->Z.

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

Definition Z_dec_Prop:=[x,y:Z]
 Cases (Z_eq_dec x y) of
   (left H) => (or_introl `x = y` `x <> y` H)
 | (right H) => (or_intror `x = y` `x <> y` H)
 end:(x,y:Z)x=y\/x<>y.

Lemma foo:(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).
Proof.
 Intros.
 Generalize H2.
 Rewrite <- H.
 Rewrite <- H0.
 Intro H3.
 Rewrite (eq_proofs_unicity Z_dec_Prop H1 H3).
 Reflexivity.
Defined.

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

Our canonical representation is essentialy like your original mkRat, we
 directly encode the unique proof of equlity (Zgcd m n)=1. So you can
consider our representation to be:

m/n -> (Zgcd m n)

Whether your method will be more efficient than ours depends on the
effieceincy of your gcd algorithm. We code the Euclid's algorithm for
gcd but without using division. It is also possible to encode the binary
gcd algorithm, but it  dosen't give a canonical representation. However
I think one can devise lazy algorithms to do more efficient computation
on this redundant representation.

Whatever representation you choose for rational numbers, if you want to
normalise the results of computations (in the sense of getting it to a
reduced fraction) you at least get the complexity of the gcd algorithm.

I guess at the end the best way to choose is to try all these suggested
rational packages on some expressions, and pick the fastest one.

> 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


Question: Isn't a result similar to eq_proofs_unicity in general true 
for any inductive type in Prop that has only one constructor (like Acc)?

> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
> .


--
Milad Niqui

Computing Science Department,                tel:+31 24 365 2631
University of Nijmegen,                      fax:+31 24 365 2525
P.O.B. 9010,                                 email: 
milad AT cs.kun.nl
6500 GL Nijmegen,                            http://www.cs.kun.nl/~milad
The Netherlands.
==============================================================================================
The University of Nijmegen will be named Radboud University Nijmegen as 
of September 1st, 2004