The goal of this lecture note is to continue to study induction principles in tCPA.
As a first-order induction principle, mathematical induction involves one induction hypothesis: to conclude about P (S k), we need P k. As a second-order induction principle, nat_ind2 involves two induction hypotheses: to conclude about P (S (S k)), we need P k and P (S k). As a third-order induction principle, nat_ind3 involves three induction hypotheses: to conclude about P (S (S k)), we need P k and P (S k). In the course-of-values induction principle, k induction hypotheses are involved: to conclude about P k, where k is positive, we need P 0, P 1, ..., and P (k - 1):
Fixpoint and_until (P : nat -> Prop) (n : nat) : Prop :=
match n with
| 0 =>
P 0
| S n' =>
P (S n') /\ and_until P n'
end.
Lemma nat_ind_course_of_values :
forall P : nat -> Prop,
P 0 ->
(forall k : nat,
and_until P k -> P (S k)) ->
forall n : nat,
P n.
The accompanying .v file revisits the soundness and completeness of evenp2 using course-of-values induction.
Revisit the soundness and completeness of ternaryp (i.e., Exercise 03) using course-of-values induction.
Revisit Property threes_and_fives (i.e., Exercise 04) using course-of-values induction.
Revisit Property fours_and_fives (i.e., Exercise 08) using course-of-values induction.
Strong induction also involves many induction hypotheses (in contrast to weak induction, a.k.a. mathematical inductin, which is a first-order induction principle and therefore only involves one induction hypothesis): to conclude about P (S k), we need P i to hold for any i that is smaller or equal to k:
Lemma nat_ind_strong :
forall P : nat -> Prop,
P 0 ->
(forall k : nat,
(forall i : nat,
i <= k -> P i) ->
P (S k)) ->
forall n : nat,
P n.
The accompanying .v file revisits the soundness and completeness of evenp2 using strong induction.
The following lemma often comes handy when use strong induction:
Lemma all_nats_are_expressible_as_a_sum :
forall n : nat,
exists n1 n2 : nat,
n1 <= n /\ n2 <= n /\ n1 + n2 = n.
Consider the following specification of a mystery function:
Definition specification_of_a_mystery_function (mf : nat -> nat -> nat) :=
(forall i : nat,
mf (S i) 1 = i)
/\
(forall j : nat,
mf 1 (S j) = j)
/\
(forall i j1 j2 : nat,
mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2)))
/\
(forall i1 i2 j : nat,
mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))).
The goal of this section is to prove the following property of this mystery function, using strong induction:
Proposition a_property_of_the_mystery_function :
forall mf : nat -> nat -> nat,
specification_of_a_mystery_function mf ->
forall i j : nat,
S (mf (S i) (S j)) = S i * S j.
Its base case is simple to prove, so let us focus on its induction step:
Proof.
unfold specification_of_a_mystery_function.
intros mf [H_mf_1_r [H_mf_1_l [H_mf_plus_r H_mf_plus_l]]].
intros i j.
induction i as [ | i' IHi'] using nat_ind_strong.
- rewrite -> H_mf_1_l.
exact (eq_sym (Nat.mul_1_l (S j))).
-
The *goal* window reads:
mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
============================
S (mf (S (S i')) (S j)) = S (S i') * S j
We first decompose i' as the sum of two natural numbers:
- destruct (all_nats_are_expressible_as_a_sum i') as [i1' [i2' [H_i1' [H_i2' H_i1'_i2']]]].
rewrite <- H_i1'_i2'.
The *goal* window reads:
mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
i1', i2' : nat
H_i1' : i1' <= i'
H_i2' : i2' <= i'
H_i1'_i2' : i1' + i2' = i'
============================
S (mf (S (S (i1' + i2'))) (S j)) = S (S (i1' + i2')) * S j
To be in position to invoke H_mf_plus_l, we first need to rewrite S (S (i1' + i2')) into S i1' + S i2':
rewrite -> (plus_n_Sm i1' i2').
rewrite <- (plus_Sn_m i1' (S i2')).
rewrite -> H_mf_plus_l.
The *goal* window reads:
mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
i1', i2' : nat
H_i1' : i1' <= i'
H_i2' : i2' <= i'
H_i1'_i2' : i1' + i2' = i'
============================
S (S (mf (S i1') (S j) + mf (S i2') (S j))) = (S i1' + S i2') * S j
To be in position to invoke the induction hypothesis on i1' and on i2', we first need to rewrite S (S (mf (S i1') (S j) + mf (S i2') (S j))) into S (mf (S i1') (S j)) + S (mf (S i2') (S j)):
rewrite -> plus_n_Sm.
rewrite <- plus_Sn_m.
rewrite -> (IHi' i1' H_i1').
rewrite -> (IHi' i2' H_i2').
The *goal* window reads:
mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
i1', i2' : nat
H_i1' : i1' <= i'
H_i2' : i2' <= i'
H_i1'_i2' : i1' + i2' = i'
============================
S i1' * S j + S i2' * S j = (S i1' + S i2') * S j
The goal is then proved using the distributivity property of multiplication over addition.
Prove the property of the mystery function using strong induction over j instead of over i.
Prove the property of the mystery function using mathematical induction instead of strong induction.
Prove the property of the mystery function using course-of-values induction.
Implement the mystery function and verify that it satisfies its specification.
In how many ways can we break a chocolate tablet into 1*1 squares?
Revisit the soundness and completeness of ternaryp (i.e., Exercise 03 and Exercise 11) using strong induction.
Revisit Property threes_and_fives (i.e., Exercise 04 and Exercise 11) using strong induction.
Revisit Property fours_and_fives (i.e., Exercise 08 and Exercise 12) using strong induction.
Created [05 Apr 2024]