coq - Coqでサブセット関係を表現するには?

Question

Yあるセットが別のセットのサブセットであることをCoqでどのように記述できXますか?

私は以下をテストしました：

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

y、要素が にYある場合、 にあることを表現しようとしていyますX。yしかし、これは驚くべきことではありませんが、について型エラーを生成します。

subsetCoqで定義する簡単な方法はありますか?

Answer 1

標準ライブラリ ( Coq.Logic.ClassicalChoice) での実行方法は次のとおりです。

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

単項述語PおよびQは、(ユニバーサル) set の一部のサブセットを表す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ます。