Persistence of auth_own.

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).

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.