(* =================================================================== *)
(* 
   This series of exercises contains three parts.
   Part 1 is devoted to the construction of trees (see lecture01_prog.pdf
   in a bottom up, left to right and interactive way.
   - Bottom up: state the type of the output,
       make it step by step using constructs which make such an output.
       If a construct has no input, the corresponding subtree is completed.
       If a construct has inputs, we get new goals for making
       outputs that are plugged at the corresponding place.
   - Left to right : inputs are considered from left to right
   - Interactive : at each step, an uncompleted tree is built,
     and commands are provided for completeing the tree.
     The basic command tu be used is "apply" (followed by the name
     of a tree which makes the desired type).
     Note for the teacher: this way we avoid considerations on the
     syntax of application, especially "currification".

   Part 2 is devoted to case analysis and 1-argument functions.
   The new tactic to be used is called "destruct".
   Small functions with only 1 argument are defined,
   including a strange function called "funny" which returns values
   in several types!
   Note for the teacher: from the beginning arguments are given 
   a name using "forall", next the arrow is introduced as a 
   special case  of "forall". This way, right association is very natural.
   We also get an early introduction to dependent types for free.
   
   Part 3 is devoted to very simple recursive functions
   and elementary proofs by reflexivity.
*)

(* ====================================================================== *)
(* Part 1: interactive construction of trees                              *)
(* ====================================================================== *)

(* Some type definitions *)

Inductive rgb: Set :=
  | Rf : rgb
  | Gf : rgb
  | Bf : rgb
.

Inductive color: Set :=
  | Red : color
  | Orange : color
  | Yellow : color
  | Green : color
  | Blue : color
  | Indigo : color
  | Violet : color
.

Definition R: color := Red.
Definition G: color.
apply Green.
Defined.

Inductive tuple4 : Set :=
  | Mk4rgb : forall x1: rgb, forall x2: rgb, forall x3: rgb, forall x4: rgb, tuple4
  | Mk4color : forall x1 x2 x3 x4: color, tuple4
  | Mk4t4 : forall x1 x2 x3 x4: tuple4, tuple4
.

(* =================================================================== *)

(* Interactive definitions of 4-tuples *)

Definition t1: tuple4.
apply Mk4rgb.
  apply Gf.
  apply Rf.
  apply Gf.
  apply Bf.
Defined.

Definition t2: tuple4.
apply Mk4rgb.
  apply Gf.
  apply Gf.
  apply Gf.
  apply Gf.
Defined.

Definition t3: tuple4.
apply Mk4color.
  apply Violet.
  apply Red.
  apply Yellow.
  apply Orange.
Defined.


(* In order to define a tuple depending on a variable,
   we use the "section" mechanism, which opens a new environment *)
Section a_tuple_with_variable.

Variable x2: rgb.
Variable x4: rgb.

Definition t4: tuple4.
apply Mk4rgb.
  apply Gf.
  apply x2.
  apply Rf.
  apply x4.
Defined.

Definition tuple_of_tuple: tuple4.
apply Mk4t4.
  apply t1.
  apply t2.
  apply t3.
  apply t4.
Defined.

End a_tuple_with_variable.

(* =================================================================== *)
(* Part 2: case analysis and 1-argument functions                      *)
(* =================================================================== *)

(* Definitions by cases *)

Section def_by_cases_on_enum.

Variable r : rgb.

(* INTERACTIVE definition by cases on each possible value of r *)
(* The relevant tactic is called "case" or "destruct" *)

(* First version of the script *)
Definition color_of_r__version1: color.
destruct r.
  (* providing a color for Rf *)
  apply Red.

  (* providing a color for Gf *)
  apply Green.

  (* providing a color for Bf *)
  apply Blue.
Defined.


(* In the previous version, r was visible in each subgoal, 
   but it is not needed *)

(* Second version of the script *)
Definition color_of_r__version2: color.
destruct r.
  (* providing a color for Rf *)
  (* Forget about r *)
  clear r. 
  apply Red.

  (* providing a color for Gf *)
  (* Forget about r *)
  clear r. apply Green.

  (* Forget about r and immediately (";") providing a color for Bf *)
  clear r; apply Blue.
Defined.

(* In the next version, r is cleared immediately on EACH subgoal *)
(* Third version of the script *)
Definition color_of_r__version3: color.
destruct r; clear r.
  apply Red.
  apply Green.
  apply Blue.
Defined.


(* Instead of an interactive definition,
   we can write a DIRECT definition *)

Definition color_of_r__version4 : color :=
  match r with
  | Rf => Red
  | Gf => Green
  | Bf => Blue
  end.

Eval compute in color_of_r__version3.

(* EXERCISE *)
(* Define a value permut_r: rgb such that 

  +---------+--------------+
  |       r | Rf | Gf | Bf |
  +---------+--------------+
  |permut_r | Gf | Bf | Rf |
  +---------+--------------+

*)


(* A trick just there in order to state exercices *)
(* Don't bother to understand it for now. *)
Definition TO_BE_REMOVED {T: Type} : T.
Admitted.

(* In the sequel, put suitable commands and, 
   when successsful, replace Admitted by Defined.
   Note that Admitted destroys the current Definition.
   --> No Admitted and no TO_BE_REMOVED should be left
       at the end. *)
Definition permut_r: rgb.
Admitted.

(* Anything of type rgb can be analyzed,
   for example we can assign a color to each possible
   value of permut_r *)

Definition color_of_permut_r: color.
clear r.
destruct permut_r.
  apply Green.
  apply Blue.
  apply Red.
Defined.

(* This applies to a constant as well!! *)

Definition color_of_Bf := 
  match Bf with
  | Rf => Red
  | Gf => Green
  | Bf => Blue
  end.

Print color_of_Bf.
Compute color_of_Bf.

(* Definition of a Set by destruct on r *)

Definition Set_of_r : Set :=
  match r with
  | Rf => rgb
  | Gf => color
  | Bf => tuple4
  end.

End def_by_cases_on_enum.


(* Parameterized definitions *)

(* We want to say that color_of provides a color
   for all possible values of r; 
   the type of color_of is then just: forall (r: rgb), color.
   what we get is just a function.
*)

Definition color_of : forall (r: rgb), color :=
  fun (r: rgb) => 
  match r with
  | Rf => Red
  | Gf => Green
  | Bf => Blue
  end.

(* A function can be applied to an argument of the expected type *)

Definition cb := color_of Bf.

(* Similarly, we want can define a Set for each r: rgb *)

Definition Set_of : forall (r: rgb), Set :=
  fun (r: rgb) => 
  match r with
  | Rf => rgb
  | Gf => color
  | Bf => tuple4
  end.

(* And we can then define a Set_of r for each r! *)

Definition funny : forall (r: rgb), Set_of r :=
  fun (r: rgb) => 
  match r with
  | Rf => Gf
  | Gf => Yellow
  | Bf => t1
  end.


(*
   In an interactive definition, we use "intro".
   New tactic "red" whose meaning is reduce -- 
   nothing to do with a color!
*)

Definition interactive_funny: forall (r: rgb), Set_of r.
intro r. (* variants: "intro a", etc. *)
destruct r.
  red. apply Gf.
  red. apply Yellow.
  red. apply t1.
Defined.

Eval compute in (funny Bf).
Print t1.

(* ========================================================= *)

(*
   Important abbreviation: when B does not depend on x,
   "forall (x: A), B"  can be written "A -> B"
   Coq displays things in this way whenever possible,
   as can be seen on the interactive definition of color_of.
*)

Definition interactive_color_of : forall (r: rgb), color.
intro r. 
destruct r.
  apply Red.
  apply Green.
  apply Blue.
Defined.


(*
   Consistently, A -> B -> C   means
   "forall (a:A), forall (b:B), C"  which reads
   "forall (a:A), (forall (b:B), C)" , i.e.
   "forall (a:A), (B -> C)" , i.e.
   "A -> (B -> C)"
*)

Definition t4_as_function : forall (x2 x4: rgb), tuple4.
intros x2 x4.
apply (Mk4rgb Gf x2 Rf x4).
Defined.

(* ========================================================================
  ** ADVANCED MATERIAL **
  Here we play with the style used earlier for the function called "funny".
  You can have a look, but you can also skip to the next exercises 
*)

(* 
   Remark that, in interactive_color_of, we can give a type of the
   result which artificially depends on r.
   We first define a stupid function providing the type of the result.
*)

Definition always_color : forall r: rgb, Set := fun r => color.

Definition artificial_interactive_color_of : forall (r: rgb), always_color r.
(* The goal is unchanged, with a forall *)
intro r.
(* now we reduce and destruct *)
red. destruct r.
  apply Red.
  apply Green.
  apply Blue.
Defined.

(* 
  ** End of ADVANCED MATERIAL **
  ======================================================================== 
*)
 


(* =================================================================== *)
(* Part 3: more functions, simple recursivity, 
           proving equations by reflexivity                            *)
(* =================================================================== *)


(* Let us first define a new type with its constructors *)

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

Definition next_weekday : forall d:day, day :=
  fun d: day =>
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => monday
  | saturday => monday
  | sunday => monday
  end.


(* Verification *)
(* What is the expected answer of the following *)

Eval compute in next_weekday (next_weekday saturday).

(* Exercise: define interactively a function which computes 
   the next weekday of the next weekday of a day d, by case on d 
*)

Definition next_next_weekday : forall d: day, day.
(* If you don't like the arrow, 
   you can use the trick in the "advanced material above *)
Admitted.

(* Now don't forget to check on some examples using Eval compute *)

(* ================================ *)
(* Next exercise *)

(* We define an inductive type with exactly two constructors *)

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


Definition negb : forall b:bool, bool := 
  fun b: bool =>
  match b with
  | true => false
  | false => true
  end.
 
Definition andb : forall b1 b2: bool, bool := 
  fun b1 => fun b2 =>
  (* the type of b1 and b2 was guessed from the previous forall *)
  match b1 with 
  | true => b2 
  | false => false
  end.

(* Define andb using the interactive technique *)
Definition andb_interactive : forall b1 b2: bool, bool.
Admitted.

(* Define the Boolean disjunction using the interactive technique
   or directly, as for andb *)
(* Replace TO_BE_REMOVED by a suitable body. *)
Definition orb (b1:bool) (b2:bool) : bool := 
  (* FILL IN HERE *) 
  TO_BE_REMOVED.

(* Now don't forget to check on some examples using Eval compute *)


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

(*
Expected results:
                  (andb3 true true true) --> true.
                  (andb3 false true true) --> false.
                  (andb3 true false true) --> false.
                  (andb3 true true false) --> false.
Where "A --> B" means that 
Eval compute in A 
returns B
*)
(* 
The purpose of the material presented here is to
provide first ideas on programming in Coq.
Students are expected to carefully read explanations,
to run the file, to observe the outputs, and 
to try to provide answers to exercises.
*)

(* Reinventing natural numbers *)

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

(* A commonly used syntax for
Definition pred := fun (n : nat) => 
  match n with etc.

*)

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

(* Let us observe that pred is really fun n : nat => etc. *)
Print pred.

(* Pattern matching can be done at a deeper level 
The following could be written
Definition minustwo (n : nat) : nat :=
  match n with
    | O => O
    | S n' => 
      match n' with
        | O => O
        | S n'' => n''
      end
  end.
*)

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

(* Useful constants *)
Definition n1 := S O.
Definition n2 := S (S O).
Definition n3 := S (S (S O)).
Definition n4 := S (S (S (S O))).
Definition n5 := S n4.
Definition n6 := S n5.
Definition n9 := S (S (S (S (S (S (S (S (S O)))))))).
Definition n10 := S n9.
Definition n12 := S (S n10).


Eval simpl in (minustwo n4).

Check S.
Check pred.
Check minustwo.

(* Next we use an inductive type (bool) defined in the library *)
(* It is the same as in lecture02.v *)

Print bool.

(* Next we use a function (negb) defined in the library *)
Compute (negb true).
Compute (negb false).

(* Recursive definitions have to be introduced in the following way 
   The syntax is similar to the one above for "pred", with the keyword
   "Fixpoint" instead of "Definition".
*)

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S p      => negb (evenb p)
  end.


(* 
The typical scheme for programming on natural numbers is

Fixpoint some_program (n: nat) : type_of_result :=
  match n with
  | O => ...
  | S p =>  ... (some_program p) ...
  end.

Note that p is structurally smaller than n when n = S p

*)


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

(* We check that our definitions return intuitively expected values *)
Compute oddb (S O).

(* A better way to check this is to state what is the expected value,
   and then to prove the expected equality *)
Example test_oddb1:    (oddb (S O)) = true.
Proof. reflexivity.  Qed.
Example test_oddb2:    (oddb (S (S (S (S O))))) = false.
Proof. reflexivity.  Qed.

(* More functions *)
Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O => m
    | S n' => S (plus n' m)
  end.

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


(* Another possible definition for even : 
   n' is structurally smaller than n when n = S (S n')
*)
Fixpoint evenb' (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb' n'
  end.

(* You can match two expressions at once.
   Moreover, note the use of the underscore "_",
   which stands for a joker.
   Any pair of values which was not captured by the previous
   pattern(s) -- here: O, S m' ; S n', O ;  or O, O  -- 
   is captured there.
   Writing _ in a pattern is the same as writing some variable that 
   doesn't get used on the right-hand side.  
   The _ avoids the need to make up a bogus name in this case. *)

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | S n', S m' => minus n' m'
  | _, _ => n
  end.

Eval compute in (fun n => minus (S n) O).


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


Example test_mult1:             (mult n3 n3) = n9.
Proof. simpl. reflexivity.  Qed.

Fixpoint factorial (n:nat) : nat := 
  (* FILL IN HERE *) TO_BE_REMOVED.

Example test_factorial1:          (factorial n3) = n6.
(* FILL IN HERE *) Admitted.
Example test_factorial2:          (factorial n5) = (mult n10 n12).
(* FILL IN HERE *) Admitted.

Notation "x + y" := (plus x y)  (at level 50, left associativity) : nat_scope.
Notation "x - y" := (minus x y)  (at level 50, left associativity) : nat_scope.
Notation "x * y" := (mult x y)  (at level 40, left associativity) : nat_scope.

Check ((O + n1) + n1).

(* Test for equality on nat  *)
Fixpoint beq_nat (n m : nat) : 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.

(* Test for less-or-equal on nat  *)
Fixpoint ble_nat (n m : nat) : 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 n2 n2) = true.
Proof. simpl. reflexivity.  Qed.
Example test_ble_nat2:             (ble_nat n2 n4) = true.
Proof. simpl. reflexivity.  Qed.
Example test_ble_nat3:             (ble_nat n4 n2) = false.
Proof. simpl. reflexivity.  Qed.


(* Test for less-than on nat  *)
Definition blt_nat (n m : nat) : bool :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Example test_blt_nat1:             (blt_nat n2 n2) = false.
(* FILL IN HERE *) Admitted.
Example test_blt_nat2:             (blt_nat n2 n4) = true.
(* FILL IN HERE *) Admitted.
Example test_blt_nat3:             (blt_nat n4 n2) = false.
(* FILL IN HERE *) Admitted.


(* * Proof by Simplification *)

Theorem plus_O_n : forall n:nat, O + n = n.
Proof.
  intros n. reflexivity.  Qed.

(** Step through this proof in Coq and notice how the goal and
    context change. *)

Theorem plus_1_l : forall n:nat, n1 + n = S n. 
Proof.
  intros n. reflexivity.  Qed.

Theorem mult_0_l : forall n:nat, O * n = O.
Proof.
  intros n. reflexivity.  Qed.