(* Polymorphism and higher-order functions
   Version of 2/22/2009
*)

Require Export Lists.

(* ---------------------------------------------------------------------- *)
(* Polymorphic lists *)

(* Lists of booleans *)
Inductive boollist : Set :=
  | bool_nil : boollist
  | bool_cons : bool -> boollist -> boollist.

(* A datatype for lists with elements drawn from any set X *)
Inductive list (X:Set) : Set :=
  | nil : list X
  | cons : X -> list X -> list X.

Check nil.
Check cons.

Check (cons nat 2 (cons nat 1 (nil nat))).

(* Polymorphic versions of some functions we've already seen *)
Fixpoint length (X:Set) (l:list X) {struct l} : nat := 
  match l with
  | nil      => 0
  | cons h t => S (length X t)
  end.

Check length.

Example test_length1 :
    length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.
Proof. reflexivity.  Qed.
Example test_length2 :
    length bool (cons bool true (nil bool)) = 1.
Proof. reflexivity.  Qed.

Fixpoint app (X : Set) (l1 l2 : list X) {struct l1} 
                : (list X) := 
  match l1 with
  | nil      => l2
  | cons h t => cons X h (app X t l2)
  end.

Fixpoint snoc (X:Set) (l:list X) (v:X) {struct l} : (list X) := 
  match l with
  | nil      => cons X v (nil X)
  | cons h t => cons X h (snoc X t v)
  end.
Fixpoint rev (X:Set) (l:list X) {struct l} : list X := 
  match l with
  | nil      => nil X
  | cons h t => snoc X (rev X t) h
  end.

(* Some examples with lists of different types.  Note that
   we are using [nil] and [cons] because we haven't yet
   defined the notations [] or ::. *)
Example test_rev1 :
    rev nat (cons nat 1 (cons nat 2 (nil nat))) 
  = (cons nat 2 (cons nat 1 (nil nat))).
Proof. reflexivity.  Qed.
Example test_rev2: 
  rev bool (nil bool) = nil bool.
Proof. reflexivity.  Qed.

(* -------------------------------------------------- *)
(* Argument synthesis *)

(* Supplying every type argument is boring... *)
Definition l_123 := 
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

(* ... but Coq can usually infer them -- just replace the
   type argument by _ and it will use unification to try
   to find a reasonable value. *)
Definition l_123' := cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

Fixpoint length' (X:Set) (l:list X) {struct l} : nat := 
  match l with
  | nil      => 0
  | cons h t => S (length' _ t)
  end.

(* -------------------------------------------------- *)
(* Implicit arguments *)

(* To avoid writing too many _'s, we can tell Coq that we
   want it ALWAYS to infer the type argument(s) of a given
   function. *)
Implicit Arguments nil [X].
Implicit Arguments cons [X].
Implicit Arguments length [X].
Implicit Arguments app [X].
Implicit Arguments rev [X].
Implicit Arguments snoc [X].

(* A small problem: this definition fails, because Coq
   doesn't know what implicit argument to use for [nil]...

Definition mynil := nil. 
*)

(* To tell Coq that we want to supply a type argument just
   this once, even though we've declared the function to
   take this argument implicitly, use @ *)
Definition mynil := @nil nat.

(* Now we can define convenient notation for lists, as
   before *)
Notation "x :: y" := (cons x y) 
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y) 
                     (at level 60, right associativity).

Definition l_123'' := [1, 2, 3].

(* -------------------------------------------------- *)
(* Polymorphism exercises *)

(* Exercise: 2 stars (poly_exercises) *)

(* A few easy exercises, just like ones in Lists.v (for
   practice with polymorphism)... *)

(** <<
Fixpoint repeat (X : Set) (n : X) (count : nat) {struct count} : list X := 
  FILL IN HERE

Example test_repeat1: 
  repeat bool true 2 = cons true (cons true nil).
Proof. reflexivity.  Qed.
>> *)

(* CMSC 631 *)
Theorem nil_app : forall X:Set, forall l:list X, 
  app [] l = l.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Some more easy exercises, not too different from things
   we've seen in Lists.v... *)

(* CMSC 631 *)
Theorem rev_snoc : forall X : Set, 
                     forall v : X,
                     forall s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* CMSC 631 *)
