The goal of this lecture note is to study induction principles in tCPA.
The mathematical induction principle already exists in Coq, as the structural induction principle associated with Peano numbers. And indeed when prompted with Check nat_ind., Coq 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
But we can still express it ourselves:
Lemma nat_ind1 :
forall P : nat -> Prop,
P 0 ->
(forall k : nat, P k -> P (S k)) ->
forall n : nat, P n.
We can also prove nat_ind1 using the resident mathematical induction principle, either implicitly or explicitly, as in the accompanying .v file.
As foreshadowed in Week 03, 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 (using f_equal instead of rewrite + reflexivity for brevity):
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.
exact (f_equal S IHi').
Let us re-prove this proposition using nat_ind explicitly instead of indirectly 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 leftmost part of the implication is r_add‘s fold-unfold lemma in the base case applied to 0 and the rightmost part is what we want to prove. Ergo:
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 have to prove (essentially) the same goal as in the induction step above:
intros i' IHi'.
exact (f_equal S IHi').
Qed.
All in all, we have proved the proposition by induction without using the induction tactic – instead, we have directly used the induction principle associated to nat.
The induction principle associated to nat – i.e., mathematical induction – is sometimes referred to as “weak”, to contrast it with the “strong” induction principle presented in the next chapter.
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).
We can also express a mathematical induction principle with two base cases and two induction hypotheses that befits the structure of the Fibonacci function:
Lemma nat_ind2 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall k : nat, P k -> P (S k) -> P (S (S k))) ->
forall n : nat, P n.
This lemma can be proved using mathematical induction by strenghtening the induction hypothesis, as elaborated in the accompanying .v file.
Reminder: The Fibonacci function can be programmed using primitive iteration:
Fixpoint fibfib (n : nat) : nat * nat :=
match n with
| O =>
(0, 1)
| S n' =>
let (fib_n', fib_succ_n') := fibfib n'
in (fib_succ_n', fib_n' + fib_succ_n')
end.
Definition fib_lin (n : nat) : nat :=
let (fib_n, _) := fibfib n
in fib_n.
The key to computing the nth Fibonacci number in n recursive calls is to compute pairs of consecutive Fibonacci numbers. Assuming that fib denotes the Fibonacci function:
Lemma about_fibfib :
forall n : nat,
fibfib n = (fib n, fib (S n)).
This lemma is proved (using mathematical induction) in the accompanying .v file.
Across the Curry-Howard correspondence, the logical counterpart of pairs is conjunctions, which is why to prove a property P n, the stronger induction hypothesis involves proving P n /\ P (S n).
The induction principle nat_ind2 makes it possible to directly prove the following theorem:
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 there_is_at_most_one_fibonacci_function :
forall fib1 fib2 : nat -> nat,
specification_of_the_fibonacci_function fib1 ->
specification_of_the_fibonacci_function fib2 ->
forall n : nat,
fib1 n = fib2 n.
Proof.
intros fib1 fib2.
unfold specification_of_the_fibonacci_function.
intros [H_fib1_0 [H_fib1_1 H_fib1_SS]]
[H_fib2_0 [H_fib2_1 H_fib2_SS]]
n.
induction n as [ | | n'' IHn'' IHSn''] using nat_ind2.
The new point here is to tell Coq to use nat_ind2 as the induction principle, which we do with the keyword using.
Often, one programs the evenness predicate tail-recursively and with no accumulator, by peeling two layers of S at a time:
Fixpoint evenp (n : nat) : bool :=
match n with
| 0 =>
true
| S n' =>
match n' with
| 0 =>
false
| S n'' =>
evenp n''
end
end.
Its soundness and completeness is messy to prove by mathematical induction but effortless using nat_ind2:
Theorem soundness_and_completeness_of_evenp :
forall n : nat,
evenp 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.
We can also express a mathematical induction principle with three base cases and three induction hypotheses, and prove it by mathematical induction or using nat_ind2:
Lemma nat_ind3 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
P 2 ->
(forall k : nat, P k -> P (S k) -> P (S (S k)) -> P (S (S (S k)))) ->
forall n : nat, P n.
Prove the induction principles nat_ind1, nat_ind2, and nat_ind3 using either of the two others.
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_ind or nat_ind2.
Use nat_ind3 to prove the following property:
Property threes_and_fives :
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,
S (S (S (3 * n))) = 3 * S n.
Prove Property threes_and_fives using mathematical induction.
In addition to three_times_S from Exercise 04, The following lemmas might prove handy:
Lemma three_times_S :
forall n : nat,
S (S (S (3 * n))) = 3 * S n.
Lemma five_times_S :
forall n : nat,
S (S (S (S (S (5 * n))))) = 5 * S n.
Halcyon: Isn’t it partly the same hint as for Exercise 04?Pablito: Yes, partly the same hint, but not the same exercise.
Use nat_ind4 (from Exercise 07) to prove the following property:
Property fours_and_fives :
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,
S (S (S (S (4 * n)))) = 4 * S n.
The Wikipedia page about mathematical induction contains an informal proof of Property fours_and_fives (from Exercise 08). Formalize this proof, i.e., prove Property fours_and_fives using mathematical induction.
The following lemma might prove handy:
Lemma five_times_S :
forall n : nat,
S (S (S (S (S (5 * n))))) = 5 * S n.
Halcyon: Isn’t it the same hint as for Exercise 05?Pablito: Yes. These lemmas must be useful since we keep reusing them.
Created [05 Apr 2024]