# IndPrinciplesInduction Principles

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:

We can directly use the induction principle with apply:

- P holds of 0
- for any n, if P holds of n, then P holds of S n.

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:

If we define type t with constructors c

t_ind : ∀ P : t → Prop,

... case for c

... case for c

... 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:

- 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.

_{1}... cn, Coq generates:t_ind : ∀ P : t → Prop,

... case for c

_{1}... →... case for c

_{2}... → ...... case for cn ... →

∀ n : t, P n

Inductive time : Type :=

| day

| night.

Check time_ind :

∀ P : time → Prop,

P day →

P night →

∀ t : time, P t.

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.

- 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 x
_{1}:a_{1}... xn:an, that case is:

"For all x_{1}:a_{1}... xn:an, if [P] holds of each of the arguments of type [t], then [P] holds of [c x_{1}... xn]"

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 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 le

_{1}: nat → nat → Prop :=

| le1_n : ∀ n, le

_{1}n n

| le1_S : ∀ n m, (le

_{1}n m) → (le

_{1}n (S m)).

Notation "m <=1 n" := (le

_{1}m n) (at level 70).

Inductive le

| le2_n : le

| le2_S m (H : le

Notation "m <=2 n" := (le

_{2}(n:nat) : nat → Prop :=| le2_n : le

_{2}n n| le2_S m (H : le

_{2}n m) : le_{2}n (S m).Notation "m <=2 n" := (le

_{2}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 n

_{0}: nat, n <=1 n

_{0}→ P n n

_{0}.

Check le2_ind :

∀ (n : nat) (P : nat → Prop),

P n →

(∀ m : nat, n <=2 m → P m → P (S m)) →

∀ n

_{0}: nat, n <=2 n

_{0}→ P n

_{0}.

The latter is simpler, and corresponds to Coq's own
definition.

# Explicit Proof Objects for Induction (Optional)

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.

(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.