Problem:  Quicksort verification
Contact:  Jeremy Gow  <jeremygo@dai.ed.ac.uk>
Date:     4/28/2000


=================================================================

For definitions see http://www.dai.ed.ac.uk/~jeremygo/defns.shtml

Quicksort verification:

forall l:(list nat). (sorted (qsort l))
forall l:(list nat). x:nat. (occ x (qsort l)) = (occ x l)


Two theorems about foldleft:

forall o1,o2:(t->t->t). l:(list t). x,y,z,a:t.
(o1 a x) = (o2 x a)
and (o1 (o2 x y) z) = (o2 x (o1 y z))
-> (foldleft o1 a l) = (foldright o2 a l)

forall o:(t->t->t). l:(list t). x,y,z,u,e:t
(o x e) = x
and (o (o x y) z) = (o x (o y z))
-> (o u (foldleft o e l)) = (foldleft o u l)


A theorem about divide and conquer functions:

forall f:(t -> t). b,x:t. l:(list t). n:nat.
(f b x) = x ->
(bin_dc f b l) =
(foldright f b (foldright app nil (map (map (f b)) (split n l))))