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?
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
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With