sorting - Coq 列表排序实践 & sortBy？

Question

Haskell 的 sortBy 相当于什么？在 Coq 中？

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

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

然而，事实似乎并非如此。

• There is a theory of a "Sorted list" ，它使用关系 Variable R : A -> A -> Prop。
，但对此 R 没有限制。我本以为这是一个命令，但不存在这样的东西。

• 还有另一个带有“mergesort implementation ”的文件，需要传递一个新模块。

• 没有“更高级别”的版本提供 sortBy 等帮助程序。

是否有我可以使用的 sortBy 实现，或者我需要手动创建它？

Answer 1

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