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 => ([],[])

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
      | [] => []

   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.