10

我是 Coq 的新手，正在尝试根据我的研究开发一个框架。我的工作非常重定义，并且由于 Coq 似乎如何处理集合，我无法对其进行编码。

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

Variable X: Type.

然后有一个库编码（子）集为“ Ensembles ”，它们是从 someType到 a的函数Prop。换句话说，它们是 a 的谓词Type：

Variable Y: Ensemble X.

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

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

现在，我知道有几种方法可以解决这个问题。问题“子集参数”提供了两个。两者都使用强制。第一个坚持Sets。第二个基本上使用Ensembles （尽管不是按名称）。但两者都需要相当多的机器来完成如此简单的事情。

问题：一致（和优雅）处理集合的推荐方法是什么？

示例：这是我想要做的一个示例：假设一个集合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以一种看似任意的方式来回走动。

那里有很多使用Ensembles 的库，因此必须有一种很好的方法来处理它们，但是这些库似乎没有很好地记录（或者……根本没有）。

更新：更复杂的是，似乎还有一些其他的集合实现，比如MSets。这一个似乎是完全分开的，不兼容的Ensemble。它也使用bool而不是Prop出于某种原因。还有FSets，但它似乎是 MSets 的过时版本。

4

1 回答 1

4

我使用 Coq 已经（字面意思）多年了，但让我尝试提供帮助。

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

我建议您看看 Matthieu Sozeau 的出色工作，他将类型类引入 Coq，这是一个基于 Haskell 类型类的非常有用的特性。特别是在标准库中，您会发现您在问题中提到的PartialOrder的基于类的定义。

另一个参考是CoLoR 库形式化证明终止术语重写所需的概念。它有一组相当大的关于订单和其他东西的通用目的定义。

于 2013-06-02T01:31:36.440 回答