Require Import Program. (* for compose, identity *) Require Import Arith. (* for leb, negb *) Require Import List. (* for filter *) Definition ident x := x. Error: Cannot infer the type of x. Definition ident_n (x:nat) := x. Compute ident_n 3. Definition ident (X:Type) (x:X) := x. Compute ident nat 3. Compute ident bool true. Compute ident nat true. Error: The term “true” has type “bool” while it is expected to have type “nat”. Definition ident2 {X:Type} (x:X) := x. ident2 is defined Compute ident2 3. Compute ident2 true. (*alternately, define them after the fact: *) Implicit Arguments ident [X]. Compute ident 3. Compute ident true. Print Implicit ident. Print Implicit ident2. (* pass functions around *) Check map. Check mult 2. Compute map (mult 2) (1::2::3::4::nil). Compute map ident [1;2;3;4]. (* doesn't work - not maximally inserted *) Compute map ident2 [1;2;3;4]. (* return functions *) Check leb. Compute map (leb 3) [1;2;3;4;5;6]. Compute map (fun x => (leb x 3)) [1;2;3;4;5;6]. Definition mycompose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). (* Check mycompose negb leb. *) Check mycompose negb (leb 3). Compute mycompose negb (leb 3). Definition mycompose2 {A B C : Type} (g : B -> C) (f : A -> B) (x : A) := g (f x). Check mycompose negb (leb 3). Check mycompose2 negb (leb 3). (* we think they're the same... let's see! [don't take my word for it]*) Theorem compose_uncurry_eq : forall (A B C : Type) (f : B -> C) (g : A -> B) (x : A), mycompose f g x = mycompose2 f g x. intros. (* simpl. *) compute. reflexivity. Qed. (* generalizing *) Fixpoint sum (l : list nat) := match l with nil => 0 | n :: ns => plus n (sum ns) end. Check plus. Fixpoint product (l: list nat) := match l with nil => 1 | n :: ns => mult n (product ns) end. Fixpoint fold_rt {A B:Type} (f:A->B->B) (z:B) (l:list A) := match l with nil => z | n :: ns => f n (fold_rt f z ns) end. Definition sum2 l := fold_rt plus 0 l. Definition prod2 := fold_rt mult 1. Compute sum2 [1;2;4]. Compute prod2 [1;2;4]. Check fold_right. Check fold_left. (* passing 'cons' and 'nil' gives the identity on lists *) Compute fold_right cons nil [true;false;false]. (* using fold_left with the same gives a reverse on lists *) (* ['flip' swaps the first two arguments of a function] *) Compute fold_left (flip cons) [true;false;false] nil. (* (* A good excercise to do ? *) Theorem fl_fr_assoc_equiv : forall (A:Type) (f:A->A->A) (l:list A), (forall (x y z:A), (f x (f y z)) = (f (f x y) z)) -> (forall (z:A), fold_left f l z = fold_right f z l). (* end excercise *) *) Check filter Check compose. Print Implicit compose. SearchAbout compose. Infix "o" := compose (at level 40, left associativity). SearchAbout compose. Locate "_ o _". (* Fixpoint quicksort_n xs := match xs with nil => nil | cons p xs' => let less := filter (compose negb (leb p)) xs' in let more := filter (leb p) xs' in (quicksort_n less) ++ (p :: nil) ++ (quicksort_n more) end. (* doesn't work! *) *) Inductive Len := Lnnil : Len | Lncons : Len -> Len. Fixpoint toLen (l : list nat) : Len := match l with nil => Lnnil | (x::xs) => Lncons (toLen xs) end. (* not needed yet!*) Fixpoint fromLen (len : Len) := match len with Lnnil => 0 | Lncons l' => S (fromLen l') end. Fixpoint quicksort_nl lst len := match len with Lnnil => nil | Lncons l => match lst with nil => nil | cons x xs => let less := filter (compose negb (leb x)) xs in let more := filter (leb x) xs in (quicksort_nl less l) ++ (cons x nil) ++ (quicksort_nl more l) end end. Definition quicksort_n lst := quicksort_nl lst (toLen lst). Compute quicksort_n (4::2::77::23::1::0::34::nil). Compute quicksort_n [34; 23;1;6;2;4;7;2;234;7;2]. (* polymorphic version *) Fixpoint quicksort_l {A:Type} (leb:A->A->bool) (lst:list A) (len:Len) := match len with Lnnil => nil | Lncons l => match lst with nil => nil | cons x xs => let less := filter (compose negb (leb x)) xs in let more := filter (leb x) xs in (quicksort_l leb less l) ++ (cons x nil) ++ (quicksort_l leb more l) end end. Check toLen. Fixpoint toLenA {A:Type} (l:list A) := match l with nil => Lnnil | cons _ l' => Lncons (toLenA l') end. Definition quicksort {A:Type} cmp (lst:list A) := quicksort_l cmp lst (toLenA lst). Check quicksort. Check quicksort_l. Compute quicksort leb (4::2::77::23::1::0::34::nil). Compute quicksort leb [34; 23;1;6;2;4;7;2;234;7;2]. Compute quicksort (fun x => negb o (leb x)) [34;23;1;6;2;4;7;2;234;7;2].