如何在Coq中表達子集關係？

Question

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

我測試了以下：

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

，試圖表達，如果一個元件y是Y，然後y是X。但這會產生關於y的類型錯誤，這並不奇怪。

有沒有簡單的方法來定義coq中的subset？

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'. 

其中In具有類型elt -> t -> Prop，這意味着elt類型的一些元件是一組t類型中的一員。