2. Induction

## 2.1  Data Types as Inductively Defined Mathematical Collections

All the notions which were studied until now pertain to traditional mathematical logic. Specifications of objects were abstract properties used in reasoning more or less constructively; we are now entering the realm of inductive types, which specify the existence of concrete mathematical constructions.

### 2.1.1  Booleans

Let us start with the collection of booleans, as they are specified in the Coq's `Prelude` module:
Coq < Inductive bool :  Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined

Such a declaration defines several objects at once. First, a new `Set` is declared, with name `bool`. Then the constructors of this `Set` are declared, called `true` and `false`. Those are analogous to introduction rules of the new Set `bool`. Finally, a specific elimination rule for `bool` is now available, which permits to reason by cases on `bool` values. Three instances are indeed defined as new combinators in the global context: `bool_ind`, a proof combinator corresponding to reasoning by cases, `bool_rec`, an if-then-else programming construct, and `bool_rect`, a similar combinator at the level of types. Indeed:
Coq < Check bool_ind.
bool_ind
: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b

Coq < Check bool_rec.
bool_rec
: forall P : bool -> Set, P true -> P false -> forall b : bool, P b

Coq < Check bool_rect.
bool_rect
: forall P : bool -> Type, P true -> P false -> forall b : bool, P b

Let us for instance prove that every Boolean is true or false.
Coq < Lemma duality : forall b:bool, b = true \/ b = false.
1 subgoal

P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
f : nat -> nat
foo : f 0 = 0
f10 : f 1 = f 0
U : Type
============================
forall b : bool, b = true \/ b = false

Coq < intro b.
1 subgoal

P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
f : nat -> nat
foo : f 0 = 0
f10 : f 1 = f 0
U : Type
b : bool
============================
b = true \/ b = false

We use the knowledge that `b` is a `bool` by calling tactic `elim`, which is this case will appeal to combinator `bool_ind` in order to split the proof according to the two cases:
Coq < elim b.
2 subgoals

P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
f : nat -> nat
foo : f 0 = 0
f10 : f 1 = f 0
U : Type
b : bool
============================
true = true \/ true = false
subgoal 2 is:
false = true \/ false = false

It is easy to conclude in each case:
Coq < left; trivial.
1 subgoal

P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
f : nat -> nat
foo : f 0 = 0
f10 : f 1 = f 0
U : Type
b : bool
============================
false = true \/ false = false

Coq < right; trivial.
Proof completed.

Indeed, the whole proof can be done with the combination of the `simple induction` tactic, which combines `intro` and `elim`, with good old `auto`:
Coq < Restart.
1 subgoal

P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
f : nat -> nat
foo : f 0 = 0
f10 : f 1 = f 0
U : Type
============================
forall b : bool, b = true \/ b = false

Coq < simple induction b; auto.
Proof completed.

Coq < Qed.
simple induction b; auto.
duality is defined

### 2.1.2  Natural numbers

Similarly to Booleans, natural numbers are defined in the `Prelude` module with constructors `S` and `O`:
Coq < Inductive nat : Set :=
Coq <   | O : nat
Coq <   | S : nat -> nat.
nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined

The elimination principles which are automatically generated are Peano's induction principle, and a recursion operator:
Coq < Check nat_ind.
nat_ind
: forall P : nat -> Prop,
P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Coq < Check nat_rec.
nat_rec
: forall P : nat -> Set,
P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Let us start by showing how to program the standard primitive recursion operator `prim_rec` from the more general `nat_rec`:
Coq < Definition prim_rec := nat_rec (fun i:nat => nat).
prim_rec is defined

That is, instead of computing for natural `i` an element of the indexed `Set` `(P i)`, `prim_rec` computes uniformly an element of `nat`. Let us check the type of `prim_rec`:
Coq < Check prim_rec.
prim_rec
: (fun _ : nat => nat) O ->
(forall n : nat, (fun _ : nat => nat) n -> (fun _ : nat => nat) (S n)) ->
forall n : nat, (fun _ : nat => nat) n

