(* Induction
   Version of 2/4/2009

   Please include the pennkey of every member of your group.
   (* FILL IN HERE *)
*)

Require Export Polysol.

(* Administrivia...

   * Midterm I is Wednesday Feb 18

   * New convention for "exercise stars"...

       - one star: very easy exercises that should be
         considered as REQUIRED (ideally they should be
         done while reading the lecture notes), but that
         are NOT TO BE HANDED IN (and will not be graded)

       - two, three, or four stars: real homework problems
         that (unless explicitly marked "optional") should
         be done and handed in for grading

   The 30,000 foot view...

     What we've seen so far:
       - inductive definitions of datatypes
       - Fixpoints over inductive datatypes
       - higher-order functions (map, filter, etc.)
       - polymorphism 
       - basic Coq
           -- inductive proofs
           -- several fundamental tactics

     Still to come (before Midterm I):
       - more on induction: generalizing the IH, induction principles
       - "programming with propositions"
       - logical connectives as inductive propositions
*)

(* ----------------------------------------------------- *)
(* Programming with Propositions *)

(* A PROPOSITION is a factual claim.  In Coq, propositions
   are written as expressions of type Prop. *)
Check (plus 2 2 = 4).
Check (ble_nat 3 2 = false).

(* Both provable and unprovable claims are perfectly good
   propositions.  Simply BEING a proposition is one thing;
   being PROVABLE is something else! *)
Check (plus 2 2 = 4).
Check (plus 2 2 = 5).

(* We've seen one way that propositions can be used in
   Coq: in [Theorem] declarations. *)
Theorem plus_2_2_is_4 : 
  plus 2 2 = 4.
Proof. reflexivity. Qed.

(* Coq allows us to do many other things with
   propositions.  For example, we can give a name to a
   proposition using a [Definition]. *)
Definition plus_fact : Prop  :=  plus 2 2 = 4.

Check plus_fact.

Theorem plus_fact_is_true : 
  plus_fact.
Proof. unfold plus_fact. reflexivity. Qed.
(* Note that we need an [unfold] in the proof because
   [plus_fact] was introduced as a [Definition]. *)

