# Library quicksort

``` ```
An implementation of QuickSort using Program.

We implement stable quicksort for any ordered type.
``` Module QuickSort(O : OrderedType). ```
Get the facts about the order.
```   Module Facts := OrderedTypeFacts O.   Import O. Import Facts. ```
We work with a decidable equality, not necessarily leibniz, hence all list-processing functions and predicates must be adapted.
```   Require Import Coq.Lists.SetoidList.   Require Import Coq.Sorting.Sorting.   Require Import Coq.Sorting.Permutation.   Require Import Coq.Sorting.PermutSetoid.   Notation permutation := (permutation eq eq_dec). ```
We write `In` for `InA eq` which is appartness up-to the decidable equality.
```   Notation In:=(InA eq). ```
First the auxilliary `split` function, which splits a list `l` into elements lower than `pivot` and the rest.
```   Program Fixpoint split (pivot : t) (l : list t) {struct l} :     { (inf,sup) : list O.t * list O.t |       (forall x, (In x inf <-> (In x l /\ lt x pivot)) /\         (In x sup <-> (In x l /\ ~ lt x pivot))) /\       permutation l (inf ++ sup) } :=     match l with       | hd :: tl =>         dest split pivot tl as (inf,sup) in           if lt_dec hd pivot then (hd :: inf, sup)             else (inf, hd :: sup)       | nil => ([],[])     end. ```
Get back the usual unfold of `In` which is burried in the inductive definition of `InA`.
```   Lemma InA_In : forall x y l, In x (y :: l) -> eq x y \/ In x l. ```
The predicate `le` is just a synonym for `~ lt`
```   Definition le x y := ~ lt y x. ```
Obviously decidable.
```   Program Definition le_dec x y : { le x y } + { le y x } :=     if lt_dec y x then right _ _ else left _ _. ```
That seems right too..
```   Lemma lt_le : forall x y, lt x y -> le x y. ```
We sort using `le` and not `lt`, hence we have to adapt this lemma from the standard library (see `sort_lt_app`).
```   Lemma sort_le_app :     forall l1 l2, sort le l1 -> sort le l2 ->       (forall x y, In x l1 -> In y l2 -> lt x y) ->       sort le (l1 ++ l2). ```
Finally we can `quicksort` a list `l` using the usual definition. Note that we ensure that the resulting list `l'` will be a sorted permutation of `l`. The obligations regarding the recursive calls are easily solved as `split` returns a permutation of its argument `tl`. From this we can easily derive that `length tl = length (inf ++ sup)`. The difficult bit is showing that we are indeed building a sorted permutation. This amounts to a 30 lines proof using quite a few lemmas from the standard library.
```   Program Fixpoint quicksort (l : list t) {measure length l} :     { l' : list t | sort le l' /\ permutation l l'} :=     match l with       | hd :: tl =>         dest split hd tl as (inf, sup) in           quicksort inf ++ [hd] ++ quicksort sup       | [] => []     end.    Solve Obligations using subtac_simpl ;      intros ; destruct_call split ; destruct x ; simpl in * ;     apply sym_eq in Heq_anonymous ; myinjection ; destruct y as [Hs Hperm] ;       pose (Hs hd) ; destruct_conjs ; auto ;    rewrite (permut_length eq_refl eq_sym eq_trans Hperm) ; rewrite app_length ; auto with arith. End QuickSort. Require Import OrderedTypeEx. Module QS := QuickSort(N_as_OT). Recursive Extraction QS. ```