The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

   You may also want to take a look at the quick sort implementation (along with the proof of its average case n log n complexity) by Eelis van der Weegen and James McKinna: http://www.xs4all.nl/~weegen/eelis/research/quicksort.

  Cheers,
   Adam

On Sat, Apr 11, 2009 at 15:37, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

>> The problem is that I have a list of integers (given unsorted unfortunately
>> in my proof) and I want to sort them in ascending order, which means I want
>> to construct the object (Sorted: sort le l), where l is a list of nat. Is
>> that possible or am I complicating things?
>
> Sure it's possible. Pick a sort algorithm. Given the structure of
> List, you probably want merge sort. Oh, will you look at that! It's
> been done!
>
> http://coq.inria.fr/V8.2/doc/html/stdlib/Coq.Sorting.Sorting.html

This library provides a merge function over two sorted lists, but
there is still some work to do to implement mergesort.  See:

http://gallium.inria.fr/~xleroy/coq/Mergesort.html
http://gallium.inria.fr/~xleroy/coq/Mergesort.v

It's a nice exercise in using "Program".

Alternatively, the Coq standard library does provide a list sorting
function based on heap sort (module Coq.Sorting.Heap), but I dislike
it for reasons explained in bug report #2047.

Enjoy,

- Xavier Leroy

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================