(* So far, all the propositions we have seen are equality
   propositions.  But we can build on equality
   propositions to make other sorts of claims.  For
   example, what does it mean to claim that "a number n is
   even"?  We have a function that (we believe) tests
   evenness, so one possible definition is "n is even
   iff (evenb n = true)." *)
Definition even (n:nat) := 
  evenb n = true.

(* [even] is a PARAMETERIZED PROPOSITION.  Think of it as a
   FUNCTION that, when applied to a number n, yields a
   proposition asserting that n is even. *)
Check even.
Check (even 4).

(* The type of [even], [nat->Prop], can be pronounced in
   two ways: either simply "[even] is a function from
   numbers to propositions" or, perhaps more helpfully,
   "[even] is a FAMILY of propositions, indexed by a
   number [n]." *)

(* Functions returning propositions are 100% first-class
   citizens in Coq.  We can use them in other
   definitions: *)
Definition even_n__even_SSn (n:nat) := 
  (even n) -> (even (S (S n))).

(* We can define them to take multiple arguments... *)
Definition between (n m o: nat) : Prop :=
  andb (ble_nat n o) (ble_nat o m) = true.

(* ... and then partially apply them: *)
Definition teen : nat->Prop := between 13 19.

(* We can pass propositions -- and even parameterized
   propositions -- as arguments to functions: *)
Definition true_for_zero (P:nat->Prop) : Prop :=
  P 0.

Definition true_for_n__true_for_Sn (P:nat->Prop) (n:nat) : Prop :=
  P n -> P (S n).

Definition preserved_by_S (P:nat->Prop) : Prop :=
  forall n', P n' -> P (S n').

Definition true_for_all_numbers (P:nat->Prop) : Prop :=
  forall n, P n.

Definition nat_induction (P:nat->Prop) : Prop :=
     (true_for_zero P)
  -> (preserved_by_S P)
  -> (true_for_all_numbers P).

(* Let's unravel what this means in concrete terms: *)
Example nat_induction_example : forall (P:nat->Prop),
    nat_induction P 
  = (   (P 0)
     -> (forall n', P n' -> P (S n'))
     -> (forall n, P n)).
Proof. 
  unfold nat_induction, true_for_zero, preserved_by_S, true_for_all_numbers.
  reflexivity.
Qed.

Theorem our_nat_induction_works : forall (P:nat->Prop), 
  nat_induction P.
Proof. 
  intros P.
  unfold nat_induction.
  intros TFZ PPS.
  unfold true_for_all_numbers. intros n. 
  induction n as [| n'].
  Case "n = O". apply TFZ.
  Case "n = S n'". apply PPS. apply IHn'.
Qed.

(* ----------------------------------------------------- *)
(* Induction axioms *)

(* You may be puzzled by the last proof because it seems
   like we're using a built-in reasoning principle of
   induction over natural numbers to prove a theorem that
   basically just says the same thing.  Indeed, this is
   exactly what we just did.

   In general, every time we declare a new datatype with
   [Inductive], Coq automatically generates an induction
   principle as an axiom (a theorem that we do not need to
   prove).

   The induction principle for a type [t] is called
   [t_ind].  Here is the one for natural numbers: *)
Check nat_ind.
(* The ":" here can be pronounced "...is a theorem proving
   the proposition..." *)

(* Here's a more direct proof that our induction principle
   is valid, using the [nat_ind] axiom directly (with [apply]
   instead of [induction]). *)
Theorem our_nat_induction_works' : 
  forall P, nat_induction P.
Proof. 
  intros P.
  unfold nat_induction, true_for_zero, 
         preserved_by_S, true_for_all_numbers.
  apply nat_ind. Qed.

(* Indeed, we can apply [nat_ind] (instead of using
   [induction]) in ANY inductive proof. *)
Theorem mult_0_r' : forall n:nat, 
  mult n 0 = 0.
Proof.
  apply nat_ind. 
  Case "O". reflexivity.
  Case "S". simpl. intros n IHn. rewrite -> IHn. 
    simpl. reflexivity. Qed.
(* Some things to note:

     - In the induction step of the proof we have to do a
       little manual bookkeeping (the [intros])

     - We do not introduce [n] into the context before
       applying [nat_ind]

     - The [apply] tactic automatically chooses variable
       names for us (in the second subgoal, here), whereas
       [induction] gives us a way to specify what names
       should be used.  The automatic choice is suboptimal.

  All this makes [inductive] nicer in practice than using
  induction principles directly. *)
Theorem plus_one_r' : forall n:nat, 
  plus n 1 = S n.
Proof.
  (* Complete this proof without using the [induction] tactic. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Our formulation of induction (the [nat_induction]
   proposition and the theorem stating that it works) can
   also be used directly to carry out proofs by
   induction. *)
Theorem plus_one_r'' : forall n:nat, 
  plus n 1 = S n.
Proof.
  (* Prove the same theorem again without [induction] or
     [apply nat_ind]. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------- *)
(* Induction principles for other datatypes *)

(* We've looked in depth now at the induction principle
   for natural numbers.  The induction principles that Coq
   generates for other datatypes defined with [Inductive]
   follow a very similar pattern. If we define a type [t]
   with constructors [c1] ... [cn], Coq generates an
   induction principle with this shape:

     t_ind :
       forall P : t -> Prop,
            ... case for c1 ...
         -> ... case for c2 ...
         -> ... 
         -> ... case for cn ...
         -> forall n : t, P n

   The specific shape of each case depends on the
   arguments to the corresponding constructor.  Before
   trying to write down a general rule, let's look at some
   more examples.
*)

Inductive yesno : Set :=
  | yes : yesno
  | no : yesno.

Check yesno_ind.
(* Yields:
    yesno_ind
        : forall P : yesno -> Prop, 
               P yes 
            -> P no 
            -> forall y : yesno, P y
*)

(* EXERCISE (one star): Write out the induction principle
   that Coq will generate for the following datatype.
   Write down your answer on paper, and then compare it
   with what Coq prints. *)
Inductive rgb : Set :=
  | red : rgb
  | green : rgb
  | blue : rgb.
Check rgb_ind.

Inductive natlist : Set :=
  | nnil : natlist
  | ncons : nat -> natlist -> natlist.
Check natlist_ind.
(* Yields (modulo a little tidying):
     natlist_ind :
        forall P : natlist -> Prop,
           P nnil 
        -> (forall (n : nat) (l : natlist), P l -> P (ncons n l)) 
        -> forall n : natlist, P n 
*)
(* EXERCISE (one star): Suppose we had written the above
   definition a little differently: *)
Inductive natlist1 : Set :=
  | nnil1 : natlist1
  | nsnoc1 : natlist1 -> nat -> natlist1.
(* Now what will the induction principle look like? *)
   
(* From these examples, we can extract this general rule:

      - each constructor c takes argument types a1...an
      - each ai can be either t (the datatype we are
        defining) or some other type s
      - the corresponding case of the induction principle
        says (in English),

          "for all values x1...xn of types a1...an, 
           if P holds for each of the xs of type t,
           then P holds for (c x1 ... xn)"
*)

(* EXERCISE (one star): Here is an induction principle for
   an inductively defined set s.

      ExSet_ind :
         forall P : ExSet -> Prop,
             (forall b : bool, P (con1 b))
          -> (forall (n : nat) (e : ExSet), P e -> P (con2 n e))
          -> forall e : ExSet, P e

  Give an [Inductive] definition of ExSet:

Inductive ExSet : Set :=
FILL IN HERE

*)

(* Now, what about polymorphic datatypes?

   The inductive definition of polymorphic lists

     Inductive list (X:Set) : Set :=
       | nil : list X
       | cons : X -> list X -> list X.

   is very similar.  The main difference is that, here, the
   whole definition is PARAMTERIZED on a set [X] -- i.e., we
   are defining a FAMILY of inductive types [list X], one
   for each [X].  Note that, wherever [list] appears in the
   body of the declaration, it is always applied to the
   parameter [X].  The induction principle is likewise
   parameterized on [X]:

     list_ind :
       forall (X : Set) (P : list X -> Prop),
            P []
         -> (forall (x : X) (l : list X), P l -> P (x :: l))
         -> forall l : list X, P l

   Note the wording here (and, accordingly, the form of
   [list_ind]): The WHOLE induction principle is
   parameterized on [X].  That is, [list_ind] can be thought
   of as a polymorphic function that, when applied to a set
   [X], gives us back an induction principle specialized to
   [list X]. *)

(* EXERCISE (one star): Write out the induction principle
   that Coq will generate for the following datatype.
   Compare your answer with what Coq prints. *)
Inductive tree (X:Set) : Set :=
  | leaf : X -> tree X
  | node : tree X -> tree X -> tree X.
Check tree_ind.

(* THOUGHT EXERCISE (not to be handed in): Find an inductive
   definition that gives rise to the following induction
   principle:
      mytype_ind :
        forall (X : Set) (P : mytype X -> Prop),
            (forall x : X, P (constr1 X x))
         -> (forall n : nat, P (constr2 X n))
         -> (forall m : mytype X, P m -> forall n : nat, 
                                           P (constr3 X m n))
         -> forall m : mytype X, P m                       *)

(* THOUGHT EXERCISE (not to be handed in): Find an inductive
   definition that gives rise to the following induction
   principle:
      foo_ind :
        forall (X Y : Set) (P : foo X Y -> Prop),
             (forall x : X, P (bar X Y x))
          -> (forall y : Y, P (baz X Y y))
          -> (forall f1 : nat -> foo X Y,
               (forall n : nat, P (f1 n)) -> P (quux X Y f1))
          -> forall f2 : foo X Y, P f2       *)

(* EXERCISE (one star): Consider the following inductive
   definition: *)

Inductive foo' (X:Set) : Set :=
  | C1 : list X -> foo' X -> foo' X
  | C2 : foo' X.

(* What induction principle will Coq generate for foo'? 
   (FILL IN THE BLANKS, then check your answer with Coq.)

     foo'_ind :
        forall (X : Set) (P : foo' X -> Prop),
              (forall (l : list X) (f : foo' X),
                    ______________________ -> _______________________)
          -> _________________________________________________
          -> forall f : foo' X, _______________________________
*)

(* ----------------------------------------------------- *)
(* Induction hypotheses *)

(* The induction principle for numbers

       forall P : nat -> Prop,
            P 0 
         -> (forall n : nat, P n -> P (S n)) 
         -> forall n : nat, P n

   is a generic statement that holds for all propositions
   [P] (strictly speaking, for all families of
   propositions [P] indexed by a number [n]).  Each time
   we use this principle, we are choosing [P] to be a
   particular expression of type [nat->Prop].

   We can make the proof more explicit by giving this
   expression a name. *)

Definition P_m0r (n:nat) : Prop := 
  mult n 0 = 0.
(* ... or equivalently... *)
Definition P_m0r' : nat->Prop := 
  fun n => mult n 0 = 0.

Theorem mult_0_r'' : forall n:nat, 
  P_m0r n.
Proof.
  apply nat_ind.
  Case "n = O". unfold P_m0r. reflexivity.
  Case "n = S n'". 
    (* Note the proof state at this point! *)
    unfold P_m0r. simpl. intros n IHn. 
    rewrite -> IHn. reflexivity.
Qed.

(* ----------------------------------------------------- *)
(* A closer look at the [induction] tactic *)

(* The [induction] tactic actually does quite a bit of
   low-level bookkeeping for us.

   Recall the informal statement of the induction principle
   for natural numbers:

     If [P n] is some proposition involving a natural number
     n, and we want to show that P holds for ALL numbers n,
     we can reason like this:

        - show that [P O] holds
        - show that, if [P n'] holds, then so does [P (S n')]
        - conclude that [P n] holds for all n.

   So, when we begin a proof with [intros n] and then
   [induction n], we are first telling Coq to consider a
   PARTICULAR [n] (by introducing it into the context) and
   then telling it to prove something about ALL numbers (by
   using induction).

   What Coq actually does in this situation, internally, is
   to "re-generalize" the variable we perform induction on.
   For example, in the proof above that [plus] is
   associative...
*)
Theorem plus_assoc' : forall n m p : nat, 
  plus n (plus m p) = plus (plus n m) p.   
Proof.
  (* ...we first introduce all 3 variables into the context,
     which amounts to saying "Consider an arbitrary [n], [m], and
     [p]..." *)
  intros n m p. 
  (* ...We now use the [induction] tactic to prove [P
     n] (that is, [plus n (plus m p) = plus (plus n m) p])
     for ALL [n], and hence also for the particular [n] that
     is in the context at the moment. *)
  induction n as [| n'].
  Case "n = O". reflexivity.
  Case "n = S n'". 
    (* In the second subgoal generated by [induction] --
       the "inductive step" -- we must prove that [P n']
       implies [P (S n')] for all [n'].  The [induction]
       tactic automatically introduces [n'] and [P n'] into
       the context for us, leaving just [P (S n')] as the
       goal. *)
    simpl. rewrite -> IHn'. reflexivity.
Qed.

(* It also works to apply [induction] to a variable that is
   quantified in the goal. *)
Theorem plus_comm' : forall n m : nat, 
  plus n m = plus m n.
Proof.
  induction n as [| n']. 
  Case "n = O". intros m. rewrite -> plus_0_r. reflexivity.
  Case "n = S n'". intros m. simpl. rewrite -> IHn'. 
    rewrite <- plus_n_Sm. reflexivity.
Qed.
(* Note that [induction n] leaves [m] still bound in the
   goal -- i.e., what we are proving inductively is a
   statement beginning with [forall m]. *)

(* If we do [induction] on a variable that is quantified in
   the goal AFTER some other quantifiers, the [induction]
   tactic will automatically introduce these quantifiers
   into the context. *)
Theorem plus_comm'' : forall n m : nat, 
  plus n m = plus m n.
Proof.
  (* Let's do induction on [m] this time, instead of
     [n]... *)
  induction m as [| m']. 
  Case "m = O". simpl. rewrite -> plus_0_r. reflexivity.
  Case "m = S m'". simpl. rewrite <- IHm'.
    rewrite <- plus_n_Sm. reflexivity.
Qed.

(* EXERCISE (one star): Rewrite the previous two theorems
   and their proofs in the same style as [mult_0_r'']
   above -- i.e., give, for each, an explicit [Definition]
   of the proposition being proved by induction and state
   the theorem and proof in terms of this defined
   proposition.  *)

(* ----------------------------------------------------- *)
(* A quick digression, for adventurous souls... If we can
   define parameterized propositions using [Definition],
   then can we also use [Fixpoint]?  Of course we can!
   However, this kind of "recursive parameterization"
   doesn't correspond to anything very familiar from
   everyday mathematics.  The following exercise gives a
   slightly contrived example. *)

(** <<
(* Define a recursive function [true_upto_n_implies_true_everywhere] 
   that makes [true_upto_n_example] work. *)
Fixpoint true_upto_n__true_everywhere 
(* OPTEXERCISE...*)
  (n:nat) (P:nat->Prop) {struct n} : Prop :=
  match n with
  | 0 =>    (forall m, P m)
  | S n' => (P (S n') -> true_upto_n__true_everywhere n' P)
  end.

Example true_upto_n_example :
    (true_upto_n__true_everywhere 3 (fun n => even n))
  = (even 3 -> even 2 -> even 1 -> forall m : nat, even m).
Proof. reflexivity. Qed.
>> *)

(* ---------------------------------------------------------- *)
(* Generalizing induction hypotheses *)

(* Last week's homework included a proof that the [double]
   function is injective.  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 here?  

   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 *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

      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 any
   *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.

(* So what we've learned 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 a nat m be given.  We prove:

    For any n, if double n = double m then n = m

  by induction on m.

  In the base case, we have m = 0.  Let a nat n be given
  such that double n = double m.  Since m = 0, we have
  double n = 0.  If n = S n' for some n', then double n =
  S (S (double n')) by the definition of double.  This
  would be a contradiction of the assumption that double n
  = 0, so n = 0, and thus n = m.

  In the inductive case, we have m = S m' for some nat m'.
  Let a nat n be given such that double n = double m.  By
  the definition of double, we therefore have:
    double n = S (S (double m'))

  If n = 0, then double n = 0 (by the definition of double),
  which we have just seen is not the case.  Thus, n = S n'
  for some n', and we have:
    S (S (double n')) = S (S (double m'))
  which implies that double n' = double m'.

  But observe that our inductive hypothesis here is: 
    for any n, if double n = double m' then n = m'

  Applying this for n' then yields n' = m', and it follows
  directly that S n' = S m'.  Since S n' = n and S m' = m,
  this is just what we wanted to show.

 *)

Theorem plus_n_n_injective_take2 : forall n m,
     plus n n = plus m m
  -> n = m.
Proof.
  (* Carry out this proof by induction on [m]. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem index_after_last : forall (n : nat) (X : Set) 
                              (l : list X),
     length l = n
  -> index (S n) l = None.
Proof.
  (* Prove this by induction on [l] *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* EXERCISE: Write an informal proof corresponding to your
   coq proof of [index_after_last]:

    Theorem: For any nat n and list l, if length l = n then
      index (S n) l = None.

    Proof:
    (* FILL IN HERE *)

*)

Theorem length_snoc''' : forall (n : nat) (X : Set) 
                              (v : X) (l : list X),
     length l = n
  -> length (snoc l v) = S n. 
Proof.
  (* Prove this by induction on [l]. *)
  (* OPTIONAL EXERCISE *) Admitted.

Theorem eqnat_false_S : forall n m,
  beq_nat n m = false -> beq_nat (S n) (S m) = false.
Proof.
  (* Prove this by induction on [m]. *)
  (* OPTIONAL EXERCISE *) Admitted.

Theorem length_append_cons : forall (X : Set) (l1 l2 : list X) 
                                  (x : X) (n : nat),
     length (l1 ++ (x :: l2)) = n
  -> S (length (l1 ++ l2)) = n.
Proof.
  (* Prove this by induction on [l1], without using [length_append]. *)
  (* OPTIONAL EXERCISE *) Admitted.
Theorem length_appendtwice : forall (X:Set) (n:nat) 
                                    (l:list X),
     length l = n
  -> length (l ++ l) = plus n n.
Proof.
  (* Prove this by induction on [l], without using length_append. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* --------------------------------------------------- *)
(* --------------------------------------------------- *)
(* --------------------------------------------------- *)
(* Constructing Evidence *)
   
(* One of the first examples in the discussion of
   propositions involved the concept of evenness.  It is
   important to notice that we have two rather different
   ways of talking about this concept:

     - a computation [evenb n] that CHECKS evenness,
       yielding a boolean
     
     - a proposition [even n] (defined in terms of
       [evenb]) that ASSERTS that [n] is even.

   There is another way of defining what it means to say
   that a number is even.  Instead of going "indirectly"
   via the [evenb] function, we can give a "direct"
   definition of evenness by saying, straight out, what we
   would be willing to accept as EVIDENCE that a given
   number is even.  *)

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

(* Informally, this definition says that there are two
   ways to give evidence that a number [m] is even:
   observe that it is zero, or observe that [n = S (S m)]
   for some [m], if we have evidence that [m] itself is
   even.  The constructors [ev_0] and [ev_SS] are names
   for these different ways of giving evidence for
   evenness.

   The role of ":" here is interesting.  Before, we've
   written "e : t" in situations where either [e] is an
   expression denoting a value and [t] is the type of this
   value or else where [e] is an expression describing
   some set and [t] is [Set].  In both cases, the ":" is
   pronounced "is a" or, more formally, "is classified by"
   or "has type."  Here, the type is a proposition and the
   thing that has that type is evidence for the
   proposition.

   In other words, we are thinking of a proposition as
   analogous to a set... a set of PROOFS (or evidence)!
   Saying "[e] has type [P]" (where [P] is a proposition)
   and saying "[e] is a proof of [P]" are exactly the same
   thing.

   The analogy 

                 propositions  ~  sets
                 proofs        ~  data values 

   is called the CURRY-HOWARD CORRESPONDENCE (or,
   sometimes, the CURRY-HOWARD ISOMORPHISM).  A great many
   things follow from it.

   First, just as a set can be empty, a singleton, finite,
   or infinite, a proposition may be "inhabited" by zero,
   one, many, or infinitely many proofs.  This makes
   sense: each inhabitant of a proposition [P] is a
   different way of giving evidence for [P].  If there are
   none, then [P] is not provable.  If there are many,
   then [P] has many different proofs.

   Second, the [Inductive] construction means exactly the
   same thing whether we are using it to define sets of
   data values (in the [Set] world) or sets of evidence.
   Let's look at the parts of the inductive definition of
   [ev] above:
      - The first line declares that [ev] is a
        proposition indexed by a natural number 
      - The second line declares that the constructor
        [ev_0] can be taken as evidence for the assertion
        [ev O].
      - The third line declares that, if [n] is a number
        and [E] is evidence for the assertion [ev n]),
        then [ev_SS n E] can be taken as evidence for
        [ev (S (S n))].  That is, we can construct
        evidence that [S (S n)] is even by applying the
        constructor [ev_SS] to evidence that [n] is
        even. 

   For example, here is a proof that [4] is even: *)

Definition four_ev : ev 4 :=
  ev_SS 2 (ev_SS 0 ev_0).

(* EXERCISE (one star): What are the [2] and [0] doing there? *)

(* Hang on a minute!  Until now, we've constructed proofs
   by giving sequences of tactics that eventually caused
   Coq to say "Proof completed."  Is this something new?

   No, it is not.  Here's the real story.  In Coq, a proof
   of a proposition [P] is a precisely term of type [P].
   So the fact that the above [Definition] typechecks
   means that [four_ev] really is a proof of [ev 4].
   The other way of giving proofs in Coq -- using
   [Theorem... Proof... Qed] -- is just a different
   notation for doing exactly the same thing.  To see
   this, let's write a proof that four is even in the more
   familiar way. *)

Theorem four_ev' :
  ev 4.
Proof.
  apply ev_SS. apply ev_SS. apply ev_0. 
Qed.
(* It's worth working through this proof slowly to make
   sure you understand what each [apply] is doing and why
   it makes sense to use [apply] with the constructors of
   [ev] instead of with hypotheses and theorems, as
   we've been doing. *)

(* Notice the similarity between the first two lines of
   this theorem and the previous [Definition] of
   [four_ev]: they can be read "[four_ev'] is
   evidence for the proposition [ev 4]."  But there's
   more.  The theorem actually builds a PROOF OBJECT that
   embodies the evidence that 4 is even.  Let's look at
   it: *)

Print four_ev'.  

(* Proof objects are the "bedrock" of reasoning in Coq.
   Tactic proofs are convenient shorthands that instruct
   Coq how to construct proof objects for us instead of
   our writing them out explicitly.  (Here, of course, the
   proof object is actually shorter than the tactic proof.
   But the proof objects for more interesting proofs can
   become quite large and complex -- building them by hand
   would be painful.)

   Third, the correspondence between values and proofs
   induces a strong correpondence between FUNCTIONS and
   PROOFS OF HYPOTHETICAL PROPOSITIONS.  For example,
   consider the proposition

      forall n, ev n -> ev (plus 4 n).

   This can be read "assuming we have evidence that [n] is
   even, we can construct evidence that [plus 4 n] is
   even."  Viewed differently, it is the type of a
   function taking a number [n] and evidence that [n] is
   even and yielding evidence that [plus 4 n] is even. *)   

Definition ev_plus4 : forall n, ev n -> ev (plus 4 n) :=
  fun (n : nat) => 
     fun (E : ev n) => 
       ev_SS (S (S n)) (ev_SS n E).
   
(* For comparison, here is a tactic proof of the same proposition. *)
Theorem ev_plus4' : forall n,
  ev n -> ev (plus 4 n).
Proof.
  intros n E. simpl. apply ev_SS. apply ev_SS. apply E.
Qed.

(* Again, the proof object constructed by this tactic
   proof is identical to the one that we built by hand. *)
Print ev_plus4'.

(* Fourth, just as hypothetical propositions have "arrow
   [implication] types", the USE of a hypothetical
   proposition exactly corresponds to function application.  

   For example, consider this theorem: *)
Definition ev_ten : ev 10 :=
  ev_plus4 6 (ev_plus4 2 (ev_SS 0 ev_0)).

(* Fifth, and finally, SIMPLIFICATION of expressions
   denoting data values also has an analog in the world of
   propositions and proofs.  Just as the computational expression
   [plus 4 (plus 4 2)] simplifies to [10]... *)
Eval simpl in (plus 4 (plus 4 2)).
(* ... the proof term [ev_ten], which contains two
   applications of the theorem [ev_plus4] (which we
   defined above as a function), can be simplified to a
   direct proof of the same proposition: *)
Eval compute in (ev_plus4 6 (ev_plus4 2 (ev_SS 0 ev_0))).
(* (Note that we have to use the more aggressive [Eval
   compute] rather than just [Eval simpl] to get Coq to
   unfold the definitions here.) *)

(* To summarize: The Curry-Howard Correspondence is a
   powerful conceptual tool, establishing deep and
   fruitful links between programming languages and
   mathematical logic.  Closer to home, it is the backbone
   for the organization of Coq.

       [PICTURE GOES HERE]

   Of course, this is just the backbone.  There are lots
   of other types (and their inhabitants) that this
   picture doesn't show.  For example, there is
   [Set->Set], which is the type of things like [list],
   there is [(nat->Prop)->Prop], the type of things like
   [nat_ind], and so on. *)

(* EXERCISE: Construct a tactic proof of the following
   proposition. *)
Theorem double_even : forall n,
  ev (double n).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* EXERCISE (optional and challenging): Try to predict
   what proof object is constructed by the above tactic
   proof.  (Before checking your answer, you'll want to
   strip out any uses of [Case], as these will make the
   proof object a bit cluttered.) *)

(* ------------------------------------------------------- *)
(* Manipulating Evidence *)

(* Besides CONSTRUCTING evidence of evenness, we can also
   REASON ABOUT evidence of evenness.  The fact that we
   introduced [ev] with an [Inductive] declaration
   tells us not only that the constructors [ev_O] and
   [ev_SS] are ways to build evidence of evenness, but
   also that these two constructors are the ONLY ways that
   evidence of evenness can be built.  

   In other words, if someone gives us evidence [E]
   justifying the assertion [ev n], then we know that
   [E] can only have one of two forms: either [E] is
   [ev_0] (and [n] is [O]), or [E] is [ev_SS m E'],
   where [n = S (S n')] and [E'] is evidence that [n'] is
   even.

   Thus, it makes sense to use all the tactics that we
   have already seen for inductively defined DATA to
   reason instead about inductively defined EVIDENCE.

   For example, here we use a [destruct] on evidence that
   [n] is even in order to show that [ev n] implies
   [ev (n-2)].  (Recall that [pred 0] is [0].)  *)
Theorem ev_minus2: forall n,
  ev n -> ev (pred (pred n)). 
Proof.
  intros n E.
  destruct E as [| n' E'].
  Case "E = ev_0". simpl. apply ev_0. 
  Case "E = ev_SS n' E'". simpl. apply E'.
Qed.
(* EXERCISE (one star): what happens if we try to
   [destruct] on [n] instead of [E]? *)

(* We can also perform INDUCTION on evidence that [n] is
   even. Here we use it show that the old [evenb] function
   returns [true] on [n] when [n] is even according to
   [ev]. *)
Theorem ev_even : forall n,
  ev n -> even n.
Proof.
  intros n E. induction E as [| n' E'].
  Case "E = ev_0". unfold even. reflexivity.
  Case "E = ev_SS n' E'".  
    unfold even. simpl. unfold even in IHE'. apply IHE'.
Qed.
(* EXERCISE (one star): Could this proof be carried out by
   induction on [n] instead of [E]? *)

(* EXERCISE: The following proof attempt will not succeed.

     Theorem l : forall n,
       ev n.
     Proof.
       intros n. induction n.
         Case "O". simpl. apply ev_0.
         Case "S".
           ...

   Briefly explain why.

(* FILL IN HERE *)

*)

(* Here's another exercise requiring induction. *)
Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Here's another situation where we want analyze evidence
   for evenness and build two sub-goals. *)
Theorem SSev_ev_firsttry : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  destruct E as [| n' E'].
  (* Oops. [destruct] destroyed far too much! *)
Admitted.

(* The right thing to use here is [inversion] (!) *)
Theorem SSev_even : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E. inversion E as [| n' E']. apply E'.
Qed.
Print SSev_even.
(* This use of [inversion] may seem a bit mysterious at
   first.  Until now, we've only used [inversion] on
   equality propositions, to utilize injectivity of
   constructors or to discriminate between different
   constructors.  But we see here that [inversion] can
   also be applied to analyzing evidence for inductively
   defined propositions.  

   Here's how [inversion] works in general.  Suppose the
   name [I] refers to an assumption [P] in the current
   context, where [P] has been defined by an [Inductive]
   declaration.  Then, for each of the constructors of
   [P], [inversion I] generates a subgoal in which [I] has
   been replaced by the exact, specific conditions under
   which this constructor could have been used to prove
   [P].  Some of these subgoals will be
   self-contradictory; [inversion] throws these away.  The
   ones that are left represent the cases that must be
   proved to establish the original goal.

   In this particular case, the [inversion] analyzed the
   construction [ev (S (S n))], determined that this
   could only have been constructed using [ev_SS], and
   generated a new subgoal with the arguments of that
   constructor as new hypotheses.  (It also produced an
   auxiliary equality, which happens to be useless.)
   We'll begin exploring this more general behavior of
   inversion in what follows. *)

(* A simple exercise for practice with [inversion]. *)
Theorem SSSSev_even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* [inversion] can also be used to derive goals by showing
   absurdity of a hypothesis. *)
Theorem even5_nonsense : 
  ev 5 -> plus 2 2 = 9.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* We can generally use [inversion] instead of [destruct]
   on inductive propositions.  This illustrates that in
   general, we get one case for each possible constructor.
   Again, we also get some auxiliary equalities which are
   rewritten in the goal but not in the other
   hypotheses. *)
Theorem ev_minus2': forall n,
  ev n -> ev (pred (pred n)). 
Proof.
  intros n E. inversion E as [| n' E']. 
  Case "E = ev_0". simpl. apply ev_0. 
  Case "E = ev_SS n' E'". simpl. apply E'.
Qed.

(* One last exercise.  (Finding the appropriate thing to
   do induction on is a bit tricky here.) *)
Theorem ev_ev_even : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ----------------------------------------------------- *)
(* More on inductively defined propositions *)

(* We have seen that the proposition "some number is even"
   can be phrased in two different ways -- indirectly, via
   a testing function [evenb], or directly, by inductively
   describing what constitutes evidence for evenness.
   These two ways of defining evenness are about equally
   easy to state and work with.

   However, for many other properties of interest, the
   direct inductive definition is preferable, since
   writing a testing function may be awkward or even
   impossible.  For example, consider the property MyProp
   defined as follows:

       1) the number 4 has property MyProp
       2) if n has property MyProp, then so does 4+n
       3) if n+2 has property MyProp, then so does n
       4) no other numbers have property MyProp

   This is a perfectly sensible definition of a set of
   numbers, but we cannot translate this definition
   directly as a Coq Fixpoint (or translate it directly
   into a recursive function in any other programming
   language).  We might be able to find a clever way of
   testing this property using a Fixpoint (indeed, it is
   not even too hard to find one in this case), but in
   general this could require arbitrarily much thinking.
   In fact, if the property we are interested in is
   uncomputable, then we cannot define it as a Fixpoint no
   matter how hard we try, because Coq requires that all
   Fixpoints correspond to terminating computations.

   On the other hand, writing an inductive definition of
   what it means to give evidence for the property MyProp
   is straightforward:
*)
Inductive MyProp : nat -> Prop :=
  | MyProp1 : MyProp 4
  | MyProp2 : forall n:nat, MyProp n -> MyProp (plus 4 n)
  | MyProp3 : forall n:nat, MyProp (plus 2 n) -> MyProp n.
(* The first three clauses in the informal definition of
   MyProp above are reflected in the first three clauses of
   the inductive definition.  The fourth clause is the
   precise force of the keyword [Inductive]. *)

(* As we did with evenness, we can now construct evidence
   that certain numbers satisfy [MyProp]. *)
Theorem MyProp_ten : MyProp 10.
Proof.
  apply MyProp3. simpl. 
  assert (12 = plus 4 8) as H12.
    Case "Proof of assertion". reflexivity.
  rewrite -> H12. 
  apply MyProp2. 
  assert (8 = plus 4 4) as H8.
    Case "Proof of assertion". reflexivity.
  rewrite -> H8.
  apply MyProp2. 
  apply MyProp1. 
Qed.

(* Here are two useful facts about MyProp.  (The proofs
   are left to you.) *)
Theorem MyProp_0 : MyProp 0.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem MyProp_plustwo : forall n:nat, MyProp n -> MyProp (S (S n)).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* With these, we can show that MyProp holds of all even
   numbers, and vice versa. *)
Theorem MyProp_ev : forall n:nat, 
  ev n -> MyProp n.
Proof.
  intros n E.
  induction E as [| n' E'].  
  Case "E = ev_0".
    apply MyProp_0.
  Case "E = ev_SS n' E'".
    apply MyProp_plustwo. apply IHE'.
Qed.

(* Here's an informal proof of this theorem:

   Theorem : For any nat n, if ev n then MyProp n.

   Proof: Let a nat n and a derivation E of ev n be given.
    We go by induction on E.  There are two case:

    1) If the last step in E is a use of ev_0, then n is 0.
      But we know by lemma MyProp_0 that MyProp 0, so the
      theorem is satisfied in this case.

    2) If the last step in E is by ev_SS, then n = S (S n')
      for some n' and there is a derivation of ev n'.  By
      lemma MyProp_plustwo, it's enough to show MyProp n'.
      This follows directly from the inductive hypothesis
      for the derivation of (ev n').
 *)

Theorem ev_MyProp : forall n:nat, 
  MyProp n -> ev n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* EXERCISE: Write an informal proof corresponding to your
   formal proof of ev_MyProp:

   Theorem: For any nat n, if MyProp n then ev n.

   Proof:
   (* FILL IN HERE *)

 *)

(* CHALLENGE PROBLEM: do MyProp_ev and ev_MyProp again by
   constructing explicit proof objects. *)
(* FILL IN HERE (OPTIONALLY) *)

Theorem ev_MyProp' : forall n:nat, 
  MyProp n -> ev n.
Proof.
  (* Complete this proof using [apply MyProp_ind] instead
     of the [induction] tactic. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.


(* --------------------------------------------------- *)
(* Induction principles for inductively defined Props *)


(* We didn't have time for the following discussion in
   class, but we'll discuss it on Monday.  For now, read
   this comment and try the thought exercise below.  Also,
   don't forget the (unrelated) palindrome exercise at the
   bottom of the file.*)

(* The induction principles for inductively defined
   propositions like [ev] are a tiny bit more complicated
   than the ones for inductively defined sets.
   Intuitively, this is because we want to use them to
   prove things by inductively considering the possible
   shapes that something in [ev] can have -- either it is
   evidence that [0] is even, or else it is evidence that,
   for some [n], [S (S n)] is even, and it includes
   evidence that [n] itself is.  But the things we want to
   prove are not statements about EVIDENCE, they are
   statements about NUMBERS.  So we want an induction
   principle that allows reasoning by induction on the
   former to prove properties of the latter.

   In English, the induction principle for [ev] goes like
   this:

      - Suppose, P is a predicate on natural numbers (that
        is, [P n] is a [Prop] for every [n]).  To show that
        [P n] holds whenever [n] is even, it suffices to
        show:
          -- [P] holds for [0]
          -- for any [n], if [n] is even and [P] holds for
            [n], then [P] holds for [S (S n)].

   Formally: *)
Check ev_ind.

(* We can apply [ev_ind] directly instead of using
   [induction], following pretty much the same pattern as
   above. *)
Theorem ev_even' : forall n,
  ev n -> even n.
Proof.
  apply ev_ind.
  Case "ev_0". unfold even. reflexivity.
  Case "ev_SS". intros n H IHE. unfold even. apply IHE.
Qed.

(* THOUGHT EXERCISE (not to be handed in, but strongly
   recommended -- there may well be questions like this on
   the midterm!).

   Write out the induction principles that Coq will generate
   for the inductive declarations [list] and [MyProp].
   Compare your answers against the results Coq prints for
   the following queries. *)
Check list_ind.
Check MyProp_ind.

(* Exercise:

   A palindrome is a sequence that reads the same backwards as forwards.

   (1) Define an inductive proposition [pal] on [list nat] that captures
   what it means to be a palindrome. (Hint: You'll need three cases.)

   (2) Prove that 

   forall l, pal(l++(rev l))

   (3) Prove that 

   forall l, pal l => l = rev l.

   Note: The converse thoerem 

   forall l, l = rev l => pal l.

   is much harder!  We won't have the tools to attack this for some time... *)

(* FILL IN HERE *)