Search code examples
coqset-theory

How to express subset relation in Coq?

How can I describe in Coq that one set Y is a subset of another set X?

I tested the following:

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

, trying to express that if an element y is in Y, then y is in X. But this generates type errors about y, not surprisingly.

Is there an easy way to define subset in Coq?

Solution

  • Here is how it is done in the standard library (Coq.Logic.ClassicalChoice):

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

    Unary predicates P and Q represent some subsets of the (universal) set U, so the above definition reads: whenever some x is in P, it is in Q at the same time.

    A somewhat similar defintion can be found in Coq.MSets.MSetInterface:

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

    where In has type elt -> t -> Prop, which means that some element of type elt is a member of a set of type t.