The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Sun, 8 Apr 2012 15:31:30 +0000, "BAILEY C. (527272)" 
<C.BAILEY.527272 AT swansea.ac.uk>
 wrote:
> 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.

I haven't looked at your code, but are you familiar with
<http://weegen.home.xs4all.nl/eelis/research/quicksort/>?
Also, you are probably more likely to get a useful response if you
indicate which particular part you are having trouble with. In
particular, I don't see any proof here at all.

  Tom