Poly

Polymorphism

Continue basic concepts of functional programming. Begin with polymoriphism.

Polymorphic Lists

List elements: One type -> Other types.

The natlist defined in the last chap.

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

Coq supports polymorphic inductive type definitions.

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

A binding for [X] has been added to the function header.

What sort of thing is [list] itself? A good way to think about it is that the definition of [list] is a function from [Type]s to [Inductive] definitions.

Now when we use them, we must provide a first argu. that is the type of the list they are building.

WHAT TYPE?

Check (nil nat) : list nat.

Check (cons nat 3 (nil nat)) : list nat.

Check nil : forall X : Type, list X.

Check cons : forall X : Type, X -> list X -> list X.

Always a type argument. No! Reducing this annotation burden.

Type Argument Synthesis

Thanks to type inference, we don't always have to write explicit type annotations everywhere (including [Type] when we use polymoriphism).

Fixpoint repeat' X x count : list X :=
  match count with
  | 0        => nil X
  | S count' => cons X x (repeat' X x count')
  end.

[X] use as the first argu. of cons. So it must be a Type. We don't have to write its annotation in the first line.

Type Argument Synthesis

Second argu must be an element of [X] (the first element). Let Coq do it. Write a "hole" [_]. "Please try to figure out for yourself what belongs here."

Definition list123 :=
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

(** ...we can use holes to write this: *)

Definition list123' :=
  cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

Implicit Arguments.

In fact, we can go further and even avoid writing [_]'s in most cases by telling Coq always to infer the type argument(s) of a given function.

Curly braces around any arguments to be treated as implicit.

Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repeat {X} x count.

