The Coq mailing list

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

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.