From 919c0bdefc7519a9bc60923e6a3c86272071a19d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Nov 2017 17:38:50 +0100
Subject: [PATCH] Prove `except_0_forall` in both directions.

Thanks to Amin Timany for an initial version of the proof.
---
 theories/base_logic/derived.v | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c0324fc45..98b903d89 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -827,8 +827,18 @@ Proof.
     by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup.
   - rewrite sep_or_r sep_elim_l sep_or_l; auto.
 Qed.
-Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
-Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
+Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊣⊢ ∀ a, ◇ Φ a.
+Proof.
+  apply (anti_symm _).
+  { apply forall_intro=> a. by rewrite (forall_elim a). }
+  trans (▷ (∀ a : A, Φ a) ∧ (∀ a : A, ◇ Φ a))%I.
+  { apply and_intro, reflexivity. rewrite later_forall. apply forall_mono=> a.
+    apply or_elim; auto using later_intro. }
+  rewrite later_false_excluded_middle and_or_r. apply or_elim.
+  { rewrite and_elim_l. apply or_intro_l. }
+  apply or_intro_r', forall_intro=> a. rewrite !(forall_elim a).
+  by rewrite /uPred_except_0 and_or_l impl_elim_l and_elim_r idemp.
+Qed.
 Lemma except_0_exist_2 {A} (Φ : A → uPred M) : (∃ a, ◇ Φ a) ⊢ ◇ ∃ a, Φ a.
 Proof. apply exist_elim=> a. by rewrite (exist_intro a). Qed.
 Lemma except_0_exist `{Inhabited A} (Φ : A → uPred M) :
-- 
GitLab