The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

Hi Matthew,

Thanks a lot for the references. None of them was precisely what I
wanted, but I could use them as a starting point for writing my own
implementation [1]. It's indeed easy, since I don't really care about
stability.

About the total preorder vs. total partial order issue: I didn't need
antisymmetry in my proofs.

Thanks,
Catalin


[1] http://www.infsec.cs.uni-saarland.de/dyn/hritcu/temp/InsertionSorting.v

On Wed, Mar 31, 2010 at 12:15 AM, Matthew Brecknell
<matthew AT brecknell.net>
 wrote:
> Hi Catalin,
>
> Catalin Hritcu wrote:
>> I have a very basic question: is there any implementation of insertion
>> sorting on lists in the Coq standard library?
>
> I don't know about the standard library, but the first chapter of the
> Coq'Art book [1] shows a simple verification of a functional insertion
> sort implementation for lists of integers. The Coq script is available
> from the website. IIRC, the example's formalisation of sortedness
> requires a decidable total order, which means there is no need to be
> concerned with the stability of the sorting algorithm.
>
> [1]http://www.labri.u-bordeaux.fr/perso/casteran/CoqArt/index.html
>
> If you are interested in generalising to lists of arbitrary type with a
> decidable total *pre*order, including verification of stability, you
> might like to take a look at Xavier Leroy's development [2]. This is for
> a merge-sort algorithm, which involves some non-trivial recursion
> schemes, so the development is considerably more involved.
>
> [2]http://moscova.inria.fr/~xleroy/coq/Mergesort.html
>
> Regards,
> Matthew
>