(** Most of the contents in the file were extracted from lec1.v 
    written by B. C. Pierce.
    You can visit 
       http://www.seas.upenn.edu/~cis500/cis500-f07/schedule.html
    for detail of lec1.v.
    Others were wtritten by Yu Zhang (yuzhang AT ustc.edu.cn) *)

(* -------------------------------------------------------------- *)
(** * Yes/no answers *)

(** Here is an even simpler type declaration, corresponding 
    to the built-in type of booleans in most programming
    languages.  We will use it heavily in what follows. *)
Inductive yesno : Set :=
  | yes : yesno
  | no : yesno.

(** Coq will define the following four types for the above 
    definitions:
      yesno
      yesno_rect
      yesno_ind
      yesno_rec
    You can use "Check <name>" command to check the 
    definition of <name>. *)
Check yesno.
(**  yesno 
     : Set   
*)

Check yesno_rect.
(**  yesno_rect
     : forall P : yesno -> Type, P yes -> P no -> forall y : yesno, P y
*)

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

Check yesno_rec.
(**  yesno_rec
     : forall P : yesno -> Set, P yes -> P no -> forall y : yesno, P y
*)

Definition swap_yesno (b:yesno) : yesno :=
  match b with
  | yes => no
  | no => yes
  end.

(* Note that functions like [swap_yesno] are also a data
   values, just like [yes] and [no].  Their types are called
   "function types." 

   The type of [swap_yesno], written [yesno->yesno], is
   pronounced "[yesno] arrow [yesno]."  It can be thought of
   like this: "Given an input of type [yesno], this function
   produces an output of type [yesno]."
*)

Check (swap_yesno).

(* [Check] just instructs Coq to print the type of an
   expression. *)

Definition both_yes (b1:yesno) (b2:yesno) : yesno :=
  match b1 with
  | yes => b2
  | no => no
  end.

(* The type of [both_yes], written [yesno->yesno->yesno],
   can be thought of like this: "Given two inputs, both of
   type [yesno], this function produces an output of type
   [yesno]." *)

Check (both_yes).

(* EXERCISE: Uncomment and then complete the definitions of
   the following functions, making sure that the assertions
   below each can be verified by Coq.

Definition one_yes (b1:yesno) (b2:yesno) : yesno :=
FILL IN HERE

Lemma check_one_yes1: 
  (one_yes yes no) = yes.
Proof. simpl. reflexivity. Qed.
Lemma check_one_yes2: 
  (one_yes no no) = no.
Proof. simpl. reflexivity. Qed.
Lemma check_one_yes3: 
  (one_yes no yes) = yes.
Proof. simpl. reflexivity. Qed.

Definition all3_yes (b1:yesno) (b2:yesno) (b3:yesno) : yesno :=
FILL IN HERE

Lemma check_all3_yes1: 
  (all3_yes yes yes yes) = yes.
Proof. simpl. reflexivity. Qed.
Lemma check_all3_yes2: 
  (all3_yes no yes yes) = no.
Proof. simpl. reflexivity. Qed.
Lemma check_all3_yes3: 
  (all3_yes yes no yes) = no.
Proof. simpl. reflexivity. Qed.
Lemma check_all3_yes4: 
  (all3_yes yes yes no) = no.
Proof. simpl. reflexivity. Qed.
*)

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

(* The types we defined above are octen called "enumerated
   types" because their definitions explicitly enumerate a
   finite collection of elements. 

   A more interesting way of defining a type is to give a
   collection of INDUCTIVE RULES describing its elements.
   For example, we can define the natural numbers as
   follows:
*)
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Check nat_ind.

(* This definition can be read: 
     - [O] is a natural number (note that this is the letter
       "O", not the numeral "0")
     - [S] is a function that takes a natural number and
       gives us another one -- that is, if [n] is a natural
       number, then [S n] is too.
*)

(* We can write some annotated inductive type definitions
   for even. *)
Inductive evenP : nat -> Prop :=
  | even_O : evenP O
  | even_SS : forall n:nat, evenP n -> evenP (S (S n)).

Check evenP_ind.

Inductive evenT : nat -> Type :=
  | evenT_O : evenT O
  | evenT_SS : forall n:nat, evenT n -> evenT (S (S n)).

Check evenT_rect.

Check evenT_rec.

Check evenT_ind.

Inductive evenS : nat -> Set :=
  | evenS_O : evenS O
  | evenS_SS : forall n:nat, evenS n -> evenS (S (S n)).

Check evenS_rect.

Check evenS_rec.

Check evenS_ind.

(* We can write definitions of mutually inductive types 
   for even and odd. *)
Inductive evenM : nat -> Prop :=
  | evenM_O : evenM O
  | evenM_S : forall n, oddM n -> evenM (S n)
with oddM : nat -> Prop :=
  | oddM_S: forall n, evenM n -> oddM (S n).

Check evenM_ind.

Check oddM_ind.

(* We can write simple functions that pattern match on
   natural numbers just as we did above: *)
Definition pred (m : nat) : nat :=
  match m with
    | O => O
    | S m' => m'
  end.
Check pred.

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

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

(* But for other kinds of function definitions, just pattern
   matching is not enough: we need something new.  For
   example, to check that a number [n] is even, we may need
   to "recursively" check whether [n-2] is even.  To write
   such functions, we use the keyword [Fixpoint].
*)
Fixpoint even (n:nat) {struct n} : yesno := 
  match n with
  | O        => yes
  | S O      => no
  | S (S n') => even n'
  end.
(* One important thing to note about this definition is the
   declaration [{struct n}] on the first line.  This tells
   Coq to check that we are performing a "structural
   recursion" over the argument [n] -- i.e., that we make
   recursive calls only on strictly smaller values of [n].
   This allows Coq to check that all calls to [even] will
   eventually terminate. *)
Check even.

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

Definition odd (n:nat) : yesno := 
  swap_yesno (even n).

Lemma check_odd1: 
  (odd (S O)) = yes.
Proof. simpl. reflexivity. Qed.
Lemma check_odd2: 
  (odd (S (S (S (S O))))) = no.
Proof. simpl. reflexivity. Qed.

(* Of course, we can also define multi-argument functions by
   recursion. *)
Fixpoint plus (m : nat) (n : nat) {struct m} : nat :=
  match m with
    | O => n
    | S m' => S (plus m' n)
  end.

Check plus.

(* A notational convenience: If two or more arguments have
   the same type, they can be written together.  Here,
   writing [(m n : nat)] is just the same as if we had
   written [(m : nat) (n : nat)]. *)
Fixpoint times (m n : nat) {struct m} : nat :=
  match m with
    | O => O
    | S m' => plus n (times m' n)
  end.

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

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

