set - Coq 中集合的一致公式？

Question

我是 Coq 的新手，并试图根据我的研究开发一个框架。我的工作非常重定义，并且由于 Coq 似乎如何对待集合，我在编码它时遇到了麻烦。

有Type和 Set ，他们称之为“排序”，我可以用它们来定义一个新的集合:

Variable X: Type.

然后有一个库编码(子)集为' Ensembles '，这是一些 Type 的函数到 Prop .换句话说，它们是 Type 上的谓词:

Variable Y: Ensemble X.

Ensemble s 感觉更像是适当的数学集。另外，它们是由许多其他库构建的。我试过专注于它们:定义一个通用集 U: Set ，然后将自己限制在(子)Ensemble上 U .但不是。 Ensemble s 不能用作其他变量的类型，也不能定义新的子集:

Variable y: Y.           (* Error *)
Variable Z: Ensemble Y.  (* Error *)

现在，我知道有几种方法可以解决这个问题。问题“Subset parameter”提供了两个。两者都使用强制。第一坚持Set s。第二个本质上使用 Ensemble s(虽然不是名字)。但是两者都需要相当多的机器来完成如此简单的事情。

问题:一致(和优雅)处理集合的推荐方法是什么？

示例:这是我想要做的一个例子:假设一个集合 DD。定义一对 dm = (D, <)，其中 D 是 DD 的有限子集，< 是 D 上的严格偏序。

我敢肯定，只要对强制或其他结构进行足够的修补，我就能完成它；但不是以特别易读的方式；并且对如何进一步操纵结构没有很好的直觉。例如，以下类型检查:

Record OrderedSet {DD: Set} : Type := {
  D     : (Ensemble DD);
  order : (relation {d | In _ D d});

  is_finite         : (Finite _ D);
  is_strict_partial : (is_strict_partial_order order)
}.

但我不太确定这是我想要的。而且它看起来肯定不是很漂亮。请注意，我在 Set 之间来回切换和 Ensemble以一种看似随意的方式。

有很多图书馆使用 Ensemble s，所以必须有一种很好的方式来对待它们，但是这些库似乎没有很好地记录(或者......根本没有)。

更新:更复杂的是，似乎还有许多其他的 set 实现，比如 MSets .这个好像是完全独立的，不兼容Ensemble .它还使用 bool而不是 Prop因为某些原因。还有FSets ，但它似乎是 MSet 的过时版本。

Answer 1

我使用 Coq 已经(从字面上)多年，但让我尝试提供帮助。

我认为从数学上讲U: Set就像在说 U是一个元素的宇宙和Ensemble U那么将意味着来自该宇宙的一组元素。因此，对于通用概念和定义，您几乎肯定会使用 Set和 Ensemble是推理元素子集的一种可能方式。

我建议你看看介绍 type classes to Coq 的 Matthieu Sozeau 的伟大作品。 ，一个基于 Haskell 类型类的非常有用的特性。特别是在标准库中，您会发现 PartialOrder 的基于类的定义。你在问题中提到的。

另一个引用是 CoLoR library形式化证明术语重写终止所需的概念。它有相当大的一组 generic purpose definitions在订单和什么不是。