(*

   Project 3.

   Due 10/26/2011

   Upload this file to the submit server with your answers filled in.
   Each section separated by a row of *'s is worth 1 point.

   You can download the file SfLib.v from the course web site.  We
   will test your code by running "coqc p3.v", to make sure your
   proofs are valid, and then manually look for any Admitted's in your
   submission.

   These exercises were taken from Basics.v, Lists.v, Poly.v, Gen.v,
   Prop.v, and Logic.v.

*)


Require Export SfLib.

Definition admit {T: Type} : T.  Admitted.

(***********************************************************************)

(** **** Exercise: 1 star *)
(** Recall the standard factorial function:
<<
    factorial(0)  =  1 
    factorial(n)  =  n * factorial(n-1)     (if n>0)
>>
    Translate this into Coq, and show the subsequent two examples are
    valid. *)
Fixpoint factorial (n:nat) : nat := 
  (* FILL IN HERE *) admit.

Example test_factorial1:          (factorial 3) = 6.
(* FILL IN HERE *) Admitted.
Example test_factorial2:          (factorial 5) = (mult 10 12).
(* FILL IN HERE *) Admitted.

(***********************************************************************)

(** **** Exercise: 1 star *)
Theorem mult_1_plus : forall n m : nat,
  (1 + n) * m = m + (n * m).
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

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

(** **** Exercise: 2 stars.  Hint: find where this lemma is defined in
    the Basics.v and use one of the lemmas that comes before it in your
    proof. *)
Lemma double_plus : forall n, double n = n + n .
Proof.  
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(** **** Exercise: 2 stars *)
Theorem beq_nat_refl : forall n : nat,
  true = beq_nat n n.
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(* 3 stars *)
(* Hint: recall that you can use other information here, e.g., facts of standard
   addition proved in SfLib or in the notes already (inherited from the standard
   Coq environment). *)
Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
  (* FILL IN HERE *) Admitted.

(* 3 stars *)
Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)
(** 3 stars *)

Theorem distr_rev : forall (X : Type) (l1 l2 : list X),
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(** **** Exercise: 2 stars *)
(** Show that [map] and [rev] commute.  You may need to define an
    auxiliary lemma. *)

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

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

(** **** Exercise: 2 stars *)
Theorem override_neq : forall {X:Type} 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 *) Admitted.

(***********************************************************************)

(** **** Exercise: 2 stars *)
(* Hint: The "remember" tactic will be helpful here, and the lemma relating 
   beq_nat to Coq equality *)

Theorem override_same : forall {X:Type} x1 k1 k2 (f : nat->X),
  f k1 = x1 -> 
  (override f k1 x1) k2 = f k2.
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(** **** Exercise: 2 stars *)
(* Hint: inversion will be useful here. *)
 
Theorem beq_nat_0_l : forall n,
  true = beq_nat 0 n -> 0 = n.
Proof.
  (* FILL IN HERE *) Admitted.

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

(***********************************************************************)

(** **** Exercise: 2 stars *)
(** You can practice using the "in" variants in this exercise. *)
(*  You may find it useful to prove
      Lemma eq_remove_S : forall n m, n = m -> S n = S m.
    as a lemma first. *)

Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n'].
    (* Hint: use the plus_n_Sm lemma: forall n m : nat, S (n + m) = n + S m *)
    (* FILL IN HERE *) Admitted.

(* NOTE *)
(* The material for the exercises below were covered in lecture after 10/10, 
   by and large. *)

(** **** Exercise: 1 star *)
Theorem proj2 : forall P Q : Prop, 
  P /\ Q -> Q.
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

Theorem iff_trans : forall P Q R : Prop, 
  (P <-> Q) -> (Q <-> R) -> (P <-> R).
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(** **** Exercise: 1 star *)
Theorem or_distributes_over_and : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

(** **** Exercise: 2 stars *)
Theorem contrapositive : forall P Q : Prop,
  (P -> Q) -> (~Q -> ~P).
Proof.
  (* FILL IN HERE *) Admitted.


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

Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
   (* FILL IN HERE *) Admitted.

(***********************************************************************)

(***********************************************************************)

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

(***********************************************************************)

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


(***********************************************************************)

(** This following definition says that there are two ways to give
    evidence that a number [m] is even.  First, [0] is even, and
    [ev_0] is evidence for this.  Second, if [m = S (S n)] for some
    [n] and we can give evidence [e] that [n] is even, then [m] is
    also even, and [ev_SS n e] is the evidence. *)

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

(** **** Exercise: 1 star, optional *)
(** Give a proof showing that four is even. *)

Theorem four_ev' :
  ev 4.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars *)
(** Prove that if [n[ is even, then so is [4+n]. *)

Theorem ev_plus4' : forall n,
  ev n -> ev (4 + n).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(***********************************************************************)

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

(***********************************************************************)

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

(***********************************************************************)

(** **** Exercise: 1 star *)
(** Theorem [five_not_even] confirms the unsurprising fact that five
    is not an even number.  Prove this more interesting fact: *)

Theorem ev_not_ev_S : forall n,
  ev n -> ~ ev (S n).
Proof. 
  unfold not. intros n H. induction H. (* not n! *)
  (* FILL IN HERE *) Admitted.

(***********************************************************************)

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

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof. 
  (* FILL IN HERE *) Admitted.

Theorem le_plus_l : forall a b,
  a <= a + b.
Proof. 
  (* FILL IN HERE *) Admitted.

Theorem ble_nat_false : forall n m,
  ble_nat n m = false -> ~(n <= m).
Proof.
  (* Hint: Do the right induction! *)
  (* FILL IN HERE *) Admitted.

(***********************************************************************)