Coq中一致的套装配方？

Question

我是Coq的新手,并试图根据我的研究开发一个框架.我的工作非常沉重,而且由于Coq似乎对待集合而我编码很困难.

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

Variable X: Type.

然后有一个库编码(子)设置为' Ensembles ',它们是从一些Type到另一个的函数Prop.换句话说,它们是对a的谓词Type:

Variable Y: Ensemble X.

Ensemble感觉更像是适当的数学集合.此外,它们是由许多其他图书馆建立的.我已经尝试过关注它们:定义一个通用集U: Set,然后将自己限制在(子)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版本.

Answer 1

我已经（字面上）使用 Coq 多年了，但让我尽力提供帮助。

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

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

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