(* Polymorphism and higher-order functions
   Version of 1/26/2009

   Do NOT submit this file!  We've put out Poly_partial.v so that you
   can review Monday's lecture and play with the new ideas.

   Again, you'll need to compile the earlier files for this one to
   work: both Basics.v and Lists.v.
*)

Require Export Lists.

(* ---------------------------------------------------------------------- *)
(* Polymorphic lists *)

(* Lists of booleans *)
Inductive boollist : Set :=
  | bool_nil : boollist
  | bool_cons : bool -> boollist -> boollist.

(* A datatype for lists with elements drawn from any set X *)
Inductive list (X:Set) : Set :=
  | nil : list X
  | cons : X -> list X -> list X.

Check nil.
Check cons.

Check (cons nat 2 (cons nat 1 (nil nat))).

(* Polymorphic versions of some functions we've already seen *)
Fixpoint length (X:Set) (l:list X) {struct l} : nat := 
  match l with
  | nil      => 0
  | cons h t => S (length X t)
  end.

Check length.

Example test_length1 :
    length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.
Proof. reflexivity. Qed.
Example test_length2 :
    length bool (cons bool true (nil bool)) = 1.
Proof. reflexivity. Qed.

Fixpoint app (X : Set) (l1 l2 : list X) {struct l1} 
                : (list X) := 
  match l1 with
  | nil      => l2
  | cons h t => cons X h (app X t l2)
  end.

Fixpoint snoc (X:Set) (l:list X) (v:X) {struct l} : (list X) := 
  match l with
  | nil      => cons X v (nil X)
  | cons h t => cons X h (snoc X t v)
  end.
Fixpoint rev (X:Set) (l:list X) {struct l} : list X := 
  match l with
  | nil      => nil X
  | cons h t => snoc X (rev X t) h
  end.

(* Some examples with lists of different types.  Note that
   we are using [nil] and [cons] because we haven't yet
   defined the notations [] or ::. *)
Example test_rev1 :
    rev nat (cons nat 1 (cons nat 2 (nil nat))) 
  = (cons nat 2 (cons nat 1 (nil nat))).
Proof. reflexivity. Qed.
Example test_rev2: 
  rev bool (nil bool) = nil bool.
Proof. reflexivity. Qed.

(* -------------------------------------------------- *)
(* Argument synthesis *)

(* Supplying every type argument is boring... *)
Definition l123 := 
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

(* ... but Coq can usually infer them -- just replace the
   type argument by _ and it will use unification to try
   to find a reasonable value. *)
Definition l123' := cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

Fixpoint length' (X:Set) (l:list X) {struct l} : nat := 
  match l with
  | nil      => 0
  | cons h t => S (length' _ t)
  end.

(* -------------------------------------------------- *)
(* Implicit arguments *)

(* To avoid writing too many _'s, we can tell Coq that we
   want it ALWAYS to infer the type argument(s) of a given
   function. *)
Implicit Arguments nil [X].
Implicit Arguments cons [X].
Implicit Arguments length [X].
Implicit Arguments app [X].
Implicit Arguments rev [X].
Implicit Arguments snoc [X].

(* A small problem: this definition fails, because Coq
   doesn't know what implicit argument to use for [nil]...

Definition mynil := nil. 
*)

(* To tell Coq that we want to supply a type argument just
   this once, even though we've declared the function to
   take this argument implicitly, use @ *)
Definition mynil := @nil nat.

(* Now we can define convenient notation for lists, as
   before *)
Notation "x :: y" := (cons x y) 
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y) 
                     (at level 60, right associativity).

Definition l123'' := [1, 2, 3].

(* -------------------------------------------------- *)
(* Polymorphism exercises *)

(* A few easy exercises, just like ones in Lists.v (for
   practice with polymorphism)... *)

(** <<
Fixpoint repeat (X : Set) (n : X) (count : nat) {struct count} : list X := 
  FILL IN HERE

Example test_repeat1: 
  repeat bool true 2 = cons true (cons true nil).
Proof. reflexivity. Qed.
>> *)

Theorem nil_app : forall X:Set, forall l:list X, 
  app [] l = l.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Example const_app : forall l:list nat, 
  app [3,4] l = 3 :: 4 :: l.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Some more easy exercises, not too different from things
   we've seen in Lists.v... *)

Theorem rev_snoc : forall X : Set, 
                     forall v : X,
                     forall s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem snoc_with_append : forall X : Set, 
                         forall l1 l2 : list X,
                         forall v : X,
  snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* -------------------------------------------------- *)
