(** * Gen: Generalizing 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 : 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) *)
(** Carry out this proof by induction on [m]. *)

Theorem plus_n_n_injective_take2 : forall n m, n + n = m + m -> n = m.
Proof.
  intros n m H.
  generalize dependent n.
  induction m as [| m'].
  Case "m = 0".
    intros n H. destruct n.
      reflexivity.
      inversion H.
  Case "m = S m'".
    intros n H. destruct n as [| n'].
      inversion H.
      assert (n' = m') as H1.
        apply IHm'. inversion H.
          rewrite <- plus_n_Sm in H1.
          rewrite <- plus_n_Sm in H1.
          inversion H1. reflexivity.
        rewrite H1. reflexivity.  Qed.

(** 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.
  intros n X l H.
  generalize dependent n.
  induction l as [| x l'].
  Case "l = nil".
    reflexivity.
  Case "l = cons x l'".
    intros n H. destruct n as [| n'].
      inversion H.
      apply IHl'. simpl in H. inversion H. reflexivity.  Qed.
(** [] *)

(** **** 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_:
      We proceed by induction on l.  Consider first the case where
      l is an empty list.  We are then to prove:
        forall n : nat, length [] = n -> index (S n) [] = None
      which follows immediately from the definition.

      Then we consider that l is not an empty list.  Our induction
      hypothesis is:
        forall n : nat, length l' = n -> index (S n) l' = None
      and we must prove:
        forall n : nat, length (x :: l') = n -> index (S n) (x :: l') = None

      We consider the cases where n is either zero or non-zero.  If
      zero, it leads to a contradiction.  If non-zero we must show
      that:
        index (S (S n')) (x :: l') = None

      We can apply the induction hypothesis here to yield our new
      goal:
        length l' = n

      Now we must simplify the hypothesis for the non-zero case
      mentioned above, which is:
        length (x :: l') = S n'

      Simplification leads to:
        S (length l') = S n'

      And by this we can prove the goal.
[] *)

(** **** 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.
  intros n X v l H.
  generalize dependent n.
  induction l as [| x l'].
  Case "l = nil".
    intros n H. simpl in H. simpl. rewrite <- H. reflexivity.
  Case "l = cons x l'".
    intros n H. destruct n as [| n'].
      inversion H.
      simpl. simpl in H. inversion H. apply eq_remove_S.
        rewrite H1. apply IHl'. apply H1.  Qed.
(** [] *)

(** **** 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.
  intros X l1 l2 x n.
  generalize dependent n.
  generalize dependent l2.
  induction l1 as [| x1 l1'].
  Case "l1 = nil".
    intros l2 n H. simpl. simpl in H. apply H.
  Case "l1 = cons x1 l1'".
    intros l2 n H. simpl. destruct n as [| n'].
      inversion H.
      apply eq_remove_S. apply IHl1'.
        simpl in H. inversion H. reflexivity.  Qed.

Theorem app_length_cons_r : forall (X : Type) (l1 l2 : list X)
                                  (x : X) (n : nat),
  S (length (l1 ++ l2)) = n -> length (l1 ++ (x :: l2)) = n.
Proof.
  intros X l1 l2 x n.
  generalize dependent n.
  generalize dependent l2.
  induction l1 as [| x1 l1'].
  Case "l1 = nil".
    intros l2 n H. simpl. simpl in H. apply H.
  Case "l1 = cons x1 l1'".
    intros l2 n H. simpl. destruct n as [| n'].
      inversion H.
      apply eq_remove_S. apply IHl1'.
        simpl in H. inversion H. reflexivity.  Qed.
(** [] *)

(** **** Exercise: 4 stars, optional (app_length_twice) *)
(** Prove this by induction on [l], without using app_length. *)

(* Theorem app_length_distr : forall (X:Type) (x:X) (l:list X), *)
(*   length (l ++ x :: l) = length l + length (x :: l). *)
(* Proof. *)
(*   intros X x l. induction l as [| h l']. *)
(*   Case "l = nil". reflexivity. *)
(*   Case "l = cons h l'". *)
(*     simpl. simpl in IHl'. apply eq_remove_S. *)
(*     rewrite <- plus_n_Sm. rewrite <- IHl'. unfold length. simpl. *)

Theorem app_length_twice : forall (X:Type) (n:nat) (l:list X),
  length l = n -> length (l ++ l) = n + n.
Proof.
  intros X n l H.
  generalize dependent n.
  induction l as [| x l'].
  Case "l = nil".
    intros n H. inversion H. reflexivity.
  Case "l = cons x l'".
    intros n H. destruct n.
      inversion H.
      inversion H. simpl. apply IHl' in H1.
      inversion H. rewrite H2. rewrite <- plus_n_Sm.
      apply eq_remove_S.
      apply app_length_cons_r.
      apply eq_remove_S. apply H1.  Qed.
(** [] *)
