The Coq mailing list

[Cody Roux <Cody.Roux AT loria.fr>]

Parametrcity is indeed sufficient to prove this lemma. I do not
understand two things though:

- Is Bruno's comment on the theorem being a consequence of
extentionality relevant?

- It is not clear to me that all theorems for free are not provable in
the calculus of (inductive) constructions

thank you for your answers

Cody




On Fri, 2008-09-05 at 15:41 +0100, Thorsten Altenkirch wrote:
> 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.
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club