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:

Coq < About 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

Coq < About prim_rec.
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.
addition is defined

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