The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Russell O'Connor wrote:

> > > (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?
> > >      
> > That sounds to me like proof irrelevance ... which is not there by
> > default. So you end with sereral representation of 1/2, after all, unless
> > you add a logical axiom.
> >    
>
> I think it will be provable even without logical axioms.  I beleive that
> is is a consquence of K_dec_set.
>
> In general unique equality isn't provable, but when it is equality over a
> decidable type (like Z) then it is.  Of course the real way to know this
> is to prove it.  Which I'll do later if no one else here gets to it first.
>
>  
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.
If  you have to prove H1=H2, then it is not better that using a setoid.

A different (better?) solution consists in using a normalized type
(Pierre Courtieu, Normalized Types, CSL 2001). This is a type with an
explicit canonical form function. Here are the rules for it (I simplify
them a bit, see Pierre's article for the exact ones):

Formation:
A:Set   nf:A->A
---------------------
A_nf:Set

Introduction
a:A
---------------
[a]_nf:A_nf

Elimination
g:A->C
-------------------------
elim_nf(g):A_nf->C

(So far just a trivial record with one field)

Reduction:
elim_nf(g,[a]_nf) ~> g(nf(a))

so the normalization function is automatically applied during reduction.

Pierre proved that the addition of this kind of types in CIC has all the
usual nice properties. Actually, he gave a reduction preserving translation.
Question for Pierre: did you implement some tactics in Coq for
normalized types.

We can define Q as (ZxPos)_nf were nf give the irreducible form of a
fraction.

There is only one problem remaining: conversion is not the congruence
relation generated by reduction anymore, but needs an extra
interpretation function to state that two elements of A_nf are
convertible if they have the same nf.
I don't find in the article a result stating that conversion is
preserved when translating in CIC.
So this seems to bring us back to the original problem of
non-sobstitutivity of equal elements.
But is it possible to restore conversion=(congruence generated by
reduction) by changing the introduction rule to:
  a:A
---------------------
[(nf a)]_nf:A_nf
? (Second question for Pierre)

-- Venanzio