The Coq mailing list

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

Some time ago, I had to manipulate rational numbers (Q) in Coq. There are
currently three possibilities (at least):

1) in Nijmegen/FTA, there is a file that proposes to take
 Q := {num:Z;den:positive}. The immediate drawback of this representation
 is that the equality over this Q can't be the usual one of Coq, but must
 be a Setoid equality.

2) in Rocq/RATIONAL, Samuel Boutin defined Q as a quotient type.
Unfortunately, part of this development is axiomatized, and that doesn't
fit well with my goal of extracting Q arithmetic in ocaml.

3) more recently in Nijmegen/QArith, Milad Niqui and Yves Bertot
investigate a canonical representation of fractions. But it seems to me
that operations like plus or mult are inefficient, since they proceed via
decoding to nat, adding or multiplying in nat and recoding the result.
Milad, Yves, am I wrong ?

Since (relatively) efficient extraction was my primary goal, I sticked to
the first choice, that is Q as Setoid. The good news is that now Coq comes
with some tools able to deal with Setoid Equality, thanks to Clement
Renard. So my proposition of QArith takes advantage of Setoid Rewrite and
Setoid Ring. I hope that some day in the future a Setoid Field and Setoid
Fourier will also be available.

At first I was thinking this new QArith could quickly become part of Coq
Standard Library, like ZArith. But these files are definitively not mature
enough, and anyway proceeding this way would be fairly un-democratic ;)
So I've finally placed my files as a new user contribution Orsay/QArith,
to open the discussion and to ask for help improving this small QArith.


Pierre Letouzey



PS: Until the next Coq release, the files of this contribution can only
be retreived via Coq anonymous CVS. To get them, you just have to run the
2 following commands:
_________________________________________________________________________________
cvs -d 
:pserver:anoncvs AT coqcvs.inria.fr:/coq
 login
 <just press enter as passwd>
cvs -z3 -d 
:pserver:anoncvs AT coqcvs.inria.fr:/coq
 checkout contrib/Orsay/QArith
________________________________________________________________________________

To compile, you need a recent CVS version of Coq (not older than 2003/11/19).
More informations can be found in the README.