The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2016-10-07 0:33 GMT+02:00 Pierre-Marie Pédrot 
<pierre-marie.pedrot AT inria.fr>:
> On 06/10/2016 18:18, Pierre-Marie Pédrot wrote:
>> You're actually right. I'll have a look to check if that is easy to
>> generate the proper induction this way.
>
> To answer myself: I've reread the strict positivity conditions, and it
> seems it is somehow straightforward to derive systematically an
> induction principle for nested inductive types, even when they feature
> complicated features (all effectively too tricky cases are ruled out by
> positivity).
>
> The idea is simply to add a new toplevel predicate for each instance of
> a nested call in the constructors, which takes the context of the
> instance as argument, and fiddle a bit with that.
>
> Nonetheless, I'm wondering about the use of such a principle. Indeed, if
> the final goal is that newcomers don't keep asking about the evergreen
> inline fixpoint trick, then this is useless. Actually, the 'induction'
> tactic cannot cope with such a complicated scheme

Can you give an example please? Is it really more complex that what
mutual can give?

P.