Coq list sorting practices & sortBy?

Question

What is the equivalent of Haskell's sortBy in Coq?

In general, I find the Coq standard library around sorting confusing.

I would have hoped for some "axiomatisation" of a sorted list, and the the availability of different sorts, to which I can provide an ordering function.

However, this does not seem to be the case.

• There is a theory of a "Sorted list", which uses a relation Variable R : A -> A -> Prop. , but there are no restrictions on this R. I would have expected it to be an ordering, but no such thing exists.

• There is another file with a "mergesort implementation", which needs a new module to be passed.

• There is no "higher level" version which provides helpers such as sortBy.

Is there some implementation of sortBy I can use, or do I need to create this manually?

Answer 1

Besides the Coq standard library, the Mathetical Components library also has an implementation of merge sort. It is called sort, and it lives in the module mathcomp.path. Its signature is forall T : Type, (T -> T -> bool) -> list T -> list T, which is closer to the original sortBy.

Answer 2

The MergeSort module in the Coq standard library does what you need. It works like sortBy in Haskell except that instead of passing an ordering function and obtaining the specialized sort, you pass a module that encapsulates the ordering function along with the proof that this function is total. See the example at the bottom of the module documentation.