你如何证明enumerateSingletonPowerset
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是命题的,检查集合成员关系通常是不可确定的。第一个想法是
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通常是不可计算的。有没有我可以添加的公理,可以允许并包括假装是可决定的,而不是让其他一切也是可决定的?
编辑:从成对改为单例,因为数量并不重要。
发布于 2021-08-16 00:02:59
我找到了一种不用任何额外的公理就能让它工作的方法,使用的是来自“用于构建世界的经典数学”https://arxiv.org/pdf/1008.1213.pdf中的"not not“技术。
(我根本没有尝试清理校样,只是为了让它进行类型检查。抱歉,在校样中使用了奇怪的措辞。)
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的结构,即隶属关系是可确定的,或经典逻辑。
https://stackoverflow.com/questions/68789154
复制相似问题