coq - 如何在 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，这意味着某个类型的元素elt是一组类型的成员t。