代码之家 › 专栏 › 技术社区 › Siddharth Bhat

COQ列表排序实践和排序?

coq sorting

Siddharth Bhat · 技术社区 · 7 年前

哈斯克尔的 sortBy 在Coq?

总的来说,我发现coq标准库在排序方面有点混乱。

我希望有一个排序列表的“公理化”,以及不同类型的可用性,我可以提供排序函数。

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

There is a theory of a "Sorted list" ,它使用关系 Variable R : A -> A -> Prop. ,但没有限制关于这个 R 是的。我本以为这是一个命令,但没有这样的事情存在。
有另一个文件带有“ mergesort implementation “,这需要传递一个新模块。
没有“更高级别”的版本提供诸如 sortBy 是的。

是否有一些 肮脏的 我可以使用,还是需要手动创建?

2 回复 | 直到 7 年前

Rob Blanco 7 年前

这个 MergeSort module 在coq标准库中做您需要的事情。它工作起来像 sortBy 在haskell中,除了传递一个ordering函数和获取特殊排序之外,还传递了一个封装ordering函数的模块,以及该函数是total的证明。请参阅模块文档底部的示例。

Arthur Azevedo De Amorim 7 年前

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

推荐文章

Mei Zhang · 定义“依赖类型”模函子

7 年前

Jason Hu · 参见Ltac中的Hintbase

7 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

7 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

7 年前

user9335697 · 实例化参数以评估函数定义

7 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

7 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

7 年前

jmite · Coq:在校样脚本编写期间查看校样术语

7 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

7 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

7 年前