Coq中集合的一致表述？ [英] Consistent formulations of sets in Coq?

问题描述

我在Coq刚起步，并试图根据我的研究开发一个框架。我的工作非常繁琐，由于Coq似乎对集合的处理方式，我难以编码。

I'm quite new at Coq and trying to develop a framework based on my research. My work is quite definition-heavy and I'm having trouble encoding it because of how Coq seems to treat sets.

有 Type 和 Set ，它们称为排序，我可以使用它们来定义新的集合：

There are Type and Set, which they call 'sorts', and I can use them to define a new set:

Variable X: Type.

然后有一个库编码（子）集为'合奏'，它们是从 Type 到 Prop 。换句话说，它们是 Type 的谓词：

And then there's a library encoding (sub)sets as 'Ensembles', which are functions from some Type to a Prop. In other words, they are predicates on a Type:

Variable Y: Ensemble X.

合奏感觉更像适当的数学集。另外，它们是由许多其他库构建的。我尝试着重于它们：定义一个通用集 U：Set ，然后将自己限制为（sub） Ensemble 在 U 上。但不是。 集成不能用作其他变量的类型，也不能定义新的子集：

Ensembles feel more like proper mathematical sets. Plus, they are built upon by many other libraries. I've tried focussing on them: defining one universal set U: Set, and then limiting myself to (sub)Ensembles on U. But no. Ensembles cannot be used as types for other variables, nor to define new subsets:

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

现在，我知道有几种解决方法。问题 子集参数提供了两个。两者都使用强制。第一个坚持使用 Set s。第二个实质上使用了 Ensemble s（尽管不是名字）。但是，两者都需要相当多的机制才能完成如此简单的事情。

Now, I know there are several ways to get around that. The question "Subset parameter" offers two. Both use coercions. The first sticks to Sets. The second essentially uses Ensembles (though not by name). But both require quite some machinery to accomplish something so simple.

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

Question: What is the recommended way of consistently (and elegantly) handling sets?

示例：以下是我要执行的操作示例：假设设置了 DD 。定义一对 dm =（D，<），其中 D 是 DD 和< 的有限子集是 D 上的严格偏序。

Example: Here's an example of what I want to do: Assume a set DD. Define a pair dm = (D, <) where D is a finite subset of DD and < is a strict partial order on D.

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

I'm sure that with enough tinkering with coercions or other structures, I could accomplish it; but not in a particularly readable way; and without a good intuition of how to manipulate the structure further. For example, the following type-checks:

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 之间以一种看似随意的方式来回移动。

But I'm not so sure it's what I want; and it certainly doesn't look very pretty. Note that I'm going backwards and forwards between Set and Ensemble in a seemingly arbitrary way.

有很多使用 Ensemble s的库，因此必须有一种很好的方法来对待它们，但是那些库却没有

There are plenty of libraries out there which use Ensembles, so there must be a nice way to treat them, but those libraries don't seem to be documented very well (or... at all).

更新：为了使事情进一步复杂化，似乎其他许多集合实现也是如此，例如 MSets 。这似乎是完全独立的，与 Ensemble 不兼容。由于某些原因，它也使用 bool 而不是 Prop 。还有 FSets ，但是它出现了

Update: To complicate matters further, there appear to be a number of other set implementations too, like MSets. This one seems to be completely separate and incompatible with Ensemble. It also uses bool rather than Prop for some reason. There is also FSets, but it appears to be an outdated version of MSets.

推荐答案

使用Coq已经（字面上）多年了，但是让我尝试帮助。

It's been (literally) years since I used Coq, but let me try to help.

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

I think mathematically speaking U: Set is like saying U is an universe of elements and Ensemble U would then mean a set of elements from that universe. So for generic notions and definitions you will almost certainly use Set and Ensemble is one possible way about reasoning about subsets of elements.

我建议您看一下Matthieu Sozeau的出色作品，他介绍了 Coq类型类，这是基于Haskell类型类型的非常有用的功能。特别是在标准库中，您会找到您在问题中提到的= noreferrer> PartialOrder 。

I'd suggest that you take a look at great work by Matthieu Sozeau who introduced type classes to Coq, a very useful feature based on Haskell's type classes. In particular in the standard library you will find a class-based definition of a PartialOrder that you mention in your question.

另一个参考是 CoLoR库形式化了证明终止术语重写所需的概念。它在订单上有相当多的通用目的定义。

Another reference would be the CoLoR library formalizing notions needed to prove termination of term rewriting. It has a fairly large set of generic purpose definitions on orders and what-not.

这篇关于Coq中集合的一致表述？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！