Lemma check_times1: 
    (times (S (S (S O))) (S (S (S O))) 
  = (S (S (S (S (S (S (S (S (S O)))))))))).
Proof. simpl. reflexivity. Qed.

(* Such examples are getting a little hard to read!  We could 
   help matters by adding some [Definition]s -- e.g., like this:

      Definition zero  := O.
      Definition one   := (S O).
      Definition two   := (S (S O)).
      Definition three := (S (S (S O))).
      Definition four  := (S (S (S (S O)))).
      Definition five  := (S (S (S (S (S O))))).
      Definition six   := (S (S (S (S (S (S O)))))).

  This would make it easier to ENTER expressions involving
  numbers.  For example, we could now write

      Lemma check_times1': 
          (times three two) 
        = six.

  However, we'd like a little more -- we'd also like for Coq
  to PRINT expressions involving numbers using our short
  names, whenever possible.  We can instruct it to do so by
  using the keyword [Notation] instead of [Definition].
*)
Notation zero  := O.
Notation one   := (S O).
Notation two   := (S (S O)).
Notation three := (S (S (S O))).
Notation four  := (S (S (S (S O)))).
Notation five  := (S (S (S (S (S O))))).
Notation six   := (S (S (S (S (S (S O)))))).
Notation seven := (S (S (S (S (S (S (S O))))))).
Notation eight := (S (S (S (S (S (S (S (S O)))))))).
Notation nine  := (S (S (S (S (S (S (S (S (S O))))))))).
Notation ten   := (S (S (S (S (S (S (S (S (S (S O)))))))))).
Notation eleven:= (S (S (S (S (S (S (S (S (S (S (S O))))))))))).
Notation twelve:= (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))).

Lemma check_times' : 
    (times three two)
  = six.
Proof. simpl. reflexivity. Qed.

(* These notations make it much less painful to see what is
   going on in larger examples: *)
Eval simpl in (exp two three).

(* EXERCISE: Recall that the factorial function is defined
   like this in mathematical notation:
        factorial(0) = 1
        factorial(n) = n * (factorial(n-1))    if n>0
   Translate this into Coq's notation.

Fixpoint factorial (n:nat) {struct n} : nat :=
FILL IN HERE

Lemma check_factorial1: 
  (factorial three) = six.
Proof. simpl. reflexivity. Qed.
Lemma check_factorial2: 
  (factorial five) = (times ten twelve).
Proof. compute. reflexivity. Qed.
*)

(* When we say that Coq comes with nothing built-in, we
   really mean it!  Even equality testing has to be
   defined. *)
Fixpoint eqnat (m n : nat) {struct m} : yesno :=
  match m with 
  | O =>
      match n with 
      | O => yes
      | S n' => no
      end
  | S m' =>
      match n with
      | O => no
      | S n' => eqnat m' n'
      end
  end.

(* EXERCISE: Complete the definitions of the following
   comparison functions.
Fixpoint lenat (m n : nat) {struct m} : yesno :=
FILL IN HERE

Lemma check_lenat1: 
  (lenat two two) = yes.
Proof. simpl. reflexivity. Qed.
Lemma check_lenat2: 
  (lenat two four) = yes.
Proof. simpl. reflexivity. Qed.
Lemma check_lenat3: 
  (lenat four two) = no.
Proof. simpl. reflexivity. Qed.

Definition ltnat (m n : nat) :=
FILL IN HERE

Lemma check_ltnat1: 
  (ltnat two two) = no.
Proof. simpl. reflexivity. Qed.
Lemma check_ltnat2: 
  (ltnat two four) = yes.
Proof. simpl. reflexivity. Qed.
Lemma check_ltnat3: 
  (ltnat four two) = no.
Proof. simpl. reflexivity. Qed.

*)