## 2. Induction

This tutorial is no longer maintained. See our documentation page for more recent references.

## 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

============================
forall b : bool, b = true \/ b = false

Coq < intro b.
1 subgoal

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

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

b : bool
============================
false = true \/ false = false

Coq < right; trivial.
No more subgoals.

Indeed, the whole proof can be done with the combination of the `destruct`, which combines `intro` and `elim`, with good old `auto`:

Coq < Lemma duality : forall b:bool, b = true \/ b = false.
1 subgoal

============================
forall b : bool, b = true \/ b = false

Coq < destruct b; auto.
No more subgoals.

Coq < Qed.
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 :=
| O : nat
| 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`:

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
Argument scopes are [_ function_scope _]
prim_rec is transparent
Expands to: Constant Top.prim_rec

Oops! Instead of the expected type `nat->(nat->nat->nat)->nat->nat` we get an apparently more complicated expression. In fact, the two types are convertible and one way of having the proper type would be to do some computation before actually defining `prim_rec` as such:

Coq < Definition prim_rec :=
Eval compute in nat_rec (fun i : nat => nat).
prim_rec is defined

prim_rec : nat -> (nat -> nat -> nat) -> nat -> nat
Argument scopes are [nat_scope function_scope nat_scope]
prim_rec is transparent
Expands to: Constant Top.prim_rec

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)))).
= 5
: nat

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 :=
match n with
| O => m
| S p => S (plus p m)
end.
plus is defined
plus is recursively defined (decreasing on 1st argument)

### 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.
No more subgoals.

Coq < Qed.
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, using the tactic `induction`, which 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 < induction n; simpl; auto.
No more subgoals.

Coq < Qed.
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 < induction m as [ | m IHm ]; simpl; auto.
1 subgoal

n, m : nat
IHm : n + m = m + n
============================
n + S m = S (m + 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 < rewrite <- IHm; auto.
No more subgoals.

Coq < Qed.
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
| O => False
| S p => True
end.
Is_S is defined

Now we may use the computational power of `Is_S` 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.
No more subgoals.

Coq < Qed.
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.
No more subgoals.

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 < Lemma no_confusion : forall n:nat, 0 <> S n.
1 subgoal

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

Coq < intro n; discriminate.
No more subgoals.

Coq < Qed.
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 :=
| le_n : le n n
| 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, m : nat
n_le_m : le n m
============================
le (S n) (S m)

Coq < elim n_le_m.
2 subgoals

n, 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, 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.
No more subgoals.

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`. `Hint Constructors le` is just an abbreviation for `Hint Resolve le_n le_S`.

Coq < Hint Constructors le.

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)

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 < induction 1; auto.
No more subgoals.

Coq < Qed.
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.
No more subgoals.

Coq < Qed.
tricky is defined