The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

On 10/06/2016 05:24 PM, Abhishek Anand wrote:

> I suspect that this pattern is encouraged by the good
> induction-principle generation (Scheme command) for mutual inductives
> and the lack thereof for nested inductives.
> This creates unnecessary duplication of combinators on lists and their
> proofs. Personally, I find this duplication very unfortunate.

Precisely. With trees as *actual* list of trees, you can use the whole
List library to manipulate those instead of duplicating the whole
List library for that specific case.

This is why I did learn and come to love writing induction principles
of my own.

But of course this might not be readily accessible for
beginners. However, I do consider that writing good (which means
tailored for the proofs you want to implement) induction principles
is a key ingredient to simplify proofs.