From af19eb9f42540ea05fcadcfbb8374fc2ce49be8c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 12 Feb 2020 14:03:15 -0500 Subject: [PATCH] Update FirstClassFunctions_template from new source material --- FirstClassFunctions_template.v | 329 ++++++++++++++++++++++++++++++--- 1 file changed, 306 insertions(+), 23 deletions(-) diff --git a/FirstClassFunctions_template.v b/FirstClassFunctions_template.v index 157ac4e..1db0a58 100644 --- a/FirstClassFunctions_template.v +++ b/FirstClassFunctions_template.v @@ -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'