Update FirstClassFunctions_template from new source material

This commit is contained in:
Adam Chlipala 2020-02-12 14:03:15 -05:00
parent 6f17daa2df
commit af19eb9f42

View file

@ -1,21 +1,26 @@
Require Import Frap.
Require Import Frap Program.
(** * Some data fodder for us to compute with later *)
(* Records are a handy way to define datatypes in terms of the named fields that
* each value must contain. *)
Record programming_language := {
Name : string;
PurelyFunctional : bool;
AppearedInYear : nat
}.
(* Here's a quick example of a set of programming languages, which we will use
* below in some example computations. *)
Definition pascal := {|
Name := "Pascal";
PurelyFunctional := false;
AppearedInYear := 1970
|}.
Definition c := {|
Definition clang := {|
Name := "C";
PurelyFunctional := false;
AppearedInYear := 1972
@ -39,11 +44,16 @@ Definition ocaml := {|
AppearedInYear := 1996
|}.
Definition languages := [pascal; c; gallina; haskell; ocaml].
Definition languages := [pascal; clang; gallina; haskell; ocaml].
(** * Classic list functions *)
(* The trio of "map/filter/reduce" are commonly presented as workhorse
* *higher-order functions* for lists. That is, they are functions that take
* functions as arguments. *)
(* [map] runs a function on every position of a list to make a new list. *)
Fixpoint map {A B} (f : A -> B) (ls : list A) : list B :=
match ls with
| nil => nil
@ -51,7 +61,9 @@ Fixpoint map {A B} (f : A -> B) (ls : list A) : list B :=
end.
Compute map (fun n => n + 2) [1; 3; 8].
(* Note the use of an *anonymous function* above via [fun]. *)
(* [filter] keeps only those elements of a list that pass a Boolean test. *)
Fixpoint filter {A} (f : A -> bool) (ls : list A) : list A :=
match ls with
| nil => nil
@ -59,7 +71,12 @@ Fixpoint filter {A} (f : A -> bool) (ls : list A) : list A :=
end.
Compute filter (fun n => if n <=? 3 then true else false) [1; 3; 8].
(* The [if ... then true else false] bit might seem wasteful. Actually, the
* [<=?] operator has a fancy type that needs converting to [bool]. We'll get
* more specific about such types in a future class. *)
(* [fold_left], a relative of "reduce," repeatedly applies a function to all
* elements of a list. *)
Fixpoint fold_left {A B} (f : B -> A -> B) (ls : list A) (acc : B) : B :=
match ls with
| nil => acc
@ -68,6 +85,7 @@ Fixpoint fold_left {A B} (f : B -> A -> B) (ls : list A) (acc : B) : B :=
Compute fold_left max [1; 3; 8] 0.
(* Another way to see [fold_left] in action: *)
Theorem fold_left3 : forall {A B} (f : B -> A -> B) (x y z : A) (acc : B),
fold_left f [x; y; z] acc = f (f (f acc x) y) z.
Proof.
@ -75,13 +93,22 @@ Proof.
equality.
Qed.
(* Let's use these classics to implement a few simple "database queries" on the
* list of programming languages. Note that each field name from
* [programming_language] is itself a first-class function, for projecting that
* field from any record! *)
Compute map Name languages.
(* names of languages *)
Compute map Name (filter PurelyFunctional languages).
(* names of purely functional languages *)
Compute fold_left max (map AppearedInYear languages) 0.
(* maximum year in which a language appeared *)
Compute fold_left max (map AppearedInYear (filter PurelyFunctional languages)) 0.
(* maximum year in which a purely functional language appeared *)
(* To avoid confusing things, we'll revert to the standard library's (identical)
* versions of these functions for the remainder. *)
@ -90,21 +117,8 @@ Reset map.
(** * Sorting, parameterized in a comparison operation *)
Fixpoint insert {A} (le : A -> A -> bool) (new : A) (ls : list A) : list A :=
match ls with
| [] => [new]
| x :: ls' =>
if le new x then
new :: ls
else
x :: insert le new ls'
end.
Fixpoint insertion_sort {A} (le : A -> A -> bool) (ls : list A) : list A :=
match ls with
| [] => []
| x :: ls' => insert le x (insertion_sort le ls')
end.
Fixpoint insertion_sort {A} (le : A -> A -> bool) (ls : list A) : list A.
Admitted.
Fixpoint sorted {A} (le : A -> A -> bool) (ls : list A) : bool :=
match ls with
@ -116,17 +130,22 @@ Fixpoint sorted {A} (le : A -> A -> bool) (ls : list A) : bool :=
end
end.
Theorem insertion_sort_sorted : forall {A} (le : A -> A -> bool) ls,
sorted le (insertion_sort le ls) = true.
(* Main theorem: [insertion_sort] produces only sorted lists. *)
Theorem insertion_sort_sorted : forall {A} (le : A -> A -> bool),
forall ls,
sorted le (insertion_sort le ls) = true.
Proof.
Admitted.
(* Let's do a quick example of using [insertion_sort] with a concrete
* comparator. *)
Definition not_introduced_later (l1 l2 : programming_language) : bool :=
if AppearedInYear l1 <=? AppearedInYear l2 then true else false.
Compute insertion_sort
not_introduced_later
[gallina; pascal; c; ocaml; haskell].
[gallina; pascal; clang; ocaml; haskell].
Corollary insertion_sort_languages : forall langs,
sorted not_introduced_later (insertion_sort not_introduced_later langs) = true.
@ -134,6 +153,272 @@ Proof.
Admitted.
(** * A language of functions and its interpreter *)
Inductive dyn :=
| Bool (b : bool)
| Number (n : nat)
| List (ds : list dyn).
Definition dmap (f : dyn -> dyn) (x : dyn) : dyn :=
match x with
| List ds => List (map f ds)
| _ => x
end.
Definition dfilter (f : dyn -> dyn) (x : dyn) : dyn :=
match x with
List ds => List (filter (fun arg => match f arg with
| Bool b => b
| _ => false
end) ds)
| _ => x
end.
Definition disZero (x : dyn) : dyn :=
match x with
| Number 0 => Bool true
| Number _ => Bool false
| _ => x
end.
Definition dnot (x : dyn) : dyn :=
match x with
| Bool b => Bool (negb b)
| x => x
end.
Inductive xform :=
| Identity
| Compose (xf1 xf2 : xform)
| Map (xf1 : xform)
| Filter (xf1 : xform)
| ConstantBool (b : bool)
| ConstantNumber (n : nat)
| IsZero
| Not.
Fixpoint transform (xf : xform) : dyn -> dyn :=
match xf with
| Identity => id
| Compose f1 f2 => compose (transform f1) (transform f2)
| Map f => dmap (transform f)
| Filter f => dfilter (transform f)
| ConstantBool b => fun _ => Bool b
| ConstantNumber n => fun _ => Number n
| IsZero => disZero
| Not => dnot
end.
Compute transform (Map IsZero) (List [Number 0; Number 1; Number 2; Number 0; Number 3]).
Compute transform (Filter IsZero) (List [Number 0; Number 1; Number 2; Number 0; Number 3]).
Fixpoint optimize (xf : xform) : xform.
Admitted.
Theorem optimize_ok : forall xf x, transform (optimize xf) x = transform xf x.
Proof.
Admitted.
(** ** Are these really optimizations? Can they ever grow a term's size? *)
Fixpoint size (xf : xform) : nat :=
match xf with
| Identity
| Not
| IsZero
| ConstantBool _
| ConstantNumber _ => 1
| Compose xf1 xf2 => 1 + size xf1 + size xf2
| Map xf
| Filter xf => 1 + size xf
end.
Theorem optimize_optimizes : forall xf, size (optimize xf) <= size xf.
Proof.
Admitted.
(** ** More interestingly, the same is true of the action of these
transformations on concrete values! *)
Fixpoint sum (ls : list nat) : nat :=
match ls with
| nil => 0
| x :: ls' => x + sum ls'
end.
Fixpoint dsize (d : dyn) : nat :=
match d with
| Bool _
| Number _ => 1
| List ds => 1 + sum (map dsize ds)
end.
Theorem neverGrow : forall xf x,
dsize (transform xf x) <= dsize x.
Proof.
Admitted.
(** * Combinators for syntax-tree transformations *)
(* Let's reprise the imperative language from the end of Interpreters. *)
Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).
Definition valuation := fmap var nat.
Fixpoint interp (e : arith) (v : valuation) : nat :=
match e with
| Const n => n
| Var x =>
match v $? x with
| None => 0
| Some n => n
end
| Plus e1 e2 => interp e1 v + interp e2 v
| Minus e1 e2 => interp e1 v - interp e2 v
| Times e1 e2 => interp e1 v * interp e2 v
end.
Inductive cmd :=
| Skip
| Assign (x : var) (e : arith)
| Sequence (c1 c2 : cmd)
| Repeat (e : arith) (body : cmd).
Fixpoint selfCompose {A} (f : A -> A) (n : nat) : A -> A :=
match n with
| O => fun x => x
| S n' => fun x => selfCompose f n' (f x)
end.
Lemma selfCompose_extensional : forall {A} (f g : A -> A) n x,
(forall y, f y = g y)
-> selfCompose f n x = selfCompose g n x.
Proof.
induct n; simplify; try equality.
rewrite H.
apply IHn.
trivial.
Qed.
Fixpoint exec (c : cmd) (v : valuation) : valuation :=
match c with
| Skip => v
| Assign x e => v $+ (x, interp e v)
| Sequence c1 c2 => exec c2 (exec c1 v)
| Repeat e body => selfCompose (exec body) (interp e v) v
end.
Fixpoint seqself (c : cmd) (n : nat) : cmd :=
match n with
| O => Skip
| S n' => Sequence c (seqself c n')
end.
(* Now consider a more abstract way of describing optimizations concisely. *)
Record rule := {
OnCommand : cmd -> cmd;
OnExpression : arith -> arith
}.
Fixpoint bottomUp (r : rule) (c : cmd) : cmd :=
match c with
| Skip => r.(OnCommand) Skip
| Assign x e => r.(OnCommand) (Assign x (r.(OnExpression) e))
| Sequence c1 c2 => r.(OnCommand) (Sequence (bottomUp r c1) (bottomUp r c2))
| Repeat e body => r.(OnCommand) (Repeat (r.(OnExpression) e) (bottomUp r body))
end.
Definition crule (f : cmd -> cmd) : rule :=
{| OnCommand := f; OnExpression := fun e => e |}.
Definition erule (f : arith -> arith) : rule :=
{| OnCommand := fun c => c; OnExpression := f |}.
Definition andThen (r1 r2 : rule) : rule.
Admitted.
Definition plus0 := erule (fun e =>
match e with
| Plus e' (Const 0) => e'
| _ => e
end).
Definition unrollLoops := crule (fun c =>
match c with
| Repeat (Const n) body => seqself body n
| _ => c
end).
Compute bottomUp plus0
(Sequence (Assign "x" (Plus (Var "x") (Const 0)))
(Assign "y" (Var "x"))).
Compute bottomUp unrollLoops
(Repeat (Plus (Const 2) (Const 0))
(Sequence (Assign "x" (Plus (Var "x") (Const 0)))
(Assign "y" (Var "x")))).
Compute bottomUp (andThen plus0 unrollLoops)
(Repeat (Plus (Const 2) (Const 0))
(Sequence (Assign "x" (Plus (Var "x") (Const 0)))
(Assign "y" (Var "x")))).
Definition correct (r : rule) : Prop.
Admitted.
Theorem crule_correct : forall f,
(forall c v, exec (f c) v = exec c v)
-> correct (crule f).
Proof.
Admitted.
Theorem erule_correct : forall f,
(forall e v, interp (f e) v = interp e v)
-> correct (erule f).
Proof.
Admitted.
Theorem andThen_correct : forall r1 r2,
correct r1
-> correct r2
-> correct (andThen r1 r2).
Proof.
Admitted.
Theorem bottomUp_correct : forall r,
correct r
-> forall c v, exec (bottomUp r c) v = exec c v.
Proof.
Admitted.
Definition rBottomUp (r : rule) : rule.
Admitted.
Theorem rBottomUp_correct : forall r,
correct r
-> correct (rBottomUp r).
Proof.
Admitted.
Definition zzz := Assign "x" (Plus (Plus (Plus (Var "x") (Const 0)) (Const 0)) (Const 0)).
Compute bottomUp plus0 zzz.
Compute bottomUp (rBottomUp plus0) zzz.
Compute bottomUp (rBottomUp (rBottomUp plus0)) zzz.
Compute bottomUp (rBottomUp (rBottomUp (rBottomUp plus0))) zzz.
(** * Motivating continuations with search problems *)
Fixpoint allSublists {A} (ls : list A) : list (list A) :=
@ -146,8 +431,6 @@ Fixpoint allSublists {A} (ls : list A) : list (list A) :=
Compute allSublists [1; 2; 3].
Definition sum ls := fold_left plus ls 0.
Fixpoint sublistSummingTo (ns : list nat) (target : nat) : option (list nat) :=
match filter (fun ns' => if sum ns' ==n target then true else false) (allSublists ns) with
| ns' :: _ => Some ns'