(* Basic programming and reasoning about programs in Coq
   Version of 2/22/2009
*)

(* HOMEWORK INSTRUCTIONS:

   Submit homeworks using Blackboard:
     <https://courseweb.library.upenn.edu/>
   
   Solution files that Coq rejects will NOT be graded.
   You should be able to run CoqIDE/ProofGeneral to the
   end of the file, or run coqc without any errors.  If
   you can't solve one of the problems, leave an
   [Admitted] in the file.  Style, readability, and
   elegance count.

   If you have any questions about the homework, please
   e-mail the TAs.

   Have fun!
*)

(* ------------------------------------------------------- *)
(* Days of the week *)

Inductive day : Set :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.

Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.

Eval simpl in (next_weekday friday).
Eval simpl in (next_weekday (next_weekday saturday)).

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity.  Qed.

(* -------------------------------------------------------------- *)
(* Booleans *)

Inductive bool : Set :=
  | true : bool
  | false : bool.

Definition negb (b:bool) := 
  match b with
  | true => false
  | false => true
  end.

Definition ifb (b1 b2 b3:bool) : bool :=
  match b1 with
    | true => b2
    | false => b3
  end.

Definition andb (b1:bool) (b2:bool) : bool := ifb b1 b2 false.

Definition orb (b1:bool) (b2:bool) : bool := ifb b1 true b2.

Example test_orb1:  (orb true  false) = true. 
Proof. simpl. reflexivity.  Qed.
Example test_orb2:  (orb false false) = false.
Proof. simpl. reflexivity.  Qed.
Example test_orb3:  (orb false true ) = true.
Proof. simpl. reflexivity.  Qed.
Example test_orb4:  (orb true  true ) = true.
Proof. simpl. reflexivity.  Qed.

(* Exercise: 1 star (nandb_andb3) *)
(* CMSC 631 *)
(* Uncomment and then complete the definitions of the
   following functions, making sure that the assertions
   below each can be verified by Coq. *)
(** <<
(* This function should return [true] if either or both of
   its inputs are [false]. *)
Definition nandb (b1:bool) (b2:bool) : bool :=
  FILL IN HERE

Example test_nandb1:               (nandb true false) = true.
Proof. simpl. reflexivity.  Qed.
Example test_nandb2:               (nandb false false) = true.
Proof. simpl. reflexivity.  Qed.
Example test_nandb3:               (nandb false true) = true.
Proof. simpl. reflexivity.  Qed.
Example test_nandb4:               (nandb true true) = false.
Proof. simpl. reflexivity.  Qed.

(* A NOTE ON NOTATION: We will often use square brackets
   [...] to delimit fragments of Coq code in comments in
   .v files; this convention, which is also used by the
   coqdoc documentation tool, keeps them visually separate
   from the surrounding text.  In the typeset notes,
   typewriter font is used for the same purpose. *)

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
  FILL IN HERE

Example test_andb31:                 (andb3 true true true) = true.
Proof. simpl. reflexivity.  Qed.
Example test_andb32:                 (andb3 false true true) = false.
Proof. simpl. reflexivity.  Qed.
Example test_andb33:                 (andb3 true false true) = false.
Proof. simpl. reflexivity.  Qed.
Example test_andb34:                 (andb3 true true false) = false.
Proof. simpl. reflexivity.  Qed.
>> *)


(* ----------------------------------------------------- *)
(* Numbers *)

(* Technical note: Coq provides a fairly fancy module
   system, to aid in organizing large and complex
   developments.  In this course, we won't need most of
   its features, but one is useful: if we enclose a
   collection of declarations between [Module X] and [End
   X] markers, then, in the remainder of the file after
   the [End], all these definitions will be referred to by
   names like [X.foo] instead of just [foo].  This means
   that the new definition will not clash with the
   unqualified name [foo] later, which would otherwise be
   an error (a name can only be defined once in a given
   scope).

   Here, we use this feature to introduce the definition
   of [nat] in an inner module so that it does not shadow
   the one from the standard library, which provides a
   little bit of magic for writing numbers using standard
   arabic numerals. *)
Module Nat.

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

End Nat.

Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.

