The Coq mailing list

["Matthew Brecknell" <matthew AT brecknell.net>]

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