The goal of this chapter is to introduce how to prove properties about Peano numbers structural induction, i.e., by induction over their structure. Since Peano numbers and natural numbers are isomorphic, the title of this chapter could have been “Mathematical induction”.
Let us revisit Peano numbers:
Inductive nat : Type :=
O : nat
| S : nat -> nat.
This representation is both sound and complete:
Peano numbers and natural numbers are therefore isomorphic.
The definition of Peano numbers is inductive in that it consists of a base case (the zero case) and an induction step (the successor case): we construct a Peano number with O, and given a Peano number, we construct a new Peano number with S.
Because of completeness, any Peano number was constructed using O and S, and in turn any Peano number that was constructed using S was constructed out of a Peano number, which itself was constructed using O and S, etc. as captured in the following Gallina fragment:
match n with
O =>
...
| S n' =>
match n' with
O =>
...
| S n'' =>
match n'' with
O =>
...
| S n''' =>
...
end
end
end
And so the induction principle associated with Peano numbers, for any property P indexed with a Peano number, reads as follows:
| IND | P O | forall n' : nat, P n' -> P (S n') | |
| forall n : nat, P n | |||
If a property holds for O (base case), and, (induction step) assuming it holds for a Peano number (which is the induction hypothesis), it holds for the successor of this Peano number, then this property holds for any Peano number.
So in the inference rule above,
And since Peano numbers and natural numbers are isomorphic, by soundness, the structural induction principle associated to Peano numbers is isomorphic to mathematical induction, i.e., induction over natural numbers.
Side note: every time we define a data type in Gallina, tCPA manufactures the corresponding induction principle, naming it as the name of this data type concatenated with “_ind”. So we can visualize the induction principle associated to nat using the Check command:
Check nat_ind.
The *response* window then reads:
nat_ind
: forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
The accompanying resource file contains two examples where nat_ind is used to prove that 0 is right-neutral for addition:
The first example involves an addition function that satisfies a specification:
Definition specification_of_the_addition_function (add : nat -> nat -> nat) :=
(forall j : nat,
add O j = j)
/\
(forall i' j : nat,
add (S i') j = S (add i' j)).
Proposition add_0_r_v0 :
forall add : nat -> nat -> nat,
specification_of_the_addition_function add ->
forall n : nat,
add n 0 = n.
The second example involves the resident addition function:
Proposition add_0_r_v1 :
forall n : nat,
n + 0 = n.
The first example hinges on the two conjuncts of the specification, and the second on the analogue resident lemmas:
plus_O_n: forall n : nat, 0 + n = n
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
For notational convenience, tCPA also features an induction tactic.
The induction tactic, applied to a natural number n, implements mathematical induction. Therefore it creates two subgoals: one for the base case, and one for the induction step. Courtesy of tCPA, we can control the names in these subgoals by specifying them:
intro n.
induction n as [ | n' IHn'].
There is nothing to name in the base case. In the induction step (i.e., the successor case), n' stands for the predecessor of n and IHn' for the induction hypothesis.
In the same vein as Proposition add_0_r_v1 above, let us prove that 0 is absorbing for multiplication on the right. Since the multiplication function is defined by induction over its first argument, let us exhibit its base case and its induction step, using the Search facility:
Nat.mul_0_l: forall n : nat, 0 * n = 0
Nat.mul_succ_l: forall n m : nat, S n * m = n * m + m
The proof is similar to the induction proof of Proposition add_0_r_v1:
To wit:
Proposition mul_0_r_v1 :
forall n : nat,
n * 0 = 0.
Proof.
intro n.
induction n as [ | n' IHn'].
- Check (Nat.mul_0_l 0).
exact (Nat.mul_0_l 0).
- Check (Nat.mul_succ_l n' 0).
rewrite -> (Nat.mul_succ_l n' 0).
rewrite -> IHn'.
Check (Nat.add_0_l 0).
exact (Nat.add_0_l 0).
Qed.
As for proving that 0 is neutral for addition on the left and that 0 is absorbing for multiplication on the left, no induction proof is necessary – we simply use the base case of addition and the base case of multiplication.
Halcyon: Seriously?Pablito: Well, apparently.Halcyon: Should we try?Pablito: Let’s!
Week 01 featured some food for thought that was revisited in Exercise 13 in Week 02. We do not know yet how to reason about recursive functions, so let us declare the two Leibniz equalities that underly foo in a specification of foo:
Definition specification_of_foo_in_Week_01 (foo : nat -> nat) :=
(foo O = 0)
/\
(forall n' : nat,
foo (S n') = S (S (foo n'))).
Here is an analogue of the theorem from Week 02, adjusted to use the specification:
Theorem about_foo :
forall foo : nat -> nat,
specification_of_foo_in_Week_01 foo ->
forall a b : nat,
foo a = b ->
b = 2 * a.
To prove this theorem, we first massage its goal into something more comfortable:
Proof.
intro foo.
unfold specification_of_foo_in_Week_01.
intros [S_foo_O S_foo_S].
intros a b H_foo.
rewrite <- H_foo.
The *goals* windows now reads:
foo : nat -> nat
S_foo_O : foo 0 = 0
S_foo_S : forall n' : nat, foo (S n') = S (S (foo n'))
a, b : nat
H_foo : foo a = b
============================
foo a = 2 * a
This form is comfortable to conduct an induction proof.
Prove the following helpful lemma:
Lemma twice_S :
forall n : nat,
2 * S n = S (S (2 * n)).
Complete the proof of Theorem about_foo just above,
The food for thought in Week 01 also featured a function named bar that was revisited in Exercise 12 in Week 02 with a theorem. Prove this theorem after proving the following helpful lemma:
Lemma thrice_S :
forall n : nat,
3 * S n = S (S (S (3 * n))).