The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

>> 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