[Coq-Club] Adding strong induction to the standard library

[Tej Chajed]

The standard library does not include strong induction. Could it be added? A proposed addition is at https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v. Comments welcome, including nitpicks on the comments and pull requests.

Thanks!
Tej

[Robbert Krebbers]

If you import Wf_nat you can make use of well-foundedness of <, i.e.:

(* Performs strong induction on n, the IH is called IH *)
induction (lt_wf n) as [n _ IH].

Post by Tej Chajed
The standard library does not include strong induction. Could it be
added? A proposed addition is
at _https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v_.
Comments welcome, including nitpicks on the comments and pull requests.
Thanks!
Tej

[Dominique Larchey-Wendling]

Post by Tej Chajed
The standard library does not include strong induction. Could it be
added? A proposed addition is
at _https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v_.
Comments welcome, including nitpicks on the comments and pull requests.
Thanks!
Tej

It is already included ...

Require Import Arith Wf.

Proof.
...
induction n as [ n IHn ] using (well_founded_induction lt_wf).
...
Qed.

Dominique

[Tej Chajed]

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]).

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.

Post by Dominique Larchey-Wendling

Post by Tej Chajed
The standard library does not include strong induction. Could it be
added? A proposed addition is
at _https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v_.
Comments welcome, including nitpicks on the comments and pull requests.
Thanks!
Tej

It is already included ...
Require Import Arith Wf.
Proof.
...
induction n as [ n IHn ] using (well_founded_induction lt_wf).
...
Qed.
Dominique

[Dominique Larchey-Wendling]

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