From 3321a5f7a7a9e7e88cc5f728d8d70abc4ebbe00f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Jun 2022 16:12:22 +0200
Subject: [PATCH] Make validy lemmas for `excl_auth` more consistent with
 `auth`.

- Rename `excl_auth_frag_validN_op_1_l` into `excl_auth_frag_op_validN` and
  `excl_auth_frag_valid_op_1_l` into `excl_auth_frag_op_valid` (similar to
  `auth_auth_op_valid`, and make them bi-implications.
- Add `excl_auth_auth_op_validN` and `excl_auth_auth_op_valid`
---
 iris/algebra/lib/excl_auth.v | 9 +++++++--
 iris/program_logic/ownp.v    | 2 +-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/iris/algebra/lib/excl_auth.v b/iris/algebra/lib/excl_auth.v
index da52b48cc..f947a7cb8 100644
--- a/iris/algebra/lib/excl_auth.v
+++ b/iris/algebra/lib/excl_auth.v
@@ -59,9 +59,14 @@ Section excl_auth.
   Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
   Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
 
-  Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_auth_op_validN n a b : ✓{n} (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_validN. Qed.
+  Lemma excl_auth_auth_op_valid a b : ✓ (●E a ⋅ ●E b) ↔ False.
+  Proof. apply auth_auth_op_valid. Qed.
+
+  Lemma excl_auth_frag_op_validN n a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
-  Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
+  Lemma excl_auth_frag_op_valid a b : ✓ (◯E a ⋅ ◯E b) ↔ False.
   Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
 
   Lemma excl_auth_update a b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index d467e21f5..c7ec1a2dd 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -100,7 +100,7 @@ Section lifting.
   Qed.
   Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof.
-    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_valid_op_1_l).
+    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_op_valid).
   Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
-- 
GitLab