The Coq mailing list

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

Hi Ian,

Dominique: My initial thought was to first ask the community to see if this work had been done before, and if not then try to find a solution myself. But well, I don't think I can blame you for giving the solution straight away! 🙂 Thanks a lot for that, it is exactly what I was looking for.

Happy to help !! Lexicographic products are all over the place in the kind of work I

do so I was just remembering earlier work.

Actually, with the accumulated experience in different Coq projects, I have come

to the conclusion that choosing/writing/tailoring induction principles is a critical

activity to get clean and understandable Coq proofs.

Always pickup the most adequate induction principle for the proof you are considering.

For instance, if you do an induction on trees and apply the induction hypothesis to strict

sub-trees only (but not necessarily direct sub-trees), then write the corresponding induction

principle instead of doing an induction on the height or size of trees. Otherwise the proof

in which you use the induction is decorated with boring and distracting sub-proofs repeating

that sub-trees have lesser height.

So when I saw you searching for a specific inductive scheme, it somehow ring​ed a bell.

Best,

Dominique