The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

Hi,

Actually, the two presentations are quite similar (and equivalent).  
The difference
being that I in-lined a possible definition of liftP. Abstracting  
liftP, as Stéphane did it,
indeed allows to avoid the fix tactic. On the other hand, one will  
want to specialize
his induction scheme for a particular liftP before using it (say, I  
would).

About using 'In' for liftP. I thought about it but wanted to avoid  
dealing with equalities
in the proof of the induction scheme. You can derive a variant with  
In easily. However
It is not obvious which version I would prefer. Maybye I am  
influenced by ssreflect so
I now replace constructors by reduction whereever possible :-)

Anyway, the good news is that we are now down to matters of taste :-)

Cheers,

Benjamin


Le 21 nov. 07 à 23:19, Thorsten Altenkirch a écrit :

> Hi Xavier,
>
> I wonder what you and Stephane mean by "most general" because it is  
> straightforward to deduce Stephane's induction principle from  
> Benjamin W's (just using induction over lists). I.e. once you  
> assume Stephane's assumptions it is easy to show
>
> forall lt:list ty,liftp P lt -> liftedP lt
>
> using induction over lists and then you use Benjamin's principle to  
> show forall t:ty,P t. Indeed the isomorphism between nested and  
> mutual inductive definition is usually referred to as "Bekic's  
> lemma" and it entails that the corresonding induction principles  
> are equivalent.
>
> > From this mutual induction principle, it is rather easy to prove more
> > specialized principles like the one Benjamin W. showed, with  
> > "liftp P"
> > as the property for "list ty" --- certainly easier than proving them
> > from scratch.
>
> Or vice versa. Benjamin's principle seems to be the more natural to  
> me, since it just generalizes the present scheme for deriving  
> induction principles to allow nested occurences of inductive types.
>
> 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.