Discussion:
Adding strong induction to the standard library
(too old to reply)
Tej Chajed
2016-12-05 15:30:55 UTC
Permalink
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
2016-12-05 15:36:49 UTC
Permalink
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
2016-12-05 15:39:51 UTC
Permalink
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
2016-12-05 15:48:38 UTC
Permalink
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
2016-12-05 16:41:24 UTC
Permalink
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

Continue reading on narkive:
Loading...