Ensemble的标准笛卡尔乘积结构是什么？
Ensemble的标准笛卡尔乘积结构是什么？
提问于 2019-05-19 01:03:29
我在Coq.Sets.Ensemble中对集合使用Ensemble类型。这个库定义了Union和Intersection，但我找不到任何笛卡尔乘积的结构。
具体地说，我正在寻找一个构造函数，它接受一个Ensemble U和一个Ensemble V，并返回一个包含所有有序对(u, v) u ∈ U和v ∈ V的集合的Ensemble (U * 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中表达这一点？
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-05-19 01:33:37
简单地将类型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开发中很少使用--它不会为您带来任何东西，而不仅仅是使用谓词。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/56201111
复制相关文章
相似问题
腾讯云开发者