Oops! Instead of the expected type `nat->(nat->nat->nat)->nat->nat` we get an apparently more complicated expression. Indeed the type of `prim_rec` is equivalent by rule β to its expected type; this may be checked in Coq  by command `Eval Cbv Beta`, which β-reduces an expression to its normal form:
Coq < Eval cbv beta in
Coq <   ((fun _:nat => nat) O ->
Coq <    (forall y:nat, (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
Coq <    forall n:nat, (fun _:nat => nat) n).
= nat -> (nat -> nat -> nat) -> nat -> nat
: Set

Let us now show how to program addition with primitive recursion:
Coq < Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n.

That is, we specify that `(addition n m)` computes by cases on `n` according to its main constructor; when `n = O`, we get `m`; when `n = S p`, we get `(S rec)`, where `rec` is the result of the recursive computation `(addition p m)`. Let us verify it by asking Coq to compute for us say 2+3:
Coq < Eval compute in (addition (S (S O)) (S (S (S O)))).
= S (S (S (S (S O))))
: (fun _ : nat => nat) (S (S O))

Actually, we do not have to do all explicitly. Coq provides a special syntax Fixpoint/match for generic primitive recursion, and we could thus have defined directly addition as:

Coq < Fixpoint plus (n m:nat) {struct n} : nat :=
Coq <   match n with
Coq <   | O => m
Coq <   | S p => S (plus p m)
Coq <   end.
plus is recursively defined

For the rest of the session, we shall clean up what we did so far with types `bool` and `nat`, in order to use the initial definitions given in Coq's `Prelude` module, and not to get confusing error messages due to our redefinitions. We thus revert to the state before our definition of `bool` with the `Reset` command:
Coq < Reset bool.

### 2.1.3  Simple proofs by induction

Let us now show how to do proofs by structural induction. We start with easy properties of the `plus` function we just defined. Let us first show that n=n+0.
Coq < Lemma plus_n_O : forall n:nat, n = n + 0.
1 subgoal

============================
forall n : nat, n = n + 0

Coq < intro n; elim n.
2 subgoals

n : nat
============================
0 = 0 + 0
subgoal 2 is:
forall n0 : nat, n0 = n0 + 0 -> S n0 = S n0 + 0

What happened was that `elim n`, in order to construct a `Prop` (the initial goal) from a `nat` (i.e. `n`), appealed to the corresponding induction principle `nat_ind` which we saw was indeed exactly Peano's induction scheme. Pattern-matching instantiated the corresponding predicate `P` to `fun n:nat => n = n ` 0+, and we get as subgoals the corresponding instantiations of the base case `(P O)` , and of the inductive step `forall y:nat, P y -> P (S y)`. In each case we get an instance of function `plus` in which its second argument starts with a constructor, and is thus amenable to simplification by primitive recursion. The Coq tactic `simpl` can be used for this purpose:
Coq < simpl.
2 subgoals

n : nat
============================
0 = 0
subgoal 2 is:
forall n0 : nat, n0 = n0 + 0 -> S n0 = S n0 + 0

Coq < auto.
1 subgoal

n : nat
============================
forall n0 : nat, n0 = n0 + 0 -> S n0 = S n0 + 0

We proceed in the same way for the base step:
Coq < simpl; auto.
Proof completed.

Coq < Qed.
intro n; elim n.
simpl in |- *.
auto.
simpl in |- *; auto.
plus_n_O is defined

Here `auto` succeeded, because it used as a hint lemma `eq_S`, which say that successor preserves equality:
Coq < Check eq_S.
eq_S
: forall x y : nat, x = y -> S x = S y

Actually, let us see how to declare our lemma `plus_n_O` as a hint to be used by `auto`:
Coq < Hint Resolve plus_n_O .

We now proceed to the similar property concerning the other constructor `S`:
Coq < Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m.
1 subgoal

============================
forall n m : nat, S (n + m) = n + S m

We now go faster, remembering that tactic `simple induction` does the necessary `intros` before applying `elim`. Factoring simplification and automation in both cases thanks to tactic composition, we prove this lemma in one line:
Coq < simple induction n; simpl; auto.
Proof completed.

Coq < Qed.
simple induction n; simpl in |- *; auto.
plus_n_S is defined

Coq < Hint Resolve plus_n_S .

Let us end this exercise with the commutativity of `plus`:

Coq < Lemma plus_com : forall n m:nat, n + m = m + n.
1 subgoal

============================
forall n m : nat, n + m = m + n

Here we have a choice on doing an induction on `n` or on `m`, the situation being symmetric. For instance:
Coq < simple induction m; simpl; auto.
1 subgoal

n : nat
m : nat
============================
forall n0 : nat, n + n0 = n0 + n -> n + S n0 = S (n0 + n)

Here `auto` succeeded on the base case, thanks to our hint `plus_n_O`, but the induction step requires rewriting, which `auto` does not handle:

Coq < intros m' E; rewrite <- E; auto.
Proof completed.

Coq < Qed.
simple induction m; simpl in |- *; auto.
intros m' E; rewrite <- E in |- *; auto.
plus_com is defined

### 2.1.4  Discriminate

It is also possible to define new propositions by primitive recursion. Let us for instance define the predicate which discriminates between the constructors `O` and `S`: it computes to `False` when its argument is `O`, and to `True` when its argument is of the form `(S n)`:
Coq < Definition Is_S (n:nat) := match n with
Coq <                            | O => False
Coq <                            | S p => True
Coq <                            end.
Is_S is defined

Now we may use the computational power of `Is_S` in order to prove trivially that `(Is_S (S n))`:
Coq < Lemma S_Is_S : forall n:nat, Is_S (S n).
1 subgoal

============================
forall n : nat, Is_S (S n)

Coq < simpl; trivial.
Proof completed.

Coq < Qed.
simpl in |- *; trivial.
S_Is_S is defined

But we may also use it to transform a `False` goal into `(Is_S O)`. Let us show a particularly important use of this feature; we want to prove that `O` and `S` construct different values, one of Peano's axioms:
Coq < Lemma no_confusion : forall n:nat, 0 <> S n.
1 subgoal

============================
forall n : nat, 0 <> S n

First of all, we replace negation by its definition, by reducing the goal with tactic `red`; then we get contradiction by successive `intros`:
Coq < red; intros n H.
1 subgoal

n : nat
H : 0 = S n
============================
False

Now we use our trick:
Coq < change (Is_S 0).
1 subgoal

n : nat
H : 0 = S n
============================
Is_S 0

Now we use equality in order to get a subgoal which computes out to `True`, which finishes the proof:
Coq < rewrite H; trivial.
1 subgoal

n : nat
H : 0 = S n
============================
Is_S (S n)

Coq < simpl; trivial.
Proof completed.

Actually, a specific tactic `discriminate` is provided to produce mechanically such proofs, without the need for the user to define explicitly the relevant discrimination predicates:

Coq < Restart.
1 subgoal

============================
forall n : nat, 0 <> S n

Coq < intro n; discriminate.
Proof completed.

Coq < Qed.
intro n;  discriminate.
no_confusion is defined

## 2.2  Logic programming

In the same way as we defined standard data-types above, we may define inductive families, and for instance inductive predicates. Here is the definition of predicate ≤ over type `nat`, as given in Coq's `Prelude` module:
Coq < Inductive le (n:nat) : nat -> Prop :=
Coq <   | le_n : le n n
Coq <   | le_S : forall m:nat, le n m -> le n (S m).

This definition introduces a new predicate `le:nat->nat->Prop`, and the two constructors `le_n` and `le_S`, which are the defining clauses of `le`. That is, we get not only the “axioms” `le_n` and `le_S`, but also the converse property, that `(le n m)` if and only if this statement can be obtained as a consequence of these defining clauses; that is, `le` is the minimal predicate verifying clauses `le_n` and `le_S`. This is insured, as in the case of inductive data types, by an elimination principle, which here amounts to an induction principle `le_ind`, stating this minimality property:
Coq < Check le.
le
: nat -> nat -> Prop

Coq < Check le_ind.
le_ind
: forall (n : nat) (P : nat -> Prop),
P n ->
(forall m : nat, le n m -> P m -> P (S m)) ->
forall n0 : nat, le n n0 -> P n0

Let us show how proofs may be conducted with this principle. First we show that nmn+1≤ m+1:
Coq < Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m).
1 subgoal

============================
forall n m : nat, le n m -> le (S n) (S m)

Coq < intros n m n_le_m.
1 subgoal

n : nat
m : nat
n_le_m : le n m
============================
le (S n) (S m)

Coq < elim n_le_m.
2 subgoals

n : nat
m : nat
n_le_m : le n m
============================
le (S n) (S n)
subgoal 2 is:
forall m0 : nat, le n m0 -> le (S n) (S m0) -> le (S n) (S (S m0))

What happens here is similar to the behaviour of `elim` on natural numbers: it appeals to the relevant induction principle, here `le_ind`, which generates the two subgoals, which may then be solved easily with the help of the defining clauses of `le`.
Coq < apply le_n; trivial.
1 subgoal

n : nat
m : nat
n_le_m : le n m
============================
forall m0 : nat, le n m0 -> le (S n) (S m0) -> le (S n) (S (S m0))

Coq < intros; apply le_S; trivial.
Proof completed.

Now we know that it is a good idea to give the defining clauses as hints, so that the proof may proceed with a simple combination of `induction` and `auto`.
Coq < Restart.
1 subgoal

============================
forall n m : nat, le n m -> le (S n) (S m)

Coq < Hint Resolve le_n le_S .

We have a slight problem however. We want to say “Do an induction on hypothesis `(le n m)`”, but we have no explicit name for it. What we do in this case is to say “Do an induction on the first unnamed hypothesis”, as follows.
Coq < simple induction 1; auto.
Proof completed.

Coq < Qed.
simple induction 1; auto.
le_n_S is defined

Here is a more tricky problem. Assume we want to show that n≤ 0 ⇒ n=0. This reasoning ought to follow simply from the fact that only the first defining clause of `le` applies.
Coq < Lemma tricky : forall n:nat, le n 0 -> n = 0.
1 subgoal

============================
forall n : nat, le n 0 -> n = 0

However, here trying something like `induction 1` would lead nowhere (try it and see what happens). An induction on `n` would not be convenient either. What we must do here is analyse the definition of `le` in order to match hypothesis `(le n O)` with the defining clauses, to find that only `le_n` applies, whence the result. This analysis may be performed by the “inversion” tactic `inversion_clear` as follows:
Coq < intros n H; inversion_clear H.
1 subgoal

n : nat
============================
0 = 0

Coq < trivial.
Proof completed.

Coq < Qed.
intros n H; inversion_clear H.
trivial.
tricky is defined