(* Higher-order functions *)

(* A function that applies another function three times *)
Definition doit3times (X:Set) (f:X->X) (n:X) : X := 
  f (f (f n)).

Example test_doit3times1:  doit3times nat minustwo 9 = 3.
Proof. reflexivity. Qed.
Example test_doit3times2:  doit3times nat (plus 3) 2 = 11.
Proof. reflexivity. Qed.
Example test_doit3times3:  doit3times bool negb true = false.
Proof. reflexivity. Qed.

Check doit3times.

Implicit Arguments doit3times [X].

(* -------------------------------------------------- *)
(* Partial application and anonymous functions *)

Check plus.
Definition plus3 := plus 3.
Check plus3.

Example test_plus3 :    plus3 4 = 7.
Proof. reflexivity. Qed.
Example test_plus3' :   doit3times plus3 0 = 9.
Proof. reflexivity. Qed.
Example test_plus3'' :  doit3times (plus 3) 0 = 9.
Proof. reflexivity. Qed.

(* Functions can be defined anonymously, in-line... *)
Example test_anon_fun: 
  doit3times (fun (n:nat) => mult n n) 2 = 256.
Proof. reflexivity. Qed.

(* Coq can infer the type of the anonymous function here
   from the fact that it is being used in a context where
   it is applied to a number *)
Example test_doit3times4: 
  doit3times (fun n => minus (mult n 2) 1) 2 = 9.
Proof. reflexivity. Qed.

(* -------------------------------------------------- *)
(* Map *)

(* Do something to each element of a list, returning a new
   list (possibly of a new type!) *)
Fixpoint map (X:Set) (Y:Set) (f:X->Y) (l:list X) {struct l} 
             : (list Y) := 
  match l with
  | []     => []
  | h :: t => (f h) :: (map _ _ f t)
  end.

Example test_map1: map nat nat (plus 3) [2,0,2] = [5,3,5].
Proof. reflexivity. Qed.

Implicit Arguments map [X Y].

Example test_map2: map oddb [2,1,2,5] = [false,true,false,true].
Proof. reflexivity. Qed.

Example test_map3: 
  map (fun n => [evenb n,oddb n]) [2,1,2,5] = 
  [[true,false],[false,true],[true,false],[false,true]].
Proof. reflexivity. Qed.

(* Exercise: show that map and rev commute.  You may need
   to define an auxiliary lemma. *)
Theorem map_rev : forall (X Y : Set) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

(* Exercise *)
(** <<
Fixpoint flat_map (X:Set) (Y:Set) (f:X -> list Y) (l:list X) {struct l} 
                   : (list Y) := 
  FILL IN HERE

Implicit Arguments flat_map [X Y].

Example test_flat_map1: 
  flat_map (fun n => [n,n,n]) [1,5,4]
  = [1, 1, 1, 5, 5, 5, 4, 4, 4].
Proof. reflexivity. Qed.
>> *)

(* -------------------------------------------------- *)
(* Filter *)

Fixpoint filter (X:Set) (test: X->bool) (l:list X) 
                {struct l} : (list X) :=
  match l with
  | []     => []
  | h :: t => if test h then h :: (filter _ test t)
                        else       filter _ test t
  end.

Implicit Arguments filter [X].

Example test_filter1: filter evenb [1,2,3,4] = [2,4].
Proof. reflexivity. Qed.
Example test_filter2: 
  filter (fun l => beq_nat (length l) 1) 
         [ [1, 2], [3], [4], [5,6,7], [], [8] ]
  = [ [3], [4], [8] ].
Proof. reflexivity. Qed.

Definition countoddmembers' (l:list nat) : nat := 
  length (filter oddb l).

Example test_countoddmembers'1:   countoddmembers' [1,0,3,1,4,5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2:   countoddmembers' [0,2,4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3:   countoddmembers' nil = 0.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------- *)
(* Polymorphic options *)

Inductive option (X:Set) : Set :=
  | Some : X -> option X
  | None : option X.

