Coq 列表排序实践 & sortBy?答案

【问题标题】：Coq list sorting practices & sortBy?Coq 列表排序实践 & sortBy?
【发布时间】：2018-07-09 12:28:06
【问题描述】：

Haskell 在 Coq 中的sortBy 是什么？

总的来说，我发现 Coq 标准库围绕排序令人困惑。

我希望对排序列表进行一些“公理化”，以及不同排序的可用性，我可以为其提供排序功能。

然而，情况似乎并非如此。

There is a theory of a "Sorted list"，它使用关系 Variable R : A -> A -> Prop.，但对此 R 没有限制。我本来希望它是一个排序，但不存在这样的东西。
还有一个“mergesort implementation”的文件，需要传递一个新的模块。
没有提供诸如sortBy 之类的帮助器的“更高级别”版本。

我可以使用sortBy 的一些实现，还是我需要手动创建它？

【问题讨论】：

标签： sorting coq

【解决方案1】：

Coq 标准库中的MergeSort module 可以满足您的需求。它的工作方式与 Haskell 中的 sortBy 类似，只是不是传递排序函数并获得专门的排序，而是传递一个封装排序函数的模块以及该函数是完全的证明。请参阅模块文档底部的示例。

【讨论】：

【解决方案2】：

除了 Coq 标准库之外，Mathetical Components library 还实现了归并排序。它被称为sort，它位于模块mathcomp.path 中。它的签名是forall T : Type, (T -> T -> bool) -> list T -> list T，更接近于原来的sortBy。

【讨论】：