Inductive Principles

induction principle, t_ind, induction hypothesis, induction tactic, induction on proof trees, proof objects for induction.

An induction proof for P(n) where n : nat can be written like this:

• Base case. (n = 0) Show P(0) holds.
• Induction step. (n = S n' for some n') IH: P(n') holds. Show P(S n') holds.

This is an application of the induction principle for natural numbers. We will call this nat_ind. In Coq, this is represented as:

Check nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.

And for any other inductively defined type t, the corresponding induction principle is called t_ind.

It turns out that the induction tactic is a wrapper that performs apply t_ind with some book-keeping.

If we define a type t with constructors c1 ... cn, Coq generates a theorem with this shape:

t_ind : forall P : t -> Prop,
           ... case for c1 ... ->
           ... case for c2 ... -> ...
           ... case for cn ... ->
           forall n : t, P n

It is important to familiarize yourself with the cases generated for the recursive constructors.

Here is a solution to an exercise.

Inductive booltree : Type :=
  | bt_empty
  | bt_leaf (b : bool)
  | bt_branch (b : bool) (t1 t2 : booltree).

Definition booltree_property_type : Type := booltree -> Prop.

Definition base_case (P : booltree_property_type) : Prop :=
  P bt_empty.

Definition leaf_case (P : booltree_property_type) : Prop :=
  forall (b : bool), P (bt_leaf b).

Definition branch_case (P : booltree_property_type) : Prop :=
  forall (b : bool) (t1 : booltree), P t1 -> forall (t2 : booltree), P t2 -> P (bt_branch b t1 t2).

Definition booltree_ind_type :=
  forall (P : booltree_property_type),
    base_case P ->
    leaf_case P ->
    branch_case P ->
    forall (b : booltree), P b.

A polymorphic type on X is a definition of a family of inductive types indexed by X.

Note that in the following polymorphic type (list), whenever list is in the body of the declaration, it is always applied to the parameter X.

Inductive list (X:Type) : Type :=
        | nil : list X
        | cons : X -> list X -> list X.
list_ind :
        forall (X : Type) (P : list X -> Prop),
           P [] ->
           (forall (x : X) (l : list X), P l -> P (x :: l)) ->
           forall l : list X, P l

The induction principle is also parametrized on X. It can be thought of as a function that when applied to type X, gives list_ind for X lists.

Recall ev, an inductive proposition, from IndProp.v.

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

Our ev_ind would then be:

Check ev_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, ev n -> P n -> P (S (S n))) ->
    forall n : nat, ev n -> P n.

This is a bit different from the induction principles on datatypes.

Quoting, this is what it is in English:

In English, ev_ind says: Suppose P is a property of natural numbers. To show that P n holds whenever n is even, it suffices to show:

• P holds for 0,
• for any n, if n is even and P holds for n, then P holds for S (S n).

It is like an inversion on ev n, plus an induction hypothesis in the recursive cases. And since P n is a proposition on n, it isn’t P that applies to ev_0 (for instance), but on n = 0 when the case is ev_0, or for le’s case (a binary relation), the inductive case is

(forall m : nat, n <=2 m -> P m -> P (S m)) ->
    forall n0 : nat, n <=2 n0

Note that we need to show P n (S m') - the induction principle is parametrized on m.

(This description may be inaccurate.)

The induction principle on ev was parametrized on n. Alternately, it could have been parametrized on the evidence that n was even.

forall P : (forall n : nat, ev'' n -> Prop),
      P O ev_0 ->
      (forall (m : nat) (E : ev'' m),
        P m E -> P (S (S m)) (ev_SS m E)) ->
      forall (n : nat) (E : ev'' n), P n E

This is more similar to the structural induction on proof trees (evisceration’sproof trees are called evidence in this book).

Why this is the case (that the induction principle is this way) is subtle - refer to the section starting at line 664.

This alternate form of induction on propositions is more flexible than the induction parametrized on n, because it is parametrized both on n and the evidence that n is even.

It might be handy to use proof terms instead of tactic-based proofs. Induction principles, as types, can of course be written as programs (proof terms).

Here is an example.

Check nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.

Fixpoint build_proof
         (P : nat -> Prop)
         (evPO : P 0)
         (evPS : forall n : nat, P n -> P (S n))
         (n : nat) : P n :=
  match n with
  | 0 => evPO
  | S k => evPS k (build_proof P evPO evPS k)
  end.

This proof term inductively builds a proof tree. It takes evidence that P 0, evidence that if P(n') then P (S n').

It is helpful to focus on what evPS does, as build_proof recurses using it.

During the recursive case, evPS takes a smaller n' and a proof for P n' and produces a proof for P (S n'). That proof P n' is provided by recursively calling build_proof on n' with the same evidences for P 0 and forall n'. P n' -> P (S n').

It’s a bit confusing, the book might explain it better.

There is an example provided where standard induction on n fails to prove a proposition because it lacks information - instead, they do induction where n decreases by 2 - this is where an explicit proof term allows you to define and use non-standard induction.

Definition nat_ind2 :
  forall (P : nat -> Prop),
  P 0 ->
  P 1 ->
  (forall n : nat, P n -> P (S(S n))) ->
  forall n : nat , P n :=
    fun P => fun P0 => fun P1 => fun PSS =>
      fix f (n:nat) := match n with
                         0 => P0
                       | 1 => P1
                       | S (S n') => PSS n' (f n')
                       end.

This induction principle on n says that if you have proof of P 0 and P 1 (you need P 1 as well, because we are inducting by twos) and P (S S n), then you have a proof of P n, which is built via the proof term:

fun P => fun P0 => fun P1 => fun PSS =>
fix fun : =>
    (n:nat) := match n with
                 0 => P0
               | 1 => P1
               | S (S n') => PSS n' (f n')
               end.

Using nat_ind2 in this proof:

Lemma even_ev : forall n, even n = true -> ev n.
Proof.
  intros.
  induction n as [ | |n'] using nat_ind2.
...

gives us the goals at the point of induction:

3 goals (ID 108)

  H : even 0 = true
  ============================
  ev 0

goal 2 (ID 109) is:
 ev 1
goal 3 (ID 113) is:
 ev (S (S n'))

It’s actually pretty clean.

Practice for this technique is given in the exercise t_tree, where the standard induction principle doesn’t introduce induction hypotheses for the subtrees (Why?).

t_tree_ind
     : forall (X : Type) (P : t_tree X -> Prop),
       P t_leaf ->
       (forall p : t_tree X * X * t_tree X,
        P (t_branch p)) -> forall t : t_tree X, P t

2 stars, standard

1 star, standard, optional

2 stars, standard

2 stars, standard

1 star, standard, optional

1 star, standard, optional

1 star, standard, optional

1 star, standard, optional

1 star, standard, optional

4 stars, standard, optional

It’s a bit hard to do the induction type!

See line 990.