(* 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.