Ensemble 的标准笛卡尔积构造是什么？

Question

我在Coq.Sets.Ensemble 中使用Ensemble 类型的集合。这个库定义了Union 和Intersection，但我找不到笛卡尔积的任何构造。

具体来说，我正在寻找一个构造函数，它接受一个Ensemble U 和一个Ensemble V 并返回一个Ensemble (U * V)，其中包含所有有序对的集合(u, v)，其中u ∈ U 和v ∈ V。

明确称为Cartesian 的东西会很棒。或者也许有一些方法可以使用普通产品类型嵌入相同的想法？

我试图构建一个这样的引理：

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).

但我收到以下错误：

The term "(A, B)" has type "(Ensemble U * Ensemble U)%type" while it is expected to have type "Ensemble (U * U)".

这种错误是有道理的。 (A, B) 给你一套产品，而我想要的是一套产品。我如何在 Coq 中表达这一点？

Answer 1

Ensemble U 类型被简单地定义为U -> Prop。我们可以很容易地为集成定义笛卡尔积，如下所示：

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).

这是你所说的引理的证明：

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.

顺便说一句，在现代 Coq 开发中很少使用 ensemble 库 —— 它不会给你带来任何东西，而不仅仅是使用谓词。