The Coq mailing list

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

Le 05/12/2016 à 16:48, Tej Chajed a écrit :
> I stand corrected, I didn’t realize strong induction was well-founded
> induction on lt (this is actually the first I’ve seen a reference to
> [well_founded induction lt_wf]).

Indeed you could have proved your strong_induction that way ...

Definition strong_induction := well_founded_induction lt_wf.

Notice you also have recursion principles (to build terms in Set/Type
instead of just prove formulas in Prop)

Check well_founded_induction_type.

and a fixpoint based on well-founded induction

Check Fix.

if you want to define terms with which you need to compute.

> In that case, it would be good to find a place in the documentation to
> mention this, such that searching for “strong induction coq” pulls this up.

A good place to start with is in the documentation of the
Standard Library module Wf.

https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Wf.html

Well founded induction is a really tremendous tool to prove
by induction in Coq. Do not hesitate to define lots of different
induction principles to suit your needs.

Best

Dominique