Theorem snoc_with_append : forall X : Set, 
                         forall l1 l2 : list X,
                         forall v : X,
  snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* ---------------------------------------------------------------------- *)
(* Polymorphic pairs *)

Inductive prod (X Y : Set) : Set :=
  pair : X -> Y -> prod X Y.

Implicit Arguments pair [X Y].

Notation "( x , y )" := (pair x y).

Notation "X * Y" := (prod X Y) : type_scope.

Definition fst (X Y : Set) (p : X * Y) : X := 
  match p with (x,y) => x end.

Definition snd (X Y : Set) (p : X * Y) : Y := 
  match p with (x,y) => y end.

Implicit Arguments snd [X Y].
Implicit Arguments fst [X Y].

Fixpoint combine (X Y : Set) (lx : list X) (ly : list Y) 
           {struct lx} : list (X*Y) :=
  match lx with
  | [] => []
  | x::tx => match ly with
             | [] => []
             | y::ty => (x,y) :: (combine _ _ tx ty)
             end
  end.

Implicit Arguments combine [X Y]. 

(* Exercise: 2 stars *)
(** <<

(* Define [split] so that it passes the test below *)
Fixpoint split 
  FILL IN HERE

Implicit Arguments split [X Y].

Example test_split:
  split [(1,false),(2,false)] = ([1,2],[false,false]).
Proof. reflexivity.  Qed.

>> *)

(* ---------------------------------------------------------------------- *)
(* Polymorphic options *)

Inductive option (X:Set) : Set :=
  | Some : X -> option X
  | None : option X.

Implicit Arguments Some [X].
Implicit Arguments None [X].

(* Exercise: 1 star *)
(** <<
Fixpoint index 
  FILL IN HERE

Implicit Arguments index [X].

Example test_index1 :    index 0 [4,5,6,7]  = Some 4.
Proof. reflexivity.  Qed.
Example test_index2 :    index  1 [[1],[2]]  = Some [2].
Proof. reflexivity.  Qed.
Example test_index3 :    index  2 [true]  = None.
Proof. reflexivity.  Qed.
>> *)

(* Exercise: 1 star *)
(** <<
Definition hd_opt (X : Set) (l : list X)  : option X :=
  FILL IN HERE

Implicit Arguments hd_opt [X].

Example test_hd_opt1 :    @hd_opt nat [] = None.
Proof. reflexivity.  Qed.
Example test_hd_opt2 :  hd_opt [1,2] = Some 1. 
Proof. reflexivity.  Qed.
Example test_hd_opt3 :   hd_opt  [[1],[2]]  = Some [1].
Proof. reflexivity.  Qed.
>> *)

(* -------------------------------------------------- *)
(* Higher-order functions *)

(* A function that applies another function three times *)
Definition doit3times (X:Set) (f:X->X) (n:X) : X := 
  f (f (f n)).

Example test_doit3times1: doit3times nat minustwo 9 = 3.
Proof. reflexivity.  Qed.
Example test_doit3times2: doit3times bool negb true = false.
Proof. reflexivity.  Qed.

Check doit3times.

Implicit Arguments doit3times [X].

(* -------------------------------------------------- *)
(* Partial application and anonymous functions *)

Check plus.
Definition plus3 := plus 3.
Check plus3.

Example test_plus3 :    plus3 4 = 7.
Proof. reflexivity.  Qed.
Example test_plus3' :   doit3times plus3 0 = 9.
Proof. reflexivity.  Qed.
Example test_plus3'' :  doit3times (plus 3) 0 = 9.
Proof. reflexivity.  Qed.

(* Functions can be defined anonymously, in-line... *)
Example test_anon_fun: 
  doit3times (fun (n:nat) => mult n n) 2 = 256.
Proof. reflexivity.  Qed.

(* Coq can infer the type of the anonymous function here
   from the fact that it is being used in a context where
   it is applied to a number *)
Example test_anon_fun': 
  doit3times (fun n => mult n n) 2 = 256.
Proof. reflexivity.  Qed.

