GenGeneralizing Induction Hypotheses

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 all is well. But if we begin it with we get stuck in the middle of the inductive case...

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:

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.

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.

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.

Now prove this by induction on l.

☐

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.

☐

Exercise: 3 stars (app_length_cons)

Prove this by induction on l1, without using app_length.

☐

Exercise: 4 stars, optional (app_length_twice)

Prove this by induction on l, without using app_length.

☐