IndPrinciplesInduction Principles

With the Curry-Howard correspondence and its realization in Coq in mind, we can now take a deeper look at induction principles.

Basics

The automatically generated induction principle for nat:
Check nat_ind.
(*  ===> nat_ind :
           forall P : nat -> Prop,
              P 0  ->
              (forall n : nat, P n -> P (S n))  ->
              forall n : nat, P n  *)
In English: Suppose P is a property of natural numbers (that is, P n is a Prop for every n). To show that P n holds of all n, it suffices to show:
  • P holds of 0
  • for any n, if P holds of n, then P holds of S n.

We can directly use the induction principle with apply:
Theorem mult_0_r' : ∀n:nat,
  n * 0 = 0.
Proof.
  apply nat_ind.
  - (* n = O *) reflexivity.
  - (* n = S n' *) simpl. intros n' IHn'. rewrite → IHn'.
    reflexivity. Qed.
Why the induction tactic is nicer than apply:
  • apply requires extra manual bookkeeping (the intros in the inductive case)
  • apply requires n to be left universally quantified
  • apply requires us to manually specify the name of the induction principle.

If we define type t with constructors c1 ... cn, Coq generates:
    t_ind : ∀P : t → Prop,
              ... case for c1 ... →
              ... case for c2 ... → ...
              ... case for cn ... →
              ∀n : t, P n
The specific shape of each case depends on the arguments to the corresponding constructor.

An example with no constructor arguments:
Inductive time : Type :=
  | day
  | night.
Check time_ind.
(* ===> time_ind : forall P : time -> Prop,
                          P day ->
                          P night ->
                          forall t : time, P t *)

An example with constructor arguments:
Inductive natlist : Type :=
  | nnil
  | ncons (n : nat) (l : natlist).
Check natlist_ind.
(* ===>
   natlist_ind :
      forall P : natlist -> Prop,
         P nnil  ->
         (forall (n : nat) (l : natlist),
            P l -> P (ncons n l)) ->
         forall n : natlist, P n *)

In general, the automatically generated induction principle for inductive type t is formed as follows:
  • Each constructor c generates one case of the principle.
  • If c takes no arguments, that case is:
    "P holds of c"
  • If c takes arguments x1:a1 ... xn:an, that case is:
    "For all x1:a1 ... xn:an,
              if [P] holds of each of the arguments of type [t],
              then [P] holds of [c x1 ... xn]"

Induction Principles in Prop

Coq also automatically produces induction priniciples for inductive propositions:
Print even.
(* ===>
Inductive even : nat -> Prop :=
  | ev_0 : even 0
  | ev_SS : forall n : nat, even n -> even (S (S n))
*)
Check even_ind.
(* ===> even_ind
        : forall P : nat -> Prop,
          P 0 ->
          (forall n : nat, even n -> P n -> P (S (S n))) ->
          forall n : nat,
          even n -> P n *)
In English, even_ind says: Suppose P is a property of natural numbers (that is, P n is a Prop for every n). 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).

The precise form of an Inductive definition can affect the induction principle Coq generates.
Inductive le1 : nat → nat → Prop :=
     | le1_n : ∀n, le1 n n
     | le1_S : ∀n m, (le1 n m) → (le1 n (S m)).
Notation "m ≤1 n" := (le1 m n) (at level 70).
n could instead be a parameter:
Inductive le2 (n:nat) : nat → Prop :=
  | le2_n : le2 n n
  | le2_S m (H : le2 n m) : le2 n (S m).
Notation "m ≤2 n" := (le2 m n) (at level 70).


Check le1_ind.
(* ===> forall P : nat -> nat -> Prop,
          (forall n : nat, P n n) ->
          (forall n m : nat, n <=1 m -> P n m -> P n (S m)) ->
          forall n n0 : nat, n <=1 n0 -> P n n0 *)
Check le2_ind.
(* ===>  forall (n : nat) (P : nat -> Prop),
           P n ->
           (forall m : nat, n <=2 m -> P m -> P (S m)) ->
           forall n0 : nat, n <=2 n0 -> P n0 *)
The latter is simpler, and corresponds to Coq's own definition.