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.
Completed the narrative with the proof that 0 is right-neutral for addition [05 Feb 2024]
Created [01 Feb 2024]