From a17e5b6e80ad9284d31c448988dd87b51cf98a56 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Jul 2016 16:34:57 +0200
Subject: [PATCH] Persistence of auth_own.

---
 algebra/auth.v       | 3 +++
 program_logic/auth.v | 4 ++++
 2 files changed, 7 insertions(+)

diff --git a/algebra/auth.v b/algebra/auth.v
index 45488923b..4e33a44a7 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -162,6 +162,9 @@ Qed.
 Canonical Structure authUR :=
   UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
 
+Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
+Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
+
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :
   x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y : uPred M).
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 58d63dcd9..9fd82aa07 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -59,6 +59,10 @@ Section auth.
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
 
+  Global Instance auth_own_persistent γ a :
+    Persistent a → PersistentP (auth_own γ a).
+  Proof. rewrite /auth_own. apply _. Qed.
+
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
-- 
GitLab