Library quicksort
An implementation of QuickSort using Program.
We implement stable quicksort for any ordered type.
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.