如何枚举 Coq Ensemble 中的集合

Question

你如何证明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 来避免扩展性。（无论哪种方式都可以。）

从概念上讲，只说我有似乎很简单 {{}} 所以功率组是 {{}, {{}}} 就是这样。但是，不清楚如何用这些原语单独说出类似的话。

如果 set 中有空集，我很想尝试 destruct on。但是，由于 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.

但是，那太强大了，让我立刻陷入了经典逻辑。有限情况很简单，但我计划处理更大的集合（例如实数），因此 In 和 Included 通常不可计算。是否有我可以添加的公理可以允许 In 和 Included 假装是可判定的而不使其他所有内容也可判定？

编辑：从成对更改为单例，因为数量并不重要。

Answer 1

我找到了一种方法，无需任何额外的公理即可使用“构造性世界的经典数学”中的“非非”技术 https://arxiv.org/pdf/1008.1213.pdf

（我根本没有尝试清理校样，只是为了让它进行类型检查。抱歉校样中的奇怪措辞。）

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 的结构，即成员资格是可判定的或经典逻辑。

如何枚举 Coq Ensemble 中的集合

How to enumerate set in Coq Ensemble

coq