如何在 Coq 中表达子集关系？

Question

我如何在 Coq 中描述一个集合Y是另一个集合的子集X？

我测试了以下内容：

Definition subset (Y X:Set) : Prop :=
  forall y:Y, y:X.

，试图表达如果一个元素y在 中Y，则y在 中X。但这会产生关于 的类型错误y，这并不奇怪。

subset在 Coq 中有一种简单的定义方法吗？

Answer 1

这是在标准库 ( Coq.Logic.ClassicalChoice) 中的实现方式：

Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.

一元谓词P和Q表示（普及）组的部分子集U，因此，上述定义如下：每当一些x是P，它是在Q以相同的时间。

可以在以下位置找到有点相似的定义Coq.MSets.MSetInterface：

Definition Subset s s' := forall a : elt, In a s -> In a s'.

where Inhas type elt -> t -> Prop，这意味着某个 type 元素是 typeelt集合的成员t。