(* A slightly more complicated anonymous function *)
Example test_doit3times4: 
  doit3times (fun n => minus (mult n 2) 1) 2 = 9.
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------- *)
(* Optional exercise: currying. *)

(* Exercise: 2 stars, optional (currying) *)
(* In Coq, a function f : A -> B -> C really has the type
   A -> (B -> C).  That is, if you give f a value of type
   A, it will give you function f' : B -> C.  If you then
   give f' a value of type B, it will return a value of
   type C.  This allows for partial application, as in
   plus3.  Processing a list of arguments with functions
   that return functions is called "currying", named in
   honor of the logician Haskell Curry.

   Conversely, we can reinterpret the type A -> B -> C
   as (A * B) -> C.  This is called "uncurrying".  In an
   uncurried binary function, both arguments must be given
   at once as a pair; there is no partial application. *)
Definition prod_curry (X Y Z : Set) 
  (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).

(* CMSC 631 - define prod_uncurry and prove uncurry_curry, curry_uncurry *)
(** <<

Definition prod_uncurry (X Y Z : Set)
  (f : X -> Y -> Z) (p : X * Y) : Z :=
  FILL IN HERE (OPTIONALLY)

Implicit Arguments prod_curry [X Y Z].
Implicit Arguments prod_uncurry [X Y Z].

(* Thought exercise: before running these commands, what
   are the types of prod_curry and prod_uncurry? *)
Check prod_curry.
Check prod_uncurry.

Theorem uncurry_curry : forall (X Y Z : Set) (f : X -> Y -> Z) x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

Theorem curry_uncurry : forall (X Y Z : Set) (f : (X * Y) -> Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

>> *)

(* -------------------------------------------------- *)
(* Map *)

(* Exercise: 1 star (implicit_args) *)
(* The definitions and uses of filter and map use implicit
   arguments in many places.  Replace every _ by an
   explicit set and use Coq to check that you've done so
   correctly.  (You may also have to remove @Implicit
   Arguments@ commands for Coq to accept explicit
   arguments.)  This exercise is not to be turned in; it
   is probably easiest to do it on a COPY of this file
   that you can throw away afterwards.
*)

(* A mapping function for options: do something to
   (Some x), but leave None alone... *)
Definition map_option (X Y : Set) (f : X -> Y) (xo : option X) 
                      : option Y :=
  match xo with
    | None => None
    | Some x => Some (f x)
  end.

Implicit Arguments map_option [X Y].

(* A mapping function for lists.  Do something to each
   element of a list, returning a new list (possibly of a
   new type!) *)
Fixpoint map (X:Set) (Y:Set) (f:X->Y) (l:list X) {struct l} 
             : (list Y) := 
  match l with
  | []     => []
  | h :: t => (f h) :: (map _ _ f t)
  end.

Example test_map1: map nat nat (plus 3) [2,0,2] = [5,3,5].
Proof. reflexivity.  Qed.

Implicit Arguments map [X Y].

Example test_map2: map oddb [2,1,2,5] = [false,true,false,true].
Proof. reflexivity.  Qed.

Example test_map3: 
  map (fun n => [evenb n,oddb n]) [2,1,2,5] = 
  [[true,false],[false,true],[true,false],[false,true]].
Proof. reflexivity.  Qed.


(* CMSC 631 *)
(* Exercise: 2 stars, optional *)
(* Show that map and rev commute.  You may need to define
   an auxiliary lemma. *)
Theorem map_rev : forall (X Y : Set) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* Exercise: 1 star *)
(** <<
Fixpoint flat_map (X:Set) (Y:Set) (f:X -> list Y) (l:list X) {struct l} 
                   : (list Y) := 
  FILL IN HERE

Implicit Arguments flat_map [X Y].

Example test_flat_map1: 
  flat_map (fun n => [n,n,n]) [1,5,4]
  = [1, 1, 1, 5, 5, 5, 4, 4, 4].
Proof. reflexivity.  Qed.
>> *)

(* -------------------------------------------------- *)
(* Filter *)

Fixpoint filter (X:Set) (test: X->bool) (l:list X) 
                {struct l} : (list X) :=
  match l with
  | []     => []
  | h :: t => if test h then h :: (filter _ test t)
                        else       filter _ test t
  end.

