# 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'. rewriteIHn'.
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 : tP 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 : natnatProp :=
| 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) : natProp :=
| 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.