# GenGeneralizing Induction Hypotheses

(* $Date: 2011-06-07 16:49:17 -0400 (Tue, 07 Jun 2011) $ *)

Require Export Poly.

In the previous chapter, we noticed the importance of
controlling the exact form of the induction hypothesis when
carrying out inductive proofs in Coq. In particular, we need to
be careful about which of the assumptions we move (using intros)
from the goal to the context before invoking the induction
tactic. In this short chapter, we consider this point in a little
more depth and introduce one new tactic, called generalize
dependent, that is sometimes useful in helping massage the
induction hypothesis into the required form.
First, let's review the basic issue. Suppose we want to show that
the double function is injective — i.e., that it always maps
different arguments to different results. The way we

*start*this proof is a little bit delicate: if we begin it with
intros n. induction n.

all is well. But if we begin it with
intros n m. induction n.

we get stuck in the middle of the inductive case...
Theorem double_injective_FAILED : ∀n m,

double n = double m →

n = m.

Proof.

intros n m. induction n as [| n'].

Case "n = O". simpl. intros eq. destruct m as [| m'].

SCase "m = O". reflexivity.

SCase "m = S m'". inversion eq.

Case "n = S n'". intros eq. destruct m as [| m'].

SCase "m = O". inversion eq.

SCase "m = S m'".

assert (n' = m') as H.

SSCase "Proof of assertion".

(* Here we are stuck. We need the assertion in order to

rewrite the final goal (subgoal 2 at this point) to an

identity. But the induction hypothesis, IHn', does

not give us n' = m' -- there is an extra S in the

way -- so the assertion is not provable. *)

Admitted.

What went wrong?
The problem is that, at the point we invoke the induction
hypothesis, we have already introduced m into the context
intuitively, we have told Coq, "Let's consider some particular
n and m..." and we now have to prove that, if double n =
double m for
The next tactic, induction n says to Coq: We are going to show
the goal by induction on n. That is, we are going to prove that
the proposition
holds for all n by showing
If we look closely at the second statement, it is saying something
rather strange: it says that, for a
then we can prove
To see why this is strange, let's think of a particular m —
say, 5. The statement is then saying that, if we can prove
then we can prove
But knowing Q doesn't give us any help with proving R! (If we
tried to prove R from Q, we would say something like "Suppose
double (S n) = 10..." but then we'd be stuck: knowing that
double (S n) is 10 tells us nothing about whether double n
is 10, so Q is useless at this point.)
To summarize: Trying to carry out this proof by induction on n
when m is already in the context doesn't work because we are
trying to prove a relation involving
The good proof of double_injective leaves m in the goal
statement at the point where the induction tactic is invoked on
n:

*this particular*n and m, then n = m.- P n = "if double n = double m, then n = m"

- P O
- P n → P (S n)

*particular*m, if we know- "if double n = double m then n = m"

- "if double (S n) = double m then S n = m".

- Q = "if double n = 10 then n = 5"

- R = "if double (S n) = 10 then S n = 5".

*every*n but just a*single*m.Theorem double_injective' : ∀n m,

double n = double m →

n = m.

Proof.

intros n. induction n as [| n'].

Case "n = O". simpl. intros m eq. destruct m as [| m'].

SCase "m = O". reflexivity.

SCase "m = S m'". inversion eq.

Case "n = S n'".

(* Notice that both the goal and the induction

hypothesis have changed: the goal asks us to prove

something more general (i.e., to prove the

statement for *every* m), but the IH is

correspondingly more flexible, allowing us to

choose any m we like when we apply the IH. *)

intros m eq.

(* Now we choose a particular m and introduce the

assumption that double n = double m. Since we

are doing a case analysis on n, we need a case

analysis on m to keep the two "in sync." *)

destruct m as [| m'].

SCase "m = O". inversion eq. (* The 0 case is trivial *)

SCase "m = S m'".

(* At this point, since we are in the second

branch of the destruct m, the m' mentioned

in the context at this point is actually the

predecessor of the one we started out talking

about. Since we are also in the S branch of

the induction, this is perfect: if we

instantiate the generic m in the IH with the

m' that we are talking about right now (this

instantiation is performed automatically by

apply), then IHn' gives us exactly what we

need to finish the proof. *)

assert (n' = m') as H.

SSCase "Proof of assertion". apply IHn'.

inversion eq. reflexivity.

rewrite → H. reflexivity. Qed.

What this teaches us is that we need to be careful about using
induction to try to prove something too specific: If we're proving
a property of n and m by induction on n, we may need to
leave m generic.
However, this strategy doesn't always apply directly; sometimes a
little rearrangement is needed. Suppose, for example, that we had
decided we wanted to prove double_injective by induction on m
instead of n.

Theorem double_injective_take2_FAILED : ∀n m,

double n = double m →

n = m.

Proof.

intros n m. induction m as [| m'].

Case "m = O". simpl. intros eq. destruct n as [| n'].

SCase "n = O". reflexivity.

SCase "n = S n'". inversion eq.

Case "m = S m'". intros eq. destruct n as [| n'].

SCase "n = O". inversion eq.

SCase "n = S n'".

assert (n' = m') as H.

SSCase "Proof of assertion".

(* Here we are stuck again, just like before. *)

Admitted.

The problem is that, to do induction on m, we must first
introduce n. (If we simply say induction m without
introducing anything first, Coq will automatically introduce
n for us!)
What can we do about this? One possibility is to rewrite the
statement of the lemma so that m is quantified before n. This
will work, but it's not nice: We don't want to have to mangle the
statements of lemmas to fit the needs of a particular strategy for
proving them — we want to state them in the most clear and
natural way.
What we can do instead is to first introduce all the
quantified variables and then

*re-generalize*one or more of them, taking them out of the context and putting them back at the beginning of the goal. The generalize dependent tactic does this.Theorem double_injective_take2 : ∀n m,

double n = double m →

n = m.

Proof.

intros n m.

(* n and m are both in the context *)

generalize dependent n.

(* Now n is back in the goal and we can do induction on

m and get a sufficiently general IH. *)

induction m as [| m'].

Case "m = O". simpl. intros n eq. destruct n as [| n'].

SCase "n = O". reflexivity.

SCase "n = S n'". inversion eq.

Case "m = S m'". intros n eq. destruct n as [| n'].

SCase "n = O". inversion eq.

SCase "n = S n'".

assert (n' = m') as H.

SSCase "Proof of assertion".

apply IHm'. inversion eq. reflexivity.

rewrite → H. reflexivity. Qed.

Let's look at an informal proof of this theorem. Note that
the proposition we prove by induction leaves n quantified,
corresponding to the use of generalize dependent in our formal
proof.

*Theorem*: For any nats n and m, if double n = double m, then n = m.*Proof*: Let m be a nat. We prove by induction on m that, for any n, if double n = double m then n = m.- First, suppose m = 0, and suppose n is a number such
that double n = double m. We must show that n = 0.
- Otherwise, suppose m = S m' and that n is again a number such
that double n = double m. We must show that n = S m', with
the induction hypothesis that for every number s, if double s =
double m' then s = m'.

#### Exercise: 3 stars, recommended (gen_dep_practice)

Carry out this proof by induction on m.Theorem plus_n_n_injective_take2 : ∀n m,

n + n = m + m →

n = m.

Proof.

(* FILL IN HERE *) Admitted.

Now prove this by induction on l.

Theorem index_after_last: ∀(n : nat) (X : Type) (l : list X),

length l = n →

index (S n) l = None.

Proof.

(* FILL IN HERE *) Admitted.

☐

☐

#### Exercise: 3 stars, optional (index_after_last_informal)

Write an informal proof corresponding to your Coq proof of index_after_last:*Theorem*: For all sets X, lists l : list X, and numbers n, if length l = n then index (S n) l = None.*Proof*: (* FILL IN HERE *)☐

#### Exercise: 3 stars (gen_dep_practice_opt)

Prove this by induction on l.Theorem length_snoc''' : ∀(n : nat) (X : Type)

(v : X) (l : list X),

length l = n →

length (snoc l v) = S n.

Proof.

(* FILL IN HERE *) Admitted.

Theorem app_length_cons : ∀(X : Type) (l1 l2 : list X)

(x : X) (n : nat),

length (l1 ++ (x :: l2)) = n →

S (length (l1 ++ l2)) = n.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 4 stars, optional (app_length_twice)

Prove this by induction on l, without using app_length.Theorem app_length_twice : ∀(X:Type) (n:nat) (l:list X),

length l = n →

length (l ++ l) = n + n.

Proof.

(* FILL IN HERE *) Admitted.

☐