The goal of this chapter is to study induction principles.
Pablito: Induction principles as in one per inductive data type we define?
Halcyon: And boy do we define inductive data types here.
Bong-sun: Actually no. This chapter is solely dedicated to Peano numbers, i.e., nat.
Pablito: Well, we already have one induction principle for Peano numbers – structural induction over them.
Alfrothul: Also known as mathematical induction.
The fourth wall: And sometimes referred to as “weak”, to contrast it with the “strong” induction principle presented in a next chapter.
Pablito: OK, so there is at least two induction principles for nat – weak and strong induction – but you are saying there are more induction principles?
Dana: Yes. Stay tuned.
A sequence of numbers obeys a recurrence relation when combining successive elements in this sequence yields a subsequent element in this sequence.
For example, consider the sequence of natural numbers and the sequence of positive natural numbers:
0, 1, 2, 3, ...
1, 2, 3, 4, ...
Adding 1 to each element of these sequences yields the next element in each sequence. Adding 2 instead of 1 yields the sequence of even numbers if the sequence starts with 0 and the sequence of odd numbers if the sequence starts with 1. Adding 3 instead of 1 or 2 yields the sequence of ternary numbers if the sequence starts with 0, the sequence of post-ternary numbers if the sequence starts with 1, the sequence of pre-ternary numbers if the sequence starts with 2.
These recurrence relations are said to be first order because each element is enough to determine the next element in the sequence. Many other sequences obey a first-order recurrence relation, e.g., arithmetic sequences, geometric sequences, the sequence of factorial numbers, etc.
A recurrence relation is second order when two consecutive elements are enough to determine the next element in the sequence. For example, Fibonacci numbers obey a second-order recurrence relation.
Likewise, a recurrence relation is third order when three consecutive elements are enough to determine the next element in the sequence, it is fourth order when four consecutive elements are enough to determine the next element in the sequence, etc. For example, Fibonacci numbers have been generalized from second order to higher order in this fashion.
The goal of this chapter is to study the induction principles that correspond to these recurrence relations, from first order and onwards.
This section is about the induction principle that corresponds to first-order recurrences over Peano numbers.
Mathematical induction already exists in tCPA, as the structural-induction principle – nat_ind – associated with Peano numbers – nat. And indeed when prompted with Check nat_ind., tCPA issues the following signature in the *response* window:
nat_ind
: forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
We can also express this induction principle ourselves:
Lemma nat_ind1 :
forall P : nat -> Prop,
P 0 ->
(forall n' : nat,
P n' ->
P (S n')) ->
forall n : nat,
P n.
We can also prove nat_ind1 using the resident mathematical induction principle, either implicitly with the induction tactic or explicitly using nat_ind, as foreshadowed in Week 04.
Anton: Wait. We can prove an induction principle?
Alfrothul: Why not? It’s a lemma.
Anton: Er... OK. I guess.
Bong-sun: Let’s get started:
intros P P_O P_S n.
Pablito (helpful): The *goals* window reads:
P : nat -> Prop
P_O : P 0
P_S : forall n' : nat, P n' -> P (S n')
n : nat
============================
P n
Anton: And now what?
Pablito: Well, we were just told that we can prove nat_ind1 using the resident mathematical induction principle, so let’s use the induction tactic:
induction n as [ | n' IHn'].
Anton (surprised): Ah, the rest of the proof is routine:
- exact P_O.
- exact (P_S n' IHn').
Alfrothul: Congratulations, Anton, you just proved an induction principle.
Anton: Harrumph.
Bong-sun: The induction tactic invokes the induction principle associated with its argument.
Dana: Here, its argument is n, which has type nat, whose induction principle is nat_ind.
Alfrothul: We could invoke this induction principle ourselves, look:
Restart.
intros P P_O P_S n.
Check (nat_ind P).
Pablito (helpful): The *response* window reads:
nat_ind P
: P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
Bong-sun: nat_ind P should first be applied to an argument of type P 0, but luckily we have one among the assumptions:
Check (nat_ind P P_O).
Pablito: The *response* window reads:
nat_ind P P_O
: (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
Bong-sun: nat_ind P P_O should be applied to an argument of type forall n : nat, P n -> P (S n), but luckily we also have one among the assumptions:
Check (nat_ind P P_O P_S).
Pablito: The *response* window reads:
nat_ind P P_O P_S
: forall n : nat, P n
Anton: Well, nat_ind P P_O P_S should be applied to an argument of type nat, but luckily we have one among the assumptions:
Check (nat_ind P P_O P_S n).
Pablito: The *response* window reads:
nat_ind P P_O P_S
: P n
Halcyon: Which coincides with the goal, yay:
exact (nat_ind P P_O P_S n).
Anton (reflectively): Either way we look at it, proving nat_ind1 is routine. Who would have thought.
Alfrothul: So bottom line, the proof reads:
Restart.
intros P P_O P_S n.
exact (nat_ind P P_O P_S n).
Halcyon: Yes.
Alfrothul: And thanks to the Curry-Howard isomorphism, the proof can be stated as a one-liner, look:
Restart.
exact (fun P P_O P_S n => nat_ind P P_O P_S n).
Bong-sun (inquisitive): What do we get if we type Show Proof. at the end of the first proof?
Pablito (diligent): The *response* window reads:
(fun (P : nat -> Prop) (P_O : P 0) (P_S : forall n' : nat, P n' -> P (S n')) (n : nat) =>
nat_ind (fun n0 : nat => P n0) P_O (fun (n' : nat) (IHn' : P n') => P_S n' IHn') n)
Bong-sun: And what do we get if we type Show Proof. at the end of the second proof?
Pablito: The *response* window reads:
(fun (P : nat -> Prop) (P_O : P 0) (P_S : forall n' : nat, P n' -> P (S n')) (n : nat) =>
nat_ind P P_O P_S n)
Bong-sun: And what do we get if we type Show Proof. at the end of the third proof?
Pablito: Exactly the same, look:
(fun (P : nat -> Prop) (P_O : P 0) (P_S : forall n' : nat, P n' -> P (S n')) (n : nat) =>
nat_ind P P_O P_S n)
Bong-sun (tireless): And what do we get if we type Show Proof. at the end of the fourth proof? Exactly the same as for the third proof, right?
Pablito: Right.
Alfrothul: The second proof is almost the same as the first, except for the arguments of nat_ind:
Halcyon: Functional equality is a semantic notion. Syntactically,
They are two sides of the same coin.
The Greek chorus: EVERYBODY LOOKS AT HALCYON.
Halcyon: What? I read.
Dana: Halcyon, you are completely right. Syntactically, fun a => f a is the eta-expansion of f, and so are
Dana (continuing): Semantically, all these expressions are functionally equal: Applying them to the same arguments gives the same results.
Alfrothul (curious): What did you read, Halcyon?
Halcyon: Mayer Goldberg’s introduction to the lambda-calculus.
Mimer: Good choice.
Bong-sun: So fun a b c => f a b c and f are equivalent?
Halcyon: Yes, syntactically and semantically.
Bong-sun: So... fun P P_O P_S n => nat_ind P P_O P_S n and nat_ind are equivalent too?
Halcyon: Yes.
Bong-sun: And fun (P : nat -> Prop) (P_O : P 0) (P_S : forall n' : nat, P n' -> P (S n')) (n : nat) => nat_ind P P_O P_S n and nat_ind are equivalent.
Halcyon: Yes. It does not matter whether we annotate the formal parameters with their type.
Bong-sun: Then allow me, because same same:
Restart.
exact nat_ind.
The Greek chorus: MIMER LAUGHS AND EVERYBODY ELSE COUGHS (IN THEIR SLEEVES (BECAUSE OF COVID)).
In tCPA, mathematical induction is formalized as structural induction over nat and expressed with nat_ind. Also, we can state our own version of nat_ind and prove this version
As foreshadowed in Week 04, we can also use it as an ordinary lemma instead of using the induction tactic. Consider, for example, the ordinary addition function:
Fixpoint r_add (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
S (r_add i' j)
end.
Lemma fold_unfold_r_add_O :
forall j : nat,
r_add 0 j = j.
Proof.
fold_unfold_tactic r_add.
Qed.
Lemma fold_unfold_r_add_S :
forall i' j : nat,
r_add (S i') j = S (r_add i' j).
Proof.
fold_unfold_tactic r_add.
Qed.
Proving that 0 is neutral on the right of r_add is done by routine induction:
Proposition r_add_0_r :
forall i : nat,
r_add i 0 = i.
Proof.
intro i.
induction i as [ | i' IHi'].
- exact (fold_unfold_r_add_O 0).
- rewrite -> fold_unfold_r_add_S.
rewrite -> IHi'.
reflexivity.
We can also prove this proposition using nat_ind explicitly instead of implicitly via the induction tactic:
Restart.
Check (nat_ind
(fun i => r_add i 0 = i)).
The *response* window reads (reformatting it from 2 to 4 lines for readability):
nat_ind (fun i : nat => r_add i 0 = i) :
r_add 0 0 = 0 ->
(forall n : nat, r_add n 0 = n -> r_add (S n) 0 = S n) ->
forall n : nat, r_add n 0 = n
The left part of the implication is r_add‘s fold-unfold lemma in the base case applied to 0:
Check (nat_ind
(fun i => r_add i 0 = i)
(fold_unfold_r_add_O 0)).
The *response* window reads:
nat_ind (fun i : nat => r_add i 0 = i) (fold_unfold_r_add_O 0) :
(forall n : nat, r_add n 0 = n -> r_add (S n) 0 = S n) ->
forall n : nat, r_add n 0 = n
Since the right part of this implication is what we want to prove, let us replace the goal (i.e., what is implicated) with the left part of the implication (i.e., what is implicating) using the apply tactic:
apply (nat_ind (fun i => r_add i 0 = i) (fold_unfold_r_add_O 0)).
The *goals* window then reads:
============================
forall n : nat, r_add n 0 = n -> r_add (S n) 0 = S n
In other words, we need to prove the same goal as in the induction step above:
intros i' IHi'.
rewrite -> fold_unfold_r_add_S.
rewrite -> IHi'.
reflexivity.
Qed.
All in all, we have proved the proposition by induction:
Bong-sun: Did you notice how in each clause of an induction proof, we start by using a fold-unfold lemma?
Dana: Well, yes, that’s the idea.
Alfrothul: Right. We simplify syntactically as much as the context allows, and then we turn to semantics to massage the goal further.
Bong-sun: Yes, that provides a useful uniformity.
Anton: In the base case, very often, the goal can be computed, and then we don’t need the fold-unfold lemma at all, look:
Proposition r_add_0_r_shorter :
forall i : nat,
r_add i 0 = i.
Proof.
intro i.
induction i as [ | i' IHi'].
-
Pablito (helpful): The *goals* window reads:
============================
r_add 0 0 = 0
Anton: See? The left-hand side is a call to r_add to two literals. So we can use the compute tactic:
Proposition r_add_0_r_shorter :
forall i : nat,
r_add i 0 = i.
Proof.
intro i.
induction i as [ | i' IHi'].
- compute.
Pablito (helpful): The *goals* window reads:
============================
0 = 0
Anton: And then we can use the reflexivity tactic. Or we could have just used the reflexivity tactic upfront, since it simplifies the goal in passing.
Bong-sun: All true.
Anton: Thank you.
Bong-sun: But then we learn nothing about the computation, and so we need to learn about it in the induction step, which adds to its complication. Also, using the reflexivity tactic does not bring clarity when we use nat_ind explicitly.
Anton: True, true. But sometimes I am in a hurry. But I agree that it is difficult to draw a line, and that the more we understand the computation, the better.
Bong-sun: Right. Uniformity in how we write things tends to foster unity in what we mean.
Anton: Bong-sun, you have been drinking deeply in the cup of life.
Bong-sun: Thank you – I guess. At any rate, rules are made to be broken, and so once we know what is in the box, we can start looking at what is outside the box.
Anton: Er... Yes?
Bong-sun: For example, look at what we want to prove in the induction step here:
i' : nat
IHi' : r_add i' 0 = i'
============================
r_add (S i') 0 = S i'
Anton: Yes. The left-hand side of the goal is a candidate for fold_unfold_r_add_S.
Bong-sun: Yes. But suppose we first rewrite the induction hypothesis on the right-hand side of the goal?
Anton: You mean like this:
rewrite <- IHi' at 2.
Bong-sun: Yes. Then the goal is an instance of the fold-unfold lemma:
exact (fold_unfold_r_add_S i' 0).
Anton: Indeed it is.
Bong-sun: Just something to keep in mind. We should not be mindless slaves to the form.
To think outside the box, one first needs to know that there is a box. It is also useful to know what is in this box.
Let us revisit the tail-recursive addition function:
Fixpoint tr_add (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
tr_add i' (S j)
end.
Using nat_ind explicitly instead of indirectly via the induction tactic,
The following proof fragment will come handy to prove the auxiliary lemma that is needed for the two proofs to go through:
Check (nat_ind
(fun i => forall j : nat, tr_add i (S j) = S (tr_add i j))).
(* wanted: forall j : nat, tr_add 0 (S j) = S (tr_add 0 j) *)
assert (H_O : forall j : nat, tr_add 0 (S j) = S (tr_add 0 j)).
{ intro j.
rewrite ->2 fold_unfold_tr_add_O.
reflexivity. }
Check (nat_ind
(fun i => forall j : nat, tr_add i (S j) = S (tr_add i j))
H_O).
And yes, these proofs use the Light of Inductil to cater for the accumulator (namely j).
This section is about the induction principle that corresponds to second-order recurrences over Peano numbers.
This induction principle features two base cases and two induction hypotheses:
Lemma nat_ind2 :
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.
This lemma can be proved using mathematical induction by strenghtening the induction hypothesis with a conjunction of goals:
Proof.
intros P P_0 P_1 P_SS.
assert (all2 :
forall n : nat,
P n /\ P (S n)).
{ intro n.
induction n as [ | n' [IHn' IHSn']].
- split.
+ exact P_0.
+ exact P_1.
- split.
+ exact IHSn'.
+ exact (P_SS n' IHn' IHSn'). }
intro n.
destruct (all2 n) as [ly _].
exact ly. (* <-- to be read aloud *)
Qed.
Across the Curry-Howard correspondence, the logical counterpart of conjunctions is pairs. And so by analogy, the Fibonacci function can be programmed to have a linear number of recursive calls using an auxiliary function that returns a pair of consecutive Fibonacci numbers:
Fixpoint fibfib (n : nat) : nat * nat :=
match n with
O =>
(0, 1)
| S n' =>
let (fib_n', fib_Sn') := fibfib n'
in (fib_Sn', fib_n' + fib_Sn')
end.
Definition fib_lin (n : nat) : nat :=
let (fib_n, _) := fibfib n
in fib_n.
Assuming that fib denotes the Fibonacci function, fibfib can be proved to return a pair of consecutive Fibonacci numbers:
Lemma about_fibfib :
forall n : nat,
fibfib n = (fib n, fib (S n)).
This lemma is proved using mathematical induction, just like all2 in the proof of nat_ind2.
The proof is in the accompanying .v file, along with a proof that fib_lin satisfies the canonical specification of Fibonacci numbers:
Definition specification_of_the_fibonacci_function (fib : nat -> nat) :=
fib 0 = 0
/\
fib 1 = 1
/\
forall n'' : nat,
fib (S (S n'')) = fib n'' + fib (S n'').
Theorem fib_lin_satisfies_the_specification_of_fib :
specification_of_the_fibonacci_function fib_lin.
Fibonacci numbers obey a second-order recurrence relation in that for any n, the Fibonacci number for n+2 is computed using the Fibonacci number for n and the Fibonacci number for n+1.
nat_ind2 is the induction principle associated to second-order recurrences in that for any P, P for n+2 is proved using P for n and P for n+1.
This second-order induction principle can be proved with an auxiliary lemma that is proved by structural induction over a Peano number.
Across the Curry-Howard correspondence, the Fibonacci function can be programmed with an auxiliary function that is programmed by structural recursion over a Peano number.
Prove Lemma nat_ind1 using nat_ind2:
Lemma nat_ind1_using_nat_ind2 :
forall P : nat -> Prop,
P 0 ->
(forall n' : nat,
P n' ->
P (S n')) ->
forall n : nat,
P n.
Proof.
intros P H_PO H_PS n.
induction n as [ | | n' IHn' IHSn'] using nat_ind2.
Abort.
The new point here is to tell Coq to use nat_ind2 as the induction principle, which we do with the keyword using.
The induction principle nat_ind2 makes it possible to directly prove the following theorem:
Theorem there_is_at_most_one_fibonacci_function :
forall fib1 : nat -> nat,
specification_of_the_fibonacci_function fib1 ->
forall fib2 : nat -> nat,
specification_of_the_fibonacci_function fib2 ->
forall n : nat,
fib1 n = fib2 n.
Proof.
unfold specification_of_the_fibonacci_function.
intros fib1 [S_fib1_O [S_fib1_SO S_fib1_SS]]
fib2 [S_fib2_O [S_fib2_SO S_fib2_SS]]
n.
induction n as [ | | n'' IHn'' IHSn''] using nat_ind2.
Anton: I can’t believe it.
Alfrothul: What can’t you believe, Anton?
Anton: The proof of Theorem there_is_at_most_one_fibonacci_function that uses nat_ind2.
Alfrothul: Yes?
Anton: It is routine.
Alfrothul: Actually yes it is. Well observed.
Anton: So we do something new and it is routine?
Alfrothul: Well, nat_ind2 is a generalization of nat_ind1.
Anton: Right, that might be why.
Bong-sun: Let me check:
Restart.
unfold specification_of_the_fibonacci_function.
intros fib1 [S_fib1_O [S_fib1_SO S_fib1_SS]]
fib2 [S_fib2_O [S_fib2_SO S_fib2_SS]].
Check (nat_ind2
(fun n : nat => fib1 n = fib2 n)).
Pablito (helpful): The *response* window reads:
nat_ind2 (fun n : nat => fib1 n = fib2 n)
: fib1 0 = fib2 0 ->
fib1 1 = fib2 1 ->
(forall n' : nat, fib1 n' = fib2 n' -> fib1 (S n') = fib2 (S n') -> fib1 (S (S n')) = fib2 (S (S n'))) ->
forall n : nat, fib1 n = fib2 n
Bong-sun: Let me see:
rewrite <- S_fib2_O in S_fib1_O at 2.
Check (nat_ind2
(fun n : nat => fib1 n = fib2 n)
S_fib1_O).
Pablito: The *response* window reads:
nat_ind2 (fun n : nat => fib1 n = fib2 n) S_fib1_O
: fib1 1 = fib2 1 ->
(forall n' : nat, fib1 n' = fib2 n' -> fib1 (S n') = fib2 (S n') -> fib1 (S (S n')) = fib2 (S (S n'))) ->
forall n : nat, fib1 n = fib2 n
Bong-sun: Right, routine.
Often, one programs the evenness predicate tail-recursively and with no accumulator, by peeling two layers of S at a time:
Fixpoint even2p (n : nat) : bool :=
match n with
0 =>
true
| S n' =>
match n' with
0 =>
false
| S n'' =>
even2p n''
end
end.
Its soundness and completeness is messy to prove by mathematical induction but effortless using nat_ind2:
Theorem soundness_and_completeness_of_even2p_using_nat_ind2 :
forall n : nat,
even2p n = true <-> exists m : nat, n = 2 * m.
Proof.
intro n.
induction n as [ | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete]] using nat_ind2.
The rest of the proof is in the accompanying .v file.
Two observations:
The proof uses the injection tactic perspicuously, as described in Week 10, when the assumptions contain:
S (S n') = S (S (2 * m'))
The proof uses the following lemma:
Lemma two_times_S :
forall n : nat,
2 * S n = S (S (2 * n)).
Pablito: It’s the twice_S lemma, right?Bong-sun: Tis, but we are about to need similar lemmas for 3, 4, and 5.Halcyon: Naming matters.
Sometimes, when using nat_ind2, only one of the induction hypotheses is used and not the other. In these cases, we can use one of the following further tailored induction principles:
Lemma nat_ind2_0 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n' : nat,
P n' ->
P (S (S n'))) ->
forall n : nat,
P n.
Lemma nat_ind2_1 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n' : nat,
P (S n') ->
P (S (S n'))) ->
forall n : nat,
P n.
This exercise revisits the tail-recursive evenness predicate evenp2:
Fixpoint evenp2 (n : nat) : bool :=
match n with
O =>
true
| S n' =>
match n' with
O =>
false
| S n'' =>
evenp2 n''
end
end.
Revisit the theorem about the soundness and completeness of even2p with two induction proofs rather than one:
Theorem soundness_and_completeness_of_even2p_using_nat_ind2_revisited :
forall n : nat,
evenp2 n = true <-> exists m : nat, n = 2 * m.
Proof.
intro n.
split.
- induction n as [ | | n' IHn' IHSn'] using nat_ind2.
...
- intros [q H_q].
rewrite -> H_q.
clear H_q n.
induction q as [ | | q' IHq' IHSq'] using nat_ind2.
...
Qed.
Analyze how IHn' and IHSn' are used in the first induction proof, and how IHq' and IHSq' are used in the second induction proof. If only one of them is used, revisit these two proofs using nat_ind2_0 or nat_ind2_1, your choice:
Theorem soundness_and_completeness_of_even2p_using_nat_ind2_re2visited :
forall n : nat,
evenp2 n = true <-> exists m : nat, n = 2 * m.
This exercise revisits the original evenness predicate:
Fixpoint evenp1 (n : nat) : bool :=
match n with
0 =>
true
| S n' =>
negb (evenp1 n')
end.
Prove that this original predicate and the tail-recursive one are functionally equivalent:
Theorem evenp1_and_evenp2_are_functionally_equal_using_nat_ind2 :
forall n : nat,
evenp1 n = evenp2 n.
This section is about the induction principle that corresponds to third-order recurrences over Peano numbers.
We can also express a mathematical induction principle with three base cases and three induction hypotheses:
Lemma nat_ind3 :
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.
Sometimes, when using nat_ind3, only one of the induction hypotheses is used, or one of the induction hypotheses is not used. In these cases, we can use one of the following further tailored induction principles:
Lemma nat_ind3_0 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P n' ->
P (S (S (S n')))) ->
forall n : nat,
P n.
Lemma nat_ind3_1 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P (S n') ->
P (S (S (S n')))) ->
forall n : nat,
P n.
Lemma nat_ind3_2 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P (S (S n')) ->
P (S (S (S n')))) ->
forall n : nat,
P n.
Lemma nat_ind3_01 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P n' ->
P (S n') ->
P (S (S (S n')))) ->
forall n : nat,
P n.
Lemma nat_ind3_02 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P n' ->
P (S (S n')) ->
P (S (S (S n')))) ->
forall n : nat,
P n.
Lemma nat_ind3_12 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall n' : nat,
P (S n') ->
P (S (S n')) ->
P (S (S (S n')))) ->
forall n : nat,
P n.
The following function implements a ternary predicate, i.e., whether a natural number is divisible by 3:
Fixpoint ternaryp (n : nat) : bool :=
match n with
0 =>
true
| 1 =>
false
| 2 =>
false
| S (S (S n')) =>
ternaryp n'
end.
Prove its soundness and completeness, and appreciate the effortlessness of using nat_ind3 compared to using nat_ind1 or nat_ind2.
Use nat_ind3 to prove the following property:
Property threes_and_fives_using_nat_ind3 :
forall n : nat,
exists a b : nat,
8 + n = 3 * a + 5 * b.
The following lemma might prove handy:
Lemma three_times_S :
forall n : nat,
3 * S n = S (S (S (3 * n))).
Prove Property threes_and_fives (in Exercise 09) using mathematical induction:
Property threes_and_fives_using_nat_ind1 :
forall n : nat,
exists a b : nat,
8 + n = 3 * a + 5 * b.
In addition to three_times_S from Exercise 09, The following lemma might prove handy:
Lemma five_times_S :
forall n : nat,
5 * S n = S (S (S (S (S (5 * n))))).
Halcyon: Isn’t it partly the same hint as for Exercise 09?Pablito: Yes, partly the same hint, but not the same exercise.
This exercise is about the induction principle that corresponds to fourth-order recurrences over Peano numbers.
Use nat_ind4 (from Exercise 11) to prove the following property:
Property fours_and_fives_using_nat_ind4 :
forall n : nat,
exists a b : nat,
12 + n = 4 * a + 5 * b.
The following lemma might prove handy:
Lemma four_times_S :
forall n : nat,
4 * S n = S (S (S (S (4 * n)))).
The Wikipedia page about mathematical induction contains an informal proof of Property fours_and_fives (from Exercise 12). Formalize this proof, i.e., prove Property fours_and_fives using mathematical induction:
Property fours_and_fives_using_nat_ind1 :
forall n : nat,
exists a b : nat,
12 + n = 4 * a + 5 * b.
The following lemma might prove handy:
Lemma five_times_S :
forall n : nat,
5 * S n = S (S (S (S (S (5 * n))))).
Halcyon: Isn’t it the same hint as for Exercise 10?Pablito: Yes. These lemmas must be useful since we keep reusing them.
Prove the following lemma by induction on x, using nat_ind3_0:
Lemma auxiliary_23 :
forall x y : nat,
2 * x = 3 * y ->
exists z : nat,
x = 3 * z.
Hint: In the course of your proof, consider using the injection tactic perspicuously, as described in Week 10, should your assumptions contain either of:
S (S (S (S (S (S (2 * x')))))) = 6
S (S (S (S (S (S (2 * x')))))) = 3 * S (S (S y'))
Prove the following lemma by induction on y, using nat_ind3_1:
Lemma auxiliary_32 :
forall x y : nat,
2 * x = 3 * y ->
exists z : nat,
y = 2 * z.
Provide two indirect proofs for the following property – one as a corollary of auxiliary_23 and the other as a corollary of auxiliary_32:
Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_indirectly :
forall (n : nat)
(q2 : nat),
n = 2 * q2 ->
forall q3 : nat,
n = 3 * q3 ->
exists q6 : nat,
n = 6 * q6.
The following lemma generalizes Lemma auxiliary_23 and Lemma auxiliary_32:
Lemma a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_indirectly_aux :
forall x y : nat,
2 * x = 3 * y ->
exists z : nat,
x = 3 * z /\ y = 2 * z.
Provide four proofs for this lemma:
In the two latter proofs, what is the simplest induction principle one could use?
Hint: The following lemma might prove handy:
Lemma times_reg_l :
forall n m p : nat,
S p * n = S p * m -> n = m.
Revisit the partial solution for Exercise 19 in Week 07.
This section is about the induction principle that corresponds to sixth-order recurrences over Peano numbers.
Here is yet another tailored induction principle:
Lemma nat_ind6_0 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
P 3 ->
P 4 ->
P 5 ->
(forall n' : nat,
P n' ->
P (S (S (S (S (S (S n'))))))) ->
forall n : nat,
P n.
Using the following handy lemma, provide a direct proof for the following property, using nat_ind6_0:
Lemma six_times_S :
forall n : nat,
6 * S n = S (S (S (S (S (S (6 * n)))))).
Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_directly :
forall (n : nat)
(q2 : nat),
n = 2 * q2 ->
forall q3 : nat,
n = 3 * q3 ->
exists q6 : nat,
n = 6 * q6.
This exercise is a variation on Exercise 15.
Prove the following property (by induction, i.e., not as a corollary of the property proved in Exercise 15):
Property a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_directly_swapped :
forall (n : nat)
(q3 : nat),
n = 3 * q3 ->
forall q2 : nat,
n = 2 * q2 ->
exists q6 : nat,
n = 6 * q6.
Proof.
intros n q3 H_q3 q2 H_q2.
exact (a_nat_is_divisible_by_6_if_it_is_divisible_by_2_and_by_3_directly n q2 H_q2 q3 H_q3).
Restart.
Pablito: How do we know which induction principle to use in a proof?
Bong-sun: We don’t know a priori.
Pablito: OK. And so?
Bong-sun: And so we attempt a proof by mathematical induction.
Pablito: OK?
Bong-sun: And then if we get stuck in the induction step, we analyze the assumptions, and we check whether we need not just an induction hypothesis on n', but perhaps also on S n', and perhaps also on S (S n'), etc.
Pablito: OK. And?
Bong-sun: Well, if we also need an induction hypothesis on S n', we attempt another proof using nat_ind2.
Pablito: And if we also need an induction hypothesis on S (S n'), we attempt another proof using nat_ind3?
Bong-sun: Yes.
Alfrothul: After a while, one can develop a sort of flair. For example, in Exercise 15, we have to prove that n is a multiple of 6, and so it makes sense to use to use nat_ind6.
Pablito: OK, thanks. And how do we know that we should rather use, e.g., nat_ind6_0, as in Exercise 15?
Dana: That one is easy. Once the proof goes through with nat_ind6, we just check which induction hypotheses are used, and then we pick the tailored version of the induction principle that only uses these induction hypotheses.
Simplicity is the highest goal,achievable when one has overcome all difficulties.
Touched up the narrative [02 Jul 2025]
Renamed the chapter and reorganized it [04 Jun 2025]
Added more exercises and streamlined the narrative [24 May 2025]
Added the postlude [23 May 2025]
Added the section about tailored induction principles as well as Exercise 07, Exercise 14, Exercise 15, and Exercise 16 [23 May 2025]
Created [04 Apr 2025]