Definition minustwo (n : nat) : nat :=
  match n with
    | O => O
    | S O => O
    | S (S n') => n'
  end.

Check (S (S (S (S O)))).
Eval simpl in (minustwo 4).

Check pred.
Check minustwo.
Check S.

Fixpoint evenb (n:nat) {struct n} : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.

Definition oddb (n:nat) : bool   :=   negb (evenb n).


Example test_oddb1:    (oddb (S O)) = true.
Proof. simpl. reflexivity.  Qed.
Example test_oddb2:    (oddb (S (S (S (S O))))) = false.
Proof. simpl. reflexivity.  Qed.

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

Eval simpl in (plus (S (S (S O))) (S (S O))).

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

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

Fixpoint exp (base power : nat) {struct power} : nat :=
  match power with
    | O => S O
    | S p => mult base (exp base p)
  end.

Example test_mult1:             (mult 3 3) = 9.
Proof. simpl. reflexivity.  Qed.

(* Exercise: 1 star *)
(* CMSC 631 *)
(** <<
Fixpoint factorial (n:nat) {struct n} : nat :=
  FILL IN HERE

Example test_factorial1:          (factorial 3) = 6.
Proof. simpl. reflexivity.  Qed.
Example test_factorial2:          (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity.  Qed.
>> *)

Fixpoint beq_nat (n m : nat) {struct n} : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.
Fixpoint ble_nat (n m : nat) {struct n} : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Example test_ble_nat1:             (ble_nat 2 2) = true.
Proof. simpl. reflexivity.  Qed.
Example test_ble_nat2:             (ble_nat 2 4) = true.
Proof. simpl. reflexivity.  Qed.
Example test_ble_nat3:             (ble_nat 4 2) = false.
Proof. simpl. reflexivity.  Qed.

(* Exercise: 1 star *)
(* CMSC 631 *)
(** <<
Definition blt_nat (n m : nat) :=
  FILL IN HERE

Example test_blt_nat1:             (blt_nat 2 2) = false.
Proof. simpl. reflexivity.  Qed.
Example test_blt_nat2:             (blt_nat 2 4) = true.
Proof. simpl. reflexivity.  Qed.
Example test_blt_nat3:             (blt_nat 4 2) = false.
Proof. simpl. reflexivity.  Qed.
>> *)

(* -------------------------------------------------- *)
(* Reasoning by "partial evaluation" *)

Theorem plus_0_l : forall n:nat, plus 0 n = n.
Proof.
  simpl. reflexivity.  Qed.

(* The [reflexivity] tactic implicitly simplifies both
   sides of the equality before testing to see if they are
   the same... *)
Theorem plus_0_l' : forall n:nat, plus 0 n = n.
Proof.
  reflexivity.  Qed.

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

(* Another proof of plus_0_l, using [intros] *)
Theorem plus_0_l'' : forall n:nat, plus 0 n = n.
Proof.
  intros n. reflexivity.  Qed.

Theorem plus_1_l : forall n:nat, plus 1 n = S n. 
Proof.
  intros n. reflexivity.  Qed.

Theorem mult_0_l : forall n:nat, mult 0 n = 0.
Proof.
  intros n. reflexivity.  Qed.

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

(* A more interesting proof involving [rewrite]. *)
Theorem plus_id_example : forall n m:nat,
  n = m -> plus n n = plus m m.
Proof.
  intros n m.   (* move both quantifiers into the context *)
  intros H.     (* move the hypothesis into the context *)
  rewrite -> H. (* Rewrite the goal using the hypothesis *)
  reflexivity.  Qed.

(* One for you: *)
(* CMSC 631 *)
(* Exercise: 1 star *)
Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> plus n m = plus m o.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Using [rewrite] with a previously proved lemma... *)
Theorem mult_0_plus : forall n m : nat,
  mult (plus 0 n) m = mult n m.
Proof.
  intros n m.
  rewrite -> plus_0_l.
  reflexivity.  Qed.

(* Exercise: 1 star *)
(* CMSC 631 *)
Theorem mult_1_plus : forall n m : nat,
  mult (plus 1 n) m = plus m (mult n m).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ----------------------------------------------------- *)
(* Case analysis *)

(* Sometimes simplification and rewriting are not
   enough... *)
Theorem plus_1_neq_0_firsttry : forall n,
  beq_nat (plus n 1) 0 = false.
Proof.
  intros n. simpl.  (* does nothing! *)
Admitted.

(* Using [destruct] to perform case analysis *)
Theorem plus_1_neq_0 : forall n,
  beq_nat (plus n 1) 0 = false.
