From 2638b55d41ff95c42b9a8af0cc7ca5af350fd6cb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Apr 2020 18:52:06 +0200
Subject: [PATCH] Make `Excl_included` and `Excl_includedN` bi-implications.

---
 theories/algebra/excl.v       | 12 ++++++++----
 theories/program_logic/ownp.v |  4 ++--
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 027517d48..a61d5e214 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -118,10 +118,14 @@ Proof. by destruct mx. Qed.
 Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
 Proof. by destruct mx. Qed.
 
-Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b → a ≡{n}≡ b.
-Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
-Lemma Excl_included a b : Excl' a ≼ Excl' b → a ≡ b.
-Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
+Lemma Excl_includedN n a b  : Excl' a ≼{n} Excl' b ↔ a ≡{n}≡ b.
+Proof.
+  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
+Qed.
+Lemma Excl_included a b : Excl' a ≼ Excl' b ↔ a ≡ b.
+Proof.
+  split; [|by intros ->]. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb.
+Qed.
 End excl.
 
 Arguments exclO : clear implicits.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 72e75d5cd..7098222ab 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -90,8 +90,8 @@ Section lifting.
   Lemma ownP_eq σ1 σ2 κs n : state_interp σ1 κs n -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
   Proof.
     iIntros "Hσ● Hσ◯". rewrite /ownP.
-    iDestruct (own_valid_2 with "Hσ● Hσ◯") as %[Hps _]%auth_both_valid.
-    by pose proof (leibniz_equiv _ _ (Excl_included _ _ Hps)) as ->.
+    by iDestruct (own_valid_2 with "Hσ● Hσ◯")
+      as %[->%Excl_included _]%auth_both_valid.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
-- 
GitLab