Quicksort proof using Coq

Question

I am writing a thesis on program verification of the quicksort algorithm using the Coq system. I have defined a quicksort in Coq but my supervisor and myself arn't very comfortable writing the actual proof using tactics. Is there anyone that can help with that section of the coq proof? The following is what we have come up with so far:

Inductive nat : Type :=
   | O : nat
   | S : nat -> nat.

Check (S (S (S (S O)))).

Definition isZero (n:nat) : bool :=
  match n with
   O => true
   |S p => false
  end.

Inductive List: Set :=
 | nil: List
 | cons: nat -> List -> List.

Fixpoint Concat (L R: List) : List :=
 match L with
 | nil => R
 | cons l ls => cons l (Concat ls R)
end.  

Fixpoint Less (n m:nat) :=
  match m with
   O => false
  |S q => match n with
          O => true
         |S p => Less p q
         end
  end.      

Fixpoint Lesseq (n m:nat) :=
  match n with
   O => true
  |S p => match m with
           O => false
          |S q => Lesseq p q
          end
  end.

Fixpoint Greatereq (n m:nat) :=
  match n with
   O => true
  |S p => match m with
           O => true
          |S q => Greatereq p q
          end
  end.


Fixpoint Allless (l:List) (n:nat) : List :=
  match l with
   nil => nil
  |cons m ls => match Less n m with
                 false => Allless ls n
                |true => cons m (Allless ls n)
                end
end.               

Fixpoint Allgeq (l:List) (n:nat) : List :=
  match l with
   nil => nil
  |cons m ls => match Greatereq n m with
                 false => Allgeq ls n
                |true => cons m (Allgeq ls n)
                end
end.  

Fixpoint qaux (n:nat) (l:List) : List := 
  match n with
  O => nil
 |S p => match l with
         nil => nil
        |cons m ls => let low := Allless ls m in
                     (let high := Allgeq ls m in 
                     Concat (qaux p low) (cons m (qaux p high)))
        end
 end.

Fixpoint length (l:List) : nat :=
 match l with
  nil => O
|cons m ls => S (length ls)
end.

Fixpoint Quicksort (l:List) : List := qaux (length l) l.

I know for a proof to work we need a lemma or a theorem but then I am not sure where to start after that. Thanks for the help :)

Answer 1

View your problem as a problem of "symbolic testing". Write a function that tests that your output is correct, and then show that all combinations of your initial code and your testing function work as intended.

Here is my favorite testing function for a sorting algorithm on your datatype.

Fixpoint sorted (l : List) : bool :=
  match l with cons a l' =>
    match l' with cons b l'' =>
      if Lesseq a b then sorted l' else false
    | nil => true
    end
  | nil => true
  end.

then you can start a proof in the following way:

Lemma Quicksort_sorted : forall l, sorted (Quicksort l) = true.

But you will have to prove many intermediate lemmas before getting to proving the main one. So formal proof is really like testing, except that you ensure full coverage of the test.

Answer 2

There are many nice theorems you can prove about your code.

• Define a function pos that maps a number and a list to the index of the number in the list.

• Th 1: For all lists S, and a, b in S, (a <= b) <-> (pos a (sort S)) <= (pos b (sort S)). This would be a correctness theorem for the sort function.

• Th 2: (sort (sort S)) = sort S

• Define the functions min and max to find the minimum and maximum elements of the list S.

• Th 3: The pos of the minimal element of the sorted list is 0.

• Th 4: The pos of the maximal element of the reverse of the sorted list is 0.

Abstract a predicate out of your sort routine, so that you can pass it as an argument.

• Th 5: Show that (sort <= S) = (reverse (sort >= S))

etc. You can continue this ad infinitum. It's lots of fun. :-)