首页
学习
活动
专区
圈层
工具
发布
首页
学习
活动
专区
圈层
工具
MCP广场
社区首页 >问答首页 >如何枚举Coq Ensemble中的集合

如何枚举Coq Ensemble中的集合
EN

Stack Overflow用户
提问于 2021-08-15 06:16:42
回答 1查看 71关注 0票数 0

你如何证明enumerateSingletonPowerset

代码语言:javascript
运行
复制
Require Import Coq.Sets.Ensembles.

Definition emptyOnly A := Singleton _ (Empty_set A).

Theorem enumerateSingletonPowerset A s (inc : Included _ s (emptyOnly A)):
  Same_set _ s (Empty_set _) \/ Same_set _ s (emptyOnly A).

我使用Same_set来避免可扩展性。(任何一种方式都可以。)

从概念上讲,似乎很简单地说我有{{}},所以powerset是{{}, {{}}},仅此而已。但是,还不清楚如何使用这些原语本身来表达类似的内容。

如果空集在集合s中,我很想尝试析构。但是,由于Emsemble是命题的,检查集合成员关系通常是不可确定的。第一个想法是

代码语言:javascript
运行
复制
Axiom In_dec : forall A a e, In A e a \/ ~In A e a.

Theorem ExcludedMiddle P : P \/ ~P.
  apply (In_dec _ tt (fun _ => P)).
Qed.

但是,这太强大了,立即将我带入了经典逻辑。有限的情况很简单,但我计划处理更大的集合(例如Reals),因此In和Included通常是不可计算的。有没有我可以添加的公理,可以允许并包括假装是可决定的,而不是让其他一切也是可决定的?

编辑:从成对改为单例,因为数量并不重要。

EN

回答 1

Stack Overflow用户

回答已采纳

发布于 2021-08-16 00:02:59

我找到了一种不用任何额外的公理就能让它工作的方法,使用的是来自“用于构建世界的经典数学”https://arxiv.org/pdf/1008.1213.pdf中的"not not“技术。

(我根本没有尝试清理校样,只是为了让它进行类型检查。抱歉,在校样中使用了奇怪的措辞。)

代码语言:javascript
运行
复制
Require Import Coq.Sets.Ensembles.

(* Classical reasoning without extra axioms. *)
Definition stable P := ~~P -> P.

Theorem stable_False : stable False.
  unfold stable; intros nnF.
  apply nnF; intros f.
  apply f.
Qed.

Definition orW P Q := ~(~P /\ ~Q).

Definition exW {A} (P : A -> Prop) := ~(forall a, ~P a).

Theorem exW_strengthen {A} P Q (stQ : stable Q) (exQ : (exists a, P a) -> Q) (exWP : exW (fun (a : A) => P a)) : Q.
  apply stQ; hnf; intros.
  apply exWP; intros; hnf; intros.
  apply H; apply exQ; apply (ex_intro _ _ H0).
Qed.


(* Ensembles *)
Definition emptyOnly A := Singleton _ (Empty_set A).

Theorem notEmpty_In A (s : Ensemble A) (ne : ~ Same_set _ s (Empty_set _)) : exW (fun a => In _ s a).
  hnf; intros; apply ne; clear ne.
  apply conj; hnf; intros; [ | destruct H0 ].
  apply (False_ind _ (H _ H0)).
Qed.

Theorem enumerateSingletonPowerset A s (inc : Included _ s (emptyOnly A)):
  orW (Same_set _ s (Empty_set _)) (Same_set _ s (emptyOnly A)).
  hnf; intros; destruct H.
  apply notEmpty_In in H.
  revert H; apply exW_strengthen; intros; [ apply stable_False | ]; destruct H.
  apply H0; clear H0; apply conj; hnf; intros; [ apply (inc _ H0) | ].
  destruct H0.
  destruct (inc _ H).
  apply H.
Qed.

因此,通过将定理重新表述为使用弱或,现在可以直接证明它,而不需要求助于A的结构,即隶属关系是可确定的,或经典逻辑。

票数 0
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/68789154

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档