The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On Fri, 28 Nov 2003 09:33:21 -0500
Venanzio Capretta 
<Venanzio.Capretta AT mathstat.uottawa.ca>
 wrote:

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

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

Actually the convertibility is **defined** by the translation (phi)
and the convertibility in CCI:

t1  =_conv t2  iff phi(t1) =_cci phi(t2),

so it is true by construction. The important property is then the
compatibility between conversion and reduction: conversion must
contain at least the congruence relation generated by the
reduction. In this case, conversion contains more that just this
congruence since [t1]_nf and [t2]_nf may be different in normal form
but convertible, like for exemple [0]_nf and [2]_nf in the quotient
Z/2Z.


> Question for Pierre: did you implement some tactics in Coq for
> normalized types.

Actually no, for two important reasons:

- it is necessary to modify the kernel of coq to add a new kind of term
(basically as Venanzio says: a special one constructor inductive type),
then change the reduction and more important the conversion. 

So it could take some time, and it won't be coq anymore, but that would
have not stop me, but:

-I discussed more recently with Benjamin Werner who is working on a
calculus in which proof irrelevance is hard-coded in the conversion (all
term of a type T:Prop are convertible). In such a calculus, normalized
types are extremly naturally defined by an existential type. I paste here a
translated mail of him:

A,Supp:Set

nf : Supp -> A   (* A can be Supp but not necessary *)

(* normalized type: the set of canonical elts, here you describe how to
find the irreducible fraction *)

Norm := {x:A | (EX y : Supp | x=(nf y)) }.

class : Supp -> Norm 
      := [y:Supp](exist ? ? (nf y)  (ex_intro ? ? y (refl_equal ? (nf y))))


Then because of the real proof-irrelevance, this would be provable
(with leibnitz equality):

(a,b:Supp)(class a)=(class b) <-> (nf a)=(nf b)

In other words:  (class x) and (class y) would compute in (nf x, H) and
(nf y, H') which are convertible if (nf x) and (nf y) are.

So I am waiting for a hard-coded PI in Coq rather than hard-coding
normalized types in Coq.




> So this seems to bring us back to the original problem of
> non-sobstitutivity of equal elements.

If the conversion is defined the way I explained above, then the problem
disappears, and it also disappears if PI is hard-coded.

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

That is what I have done in my thesis (which is in french), I don't
remember well the paper.

Cheers,

Pierre