Proof.
  intros n. destruct n as [| n'].
    reflexivity.
    reflexivity.  Qed.

(* Another example (using booleans) *)
Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b.
    reflexivity.
    reflexivity.  Qed.

(* Exercise: 1 star *)
(* CMSC 631 *)
Theorem zero_nbeq_plus_1 : forall n,
  beq_nat 0 (plus n 1) = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.


(* Exercise: 1 star (plus_simpl) *)
(* CMSC 631 *)
(* Recall the definition of plus:

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

What will Coq print in response to this query?
  Eval simpl in (forall n, plus n 0 = n).

What will Coq print in response to this query?
  Eval simpl in (forall n, plus 0 n = n).

Briefly explain the difference.
*)


(* ------------------------------------------------------- *)
(* The [Case] annotation *)

(* One of the less nice things about Coq's mechanisms for
   interactive proof is the way subgoals seem to come and
   go almost at random, with no explicit indication of
   where we are -- which case of an induction or case
   analysis we are in -- at any given moment.  In very
   short proofs, this is not a big deal.  But in more
   complex proofs it can become quite difficult to stay
   oriented.

   Here is a simple hack that helps things quite a bit.
   It uses some facilities of Coq that we have not
   discussed -- the string library (just for the concrete
   syntax of quoted strings) and the [Ltac] command, which
   allows us to declare custom tactics.  We will come back
   to [Ltac] in more detail later.  For now, don't worry
   about the details of this declaration. *)

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case." ].

Ltac Case name := Case_aux Case name.
Ltac SCase name := Case_aux SCase name.
Ltac SSCase name := Case_aux SSCase name.
Ltac SSSCase name := Case_aux SSSCase name.
Ltac SSSSCase name := Case_aux SSSSCase name.
Ltac SSSSSCase name := Case_aux SSSSSCase name.
Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.

(* Step through the following proof and observe how the
   context changes. *)
Theorem andb_true_l : forall b c,
  andb b c = true -> b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true".
    reflexivity.
  Case "b = false".
    rewrite <- H. reflexivity.  Qed.

(* Exercise: 1 star *)
(* CMSC 631 *)
(* Prove andb_true_r, marking cases (and subcases) when
   you use [destruct]. *)
Theorem andb_true_r : forall b c,
  andb b c = true -> c = true.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ---------------------------------------------------- *)
(* Induction on numbers *)

(* The fact that 0 is also a neutral element for plus on
   the RIGHT cannot be proved with just
   simplification... *)
Theorem plus_0_r_firsttry : forall n:nat,
  plus n 0 = n.
Proof.
  intros n.
  simpl. (* Does nothing! *)
Admitted.

(* Case analysis gets us a little further, but not all the
   way. *)
Theorem plus_0_r_secondtry : forall n:nat,
  plus n 0 = n.
Proof.
  intros n. destruct n as [| n'].
  Case "n = 0".
    reflexivity. (* so far so good... *)
  Case "n = S n'".
    simpl.       (* ...but here we are stuck again *)
Admitted.
(* We need a bigger hammer... *)

(* The PRINCIPLE OF INDUCTION over 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.

   In Coq, the style of reasoning is "backwards": we begin
   with the goal of proving [P(n)] for all n and break it
   down (by applying the [induction] tactic) into two
   separate subgoals: first showing P(O) and then showing
   [P(n) -> P(S n)]. *)

(* For example... *)
Theorem plus_0_r : forall n:nat, plus n 0 = n.
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".     reflexivity.
  Case "n = S n'".  simpl. rewrite -> IHn'. reflexivity.  Qed.

Theorem plus_assoc : forall n m p : nat,
  plus n (plus m p) = plus (plus n m) p.
Proof.
  intros n m p. induction n as [| n']. 
  Case "n = 0".
    reflexivity. 
  Case "n = S n'".
    simpl. rewrite -> IHn'. reflexivity.   Qed.

(* An exercise to be worked together: *)
Theorem minus_n_n : forall n,
  minus n n = 0.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Exercise: 1 star (basic_induction) *)
(* And some for you... *)

(* CMSC 631 *)
Theorem mult_0_r : forall n:nat,
  mult n 0 = 0.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* CMSC 631 *)
Theorem plus_n_Sm : forall n m : nat, 
  S (plus n m) = plus n (S m).
Proof. 
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* CMSC 631 *)
Theorem plus_comm : forall n m : nat,
  plus n m = plus m n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ----------------------------------------------------------------------- *)
(* Formal vs. informal proof *)

(* An unreadable formal proof *)
Theorem plus_assoc' : forall n m p : nat,
  plus n (plus m p) = plus (plus n m) p.
Proof. intros n m p. induction n as [| n']. reflexivity. 
simpl. rewrite -> IHn'. reflexivity.  Qed.

(* A careful informal proof of the same theorem:

   By induction on n.
     - First, suppose n = 0.  We must show
         plus 0 (plus m p) = plus (plus 0 m) p.
       This follows directly from the definition of plus.
     - Next, suppose n = S n', with
         plus n' (plus m p) = plus (plus n' m) p.
       We must show
         plus (S n') (plus m p) = plus (plus (S n') m) p.
       By the definition of plus, this follows from
         S (plus n' (plus m p)) = S (plus (plus n' m) p),
       which is immediate from the induction hypothesis.
*)

