set - 如何在coq中定义集合而不将集合定义为元素列表

Question

我试图将 (1,2,3) 定义为 coq 中的一组元素。我可以使用列表将其定义为 (1::(2::(3::nil)))。有没有办法在不使用列表的情况下在 coq 中定义 set。

Answer 1

在 Coq 中定义集合时，基本上有四种可能的选择，具体取决于您对集合的基本类型和计算需求的约束:

如果基类型没有可判定的相等性，通常使用:

Definition Set A := A -> Prop
Definition cup A B := fun x => A x /\ B x.
...

基本上，Coq 的 Ensembles .这种表示无法“计算”，因为我们甚至无法确定两个元素是否相等。

如果基本数据类型具有可判定的相等性，则有两种选择取决于是否需要扩展性:

扩展性意味着两个集合在 Coq 的逻辑中是相等的，如果它们具有相同的元素，形式上:

forall (A B : set T), (A = B) <-> (forall x, x \in A <-> x \in B).

如果需要扩展性，集合应该由规范排序的无重复结构表示，通常是一个列表。一个很好的例子是 Cyril 的 Cohen finmap图书馆。然而，这种表示对于计算来说非常低效，因为每次修改集合时都需要重新排序。

如果不需要扩展性(如果需要证明通常是个坏主意)，您可以使用基于二叉树的表示，例如 Coq 的 MSet ，它们类似于标准的函数式编程集实现并且可以有效地工作。

最后，当基类型为有限时，所有集合的集合也是有限类型。这种方法的最好例子是 IMO math-comp 的 finset ，它将有限集编码为有限支持的隶属函数空间，它是可拓的，并形成一个完整的格。