How to enumerate set in Coq Ensemble

Question

How do you prove 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).
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
Same_set (Ensemble A) s (Empty_set (Ensemble A)) \/
Same_set (Ensemble A) s (emptyOnly A)

I'm using Same_set to avoid extensionality. (Either way is fine.)

Conceptually, it seems simple to just say I have {{}} so the powerset is {{}, {{}}} and that's it. But, it's not clear how to say anything like that with these primitives on their own.

I'd be tempted to try destructing on if empty set was in the set s. But, since Ensemble is propositional, checking set membership is not generally decidable. A first thought is

Axiom In_dec : forall A a e, In A e a \/ ~In A e a.

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

But, that is too powerful and immediately puts me into classical logic. The finite case is easy, but I plan on dealing with larger sets (e.g. Reals), so In and Included would not generally be computable. Are there axioms I could add that could allow In and Included to pretend to be decidable without making everything else decidable too?

Edit: Changed from pair to singleton since quantity isn't important.

Answer

I found a way to get it to work without any additional axioms using the "not not" technique from "Classical Mathematics for a Constructive World" https://arxiv.org/pdf/1008.1213.pdf

(I haven't tried to clean up the proofs at all, just to get it to type check. Sorry for weird phrasing in proofs.)

Require Import Coq.Sets.Ensembles.

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

Theorem stable_False : stable False.
stable False
  unfold stable; intros nnF.
nnF: ~ ~ False
False
  apply nnF; intros f.
nnF: ~ ~ False
f: False
False
  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.
A: Type
P: A -> Prop
Q: Prop
stQ: stable Q
exQ: (exists a : A, P a) -> Q
exWP: exW (fun a : A => P a)
Q
  apply stQ; hnf; intros.
A: Type
P: A -> Prop
Q: Prop
stQ: stable Q
exQ: (exists a : A, P a) -> Q
exWP: exW (fun a : A => P a)
H: ~ Q
False
  apply exWP; intros; hnf; intros.
A: Type
P: A -> Prop
Q: Prop
stQ: stable Q
exQ: (exists a : A, P a) -> Q
exWP: exW (fun a : A => P a)
H: ~ Q
a: A
H0: P a
False
  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).
A: Type
s: Ensemble A
ne: ~ Same_set A s (Empty_set A)
exW (fun a : A => In A s a)
  hnf; intros; apply ne; clear ne.
A: Type
s: Ensemble A
H: forall a : A, ~ In A s a
Same_set A s (Empty_set A)
  apply conj; hnf; intros; [ | destruct H0 ].
A: Type
s: Ensemble A
H: forall a : A, ~ In A s a
x: A
H0: In A s x
In A (Empty_set A) x
  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)).
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
orW (Same_set (Ensemble A) s (Empty_set (Ensemble A)))
  (Same_set (Ensemble A) s (emptyOnly A))
  hnf; intros; destruct H.
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
H: ~ Same_set (Ensemble A) s (Empty_set (Ensemble A))
H0: ~ Same_set (Ensemble A) s (emptyOnly A)
False
  apply notEmpty_In in H.
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
H: exW (fun a : Ensemble A => In (Ensemble A) s a)
H0: ~ Same_set (Ensemble A) s (emptyOnly A)
False
  revert H; apply exW_strengthen; intros; [ apply stable_False | ]; destruct H.
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
H0: ~ Same_set (Ensemble A) s (emptyOnly A)
x: Ensemble A
H: In (Ensemble A) s x
False
  apply H0; clear H0; apply conj; hnf; intros; [ apply (inc _ H0) | ].
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
x: Ensemble A
H: In (Ensemble A) s x
x0: Ensemble A
H0: In (Ensemble A) (emptyOnly A) x0
In (Ensemble A) s x0
  destruct H0.
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
x: Ensemble A
H: In (Ensemble A) s x
In (Ensemble A) s (Empty_set A)
  destruct (inc _ H).
A: Type
s: Ensemble (Ensemble A)
inc: Included (Ensemble A) s (emptyOnly A)
H: In (Ensemble A) s (Empty_set A)
In (Ensemble A) s (Empty_set A)
  apply H.
Qed.

So, by rephrasing the theorem to use weak or, it is now possible to prove it directly, and without appealing to the structure of A, that membership is decidable, or classical logic.