如何在没有将set定义为元素列表的情况下定义coq中的set

Question

我试图将(1,2,3)定义为coq中的一组元素.我可以使用list定义它(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的合奏.这种表示不能"计算",因为我们甚至无法确定两个元素是否相等.

• 如果基本数据类型具有可判定的相等性,那么根据是否需要扩展性,有两种选择:

  • 如果它们具有相同的元素,则可扩展性意味着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,它将有限集编码为有限支持的隶属函数的空间,它是伸展的,并形成一个完整的格.

Answer 2

coq的标准库提供以下有限集模块:

1. Coq.MSets抽象出集合的实现细节.例如,有一个使用AVL树的实现和另一个基于lists的实现.
2. Coq.FSets抽象出集合的实现细节; 它是以前的版本MSets.
3. Coq.Lists.ListSet 是列表的集合编码,为了完整起见,我将其包括在内

以下是如何使用以下内容定义集合的示例FSets:

Require Import Coq.Structures.OrderedTypeEx.
Require Import Coq.FSets.FSetAVL.

Module NSet := FSetAVL.Make Nat_as_OT.
(* Creates a set with only element 3 inside: *)
Check (NSet.add 3 NSet.empty).

Answer 3

Coq 中有许多集合的编码（列表、函数、树……），它们可以是有限的，也可以是无限的。您应该看看 Coq 的标准库。例如，我知道的“最简单”集合定义是这个