Implicit Arguments filter [X].

Example test_filter1: filter evenb [1,2,3,4] = [2,4].
Proof. reflexivity.  Qed.
Example test_filter2: 
  filter (fun l => beq_nat (length l) 1) 
         [ [1, 2], [3], [4], [5,6,7], [], [8] ]
  = [ [3], [4], [8] ].
Proof. reflexivity.  Qed.

Definition countoddmembers' (l:list nat) : nat := 
  length (filter oddb l).

Example test_countoddmembers'1:   countoddmembers' [1,0,3,1,4,5] = 4.
Proof. reflexivity.  Qed.
Example test_countoddmembers'2:   countoddmembers' [0,2,4] = 0.
Proof. reflexivity.  Qed.
Example test_countoddmembers'3:   countoddmembers' nil = 0.
Proof. reflexivity.  Qed.

(* ------------------------------------------------------- *)
(* The [unfold] tactic *)

(* The [simpl] tactic doesn't unfold Definitions. The
   [unfold] tactic can be used to explicitly replace a
   defined name by the right-hand side of its
   definition. *)

Eval simpl in (plus 3 5).
Eval simpl in (plus3 5).

(* Doing [simpl] instead of [unfold] here does nothing.
   We are stuck unless we know something about the way
   plus3 is defined. *)
Theorem unfold_example : 
  plus3 5 = 8.
Proof.
  unfold plus3. 
  reflexivity.
Qed.

(* ----------------------------------------------------- *)
(* Functions as Data *)

Definition constfun (X : Set) (x : X) := 
  fun (k:nat) => x.

Implicit Arguments constfun [X].

Definition override (X : Set) (f : nat->X) (k:nat) (x:X) :=
  fun k' => if beq_nat k k' then x else f k'.

Implicit Arguments override [X].

Theorem override_eq : forall (X:Set) x k (f : nat->X),
  (override f k x) k = x.
Proof.
  intros X x k f.
  unfold override.
  rewrite <- beq_nat_refl.
  reflexivity.
Qed.

(* Exercise: 2 stars *)
(* Before starting to play with tactics, make sure you 
   understand exactly what this theorem is saying. *)
Theorem override_example : forall (b:bool), 
  (override (constfun b) 3 true) 2 = b.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Exercise: 2 stars *)
Theorem override_neq : forall (X:Set) x1 x2 k1 k2 (f : nat->X),
  f k1 = x1 ->
  beq_nat k2 k1 = false ->
  (override f k2 x2) k1 = x1.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ---------------------------------------------------- *)
(* Inversion *)

(* A fundamental property of inductive definitions is that
   their constructors are INJECTIVE.  For example, the only
   way we can have [S n = S m] is if [m = n].

   The [inversion] tactic uses this injectivity principle to
   derive useful consequences of an equality hypothesis. *)
Theorem eq_add_S : forall (n m : nat),
     S n = S m
  -> n = m.
Proof.
  intros n m eq. inversion eq. reflexivity.
Qed.

(* The same principle applies to other inductively defined
   sets, such as lists. *)
Theorem silly4 : forall (n m : nat),
     [n] = [m]
  -> n = m.
Proof.
  intros n o eq. inversion eq. reflexivity.
Qed.

(* As a convenience, the [inversion] tactic can also
   destruct equalities between complex values, binding
   multiple variables as it goes. *)
Theorem silly5 : forall (n m o : nat),
     [n,m] = [o,o]
  -> [n] = [m].
Proof.
  intros n m o eq. inversion eq. reflexivity.
Qed.

(* CMSC 631 *)
(* Exercise: 1 star *) 
Example sillyex1 : forall (X : Set) (x y z : X) (l j : list X),
     x :: y :: l = z :: j
  -> y :: l = x :: j
  -> x = y.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Another critical property of inductive definitions is
   that applications of distinct constructors are never
   equal, no matter what they are applied to.  For
   example, [S n] can never be equal to [O], no matter
   what [n] is.  This means that anytime we can see a
   HYPOTHESIS of the form [S n = O], we know that we must
   have made contradictory assumptions at some point.  The
   [inversion] tactic can be applied to this hypothesis to
   finish the proof. *)
