I am using the Ensemble type for sets in Coq.Sets.Ensemble. This library defines Union and Intersection but I cannot find any construction for a Cartesian product.
To be specific, I am looking for a constructor that takes an Ensemble U and an Ensemble V and returns an Ensemble (U * V) that contains the set of all ordered pairs (u, v) where u ∈ U and v ∈ V.
Something explicitly called Cartesian would be great. Or maybe there is some way to embed the same idea using normal product types?
I tried to construct a lemma like this:
Lemma cartesian_inclusion : forall A B C D : Ensemble U,
Included U A C /\ Included U B D -> Included (U * U) (A, B) (C, D).
But I get the following error:
The term "(A, B)" has type "(Ensemble U * Ensemble U)%type" while it is expected to have type "Ensemble (U * U)".
This error sort of makes sense. (A, B) gives you a product of sets, whereas what I want is a set of products. How can I express this in Coq?
The type Ensemble U is simply defined as U -> Prop. We can easily define a cartesian product for ensembles as follows:
Require Import Coq.Sets.Ensembles.
Definition Cartesian (U V : Type) (A : Ensemble U) (B : Ensemble V)
: Ensemble (U * V) :=
fun x => In _ A (fst x) /\ In _ B (snd x).
Here is a proof of the lemma you stated:
Lemma cartesian_inclusion U V A B C D :
Included U A C /\ Included V B D ->
Included (U * V) (Cartesian _ _ A B) (Cartesian _ _ C D).
Proof.
intros [HU HV] [x y] [HA HB].
split.
- now apply HU.
- now apply HV.
Qed.
As an aside, the ensemble library is rarely used in modern Coq developments -- it does not buy you anything over just working with predicates.