From 3e51bdd77b75333a98b2b838f0dfcf7de1166387 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Sep 2020 14:56:46 +0200
Subject: [PATCH] Prove that `BiPureForall` holds if we assume classical logic
 in Coq.

---
 theories/bi/derived_laws.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 4cb4773e7..e9191e134 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -547,6 +547,13 @@ Proof.
   - apply exist_elim=> x. eauto using pure_mono.
 Qed.
 
+Lemma bi_pure_forall_em : (∀ φ : Prop, φ ∨ ¬φ) → BiPureForall PROP.
+Proof.
+  intros Hem A φ. destruct (Hem (∃ a, ¬φ a)) as [[a Hφ]|Hφ].
+  { rewrite (forall_elim a). by apply pure_elim'. }
+  apply pure_intro=> a. destruct (Hem (φ a)); naive_solver.
+Qed.
+
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
 Proof.
   apply (anti_symm _).
-- 
GitLab