The goal of this chapter is to present another generalization of the higher-order induction principles from Chapter Induction principles: from first-order to higher-order induction to an induction principle over Peano numbers where the induction step does not use k explicit conjunctions as in course-of-values induction (nat_ind_course_of_values):
forall k : nat, P k /\ ... /\ P 2 /\ P 1 /\ P 0 -> P (S k)
Instead, we wish for this induction step to quantify the index of the k+1 conjuncts and to be:
forall k : nat, (forall i : nat, i <= k -> P i) -> P (S k)
In words, to conclude about P (S k), P i should hold for any i that is smaller than or equal to k.
This induction principle where the induction step quantifies over all the possible induction hypotheses is known as “strong induction”.
Let us first prove that the induction step for course-of-value induction and the induction step for strong induction are equivalent:
Fixpoint conjunction_upto (m : nat) (P : nat -> Prop) : Prop :=
match m with
| 0 =>
P 0
| S m' =>
P (S m') /\ conjunction_upto m' P
end.
Theorem the_same_dame :
forall P : nat -> Prop,
(forall m : nat,
(forall i : nat,
i <= m -> P i) ->
P (S m))
<->
(forall m : nat,
conjunction_upto m P -> P (S m)).
Mugsy: She’s the same dame!Preston Sturges (nonchalant): That’s what the theorem says.Mimer: Mr. Sturges! Thanks for passing by!
The strong-induction principle has two premises – a base case and an induction step that quantifies over the possible induction hypotheses:
Lemma nat_ind_strong :
forall P : nat -> Prop,
P 0 ->
(forall n' : nat,
(forall i : nat,
i <= n' -> P i) ->
P (S n')) ->
forall n : nat,
P n.
The proof is by course-of-value induction, using the equivalence between the two induction steps:
Proof.
intros P P_O P_S.
destruct (the_same_dame P) as [strong_implies_course_of_values _].
exact (nat_ind_course_of_values P P_O (strong_implies_course_of_values P_S)).
Qed.
Re-prove Lemma nat_ind_course_of_values by strong induction:
Lemma nat_ind_course_of_values_using_nat_strong :
forall P : nat -> Prop,
P 0 ->
(forall n' : nat,
conjunction_upto n' P -> P (S n')) ->
forall n : nat,
P n.
As a followup of the section about first-order mathematical induction in Chapter Induction principles: from first-order to higher-order induction, prove nat_ind1 using strong induction:
Lemma nat_ind1_using_strong_induction :
forall P : nat -> Prop,
P 0 ->
(forall n' : nat,
P n' ->
P (S n')) ->
forall n : nat,
P n.
Bong-sun: So let’s use the strong induction principle and focus on the base case:
intros P P_0 P_S n.
induction n as [ | n' IHn'] using nat_ind_strong.
-
Pablito (helpful): The *goals* window reads:
P : nat -> Prop
P_0 : P 0
P_S : forall n' : nat, P n' -> P (S n')
============================
P 0
Anton: Lucky us, the base case lies among the assumptions, so we can focus on the induction step:
- exact P_0.
-
Pablito: The *goals* window reads:
P : nat -> Prop
P_0 : P 0
P_S : forall n' : nat, P n' -> P (S n')
n' : nat
IHn' : forall i : nat, i <= n' -> P i
============================
P (S n')
Dana: The less-than-or-equal-to predicate is reflexive:
- Check (Nat.le_refl n').
Pablito: The *response* window reads:
Nat.le_refl n'
: n' <= n'
Alfrothul: So we can apply the induction hypothesis:
Check (IHn' n' (Nat.le_refl n')).
Pablito: The *response* window reads:
IHn' n' (Nat.le_refl n')
: P n'
Anton: Right. We are done here:
exact (P_S n' (IHn' n' (Nat.le_refl n'))).
Halcyon: Indeed we are.
As a followup of the section about second-order mathematical induction in Chapter Induction principles: from first-order to higher-order induction, prove nat_ind2 using strong induction:
Lemma nat_ind2_using_strong_induction :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n' : nat,
P n' ->
P (S n') ->
P (S (S n'))) ->
forall n : nat,
P n.
Prove nat_ind2_0 (i.e., second-order mathematical induction that only uses its first induction hypothesis) using strong induction:
Lemma nat_ind2_0_using_strong_induction :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n' : nat,
P n' ->
P (S (S n'))) ->
forall n : nat,
P n.
Prove nat_ind2_1 (i.e., second-order mathematical induction that only uses its second induction hypothesis) using strong induction:
Lemma nat_ind2_1_using_strong_induction :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n' : nat,
P (S n') ->
P (S (S n'))) ->
forall n : nat,
P n.
See the accompanying .v file.
As a followup of the section about third-order mathematical induction in Chapter Induction principles: from first-order to higher-order induction, prove nat_ind3 and its variants using strong induction:
Lemma nat_ind3_using_strong_induction :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P n' ->
P (S n') ->
P (S (S n')) ->
P (S (S (S n')))) ->
forall n : nat,
P n.
As a followup of the exercise about fourth-order mathematical induction in Chapter Induction principles: from first-order to higher-order induction, prove nat_ind4 using strong induction:
Lemma nat_ind4_using_strong_induction :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
P 3 ->
(forall n' : nat,
P n' ->
P (S n') ->
P (S (S n')) ->
P (S (S (S n'))) ->
P (S (S (S (S n'))))) ->
forall n : nat,
P n.
As a followup of the section about the evenness predicate in Chapter Induction principles: from first-order to higher-order induction, prove the soundness and completeness of evenp2 using strong induction:
Fixpoint evenp2 (n : nat) : bool :=
match n with
O =>
true
| S n' =>
match n' with
O =>
false
| S n'' =>
evenp2 n''
end
end.
Theorem soundness_and_completeness_of_evenp2_using_strong_induction :
forall n : nat,
evenp2 n = true <-> exists m : nat, n = 2 * m.
The accompanying .v file contains the skeleton of a proof for this theorem.
As a followup of the exercise about the ternary predicate in Chapter Induction principles: from first-order to higher-order induction, revisit the soundness and completeness of ternaryp using strong induction.
As a followup of Exercise 09 and Exercise 10 in Chapter Induction principles: from first-order to higher-order induction, revisit Property threes_and_fives using strong induction:
Property threes_and_fives_using_strong_induction :
forall n : nat,
exists a b : nat,
8 + n = 3 * a + 5 * b.
As a followup of Exercise 12 and Exercise 13 in Chapter Induction principles: from first-order to higher-order induction, revisit Property fours_and_fives using strong induction:
Property fours_and_fives_using_strong_induction :
forall n : nat,
exists a b : nat,
12 + n = 4 * a + 5 * b.
Completed [08 Jul 2025]
Factored out from a previous chapter about course-of-values induction and strong induction [28 May 2025]