(** 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 :=
(** Solution *)
  match b1 with
  | yes => yes
  | no => b2
  end.

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 :=
(** Solution *)
  match b1 with
  | yes =>
      match b2 with
      | yes => b3
      | no => no
      end
  | no => no
  end.

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 :=
(** Solution *)
  match n with
  | O => S O
  | S n' => times n (factorial n')
  end.

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 :=
(** Solution *)
  match m with
  | O => yes
  | S m' =>
      match n with
      | O => no
      | S n' => lenat m' n'
      end
  end.

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) :=
(** Solution *)
  match m with
  | O => 
      match n with
      | O => no
      | S n' => yes
      end
  | S m' =>
      match n with
      | O => no
      | S n' => lenat m n'
      end
  end. 

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.