Coq列表排序实践& sortBy？
提问于 2018-07-09 04:28:06
在Coq中，Haskell的sortBy相当于什么？
一般来说，我发现Coq标准库中围绕排序混淆。
我本来希望排序列表的一些“公理化”，以及不同类型的可用性，我可以提供一个排序函数。
然而，情况似乎并非如此。
- 有一个“排序列表”的理论。，它使用关系
Variable R : A -> A -> Prop.，但对此R没有任何限制。我原以为这是一种命令，但不存在这样的事情。 - 还有一个带有"合并实施“的文件，它需要一个新的模块来传递。
- 没有提供像
sortBy这样的帮助的“高级”版本。
我是否可以使用sortBy的某些实现，或者是否需要手动创建它？
回答 2
Stack Overflow用户
回答已采纳
发布于 2018-07-09 04:47:30
Coq标准库中的MergeSort模块可以满足您的需要。它的工作方式类似于Haskell中的sortBy，除了传递一个排序函数和获得专门的排序之外，您还传递了一个封装排序函数的模块，以及该函数是完全函数的证明。参见模块文档底部的示例。
Stack Overflow用户
发布于 2018-07-09 06:00:17
除了Coq标准库之外，图形组件库还实现了合并排序。它被称为sort，它驻留在模块mathcomp.path中。它的签名是forall T : Type, (T -> T -> bool) -> list T -> list T，它更接近于原始的sortBy。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/51245616
复制
腾讯云开发者
