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

Question

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

具体来说，我正在寻找一个构造函数，它采用 Ensemble U 和 Ensemble V 以及 returns 和包含所有有序对集合的 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 的标准笛卡尔积结构是什么？

What is the standard Cartesian-product construction for Ensemble?

set-theory

cartesian-product

coq