(** * 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. (** [] *)