The goal of this chapter is to generalize 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 is not
Instead, we wish for this induction step to be:
forall k : nat,
P (k - (k - 0)) ->
P (k - (k - 1)) ->
P (k - (k - 2)) ->
... ->
P (k - 2) ->
P (k - 1) ->
P (k - 0) ->
P (k + 1)
Or again, stated more simply:
forall k : nat, P 0 -> P 1 -> P 2 -> ... -> P k -> P (k + 1)
In other words, for any k, we wish to have k+1 induction hypotheses to prove P(k+1).
To be able to construct these k+1 induction hypotheses inductively, we uncurry the induction step k times:
forall k : nat, P 0 /\ P 1 /\ P 2 /\ ... /\ P k -> P (k + 1)
In tCPA, conjunction associates to the right, and so to facilitate the access to P k while maintining readability, we swap the order of the induction hypotheses. All told, the induction step reads:
forall k : nat, P k /\ ... /\ P 2 /\ P 1 /\ P 0 -> P (k + 1)
In this generalized induction principle, the number of induction hypotheses is maximized (unlike, e.g., in nat_ind1 where this number is fixed to be 1, in nat_ind2 where this number is fixed to be 2, etc.) and represented as a conjunction.
This induction principle where the induction step features a conjunction of all the possible induction hypotheses is known as “course-of-values induction”.
As a first-order induction principle, mathematical induction involves one induction hypothesis: To conclude about P (S n'), we need P n'. As a second-order induction principle, nat_ind2 involves two induction hypotheses: To conclude about P (S (S n')), we need P (S n') and P n'. As a third-order induction principle, nat_ind3 involves three induction hypotheses: To conclude about P (S (S (S n'))), we need P (S (S n')), P (S n'), and P n'. In the course-of-values induction principle, all the possible induction hypotheses are involved: To conclude about P (S n'), we need P n', ..., P 1, and P 0. Let us program this conjunction:
Fixpoint conjunction_upto (n : nat) (P : nat -> Prop) : Prop :=
match n with
| 0 =>
P 0
| S n' =>
P (S n') /\ conjunction_upto n' P
end.
To crystallize, here is a sketchy characterization:
Property sketchy_characterization_of_conjunction_upto :
forall P : nat -> Prop,
(conjunction_upto 0 P = (P 0))
/\
(conjunction_upto 1 P = (P 1 /\ P 0))
/\
(conjunction_upto 2 P = (P 2 /\ P 1 /\ P 0))
/\
(conjunction_upto 3 P = (P 3 /\ P 2 /\ P 1 /\ P 0)).
The rest of this chapter makes uses of the following lemmas.
If the conjunction of a property holds from 0 to n, this property holds at n:
Lemma conjunction_upto_a_number_implies_the_property_at_this_number :
forall (n : nat)
(P : nat -> Prop),
conjunction_upto n P ->
P n.
If the conjunction of a property holds from 0 to n, this property holds at 0:
Lemma conjunction_upto_a_number_implies_the_property_at_O :
forall (n : nat)
(P : nat -> Prop),
conjunction_upto n P ->
P 0.
If the conjunction of a property holds from 0 to k1 + k2, this conjunction holds from 0 to k2:
Lemma conjunction_upto_an_addition_implies_conjunction_upto_the_addend :
forall (k1 k2 : nat)
(P : nat -> Prop),
conjunction_upto (k1 + k2) P ->
conjunction_upto k2 P.
The course-of-values induction principle has two premises – a base case and an induction step with all the possible induction hypotheses:
Lemma nat_ind_course_of_values :
forall P : nat -> Prop,
P 0 ->
(forall n' : nat,
conjunction_upto n' P -> P (S n')) ->
forall n : nat,
P n.
The proof is by cases on n – which is either O or S n' – and then by induction on n'. (See the accompanying .v file.)
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 course-of-values induction:
Lemma nat_ind1_using_course_of_values_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 course-of-values induction principle and focus on the base case:
intros P P_0 P_S n.
induction n as [ | n' IHn'] using nat_ind_course_of_values.
-
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' : conjunction_upto n' (fun n : nat => P n)
============================
P (S n')
Alfrothul: Lucky us, instantiating P_S to n' gives us an implication that implies the goal:
- Check (P_S n').
Pablito: The *response* window reads:
P_S n'
: P n' -> P (S n')
Bong-sun: Hmmm. If the conjunction of a property holds from 0 to n’, doesn’t this property holds at n’? Let me see:
Check (conjunction_upto_a_number_implies_the_property_at_this_number n' P IHn').
Pablito: The *response* window reads:
conjunction_upto_a_number_implies_the_property_at_this_number n' P IHn'
: P n'
Anton: Right. We are done here:
exact (P_S n' (conjunction_upto_a_number_implies_the_property_at_this_number n' P IHn')).
Halcyon: Indeed we are.
Dana: I see that the accompanying .v file contain an alternative proof that further distinguishes between O and S ... in the induction step.
Alfrothul: Right. And then it bypasses Lemma conjunction_upto_a_number_implies_the_property_at_this_number.
Halcyon: It’s an alternative.
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 course-of-values induction:
Lemma nat_ind2_using_course_of_values_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 course-of-values induction:
Lemma nat_ind2_0_using_course_of_values_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 course-of-values induction:
Lemma nat_ind2_1_using_course_of_values_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 course-of-values induction:
Lemma nat_ind3_using_course_of_values_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 course-of-values induction:
Lemma nat_ind4_using_course_of_values_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 course-of-values 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_course_of_values_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 course-of-values 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 course-of-values induction:
Property threes_and_fives_using_course_of_value_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 course-of-values induction:
Property fours_and_fives_using_course_of_value_induction :
forall n : nat,
exists a b : nat,
12 + n = 4 * a + 5 * b.
Completed [02 Jul 2025]
Factored out from a previous chapter about course-of-values induction and strong induction [28 May 2025]