The Coq mailing list

[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, so that it would make
the automatic generation moot. This means we also need to enhance the
tactic-world...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature