(** * Props: Programming with Propositions *)
(* Version of 9/10/2009 *)

Require Export Poly.

(* ################################################################## *)
(** * Quick Review *)

(** We've now seen a bunch of Coq's fundamental tactics --
    enough, in fact, to do pretty much everything we'll want for
    a while.  We'll introduce one or two more as we go along
    through the next few lectures, and later in the course we'll
    introduce some more powerful _automation_ tactics that make
    Coq do more of the low-level work in many cases, but
    basically this is the set we need. *)

(** 
  - [intros]
  
    move hypotheses/variables from goal to context 
  
  - [reflexivity]

    finish the proof (when the goal looks like [e = e])

  - [apply]

    prove goal using a hypothesis, lemma, or constructor

  - [apply... in H] 

    apply a hypothesis, lemma, or constructor to a hypothesis in
    the context (forward reasoning)

  - [apply... with...]

    explicitly specify values for variables that cannot be
    determined by pattern matching

  - [simpl]
  
    simplify computations in the goal 

  - [simpl in H]

    ... or a hypothesis 

  - [rewrite]

    use an equality to rewrite the goal 

  - [rewrite ... in H]

    ... or a hypothesis 

  - [unfold]
  
    replace a defined constant by its RHS in the goal 

  - [unfold... in H]

    ... or a hypothesis  

  - [destruct... as...]

    case analysis on values of inductively defined types 

  - [induction... with...]

    induction on values of inductively defined types [inversion]
    reason by injectivity and distinctness of constructors

  - [remember (e) as x]

    give a name ([x]) to an expression ([e]) so that we can
    destruct [x] without "losing" [e]

  - [assert (e) as H]

    introduce a "local lemma" [e] and call it [H] *)

(* ##################################################### *)
(** * Programming with Propositions *)

(** A _proposition_ is a statement expressing a factual
    claim.  In Coq, propositions are written as expressions of
    type [Prop].  Although we haven't mentioned it explicitly, we
    have already seen numerous examples of such expressions. *)
(* 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). *)

(** Both [plus 2 2 = 4] and [plus 2 2 = 5] are valid
    expressions of type [Prop]. *)

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

(** But they can be used in many other ways.  For example,
    we can give a name to a proposition using a [Definition],
    just as we have given names to expressions of other
    sorts (numbers, functions, types, type functions, ...). *)

Definition plus_fact : Prop  :=  plus 2 2 = 4.
(* Check plus_fact. *)

(** Now we can use this name in any situation where a proposition
    is expected -- for example, as the subject of a theorem. *)

Theorem plus_fact_is_true : 
  plus_fact.
Proof. reflexivity.  Qed.

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

(** This defines [even] as 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-percent 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 last one 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.

(** That is, [nat_induction] expresses exactly the
    _principle of induction_ for natural numbers that we've been
    using for most of our proofs about numbers.  Indeed, we can
    use the [induction] tactic to prove very straightforwardly
    that [nat_induction P] holds for all [P]. *)

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. *)
(* ===> nat_ind : forall P : nat -> Prop,
                    P 0 
                 -> (forall n : nat, P n -> P (S n)) 
                 -> forall n : nat, P n *)

(** The ":" here can be pronounced "...is a theorem proving
    the proposition..." *)

(** In general, every time we declare a new datatype [t]
    with [Inductive], Coq automatically generates an _axiom_
    [t_ind] (i.e., a theorem whose truth is assumed rather than
    being proved from other axioms).  This axiom expresses the
    induction principle for [t].  The [induction] tactic is a
    straightforward wrapper that, at its core, simply performs
    [apply t_ind].

    To see this more clearly, let's experiment a little with
    using [apply nat_ind] directly, instead of [induction], to
    carry out some proofs.

    First, here is a direct proof of the validity of our
    formulation of the induction principle.  The proof amounts to
    observing that, after unfolding the names we defined, our
    principle coincides with the built-in one. *)

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. *)
(** For example, here's an alternate proof of a theorem
    that we saw in the [Basics] chapter: *)

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.

(** Several details in this proof are worth noting.  First,
    in the induction step of the proof (the ["S"] case), we have
    to do a little bookkeeping manually (the [intros]) that
    [induction] does automatically.  

    Second, we do not introduce [n] into the context before
    applying [nat_ind] -- the conclusion of [nat_ind] is a
    quantified formula, and [apply] needs this conclusion to
    exactly match the shape of the goal state, including the
    quantifier.  The [induction] tactic works either with a
    variable in the context or a quantified variable in the goal.

    Third, the [apply] tactic automatically chooses variable
    names for us (in the second subgoal, here), whereas
    [induction] lets us specify (with the [as...]  clause) what
    names should be used.  The automatic choice is actually a
    little unfortunate, since it re-uses the name [n] for a
    variable that is different from the [n] in the original
    theorem.  This is why the [Case] annotation is just [S] -- if
    we tried to write it out in the more explicit form that we've
    been using for most proofs, we'd have to write [n = S n],
    which doesn't make a lot of sense!  All of these conveniences
    make [induction] nicer to use in practice than applying
    induction principles like [nat_ind] directly.  But it is
    important to realize that, modulo this little bit of
    bookkeeping, applying [nat_ind] is what we are really
    doing. *)

(** **** Exercise: 2 stars *)
(** Complete this proof without using the [induction] tactic. *)

Theorem plus_one_r' : forall n:nat, 
  plus n 1 = S n.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars *)
(** 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. 

    Prove the same theorem again without [induction] or [apply
    nat_ind]. *)

Theorem plus_one_r'' : forall n:nat, 
  plus n 1 = S n.
Proof.
  (* FILL IN HERE *) 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 : Type :=
  | yes : yesno
  | no : yesno.

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

(** **** Exercise: 1 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 : Type :=
  | red : rgb
  | green : rgb
  | blue : rgb.
(* Check rgb_ind. *)
(** [] *)

Inductive natlist : Type :=
  | nnil : natlist
  | ncons : nat -> natlist -> natlist.

(* Check natlist_ind. *)
(* ===> (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: 1 star *)
(** Suppose we had written the above definition a little
   differently: *)

Inductive natlist1 : Type :=
  | 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 [x]s of type [t], then [P]
           holds for [c x1 ... xn]". *)

(** **** Exercise: 1 star (ExSet) *)
(** Here is an induction principle for an inductively defined
    set.
[[
      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 : Type :=
(* FILL IN HERE *)
*)
(** [] *)

(** Now, what about polymorphic datatypes?

    The inductive definition of polymorphic lists
[[ 
      Inductive list (X:Type) : Type :=
        | 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 : Type) (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: 1 star *)
(** Write out the induction principle that Coq will generate for
   the following datatype.  Compare your answer with what Coq
   prints. *)
Inductive tree (X:Type) : Type :=
  | leaf : X -> tree X
  | node : tree X -> tree X -> tree X.
(* Check tree_ind. *)
(** [] *)

(** **** Exercise: 1 star (mytype) *)
(** Find an inductive definition that gives rise to the
    following induction principle:
[[
      mytype_ind :
        forall (X : Type) (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                   
]]
*)

(** [] *)

(** **** Exercise: 1 star (foo) *)
(** Find an inductive definition that gives rise to the
    following induction principle:
[[
      foo_ind :
        forall (X Y : Type) (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: 1 star *)
(** Consider the following inductive definition: *)
Inductive foo' (X:Type) : Type :=
  | 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 : Type) (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. *)

(** For example, instead of stating the theorem [mult_0_r]
    as "[forall n, mult n 0 = 0]," we can write it as "[forall n,
    P_m0r n]", where [P_m0r] is defined as... *)

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.

(** This extra naming step isn't something that we'll do in
    normal proofs, but it is something that we should be _able_
    to do, because it allows us to see exactly what is the
    induction hypothesis.  If we prove [forall n, P_m0r n] by
    induction on [n] (using either [induction] or [apply
    nat_ind]), we see that the first subgoal requires us to prove
    [P_m0r 0] ("[P] holds for zero"), while the second subgoal
    requires us to prove [forall n', P_m0r n' -> P_m0r n' (S n')]
    (that is "[P] holds of [S n'] if it holds of [n']" or, more
    elegantly, "[P] is preserved by [S]").  The _induction
    hypothesis_ is the premise of this latter implication -- the
    assumption that [P] holds of [n'], which we are allowed to
    use in proving that [P] holds for [S n']. *)


(* ##################################################### *)
(** *** 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: 1 star (plus_comm) *)
(** 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 define them using [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. *)

(** **** Exercise: 4 stars, optional *)
(** Define a recursive function
    [true_upto_n_implies_true_everywhere] that makes
    [true_upto_n_example] work. *)
(** <<
Fixpoint true_upto_n__true_everywhere 
(* FILL IN HERE *)

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

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

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

(** **** 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, optional *)
(** Prove this by induction on [m]. *)
Theorem eqnat_false_S : forall n m,
  beq_nat n m = false -> beq_nat (S n) (S m) = false.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, optional *)
(** Prove this by induction on [l1], without using [app_length]. *)

Theorem length_append_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 *)
(** Prove this by induction on [l], without using app_length. *)

Theorem length_appendtwice : forall (X:Type) (n:nat) 
                                    (l:list X),
     length l = n
  -> length (l ++ l) = plus n n.
Proof.
  (* FILL IN HERE *) 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
    [Type].  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 [Type] 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: 1 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)). *)

(** ..f. 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 fthat 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 [Type->Type], which is the type of
    things like [list], there is [(nat->Prop)->Prop], the type of
    things like [nat_ind], and so on. *)

(** **** Exercise: 2 stars *)
(** Construct a tactic proof of the following proposition. *)

Theorem double_even : forall n,
  ev (double n).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 4 stars, optional (double_even_pfobj) *)
(** 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 n' E'] (and [n] is [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 [evf (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: 1 star (ev_minus2_n) *)
(** 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: 1 star (ev_even_n) *)
(** Could this proof be carried out by induction on [n] instead
    of [E]? *)
(** [] *)

(** **** Exercise: 3 stars (l_fails) *)
(** 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 *)
*)
(** [] *)

(** **** Exercise: 2 stars *)
(** Here's another exercise requiring induction. *)

Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof. 
  (* FILL IN HERE *) 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! 
     In the first sub-goal, we don't know that [n] is [0]. *)
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
    genefral behavior of inversion in what follows. *)

(** **** Exercise: 1 star (inversion_practice) *)

Theorem SSSSev_even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
  (* FILL IN HERE *) 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.
  (* FILL IN HERE *) 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
    getf 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.

(** **** Exercise: 3 stars *)
(** 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 *) 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:

       - the number 4 has property MyProp
       - if n has property MyProp, then so does 4+n
       - if n+2 has property MyProp, then so does n
       - 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.

(** **** Exercise: 2 stars (MyProp) *)
(** Here are two useful facts about MyProp.  (The proofs are left
    to you.) *)

Theorem MyProp_0 : MyProp 0.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem MyProp_plustwo : forall n:nat, MyProp n -> MyProp (S (S n)).
Proof.
  (* FILL IN HERE *) 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:

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

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

(** **** Exercise: 3 stars *)
Theorem ev_MyProp : forall n:nat, 
  MyProp n -> ev n.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars (ev_MyProp_informal) *)
(** 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 *)
[]
 *)

(** **** Exercise: 4 stars, optional (MyProp_pfobj) *)
(** Prove [MyProp_ev] and [ev_MyProp] again by constructing
    explicit proof objects by hand (as we did above in
    [ev_plus4], for example). *)
(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 3 stars *)
(** Complete this proof using [apply MyProp_ind] instead
    of the [induction] tactic. *)

Theorem ev_MyProp' : forall n:nat, 
  MyProp n -> ev n.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ##################################################### *)
(** * Induction principles in Prop *)

(** Last week, we looked in detail at the induction principles
    that Coq generates for inductively defined _sets_.
    Inductively defined _propositions_ are handled slightly
    differently.  For example, from what we've said so far, you
    might expect the inductive definition of [ev]
[[
    Inductive ev : nat -> Prop :=
       | ev_0 : ev O
       | ev_SS : forall n:nat, ev n -> ev (S (S n)).
]]
    to give rise to an induction principle that looks like this...
[[
    ev_ind_max :
       forall P : (forall n : nat, ev n -> Prop),
            P O ev_0
         -> (forall (n : nat) (e : ev n), 
              P n e -> P (S (S n)) (ev_SS n e))
         -> forall (n : nat) (e : ev n), P n e
]]
   ... because:

     - Since [ev] is indexed by a number [n] (every [ev] object
       [e] is a piece of evidence that some particular number [n]
       is even), the proposition [P] is parameterized by both [n]
       and [e] -- that is, the induction principle can be used to
       prove assertions involving both an even number and the
       evidence that it is even.

     - Since there are two ways of giving evidence of evenness
       ([ev] has two constructors), applying the induction
       principle generates two subgoals:

         - We must prove that [P] holds for [O] and [ev_0].

         - We must prove that, whenever [n] is an even number and
           [e] is evidence of its evenness, if [P] holds of [n]
           and [e], then it also holds of [S (S n)] and [ev_SS n
           e].

     - If these subgoals can be proved, then the induction
       principle tells us that [P] is true for _all_ even numbers
       [n] and evidence [e] of their evenness.

   But this is a little more flexibility than we actually need or
   want: it is giving us a way to prove logical assertions
   involving _evidence_ of evenness, while all we really care
   about is proving properties of _numbers_ that are even -- we
   are interested in assertions about numbers, not about
   evidence.  It would therefore be more convenient to have an
   induction principle for proving propositions [P] that are
   parameterized just by [n] and whose conclusion establishes [P]
   for all even numbers [n]:
[[
       forall P : nat -> Prop,
          ...
          -> forall n : nat, ev n -> P n
]]
   For this reason, Coq actually generates the following
   simplified induction principle for [ev]:
[[
     ev_ind :
       forall P : nat -> Prop,
            P O
         -> (forall n : nat, ev n -> P n -> P (S (S n)))
         -> forall n : nat, ev n -> P n
]]
   Similarly, from the inductive definition of the proposition
   [and A B]
[[
     Inductive and (A B : Prop) : Prop :=
       conj : A -> B -> (and A B).
]]
   we might expect Coq to generate this induction principle
[[
     and_ind_max :
       forall (A B : Prop) (P : A /\ B -> Prop),
            (forall (a : A) (b : B), P (conj A B a b))
         -> forall a : A /\ B, P a
]]
   but actually it generates this simpler and more useful one:
[[
     and_ind :
       forall A B P : Prop,
            (A -> B -> P)
         -> A /\ B -> P
]]
   In the same way, when given the inductive definition of [or A B]
[[
     Inductive or (A B : Prop) : Prop :=
       | or_introl : A -> or A B
       | or_intror : B -> or A B.
]]
   instead of the "maximal induction principle"
[[
     or_ind_max :
       forall (A B : Prop) (P : A \/ B -> Prop),
            (forall a : A, P (or_introl A B a))
         -> (forall b : B, P (or_intror A B b))
         -> forall o : A \/ B, P o
]]
   what Coq actually generates is this:
[[
     or_ind :
       forall A B P : Prop,
            (A -> P)
         -> (B -> P)
         -> A \/ B -> P
]]
*)

Module P.

(** **** Exercise: 3 stars (p_provability) *)
(** Consider the following inductively defined proposition: *)

    Inductive p : (tree nat) -> nat -> Prop :=
      | c1 : forall n, p (leaf _ n) 1
      | c2 : forall t1 t2 n1 n2,
                p t1 n1 -> p t2 n2 -> p (node _ t1 t2) (plus n1 n2)
      | c3 : forall t n, p t n -> p t (S n).

(** Describe, in English, the conditions under which the
   proposition [p t n] is provable. 

   (* FILL IN HERE *)
*)
(** [] *)

End P.

(* ####################################################### *)
(** * Informal proofs, again *)

(** Q: What is the relation between a formal proof of a 
       proposition P and an informal proof of the same proposition P?

    A: The latter should *teach* the reader how to produce the
       former.

    Q: How much detail is needed?

    A: There is no single right answer; rather, there is a range
       of choices.  

      At one end of the spectrum, we can essentially give the
      reader the whole formal proof (i.e., the informal proof
      amounts to just transcribing the formal one into words).
      This gives the reader the *ability* to reproduce the formal
      one for themselves, but it doesn't *teach* them anything.

      At the other end of the spectrum, we can say "The theorem
      is true and you can figure out why for yourself if you
      think about it hard enough."  This is also not a good
      teaching strategy, because usually writing the proof
      requires some deep insights into the thing we're proving,
      and most readers will give up before they rediscover all
      the same insights as we did.

      In the middle is the golden mean -- a proof that includes
      all of the essential insights (saving the reader the hard
      part of work that we went through to find the proof in the
      first place) and clear high-level suggestions for the more
      routine parts to save the reader from spending too much
      time reconstructing these parts (e.g., what the IH says and
      what must be shown in each case of an inductive proof), but
      not so much detail that the main ideas are obscured.

                           -----------------

   Another key point: if we're talking about a formal proof of a
   proposition P and an informal proof of P, the proposition P
   doesn't change.  That is, formal and informal proofs are
   _talking about the same world_ and they must _play by the same
   rules_.

   In particular, whether we are talking about formal or informal
   proofs, propositions and booleans are different things!

   - Booleans are _values_ in the _computational_ world.  Every
     expression of type [bool] (with no free variables) can be
     simplified to either [true] or [false].

   - Propositions are _types_ in the _logical_ world.  They are
     either _provable_ (i.e., there is some expression that has
     this type) or not (there is no such expression).  It doesn't
     make sense to say that a proposition is "equivalent to
     [true]," and it is not necessarily the case that, if a
     proposition [P] is not provable, then [~P] is provable.

     We do sometimes use the words "true" and "false" when
     referring to propositions.  Strictly speaking, we should
     not: a proposition is either provable or it is not.
*)

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

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

(** **** Exercise: 3 stars, optional (prop_ind) *)
(** 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. *)
(** [] *)

(* ####################################################### *)
(** *** Additional Exercises *)

(** **** Exercise: 2 stars, optional *)
(** The following proof attempt is not going to succeed.  Briefly
    explain why. *)

Lemma failed_proof : forall n,
  ev n.
Proof.
  intros n. induction n as [| n' ].
    Case "n = O". simpl. apply ev_0.
    Case "n = S n'".
      Admitted.

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 4 stars *)
(** A palindrome is a sequence that reads the same backwards as
    forwards.

    - Define an inductive proposition [pal] on [list nat] that
      captures what it means to be a palindrome. (Hint: You'll
      need three cases.)
 
    - Prove that 
[[
       forall l, pal(l++(rev l))
]]
    - 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 *)
(** [] *)