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 :
  ∀ P : nat → Prop,
    P 0 →
    (∀ n : nat, P n → P (S n)) →
    ∀ 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.

Coq generates induction principles for every datatype defined with Inductive, including those that aren't recursive.
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 :
  ∀ P : time → Prop,
    P day →
    P night →
    ∀ t : time, P t.

An example with constructor arguments:

Inductive natlist : Type :=
  | nnil
  | ncons (n : nat) (l : natlist).
Check natlist_ind :
  ∀ P : natlist → Prop,
    P nnil →
    (∀ (n : nat) (l : natlist),
        P l → P (ncons n l)) →
    ∀ l : natlist, P l.

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]"
    But that oversimplifies a little. An assumption about P holding of an argument x of type t actually occurs immediately after the quantification of x.

For example, suppose we had written the definition of natlist a little differently:

Inductive natlist' : Type :=
  | nnil'
  | nsnoc (l : natlist') (n : nat).
Now the induction principle case for nsnoc1 is a bit different than the earlier case for ncons:

Check natlist'_ind :
  ∀ P : natlist' → Prop,
    P nnil' →
    (∀ l : natlist', P l → ∀ n : nat, P (nsnoc l n)) →
    ∀ n : natlist', P n.

Induction Principles for Propositions

Inductive definitions of propositions also cause Coq to generate induction priniciples. For example, recall our proposition ev, repeated here as ev'':

Inductive ev'' : nat → Prop :=
| ev_0 : ev'' 0
| ev_SS (n : nat) : ev'' n → ev'' (S (S n)).
Check ev''_ind :
  ∀ P : nat → Prop,
    P 0 →
    (∀ n : nat, ev'' n → P n → P (S (S n))) →
    ∀ n : nat, ev'' n → P n.
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).

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 :
  ∀ P : nat → nat → Prop,
    (∀ n : nat, P n n) →
    (∀ n m : nat, n <=1 m → P n m → P n (S m)) →
    ∀ n n0 : nat, n <=1 n0 → P n n0.
Check le2_ind :
  ∀ (n : nat) (P : nat → Prop),
    P n →
    (∀ m : nat, n <=2 m → P m → P (S m)) →
    ∀ n0 : nat, n <=2 n0 → P n0.
The latter is simpler, and corresponds to Coq's own definition.

Explicit Proof Objects for Induction (Optional)

Recall again the induction principle on naturals that Coq generates for us automatically from the Inductive declation for nat.

Check nat_ind :
  ∀ P : nat → Prop,
    P 0 →
    (∀ n : nat, P n → P (S n)) →
    ∀ n : nat, P n.
There's nothing magic about this induction lemma: it's just another Coq lemma that requires a proof. Coq generates the proof automatically too...

Print nat_ind.
We can rewrite that more tidily as follows:
Fixpoint build_proof
         (P : nat → Prop)
         (evPO : P 0)
         (evPS : ∀ 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.
Definition nat_ind_tidy := build_proof.
Recursive function build_proof thus pattern matches against n, recursing all the way down to 0, and building up a proof as it returns.