Implicit Arguments Some [X].
Implicit Arguments None [X].

(* A mapping function for options: do something to
   (Some x), but leave None alone... *)
Definition map_option (X Y : Set) (f : X -> Y) (xo : option X) 
                      : option Y :=
  match xo with
    | None => None
    | Some x => Some (f x)
  end.

Implicit Arguments map_option [X Y].

(* Exercise *)
(** <<
Fixpoint index 
  FILL IN HERE

Implicit Arguments index [X].

Example test_index1 :    index 0 [4,5,6,7]  = Some 4.
Proof. reflexivity. Qed.
Example test_index2 :    index  1 [[1],[2]]  = Some [2].
Proof. reflexivity. Qed.
Example test_index3 :    index  2 [true]  = None.
Proof. reflexivity. Qed.
>> *)

(* Exercise *)
(** <<
Definition hd_opt (X : Set) (l : list X)  : option X :=
  FILL IN HERE

Implicit Arguments hd_opt [X].

Example test_hd_opt1 :    @hd_opt nat [] = None.
Proof. reflexivity. Qed.
Example test_hd_opt2 :  hd_opt [1,2] = Some 1. 
Proof. reflexivity. Qed.
Example test_hd_opt3 :   hd_opt  [[1],[2]]  = Some [1].
Proof. reflexivity. Qed.
>> *)

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

(* Sometimes the [simpl] tactic doesn't make things quite
   as simple as we need.  (Explaining exactly what [simpl]
   does is actually fairly tricky, but two points are very
   useful to understand: First, [simpl] does not unfold
   Definitions.  Second, [simpl] only unfolds a [Fixpoint]
   if this unfolding enables an ADDITIONAL reduction
   afterwards, e.g. by exposing a pattern match applied to
   a known constructor.  If it doesn't, then [simpl]
   leaves the application unchanged.)

   The [unfold] tactic can be used in both of these cases
   to explicitly replace a defined name by the right-hand
   side of its definition. *)
Theorem plus3_example : 
  plus3 5 = 8.
Proof.
  simpl.
  (* This [simpl] does nothing.  We are stuck unless we
     know something about the way plus3 is defined.
     Instead, use [unfold]. *) 
  unfold plus3. 
  reflexivity.
Qed.

(* ----------------------------------------------------- *)
(* Mappings *)

(* In the rest of the course, we'll often need to talk
   about "identifiers," such as program variables.  We
   could use strings for this, or (as in a real compiler)
   some kind of fancier structures like symbols from a
   symbol table.  For simplicity, here, let's just use
   natural numbers as identifiers. *)

Definition id := nat. 

(* Now, a [mapping] is a partial function from identifiers
   to members of some other type, [X].  We use an [option]
   in the result type to represent partiality: A result of
   [None] means that the mapping is not defined for the
   given id. *)
Definition mapping (X : Set) := id -> option X.

Definition lookup (X : Set) (k : id) (f : mapping X) 
                  : option X := 
  f k.

Implicit Arguments lookup [X].

Definition binds (X:Set) (k:id) (v:X) (f:mapping X) :=
  lookup k f = Some v.

Implicit Arguments binds [X].

Definition not_bound_in (X:Set) (k:id) (f:mapping X) :=
  lookup k f = None.

Implicit Arguments not_bound_in [X].

Definition empty_mapping (X:Set) : (mapping X) := 
  fun k => None.

Definition extend (X:Set) (f: mapping X) (k:id) (x:X) 
                  : mapping X :=
  fun k' => if beq_nat k k' then Some x else f k'.

Implicit Arguments extend [X].

Theorem extend_eq : forall X x k (f : mapping X),
  binds k x (extend f k x).
Proof.
  intros X x k f.
  (* Note that we can [unfold] more than one definition 
     at a time. *)
  unfold binds, lookup, extend.
  rewrite <- beq_nat_refl.
  reflexivity.
Qed.

Theorem extend_shadow : forall X x1 x2 k1 k2 (f : mapping X),
  binds k1 x1 f ->
  k2 = k1 ->
  binds k1 x2 (extend f k2 x2).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Theorem extend_same_equiv : forall X x1 x2 k1 k2 (f : mapping X),
  lookup k1 (extend (extend f k2 x1) k2 x2) = lookup k1 (extend f k2 x2).
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.