The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

On Thu, 27 Nov 2003, Venanzio Capretta wrote:

> The real point in which a canonical representation of some set is better
> than a setoid representation is that equality becomes convertibility.
> That means that we can substitute equal objects in any context. You want
> that (mkRat t1 b1 H1) is convertible with (mkRat t2 b2 H2) if t1 is
> convertible with t2 and b1 with b2. This is not in general true even if
> you have unicity of equality proofs.

This is a really interesting point.  Let me see if I undersand.  In
the context

t : Z
b : POS
H1,H2 : `(Zgcd top (POS bottom))=1`

We can prove that (mkRat t b H1)=(mkRat t b H2), but we they are not
convertable since H1 and H2 are not convertable.

But still, it seems better than using a Setoid, because you can at least
use eq_rec_r to replace any instance of (mkRat t b H1) with
(mkRat t b H2).  If we were using Setoids, wouldn't we have to show that
every intermeditate function is a Morphism?

In otherwords using this structure only requires a constant size increase
in the length of a proof, while using a Setoid would require increasing
the proof size proportional to the number if function we need to prove are
Morphisms.  I don't use Setoids much, so I may be in error.

-- 
Russell O'Connor                <http://math.berkeley.edu/~roconnor/>
                Work to ensure that Iraq is run by Iraqis.