Theorem silly6 : forall (n : nat),
     S n = O
  -> plus 2 2 = 5.
Proof.
  intros n contra. inversion contra. 
Qed.

(* Similarly, if we assume that [false = true], then
   anything at all becomes provable. *)
Theorem silly7 : forall (n m : nat),
     false = true
  -> [n] = [m].
Proof.
  intros n m contra. inversion contra. 
Qed.

(* Exercise: 1 star *)
Example sillyex2 : forall (X : Set) (x y z : X) (l j : list X),
     x :: y :: l = []
  -> y :: l = z :: j
  -> x = z.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Here is a more realistic use of inversion to prove a
   property that we will find useful in many places later
   on... *)
Theorem beq_nat_eq : forall n m,
  true = beq_nat n m -> n = m.
Proof.
  intros n. induction n as [| n']. 
  Case "n = 0". 
    intros m. destruct m as [| m'].
    SCase "m = 0". reflexivity.  
    SCase "m = S m'". simpl. intros contra. inversion contra. 
  Case "n = S n'". 
    intros m. destruct m as [| m'].
    SCase "m = 0". intros contra. inversion contra.
    SCase "m = S m'". simpl. intros H.
      assert (n' = m') as H1.
        apply IHn'. apply H.
      rewrite -> H1. reflexivity.
Qed.

(* Exercise: 2 stars (beq_nat_eq_informal) *)
(* Informal proof:
Theorem: beq_nat equal numbers are equal.
Proof:
   (* FILL IN HERE *)

*)


(* Exercise: 1 star *)
Theorem override_same : forall (X:Set) x1 k1 k2 (f : nat->X),
  f k1 = x1 -> 
  (override f k1 x1) k2 = f k2.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* CMSC 631 *)
(* Exercise: 2 stars *)
(* We can also prove beq_nat_eq by induction on [m]
   (though we have to be a little careful about which
   order we introduce the variables, so that we get a
   general enough induction hypothesis; this is done for
   you below).  Finish the following proof.  To get
   maximum benefit from the exercise, try first to do it
   without looking back at the one above. *)
Theorem beq_nat_eq' : forall m n,
  beq_nat n m = true -> n = m.
Proof.
  intros m. induction m as [| m']. 
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Another illustration of [inversion].  This is a
   slightly roundabout way of stating a fact that we have
   already proved above.  The extra equalities force us to
   do a little more equational reasoning and exercise some
   of the tactics we've seen recently. *)
Theorem length_snoc' : forall (X : Set) (v : X)
                              (l : list X) (n : nat),
     length l = n
  -> length (snoc l v) = S n. 
Proof.
  intros X v l. induction l as [| v' l'].
  Case "l = []". intros n eq. rewrite <- eq. reflexivity.
  Case "l = v' :: l'". intros n eq. simpl. destruct n as [| n'].
    SCase "n = 0". inversion eq.
    SCase "n = S n'". 
      assert (length (snoc l' v) = S n').
        SSCase "Proof of assertion". apply IHl'. 
        inversion eq. reflexivity.
      rewrite -> H. reflexivity.
Qed.

(* Micro-sermon: Mindless proof-hacking is a terrible
   temptation in Coq... Try to resist it!! *)
     
(* -------------------------------------------------- *)
(* Practice session *)

(* Exercise: 2 stars (practice) *)
(* Some nontrivial but not-too-complicated proofs to work
   together in class, and some for you to work as
   exercises.  

   Note that some of the exercises may
   involve applying lemmas from earlier lectures or
   homeworks. *)

(* A slightly different way of making the same assertion
   as above. *)
Theorem length_snoc'' : forall (X : Set) (v : X)
                             (l : list X) (n : nat),
     S (length l) = n
  -> length (snoc l v) = n.
Proof.
  intros X v l. induction l as [| v' l'].
    Case "l = []". intros n eq. rewrite <- eq. reflexivity.
    Case "l = v' :: l'". 
      intros n eq. simpl.
      (* Note the care we take here: first we introduce n
         and the equality, then we simplify.  This leaves
         the equation about length UN-simplified, which
         means our context will make a little bit more
         sense.  (The proof will work either way.)
      *)
      destruct n as [| n'].
      (* Now we destruct n; if it's 0, we have a
         contradiction immediately. *)
      SCase "n = 0". inversion eq.
      SCase "n = S n'".
        assert (length (snoc l' v) = n').
          SSCase "Proof of assertion". 
            (* We use the IH and the inversion of eq to
               prove the equation we want about length. *)
            apply IHl'. inversion eq. reflexivity.
        rewrite -> H. reflexivity.
Qed.

Theorem beq_nat_0_l : forall n,
  true = beq_nat 0 n -> 0 = n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem beq_nat_0_r : forall n,
  true = beq_nat n 0 -> 0 = n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Fixpoint double (n:nat) {struct n} :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Theorem double_injective : forall n m,
     double n = double m
  -> n = m.
Proof.
  intros n. induction n as [| n'].
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* --------------------------------------------------------- *)
(* Using tactics on hypotheses *)

(* By default, most tactics work on the goal formula and
   leave the context unchanged.  But tactics often come
   with a variant that performs a similar operation on a
   statement in the context. *)

(* For example, the tactic [simpl in H] performs
   simplification in the hypothesis named [H] in the
   context. *)
Theorem S_inj : forall (n m : nat) (b : bool),
     beq_nat (S n) (S m) = b 
  -> beq_nat n m = b. 
Proof.
  intros n m b H. simpl in H. apply H. 
Qed.

(* Similarly, the tactic [apply L in H] matches some
   conditional statement [L] (of the form [L1->L2], say)
   against a hypothesis H in the context.  However, unlike
   ordinary [apply] (which rewrites a goal matching [L2]
   into a subgoal [L1]), [apply L in H] matches [H] against
   [L1] and, if successful, replaces it with [L2].

   In other words, [apply L in H] gives us a form of FORWARD
   REASONING -- from [L1->L2] and a hypothesis matching
   [L1], it gives us a hypothesis matching [L2].

   By contrast, [apply L] is BACKWARD REASONING -- it says
   that if we know [L1->L2] and we are trying to prove [L2],
   it suffices to prove [L1]. *)

(* Brief digression to record a convenient fact about equality... *) 
Theorem sym_eq : forall (X : Set) (n m : X),
  n = m -> m = n.
Proof.
  intros X n m H. rewrite -> H. reflexivity.
Qed.

(* Here is a variant of a proof from above, using forward
   reasoning throughout instead of backward reasoning. *)
Theorem silly3' : forall (n : nat),
  (beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true)
  -> true = beq_nat n 5 
  -> true = beq_nat (S (S n)) 7.
Proof.
  intros n eq H.
  apply sym_eq in H. apply eq in H. apply sym_eq in H. 
  apply H.
Qed.

(* Exercise: 2 stars *)
Theorem plus_n_n_injective : forall n m,
     plus n n = plus m m
  -> n = m.
Proof.
  intros n. induction n as [| n'].
    (* Hint: use the plus_n_Sm lemma *)
    (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ---------------------------------------------------- *)
(* Using [destruct] on compound expressions *)

(* We have seen many examples where the [destruct] tactic
   is used to perform case analysis of the value of some
   variable.  But sometimes we need to reason by cases on
   the result of some EXPRESSION.  We can also do this
   with [destruct]. *)

Definition sillyfun (n : nat) : bool :=
  if beq_nat n 3 then false
  else if beq_nat n 5 then false
  else false.

Theorem sillyfun_false : forall (n : nat),
  sillyfun n = false.
Proof.
  intros n. unfold sillyfun. 
  destruct (beq_nat n 3).
    Case "beq_nat n 3 = true". reflexivity.
    Case "beq_nat n 3 = false". destruct (beq_nat n 5).
      SCase "beq_nat n 5 = true". reflexivity.
      SCase "beq_nat n 5 = false". reflexivity.
Qed.

(* Exercise: 1 star *)
Theorem override_shadow : forall (X:Set) x1 x2 k1 k2 (f : nat->X),
  (override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Exercise: 2 stars *)
(** <<

Theorem split_combine : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros X Y l. induction l as [| [x y] l'].
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

>> *)

(* Thought exercise: We have just proven that for all
   lists of pairs, combine is the inverse of split.  How
   would you state the theorem showing that split is the
   inverse of combine?

   Hint: what property do you need of l1 and l2 for split
   (combine l1 l2) = (l1,l2) to be true?
*)

(* ----------------------------------------------------- *)
(* The [remember] tactic *)

(* We have seen how the [destruct] tactic can be used to
   perform case analysis of the results of arbitrary
   computations.  If [e] is an expression whose type is some
   inductively defined set [T], then, for each constructor
   [c] of [T], [destruct e] generates a subgoal in which all
   occurrences of [e] (in the goal and in the context) are
   replaced by [c].

   Sometimes, however, this substitution process loses
   information that we need in order to complete the proof.
   For example, suppose we define a function [sillyfun1]
   like this... *)
Definition sillyfun1 (n : nat) : bool :=
  if beq_nat n 3 then true
  else if beq_nat n 5 then true
  else false.

(* ... and suppose that we want to convince Coq of the
   rather obvious observation that [sillyfun1 n] yields
   [true] only when [n] is odd.  By analogy with the proofs
   we did with [sillyfun] above, it is natural to start the
   proof like this: *)
Theorem sillyfun1_odd_FAILED : forall (n : nat),
     sillyfun1 n = true
  -> oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (beq_nat n 3).
Admitted.

(* At this point, we are stuck: the context does not
   contain enough information to prove the goal!  The
   problem is that the substitution peformed by [destruct]
   is too brutal -- it threw away every occurrence of
   [beq_nat n 3], but we need to keep at least one of these
   because we need to be able to reason that since, in
   this branch of the case analysis, [beq_nat n 3 = true],
   it must be that [n = 3], from which it follows that [n]
   is odd. *)

(* What we would really like is not to use [destruct]
   directly on [beq_nat n 3] and substitute away all
   occurrences of this expression, but rather to use
   [destruct] on something else that is EQUAL to [beq_nat n
   3] -- e.g., if we had a variable that we knew was equal
   to [beq_nat n 3], we could [destruct] this variable
   instead.

   The [remember] tactic allows us to introduce such a
   variable. *)

Theorem sillyfun1_odd : forall (n : nat),
     sillyfun1 n = true
  -> oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  remember (beq_nat n 3) as e3.
  (* At this point, the context has been enriched with a new
     variable [e3] and an assumption that [e3 = beq_nat n 3].
     Now if we do [destruct e3]... *)
  destruct e3.
  (* ... the variable [e3] gets substituted away (it
     disappears completely) and we are left with the same
     state as at the point where we got stuck above, except
     that the context still contains the extra equality
     assumption -- now with [true] substituted for [e3] --
     which is exactly what we need to make progress. *)
    Case "e3 = true". apply beq_nat_eq in Heqe3.
      rewrite -> Heqe3. reflexivity.
    Case "e3 = false".
      (* When we come to the second equality test in the
         body of the function we are reasoning about, we can
         use [remember] again in the same way, allowing us
         to finish the proof. *)
      remember (beq_nat n 5) as e5. destruct e5.
        SCase "e5 = true".
          apply beq_nat_eq in Heqe5.
          rewrite -> Heqe5. reflexivity.
        SCase "e5 = false". inversion eq.
Qed.

(* Exercise: 2 stars, optional *)
(* This one is a bit challenging.  Be sure your initial intros go
   only up through the parameter on which you want to do induction! *)
Theorem filter_exercise : forall (X : Set) (test : X -> bool)
                               (x : X) (l lf : list X),
     filter test l = x :: lf
  -> test x = true.
Proof.
  (* OPTIONAL EXERCISE *) Admitted.

(* ----------------------------------------------------- *)
(* The [apply ... with ...] tactic *)

(* The following (silly) example uses two rewrites in a row
   to get from [ [m,n] ] to [ [r,s] ]. *)
Example trans_eq_example : forall (a b c d e f : nat),
     [a,b] = [c,d]
  -> [c,d] = [e,f]
  -> [a,b] = [e,f].
Proof.
  intros a b c d e f eq1 eq2. 
  rewrite -> eq1. rewrite -> eq2. reflexivity.
Qed.

(* Since this is a common pattern, we might abstract it out
   as a lemma recording once and for all the fact that
   equality is transitive. *)
Theorem trans_eq : forall (X:Set) (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2. 
  reflexivity.
Qed.

(* Now, we should be able to use [trans_eq] to prove the
   above example.  However, to do this we need a slight
   refinement of the [apply] tactic... *)
Example trans_eq_example' : forall (a b c d e f : nat),
     [a,b] = [c,d]
  -> [c,d] = [e,f]
  -> [a,b] = [e,f].
Proof.
  intros a b c d e f eq1 eq2. 
  (* If we simply tell Coq [apply trans_eq] at this point,
     it can tell (by matching the goal against the
     conclusion of the lemma) that it should instantiate [X]
     with [nat], [n] with [[a,b]], and [o] with [[e,f]].
     However, the matching process doesn't determine an
     instantiation for [m]: we have to supply one explicitly
     by adding [with (m:=[c,d])] to the invocation of
     [apply]. *)
  apply trans_eq with (m:=[c,d]). apply eq1. apply eq2. 
Qed.

(* Actually, we usually don't have to include the name [m]
   in the [with] clause; Coq is often smart enough to
   figure out which instantiation we're giving. We could
   instead write: apply trans_eq with [c,d]. *)

(* Exercise: 2 stars (apply_exercises) *)

Example trans_eq_exercise : forall (n m o p : nat),
     m = (minustwo o)
  -> (plus n p) = m
  -> (plus n p) = (minustwo o). 
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* CMSC 631 *)
Theorem beq_nat_trans : forall n m p,
  true = beq_nat n m ->
  true = beq_nat m p ->
  true = beq_nat n p.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem override_permute : forall (X:Set) x1 x2 k1 k2 k3 (f : nat->X),
  false = beq_nat k2 k1 ->
  (override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ---------------------------------------------------------------------- *)
(* Additional exercises *)

Module MumbleBaz.
(* Exercise: 2 stars, optional *)
(* Consider the following two inductively defined sets. *)

(* CMSC 631 - you don't need to turn in the following, but you should *)
(*do it to make sure you understand inductive definitions. *)
Inductive mumble : Set :=
  | a : mumble
  | b : mumble -> nat -> mumble
  | c : mumble.
Inductive grumble (X:Set) : Set :=
  | d : mumble -> grumble X
  | e : X -> grumble X.
(* Which of the following are well-typed elements of [grumble]? 
       d (b a 5) 
       d mumble (b a 5) 
       d bool (b a 5) 
       e bool true
       e mumble (b c 0) 
       e bool (b c 0) 
       c 
*)

(* Exercise: 2 stars, optional *)
(* Consider the following inductive definition: *)
Inductive baz : Set :=
   | x : baz -> baz
   | y : baz -> bool -> baz.
(* How MANY elements does the set [baz] have? 
FILL IN HERE

*)
End MumbleBaz.

(* Exercise: 2 stars, optional *)
Fixpoint fold (X:Set) (Y:Set) (f: X->Y->Y) (l:list X) (b:Y) {struct l} : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold _ _ f t b)
  end.

(* Exercise: 3 stars! (forall_exists_challenge) *)
(* Challenge problem.  (This is a tiny bit more difficult
   and open-ended, but it will be worth only one point
   when the homework is graded.) 

   Define two recursive Fixpoints, forallb and existsb.

   forallb checks whether every element in a list
   satisfies a given predicate:
   
     forallb oddb [1,3,5,7,9] = true
     forallb negb [false,false] = true
     forallb evenb [0,2,4,5] = false
     forallb (beq_nat 5) [] = true

   existsb checks whether there exists an element in the
   list that satisfies a given predicate:

     existsb (beq_nat 5) [0,2,3,6] = false
     existsb (andb true) [true,true,false] = true
     existsb oddb [1,0,0,0,0,3] = true
     existsb evenb [] = false

   Next, create a NONRECURSIVE Definition, existsb', using
   forallb and negb.

   Prove that existsb' and existsb have the same behavior.
*)

(** <<
(* FILL IN HERE *)


>> *)