From 8ab2971ed5f52703fe97016eca0505afeae24270 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Thu, 8 Apr 2021 17:04:56 +0200
Subject: [PATCH] fix bij_own_elem_agree; add bij_own_elem_auth_agree

---
 iris/base_logic/lib/gset_bij.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 00f82ec26..4c30daa54 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -98,7 +98,7 @@ Section gset_bij.
     by iDestruct (own_valid with "Hauth") as %?%gset_bij_auth_dfrac_valid.
   Qed.
 
-  Lemma gset_bij_own_elem_agree γ L a a' b b' :
+  Lemma gset_bij_own_elem_agree γ a a' b b' :
     gset_bij_own_elem γ a b -∗ gset_bij_own_elem γ a' b' -∗
     ⌜a = a' ↔ b = b'⌝.
   Proof.
@@ -113,6 +113,15 @@ Section gset_bij.
     intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
     by apply own_mono, bij_view_included.
   Qed.
+
+  Lemma gset_bij_own_elem_auth_agree {γ q L} a b :
+    gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b -∗ ⌜(a, b) ∈ L⌝.
+  Proof.
+    iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
+    iPoseProof (own_valid_2 with "Hauth Helem") as "%Ha".
+    iPureIntro. revert Ha. rewrite bij_both_dfrac_valid. intros (_ & _ & ?); done.
+  Qed.
+
   Lemma gset_bij_own_elem_get_big γ q L :
     gset_bij_own_auth γ q L -∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
   Proof.
-- 
GitLab