The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Another idea is to use a "default" fold/logical predicate on the inductive,

like Forall for lists, avoiding the new predicate. Why do you think induction

couldn't work with those eliminators though? You might need with (P0:=...)...

to specify the predicates for nested occurrences in your case but that's handled I think.

-- Matthieu

On Fri, Oct 7, 2016 at 1:45 AM Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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.