(** Now, we don't have to supply type arguments at all: *)

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0        => nil
  | S count' => cons x (repeat''' x count')
  end.

We will use the latter style whenever possible, but we will continue to use explicit [Argument] declarations for [Inductive] constructors. The reason for this is that marking the parameter of an inductive type as implicit causes it to become implicit for the type itself, not just for its constructors. For instance, consider the following alternative definition of the [list] type:

Supplying Type Arguments Explicitly

For enough local information to determine a type argument.

@ prefix the function name.

Exercise: re-proof the theorm in Pilymorphism.

Polymorphic Pairs

Polymorphic Pairs, often called Products.

annotation type_scope?

Tells Coq that this abbreviation should only be used when parsing types, not when parsing expressions. This avoids a clash with the multiplication symbol.

Check (bool,bool).
Notation "X * Y" := (prod X Y) : type_scope.
Check (bool,bool).

We can find the differences.

From

(bool, bool)
     : prod Set Set

To

(bool, bool)
     : Set * Set

Becareful to [(x,y)] and [X*Y]. Remeber the first is a value built from two other values, while [X*Y] is a type built from two other types.

First use let...in in Coq, remember to use := instead of = which is usually used in OCaml.

Fixpoint split {X Y : Type} (l : list (X*Y))
  : (list X) * (list Y) :=
  match l with
  | nil => ([],[])
  (* First time use let...in in Coq *)
  | (x,y) :: tl => let (x',y') := split tl
                 in
                 (x::x',y::y')
  end.

Polymorphic Options

After polymorphic lists and pairs, now options.

Functions as Data

Functions as first-class citizens.

Like most modern programming languages -- especially other "functional" languages, including OCaml, Haskell, Racket, Scala, Clojure, etc. -- Coq treats functions as first-class citizens, allowing them to be passed as arguments to other functions, returned as results, stored in data structures, etc.

Higher-Order Functions

Manipulate other functions are often called higher-order functions.

操作其他的函数——高阶函数。

Learning this sub-chap is similar to the learning of functional programming in OCaml.

Filter

过滤器

“Filtering” the list.

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

(** For example, if we apply [filter] to the predicate [evenb]
    and a list of numbers [l], it returns a list containing just the
    even members of [l]. *)


Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.

(* My exercise *)
Theorem filter_false_nil :forall X : Type, forall l: list X,
      filter (fun n => false) l = nil.
  intros.
  induction l.
  - simpl. reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

Anonymous Functions

Construct a function "on the fly" without declaring it at the top or giving it a name.

随时使用，用完即扔（逃

Exercise: partition.

(Github repo)

Map

Map apply the function to each ele. in the lists.

About map_rev, first prove the lemma about map and app.

Here.

(** **** Exercise: 3 stars, standard (map_rev)

    Show that [map] and [rev] commute.  You may need to define an
    auxiliary lemma. *)

Lemma map_app : forall (X Y:Type) (f : X -> Y)  (l1 l2 : list X),
    map f l1 ++ map f l2 = map f (l1 ++ l2).
Proof.
  intros.
  induction l1.
  - simpl. reflexivity.
  - simpl. rewrite IHl1. reflexivity.
Qed.

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  induction l.
  - simpl. reflexivity.
  - simpl. rewrite <- IHl. simpl.
    (* we need a lemma to proof the map_app *)
    rewrite <- map_app. simpl. reflexivity.
Qed.

Fold

An even more powerful higher-order function is called fold. This function is the inspiration for the "[reduce]" operation that lies at the heart of Google's map/reduce distributed programming framework.

Functions That Construct Functions

Curring Functions.

The function with type \(\forall X, X \rightarrow nat \rightarrow X\) is, in fact, same to \(\forall X, X \rightarrow (nat \rightarrow X)\). So we can def a func with one argu and return a \(\nat \rightarrow X\) func.

When we only give the first argu, we get a new func. This kind of usage is also named as partial application.

In Coq, a function [f : A -> B -> C] really has the type [A -> (B -> C)]. That is, if you give [f] a value of type [A], it will give you function [f' : B -> C]. If you then give [f'] a value of type [B], it will return a value of type [C]. This allows for partial application, as in [plus3]. Processing a list of arguments with functions that return functions is called currying, in honor of the logician Haskell Curry.

Definition constfun {X: Type} (x: X) : nat->X :=
  fun (k:nat) => x.

(* The type of function forall X :X->nat->X,
   Actually, it is same to X->(nat->X).
   So we can organize it with one argu [X] and
   return a nat->X function.

   There exists another use for currying function
   named "Partial Application". *)

Check plus : nat -> nat -> nat.

(** Each [->] in this expression is actually a _binary_ operator
    on types.  This operator is _right-associative_, so the type of
    [plus] is really a shorthand for [nat -> (nat -> nat)] -- i.e., it
    can be read as saying that "[plus] is a one-argument function that
    takes a [nat] and returns a one-argument function that takes
    another [nat] and returns a [nat]."  In the examples above, we
    have always applied [plus] to both of its arguments at once, but
    if we like we can supply just the first.  This is called _partial
    application_. *)

Definition plus3 := plus 3.
Check plus3 : nat -> nat.

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.

Additional Exercise

[reflexivity] simplifies expressions a bit more aggressively than [simpl] does.

Currying and uncrrying with the proof of equ.

Definition prod_curry {X Y Z : Type}
  (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).
Check @prod_curry.
(** As an exercise, define its inverse, [prod_uncurry].  Then prove
    the theorems below to show that the two are inverses. *)


Definition prod_uncurry {X Y Z : Type}
           (f : X -> Y -> Z) (p : X * Y) : Z :=
  let (x,y) := p in
  f x y.

(** As a (trivial) example of the usefulness of currying, we can use it
    to shorten one of the examples that we saw above: *)

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

(** Thought exercise: before running the following commands, can you
    calculate the types of [prod_curry] and [prod_uncurry]? *)

Check @prod_curry.
Check @prod_uncurry.

(* the interpretation of curry or uncurring *)

Theorem uncurry_curry : forall (X Y Z : Type)
                        (f : X -> Y -> Z)
                        x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Theorem curry_uncurry : forall (X Y Z : Type)
                        (f : (X * Y) -> Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
  intros.
  unfold prod_curry.
  destruct p as (x,y).
  (* Here we nned destruct p *)
  simpl.
  reflexivity.
Qed.