Quicksort in Coq

quicksort.v

Require Import List.
Require Import Bool.
Require Import Arith.

Definition filter_lte (a: nat) list := filter (fun n=> n <=? a) list.
Definition filter_gt (a: nat) list := filter (fun n=> negb(n <=? a)) list.

Fixpoint quicksort (l: list nat) :=
    match l with
      nil => nil
    | h :: t => let sorted_t := quicksort t in
                    filter_lte h sorted_t
                    ++ h :: filter_gt h sorted_t
    end.

Compute quicksort (nil).
Compute quicksort (1::2::3::6::1::2::1::0::nil).

Fixpoint length (l: list nat) : nat :=
    match l with
      nil => 0
    | a :: tl => 1 + (length (tl))
    end.

Theorem lengthIsCommutative: forall l m : list nat, length(l ++ m) = length(m ++ l).
Proof.
    induction l.
    intros.
    simpl.
    rewrite app_nil_r.
    reflexivity.
    intros.
    simpl.
    rewrite IHl.
    induction m.
    simpl.
    reflexivity.
    simpl.
    rewrite IHm.
    reflexivity.
Qed.

Theorem lengthIsDistributive: forall l j:(list nat), length (l ++ j) = length l + length j.
Proof.
    induction j.
    simpl.
    rewrite app_nil_r.
    firstorder.
    rewrite lengthIsCommutative.
    simpl.
    rewrite Nat.add_succ_r with (n:=length l) (m:=length j).
    rewrite lengthIsCommutative.
    rewrite IHj.
    firstorder.
Qed.

Theorem twoFilterLengthEq: forall n l, length(filter_lte n l) + length(filter_gt n l) = length(l).
Proof.
    intros.
    induction l.
    simpl.
    reflexivity.
    unfold filter_lte.
    assert ((fun n0 : nat => n0 <=? n) a = true \/ (fun n0 : nat => negb(n0 <=? n)) a = true).
    case (a <=? n).
    left; reflexivity.
    right; simpl; reflexivity.
    destruct H.
    simpl.
    rewrite H.
    simpl.
    assert (filter_lte n l = filter (fun n0 : nat => n0 <=? n) l).
    unfold filter_lte.
    firstorder.
    rewrite <- H0.
    rewrite IHl.
    firstorder.
    assert (filter_lte n (a::l) = filter (fun n0 : nat => n0 <=? n) (a::l)).
    unfold filter_lte.
    firstorder.
    rewrite <- H0.
    simpl.
    rewrite H.
    assert((a <=? n) = false).
    rewrite <- negb_involutive with (b:=(a <=? n)).
    rewrite H.
    firstorder.
    rewrite H1.
    simpl.
    rewrite Nat.add_succ_r with (n:=length(filter_lte n l)) (m:=(length (filter_gt n l))).
    rewrite IHl.
    firstorder.
Qed.

Theorem sortLengthUnchanged :
    forall l:(list nat),
    length l = length (quicksort l).
Proof.
    induction l.
    simpl.
    reflexivity.
    simpl.
    rewrite IHl.
    rewrite lengthIsDistributive.
    simpl.
    rewrite Nat.add_succ_r with
        (n:=length(filter_lte a (quicksort l)))
        (m:=(length (filter_gt a (quicksort l)))).
    rewrite twoFilterLengthEq.
    reflexivity.
Qed.

The definition of quickSort is wrong. The definition above recurses on quickSort with the entire tail. The filter is only applied once the result is pushed back up. This avoids the large challanges of defining quickSort.

Hi Wouter, thanks for the the comment. I'm not sure I quite follow—how should it be defined?

Also curious how you came across this gist. Hope all is well :)

Hello Adam the problem with your definition is quite simple however defining quicksort itself is not. Your definition of quicksort with the let statement hides the mistake a bit. I suspect that while defining quicksort you encountered some problems. You accidentally introduced an error which avoids the main difficulties of quicksort.

