The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

On 4 Sep 2008, at 15:02, Paul Brauner wrote:

> My question is : is the dual lemma provable ?
>
> > Lemma cnat_to_nat_to_cnat :
> >  forall cn:cnat, (nat_to_cnat (cnat_to_nat cn)) = cn).
>
> It seems like it is not, but do you know why ?

You need parametricity to prove this, e.g. see
http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=83

I don't know any decent presentation of parametricity for the calculus  
of constructions.

Why not? Not sure, in Coq you cannot prove anything *interesting*  
about an inhabitant of a polymorphic type, e.g. you cannot prove that

forall f : (forall X:Set,X -> X) , f = fun X x => x.

for an impredicative Set.

This is similar to the fact that you cannot prove anything  
*interesting* about functions. I guess, it should be possible to give  
an interpretation where every polymorphic type contains some garbage,  
and hence the alleged theorems don't hold.

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.