(* Exercise: 2 stars (plus_comm_informal) *)
(* CMSC 631 *)
(* As an exercise, try translating your solution for
plus_comm into an informal proof. *)
(* Informal proof:
Theorem: plus is commutative.
Proof:
   FILL IN HERE

     - Next, suppose m = S m' for some m' such that plus n m' = plus m' n.
       By the definition of plus and the inductive hypothesis, 
       plus (S m') n = S (plus m' n) = S (plus n m').  It
       remains to show plus n (S m') = S (plus n m') as well, but
       this is precisely lemma plus_n_Sm.

*)

(* Exercise: write a formal proof of the following theorem, using
   the provided informal proof as a guide

Theorem : For any n, true = beq_nat n n
Proof :
   By induction on n.
     - First, suppose n = 0.  We must show
         true = beq_nat n n.
       This follows directly from the definition of beq_nat.
     - Next, suppose n = S n', with
         true = beq_nat n' n'.
       We must show
         true = beq_nat (S n') (S n')
       This follows directly from the IH and the definition of
       beq_nat.
*)

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

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

(* An alternate proof of [mult_0_plus], using an
   in-line assertion instead of a separate lemma. *)
Theorem mult_0_plus' : forall n m : nat,
  mult (plus 0 n) m = mult n m.
Proof.
  intros n m.
  assert (plus 0 n = n). 
    Case "Proof of assertion". reflexivity.
  rewrite -> H.
  reflexivity.  Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  plus (plus n m) (plus p q) = plus (plus m n) (plus p q).
Proof.
  intros n m p q.
  (* We just need to swap (plus n m) for (plus m n)...
     it seems like plus_comm should do the trick! *)
  rewrite -> plus_comm. 
  (* Doesn't work...Coq rewrote the wrong plus! *)
Admitted.

Theorem plus_rearrange : forall n m p q : nat,
  plus (plus n m) (plus p q) = plus (plus m n) (plus p q).
Proof.
  intros n m p q.
  assert (plus n m = plus m n).
    Case "Proof of assertion".
    rewrite -> plus_comm. reflexivity.
  rewrite -> H. reflexivity.  Qed.

(* Exercise: 2 stars (mult_comm) *)
(* CMSC 631 *)
(* Use assert to help prove this theorem. *)
Theorem plus_swap : forall n m p : nat, 
  plus n (plus m p) = plus m (plus n p).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* HIDE WHEN EXERCISE *)
Theorem mult_m_Sn : forall m n : nat,
 mult m (S n) = plus m (mult m n).
Proof.
  induction m as [| m'].
  Case "m = 0".
    intros n. simpl. reflexivity.
  Case "m = S m'".
    intros n.
    simpl.
    rewrite -> IHm'.
    rewrite -> plus_swap.
    reflexivity.  Qed.

(* Prove commutativity of multiplication.  (You will
   probably need to define and prove a subsidiary theorem
   to be used in the proof of this one.  Either give it a
   separate name or else use an in-line [assert].) You may
   find that [plus_swap] comes in handy. *)
(* CMSC 631 *)
Theorem mult_comm : forall m n : nat,
 mult m n = mult n m.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Exercise: 2 stars *)
(* CMSC 631 *)
Theorem evenb_n__oddb_Sn : forall n,
  evenb n = negb (evenb (S n)).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* ------------------------------------------------------- *)
(* More exercises *)

(* Exercise: 2 stars (more_exercises) *)
(* In this set of exercises, you should think about which
   theorems need induction, which need [destruct], and
   which can be proved using just the [simpl] and
   [reflexivity] tactics and existing lemmas?  Make your
   prediction before attempting the proof in Coq. *)

Theorem ble_nat_refl : forall n,
  true = ble_nat n n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem plus_ble_compat_l : forall n m p, 
  ble_nat n m = true -> ble_nat (plus p n) (plus p m) = true.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem S_nbeq_0 : forall n:nat,
  beq_nat (S n) 0 = false.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem mult_1_l : forall n:nat, mult 1 n = n.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem all3_spec : forall b c : bool,
    orb
      (andb b c)
      (orb (negb b)
               (negb c))
  = true.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem mult_plus_distr_r : forall n m p : nat,
  mult (plus n m) p = plus (mult n p) (mult m p).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem mult_assoc : forall n m p : nat,
  mult n (mult m p) = mult (mult n m) p.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* -------------------------------------------------- *)
(* A few more miscellaneous facts that we'll need later on
   in the course... *)

Theorem orb_true_r : forall b,
  orb b true = true.
Proof.
  intros b.
  destruct b.
    reflexivity.
    reflexivity.  Qed.

Theorem negb_flip : forall b1 b2,
  negb b1 = b2 ->
  b1 = negb b2.
Proof.
  intros b1 b2. intros H.
  rewrite <- H.
  rewrite -> negb_involutive.
  reflexivity.  Qed.

Theorem plus_1_r : forall n:nat,
  plus n 1 = S n.
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".
    reflexivity.
  Case "n = S n'".
    simpl. rewrite -> IHn'. reflexivity.  Qed.

Theorem mult_1_r : forall n:nat,
  mult n 1 = n.
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".
    reflexivity.
  Case "n = S n'".
    simpl. rewrite -> IHn'. reflexivity.  Qed.