Yes.
No. It is the one from multiplication, or rather, it is the one found in expressions such as “Cartesian product” (i.e., tuple). Anyway, that does not change the meaning, you can only destruct
something with an inductive type.
An object S
of type U -> Prop
should be seen as a predicate over U
, or equivalently, as the characteristic function of a subset of U
. Then, an element x
is part of S
, if the property S x
holds. Suppose T
is another object of type U -> Prop
. The element x
is part of both S
and T
if it satisfies S x /\ T x
. In other words, you can define the predicate characterizing the intersection of S
and T
as fun x => S x /\ T x
(which still has type U -> Prop
). More generally, you can define an intersection operator as fun S T x => S x /\ T x
, and if you want to make it implicitly generic with respect to U
, you get fun {U} (S T: U -> Prop) x => S x /\ T x
. The exact same thing can be done to define the union, except that you would replace the conjunction by a disjunction.
The Ensembles
library provides all these definitions, but I would recommend against using it, especially if you are a beginner with Coq. (And if you are not a beginner, you do not need it anyway.) I think it would be much more instructive for you to directly manipulate predicates by hand:
Definition union {U} (S T : U -> Prop) (x : U) := S x \/ T x.
Definition inter {U} (S T : U -> Prop) (x : U) := S x /\ T x.
Definition empty {U} (x : U) := False.
Definition subset {U} (S T : U -> Prop) := forall x, S x -> T x.
Goal forall U (S T : U -> Prop), subset (union S T) (union T S).
Proof. intros U S T x. unfold union. tauto. Qed.