The Coq mailing list

["BAILEY C. (527272)" <C.BAILEY.527272 AT swansea.ac.uk>]

Hi, I am currently writing a thesis about program verification in the coq system with the main goal being focused on the quicksort algorithm.

First of all thank you for all of your work that you have done concerning Coq as it has helped me extensively. Secondly I was wondering if I may use your help to do the last part of my quicksort proof. I have done my implementation slightly differently to how most people have tackled the quicksort problem before myself. So far I have defined the quicksort, now as the next step I need to actually proof the algorithm using tactics which is where I find myself to be slightly stuck. I'm not really sure where to start to actually proof this and was wondering if you would be so kind as to help please.

The following is what I have done 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.

Hopefully you can help and thank you very much for your time.

Regards,

Callum Bailey.