(** * Gen: Generalizing Induction Hypotheses *)
(* $Date: 2011-06-07 16:49:17 -0400 (Tue, 07 Jun 2011) $ *)
Require Export Ch03_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 : forall 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 _this particular_ [n] and [m], then [n = m].
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
- [P n] = "if [double n = double m], then [n = m]"
holds for all [n] by showing
- [P O]
(i.e., "if [double O = double m] then [O = m]")
- [P n -> P (S n)]
(i.e., "if [double n = double m] then [n = m]" implies "if
[double (S n) = double m] then [S n = m]").
If we look closely at the second statement, it is saying something
rather strange: it says that, for a _particular_ [m], if we know
- "if [double n = double m] then [n = m]"
then we can prove
- "if [double (S n) = double m] then [S n = m]".
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
- [Q] = "if [double n = 10] then [n = 5]"
then we can prove
- [R] = "if [double (S n) = 10] then [S n = 5]".
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 _every_ [n] but just a
_single_ [m]. *)
(** The good proof of [double_injective] leaves [m] in the goal
statement at the point where the [induction] tactic is invoked on
[n]: *)
Theorem double_injective' : forall 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 : forall 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 : forall 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].
Since [m = 0], by the definition of [double] we have [double n =
0]. There are two cases to consider for [n]. If [n = 0] we are
done, since this is what we wanted to show. Otherwise, if [n = S
n'] for some [n'], we derive a contradiction: by the definition of
[double] we would have [n = S (S (double n'))], but this
contradicts the assumption that [double 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'].
By the fact that [m = S m'] and the definition of [double], we
have [double n = S (S (double m'))]. There are two cases to
consider for [n].
If [n = 0], then by definition [double n = 0], a contradiction.
Thus, we may assume that [n = S n'] for some [n'], and again by
the definition of [double] we have [S (S (double n')) = S (S
(double m'))], which implies by inversion that [double n' = double
m'].
Instantiating the induction hypothesis with [n'] thus allows us to
conclude that [n' = m'], and it follows immediately that [S n' = S
m']. Since [S n' = n] and [S m' = m], this is just what we wanted
to show. [] *)
(** **** Exercise: 3 stars, recommended (gen_dep_practice) *)
(* EXPECTED *)
(** Carry out this proof by induction on [m]. *)
Theorem plus_n_n_injective_take2 : forall n m,
n + n = m + m ->
n = m.
Proof.
(* FILL IN HERE *) Admitted.
(** Now prove this by induction on [l]. *)
Theorem index_after_last: forall (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 *) Admitted.
[] *)
(** **** Exercise: 3 stars (gen_dep_practice_opt) *)
(** Prove this by induction on [l]. *)
Theorem length_snoc''' : forall (n : nat) (X : Type)
(v : X) (l : list X),
length l = n ->
length (snoc l v) = S n.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 3 stars (app_length_cons) *)
(** Prove this by induction on [l1], without using [app_length]. *)
Theorem app_length_cons : forall (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) *)
(* NO SOLUTION *)
(** Prove this by induction on [l], without using app_length. *)
Theorem app_length_twice : forall (X:Type) (n:nat) (l:list X),
length l = n ->
length (l ++ l) = n + n.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)