The mistake becomes clear if we remove the let statement. We then get:

Fixpoint quicksort (l: list nat) :=
    match l with
        | nil => nil
    	| h :: t => (filter_lte h (quicksort t)) ++ h :: (filter_gt h (quicksort t))
    end.

Here quickSort first recurses on t (all the way down to nil) and then stats filtering. While this results in a sorted array it is inefficient and not a good sorting algorithm. For quicksort we want to first filter out all elements which we don’t need and then pass the filtered array recursively. As shown below.

Fixpoint quicksort (l: list nat) :=
    match l with
    	| nil => nil
    	| h :: t => (quicksort (filter_lte h t)) ++ h :: (quicksort (filter_gt h t))
    end.

Note that the only change is that we apply the filter before we recurse.
This is a correct mathematical definition of quicksort however Coq can’t work with this. Coq can only work with finite fixpoints. No infinite structures are allowed, this is usually not a problem, in your implementation quicksorts recursive call is (quicksort t) which is one element shorter then l. Since lists are finite Coq sees that the parameter l decreases after every recursive call. If we have (a set of) strictly decreasing parameters in a recursive call then the recursion terminates. So Coq accepts your definition. In the “correct” definition shown above we recurse on (quicksort (filter_lte h t)) trivially (filter_lte h t) is strictly smaller then l, however Coq does not know this. Coq therefore does not accept our definition. We can solve this by adding a strictly decreasing parameter of type:

Inductive qs_tree : list nat -> Type :=
| qs_ leaf : qs_concat nil
| qs_ node : forall ( x: nat) (xs: list nat), 
  qs_tree (filter (fun y => leb y  x) (xs)) -> 
  qs_tree (filter (fun y => negb (leb y x)) (xs)) -> 
    qs_tree (cons x xs).

While this type looks very impressive it can be seen as the recursion tree of quicksort. You can look at the leaves of the tree (qs_leaf) as a call (quicksort nil). You can look as the nodes in the tree (qs_node) as a call (quicksort (x:xs)) now the left subtree contains qs_tree (filter (fun y => leb y x) (xs)) and the right sub tree contains filter (fun y => negb (leb y x)) (xs), these are indeed just the calls quicksort (x:xs) makes to recurse.

We could now define a quicksort function with one more parameter:

Definition qs (xl : list nat) (tree : qs_tree xl) : list nat.
...

Here tree is a finite structure which is strictly decreasing and finite so coq understands the recursion terminates. I am currently still working on one last challenge. You need to create an opaque lemma (which you can run using simpl and compute) to create the recursion tree for a given list xl. However if you do not mind the extra argument you can probably still prove the lemmas which you have proven without it. Here is a very simple definition of quicksort which you can run and use to prove your lemmas, however you will need to give it the recursion tree to run it.

Definition qs (xl : list nat) (conc : qs_tree xl) : list nat.
induction conc.
exact nil.
exact (IHconc1 ++ (cons x IHconc2)).
Defined.
Definition xs := 5 :: 3 :: 0 :: nil. (*some list to sort*)
Definition xsTree : (qs_tree xs). (*create the recursion tree for the list*)
unfold lexample.
try repeat constructor.
Defined.
(*And now you can run it:*)
Eval compute in (qs xs xsTree)

You could also prove lemmas like:

Lemma qs_contains : forall (xs : list nat) (x : nat) (tree : (qs_tree xs),  (In x xs) <-> (In x (qs xs tree)).
...

I will link my complete code once I am done with the last part.

Hope this helps,

Wouter

Ahh and i found this git you are one of the first result if you google Coq quicksort

Wouter, that's awesome, thanks for the write up!!!!

Also, what's your interest in Coq and quicksort? Are you a student?

Yes I am a student I specialise in formal system analysis and I am working on a project to prove correctness for functional programs

For anyone looking for a complete correctness proof of quicksort it can be found here:
https://github.com/WouterSchols/Coq_Quiksort