# IndPrinciplesInduction Principles

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".

From LF Require Export ProofObjects.

From LF Require Export ProofObjects.

Check nat_ind :

∀ P : nat → Prop,

P 0 →

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

∀ n : nat, P n.

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

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 The specific shape of each case depends on the arguments to the corresponding constructor.

Inductive time : Type :=

| day

| night.

Check time_ind :

∀ P : time → Prop,

P day →

P night →

∀ t : time, P t.

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

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

Inductive natlist' : Type :=

| nnil'

| nsnoc (l : natlist') (n : nat).

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

∀ P : natlist' → Prop,

P nnil' →

(∀ l : natlist', P l → ∀ n : nat, P (nsnoc l n)) →

∀ n : natlist', P n.

# Induction Principles for Propositions

Print ev.

(* ===>

Inductive ev : nat -> Prop :=

| ev_0 : ev 0

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

(* ===>

Inductive ev : nat -> Prop :=

| ev_0 : ev 0

| ev_SS : forall 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

| le1_n : ∀ n, le

| le1_S : ∀ n m, (le

Notation "m <=1 n" := (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

Check le2_ind :

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

P n →

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

∀ n

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

∀ 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.
We can also define

*non-standard*induction principles in this style. Recall this troublesome thoerem:
Lemma even_ev : ∀ n: nat, even n = true → ev n.

Proof.

induction n; intros.

- apply ev_0.

- destruct n.

+ simpl in H. inversion H.

+ simpl in H.

apply ev_SS.

Abort.

Proof.

induction n; intros.

- apply ev_0.

- destruct n.

+ simpl in H. inversion H.

+ simpl in H.

apply ev_SS.

Abort.

Attempts to prove this by standard induction on n fail in the case for
S (S n), because the induction hypothesis only tells us something about
S n, which is useless. There are various ways to hack around this problem;
for example, we
Lemma even_ev' : ∀ n : nat,
(even n = true → ev n) ∧ (even (S n) = true → ev (S n)).
But we can make a much better proof by defining and proving a
non-standard induction principle that goes "by twos":

*can*use ordinary induction on n to prove this (try it!):
Definition nat_ind2 :

∀ (P : nat → Prop),

P 0 →

P 1 →

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

∀ n : nat , P n :=

fun P ⇒ fun P

fix f (n:nat) := match n with

0 ⇒ P

| 1 ⇒ P

| S (S n') ⇒ PSS n' (f n')

end.

∀ (P : nat → Prop),

P 0 →

P 1 →

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

∀ n : nat , P n :=

fun P ⇒ fun P

_{0}⇒ fun P_{1}⇒ fun PSS ⇒fix f (n:nat) := match n with

0 ⇒ P

_{0}| 1 ⇒ P

_{1}| S (S n') ⇒ PSS n' (f n')

end.

Once you get the hang of it, it is entirely straightforward to
give an explicit proof term for induction principles like this.
Proving this as a lemma using tactics is much less intuitive.
The induction ... using tactic variant gives a convenient way to
utilize a non-standard induction principle like this.

Lemma even_ev : ∀ n, even n = true → ev n.

Proof.

intros.

induction n as [ | |n'] using nat_ind2.

- apply ev_0.

- simpl in H.

inversion H.

- simpl in H.

apply ev_SS.

apply IHn'.

apply H.

Qed.

Proof.

intros.

induction n as [ | |n'] using nat_ind2.

- apply ev_0.

- simpl in H.

inversion H.

- simpl in H.

apply ev_SS.

apply IHn'.

apply H.

Qed.

#### Exercise: 4 stars, standard, optional (t_tree)

What if we wanted to define binary trees as follows, using a constructor that bundles the children and value at a node into a tuple?
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

Inductive t_tree (X : Type) : Type :=

| t_leaf

| t_branch : (t_tree X × X × t_tree X) → t_tree X.

Arguments t_leaf {X}.

Arguments t_branch {X}.

Inductive t_tree (X : Type) : Type :=

| t_leaf

| t_branch : (t_tree X × X × t_tree X) → t_tree X.

Arguments t_leaf {X}.

Arguments t_branch {X}.

Unfortunately, the automatically-generated induction principle is
not as strong as we need. It doesn't introduce induction hypotheses
for the subtrees.

Check t_tree_ind.

That will get us in trouble if we want to prove something by
induction, such as that reflect is an involution.

Fixpoint reflect {X : Type} (t : t_tree X) : t_tree X :=

match t with

| t_leaf ⇒ t_leaf

| t_branch (l, v, r) ⇒ t_branch (reflect r, v, reflect l)

end.

Theorem reflect_involution : ∀ (X : Type) (t : t_tree X),

reflect (reflect t) = t.

Proof.

intros X t. induction t.

- reflexivity.

- destruct p as [[l v] r]. simpl. Abort.

match t with

| t_leaf ⇒ t_leaf

| t_branch (l, v, r) ⇒ t_branch (reflect r, v, reflect l)

end.

Theorem reflect_involution : ∀ (X : Type) (t : t_tree X),

reflect (reflect t) = t.

Proof.

intros X t. induction t.

- reflexivity.

- destruct p as [[l v] r]. simpl. Abort.

We get stuck, because we have no inductive hypothesis for l or
r. So, we need to define our own custom induction principle, and
use it to complete the proof.
First, define the type of the induction principle that you want to
use. There are many possible answers. Recall that you can use
match as part of the definition.

Definition better_t_tree_ind_type : Prop

(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Second, define the induction principle by giving a term of that
type. Use the examples about nat, above, as models.

Definition better_t_tree_ind : better_t_tree_ind_type

(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Finally, prove the theorem. If induction...using gives you an
error about "Cannot recognize an induction scheme", don't worry
about it. The induction tactic is picky about the shape of the
theorem you pass to it, but it doesn't give you much information
to debug what is wrong about that shape. You can use apply
instead, as we saw at the beginning of this file.

Theorem reflect_involution : ∀ (X : Type) (t : t_tree X),

reflect (reflect t) = t.

Proof. (* FILL IN HERE *) Admitted.

☐

reflect (reflect t) = t.

Proof. (* FILL IN HERE *) Admitted.

☐