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

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.

Exercise: 3 stars (app_length_cons)

Prove this by induction on l1, without using app_length.

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.