Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

_CoqProject

@@ -89,10 +89,10 @@ heap_lang/par.v
 heap_lang/tests.v
 heap_lang/substitution.v
 heap_lang/assert.v
-heap_lang/one_shot.v
 barrier/barrier.v
 barrier/specification.v
 barrier/protocol.v
 barrier/proof.v
 barrier/client.v
 examples/joining_existentials.v
+examples/one_shot.v

algebra/agree.v

@@ -118,6 +118,9 @@ Proof.
 Qed.
 Canonical Structure agreeR : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin.
 
+Global Instance agree_persistent (x : agree A) : Persistent x.
+Proof. done. Qed.
+
 Program Definition to_agree (x : A) : agree A :=
   {| agree_car n := x; agree_is_valid n := True |}.
 Solve Obligations with done.

algebra/cmra.v

@@ -120,6 +120,10 @@ Class CMRAUnit (A : cmraT) `{Empty A} := {
 }.
 Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate ∅.
 
+(** * Persistent elements *)
+Class Persistent {A : cmraT} (x : A) := persistent : core x ≡ x.
+Arguments persistent {_} _ {_}.
+
 (** * Discrete CMRAs *)
 Class CMRADiscrete (A : cmraT) := {
   cmra_discrete :> Discrete A;
@@ -229,6 +233,8 @@ Lemma cmra_core_validN n x : ✓{n} x → ✓{n} core x.
 Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
 Lemma cmra_core_valid x : ✓ x → ✓ core x.
 Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
+Global Instance cmra_core_persistent x : Persistent (core x).
+Proof. apply cmra_core_idemp. Qed.
 
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
@@ -336,8 +342,8 @@ Section unit.
   Proof. by exists x; rewrite left_id. Qed.
   Global Instance cmra_unit_right_id : RightId (≡) ∅ (⋅).
   Proof. by intros x; rewrite (comm op) left_id. Qed.
-  Lemma cmra_core_unit : core ∅ ≡ ∅.
-  Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
+  Global Instance cmra_unit_persistent : Persistent ∅.
+  Proof. by rewrite /Persistent -{2}(cmra_core_l ∅) right_id. Qed.
 End unit.
 
 (** ** Local updates *)
@@ -454,6 +460,8 @@ Section cmra_transport.
   Proof. by destruct H. Qed.
   Global Instance cmra_transport_timeless x : Timeless x → Timeless (T x).
   Proof. by destruct H. Qed.
+  Global Instance cmra_transport_persistent x : Persistent x → Persistent (T x).
+  Proof. by destruct H. Qed.
   Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
     x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
   Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
@@ -509,6 +517,8 @@ Section unit.
   Global Instance unit_cmra_unit : CMRAUnit unitR.
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
   Proof. by apply discrete_cmra_discrete. Qed.
+  Global Instance unit_persistent (x : ()) : Persistent x.
+  Proof. done. Qed.
 End unit.
 
 (** ** Product *)
@@ -564,6 +574,10 @@ Section prod.
     CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodR.
   Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
 
+  Global Instance pair_persistent x y :
+    Persistent x → Persistent y → Persistent (x,y).
+  Proof. by split. Qed.
+
   Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
   Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
   Lemma prod_updateP P1 P2 (Q : A * B → Prop)  x :

algebra/dec_agree.v

@@ -45,7 +45,7 @@ Qed.
 Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
 
 (* Some properties of this CMRA *)
-Lemma dec_agree_core_id (x : dec_agree A) : core x = x.
+Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
 Proof. done. Qed.
 
 Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.

algebra/fin_maps.v

@@ -215,6 +215,12 @@ Lemma map_op_singleton (i : K) (x y : A) :
   {[ i := x ]} ⋅ {[ i := y ]} = ({[ i := x ⋅ y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
 
+Global Instance map_persistent m : (∀ x : A, Persistent x) → Persistent m.
+Proof. intros ? i. by rewrite lookup_core persistent. Qed.
+Global Instance map_singleton_persistent i (x : A) :
+  Persistent x → Persistent {[ i := x ]}.
+Proof. intros. by rewrite /Persistent map_core_singleton persistent. Qed.
+
 Lemma singleton_includedN n m i x :
   {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ x ≼{n} y.
 Proof.

algebra/iprod.v

@@ -208,11 +208,15 @@ Section iprod_cmra.
   Lemma iprod_core_singleton x (y : B x) :
     core (iprod_singleton x y) ≡ iprod_singleton x (core y).
   Proof.
-    by move=>x'; destruct (decide (x = x')) as [->|];
-      rewrite iprod_lookup_core ?iprod_lookup_singleton
-      ?iprod_lookup_singleton_ne // cmra_core_unit.
+    move=>x'; destruct (decide (x = x')) as [->|];
+      by rewrite iprod_lookup_core ?iprod_lookup_singleton
+      ?iprod_lookup_singleton_ne // (persistent ∅).
   Qed.
 
+  Global Instance iprod_singleton_persistent x (y : B x) :
+    Persistent y → Persistent (iprod_singleton x y).
+  Proof. intros. rewrite /Persistent iprod_core_singleton. by f_equiv. Qed.
+
   Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
     iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
   Proof.

algebra/one_shot.v

@@ -210,16 +210,15 @@ Proof.
   intros [|a| |]; simpl; auto using cmra_discrete_valid.
 Qed.
 
+Global Instance Shot_persistent a : Persistent a → Persistent (Shot a).
+Proof. by constructor. Qed.
+
 Lemma one_shot_validN_inv_l n y : ✓{n} (OneShotPending ⋅ y) → y = ∅.
-Proof.
-  destruct y as [|b| |]; [done| |done|done]. destruct 1.
-Qed.
+Proof. by destruct y; inversion_clear 1. Qed.
 Lemma one_shot_valid_inv_l y : ✓ (OneShotPending ⋅ y) → y = ∅.
 Proof. intros. by apply one_shot_validN_inv_l with 0, cmra_valid_validN. Qed.
 Lemma one_shot_bot_largest y : y ≼ OneShotBot.
-Proof.
-  destruct y; exists OneShotBot; constructor.
-Qed.
+Proof. destruct y; exists OneShotBot; constructor. Qed.
 
 (** Internalized properties *)
 Lemma one_shot_equivI {M} (x y : one_shot A) :
@@ -259,9 +258,8 @@ Proof.
   - destruct (Hx n b) as (c&?&?); try done.
     exists (Shot c). auto.
   - destruct (Hx n (core a)) as (c&?&?); try done.
-    { rewrite cmra_core_r. done. }
-    exists (Shot c). split; first by auto.
-    simpl. by eapply cmra_validN_op_l.
+    { by rewrite cmra_core_r. }
+    exists (Shot c). split; simpl; eauto using cmra_validN_op_l.
 Qed.
 Lemma one_shot_updateP' (P : A → Prop) a :
   a ~~>: P → Shot a ~~>: λ m', ∃ b, m' = Shot b ∧ P b.

algebra/option.v

@@ -130,6 +130,12 @@ Proof. by destruct mx, my; inversion_clear 1. Qed.
 Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None.
 Proof. by destruct mx, my; inversion_clear 1. Qed.
 
+Global Instance Some_persistent (x : A) : Persistent x → Persistent (Some x).
+Proof. by constructor. Qed.
+Global Instance option_persistent (mx : option A) :
+  (∀ x : A, Persistent x) → Persistent mx.
+Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
+
 (** Internalized properties *)
 Lemma option_equivI {M} (x y : option A) :
   (x ≡ y) ⊣⊢ (match x, y with

algebra/upred.v

@@ -304,8 +304,8 @@ Infix "↔" := uPred_iff : uPred_scope.
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
 Arguments timelessP {_} _ {_}.
 
-Class Persistent {M} (P : uPred M) := persistent : P ⊢ □ P.
-Arguments persistent {_} _ {_}.
+Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
+Arguments persistentP {_} _ {_}.
 
 Module uPred.
 Definition unseal :=
@@ -1002,8 +1002,8 @@ Proof.
   rewrite -(cmra_core_idemp a) Hx.
   apply cmra_core_preservingN, cmra_includedN_l.
 Qed.
-Lemma always_ownM (a : M) : core a ≡ a → (□ uPred_ownM a) ⊣⊢ uPred_ownM a.
-Proof. by intros <-; rewrite always_ownM_core. Qed.
+Lemma always_ownM (a : M) : Persistent a → (□ uPred_ownM a) ⊣⊢ uPred_ownM a.
+Proof. intros. by rewrite -(persistent a) always_ownM_core. Qed.
 Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
 Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
 Lemma ownM_empty `{Empty M, !CMRAUnit M} : True ⊢ uPred_ownM ∅.
@@ -1120,53 +1120,53 @@ Proof.
 Qed.
 
 (* Always stable *)
-Global Instance const_persistent φ : Persistent (■ φ : uPred M)%I.
-Proof. by rewrite /Persistent always_const. Qed.
-Global Instance always_persistent P : Persistent (□ P).
+Global Instance const_persistent φ : PersistentP (■ φ : uPred M)%I.
+Proof. by rewrite /PersistentP always_const. Qed.
+Global Instance always_persistent P : PersistentP (□ P).
 Proof. by intros; apply always_intro'. Qed.
 Global Instance and_persistent P Q :
-  Persistent P → Persistent Q → Persistent (P ∧ Q).
-Proof. by intros; rewrite /Persistent always_and; apply and_mono. Qed.
+  PersistentP P → PersistentP Q → PersistentP (P ∧ Q).
+Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
 Global Instance or_persistent P Q :
-  Persistent P → Persistent Q → Persistent (P ∨ Q).
-Proof. by intros; rewrite /Persistent always_or; apply or_mono. Qed.
+  PersistentP P → PersistentP Q → PersistentP (P ∨ Q).
+Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
 Global Instance sep_persistent P Q :
-  Persistent P → Persistent Q → Persistent (P ★ Q).
-Proof. by intros; rewrite /Persistent always_sep; apply sep_mono. Qed.
+  PersistentP P → PersistentP Q → PersistentP (P ★ Q).
+Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
 Global Instance forall_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
-Proof. by intros; rewrite /Persistent always_forall; apply forall_mono. Qed.
+  (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
+Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
 Global Instance exist_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
-Proof. by intros; rewrite /Persistent always_exist; apply exist_mono. Qed.
+  (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
+Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
 Global Instance eq_persistent {A : cofeT} (a b : A) :
-  Persistent (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /Persistent always_eq. Qed.
+  PersistentP (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /PersistentP always_eq. Qed.
 Global Instance valid_persistent {A : cmraT} (a : A) :
-  Persistent (✓ a : uPred M)%I.
-Proof. by intros; rewrite /Persistent always_valid. Qed.
-Global Instance later_persistent P : Persistent P → Persistent (▷ P).
-Proof. by intros; rewrite /Persistent always_later; apply later_mono. Qed.
-Global Instance ownM_core_persistent (a : M) : Persistent (uPred_ownM (core a)).
-Proof. by rewrite /Persistent always_ownM_core. Qed.
+  PersistentP (✓ a : uPred M)%I.
+Proof. by intros; rewrite /PersistentP always_valid. Qed.
+Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
+Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
+Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
+Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 Global Instance default_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
-  Persistent P → (∀ x, Persistent (Ψ x)) → Persistent (default P mx Ψ).
+  PersistentP P → (∀ x, PersistentP (Ψ x)) → PersistentP (default P mx Ψ).
 Proof. destruct mx; apply _. Qed.
 
 (* Derived lemmas for always stable *)
-Lemma always_always P `{!Persistent P} : (□ P) ⊣⊢ P.
+Lemma always_always P `{!PersistentP P} : (□ P) ⊣⊢ P.
 Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_intro P Q `{!Persistent P} : P ⊢ Q → P ⊢ □ Q.
+Lemma always_intro P Q `{!PersistentP P} : P ⊢ Q → P ⊢ □ Q.
 Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!Persistent P} : (P ∧ Q) ⊣⊢ (P ★ Q).
+Lemma always_and_sep_l P Q `{!PersistentP P} : (P ∧ Q) ⊣⊢ (P ★ Q).
 Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!Persistent Q} : (P ∧ Q) ⊣⊢ (P ★ Q).
+Lemma always_and_sep_r P Q `{!PersistentP Q} : (P ∧ Q) ⊣⊢ (P ★ Q).
 Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!Persistent P} : P ⊣⊢ (P ★ P).
+Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ (P ★ P).
 Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ (Q ★ P).
+Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ (Q ★ P).
 Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ (P ★ Q).
+Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ (P ★ Q).
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 End uPred_logic.
 

algebra/upred_big_op.v

@@ -30,7 +30,7 @@ Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
 
 (** * Always stability for lists *)
 Class PersistentL {M} (Ps : list (uPred M)) :=
-  persistentL : Forall Persistent Ps.
+  persistentL : Forall PersistentP Ps.
 Arguments persistentL {_} _ {_}.
 
 Section big_op.
@@ -216,21 +216,21 @@ Section gset.
 End gset.
 
 (* Always stable *)
-Global Instance big_and_persistent Ps : PersistentL Ps → Persistent (Π∧ Ps).
+Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP (Π∧ Ps).
 Proof. induction 1; apply _. Qed.
-Global Instance big_sep_persistent Ps : PersistentL Ps → Persistent (Π★ Ps).
+Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP (Π★ Ps).
 Proof. induction 1; apply _. Qed.
 
 Global Instance nil_persistent : PersistentL (@nil (uPred M)).
 Proof. constructor. Qed.
 Global Instance cons_persistent P Ps :
-  Persistent P → PersistentL Ps → PersistentL (P :: Ps).
+  PersistentP P → PersistentL Ps → PersistentL (P :: Ps).
 Proof. by constructor. Qed.
 Global Instance app_persistent Ps Ps' :
   PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps').
 Proof. apply Forall_app_2. Qed.
 Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys :
-  (∀ x y, Persistent (f x y)) → PersistentL (zip_with f xs ys).
+  (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys).
 Proof.
   unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
 Qed.

barrier/proof.v

@@ -51,7 +51,7 @@ Definition recv (l : loc) (R : iProp) : iProp :=
     saved_prop_own i Q ★ ▷ (Q -★ R))%I.
 
 Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp) :
-  Persistent (barrier_ctx γ l P).
+  PersistentP (barrier_ctx γ l P).
 Proof. apply _. Qed.
 
 (* TODO: Figure out if this has a "Global" or "Local" effect.

heap_lang/one_shot.v → examples/one_shot.v

@@ -103,9 +103,7 @@ Proof.
         rewrite -(exist_intro n). ecancel [inv _ _]%I.
         rewrite [(_ ★ _)%I]comm -assoc. apply const_elim_sep_l=>->.
         rewrite const_equiv // left_id /one_shot_inv -or_intro_r.
-        rewrite -(exist_intro n).
-        rewrite -(dec_agree_core_id (DecAgree n))
-          -(Shot_core (DecAgree n : dec_agreeR _)) {1}(always_sep_dup (own _ _)).
+        rewrite -(exist_intro n) {1}(always_sep_dup (own _ _)).
         solve_sep_entails. }
     cancel [one_shot_inv γ l].
     (* FIXME: why aren't laters stripped? *)

heap_lang/heap.v

@@ -33,7 +33,7 @@ Section definitions.
 
   Global Instance heap_inv_proper : Proper ((≡) ==> (⊣⊢)) heap_inv.
   Proof. solve_proper. Qed.
-  Global Instance heap_ctx_persistent N : Persistent (heap_ctx N).
+  Global Instance heap_ctx_persistent N : PersistentP (heap_ctx N).
   Proof. apply _. Qed.
 End definitions.
 Typeclasses Opaque heap_ctx heap_mapsto.

program_logic/auth.v

@@ -30,7 +30,7 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance auth_own_timeless a : TimelessP (auth_own a).
   Proof. apply _. Qed.
-  Global Instance auth_ctx_persistent N φ : Persistent (auth_ctx N φ).
+  Global Instance auth_ctx_persistent N φ : PersistentP (auth_ctx N φ).
   Proof. apply _. Qed.
 End definitions.
 

program_logic/ghost_ownership.v

@@ -36,10 +36,6 @@ Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ (own γ a1 ★ own γ a2).
 Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
 Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (own γ).
 Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
-Lemma always_own_core γ a : (□ own γ (core a)) ⊣⊢ own γ (core a).
-Proof. by rewrite /own -to_globalF_core always_ownG_core. Qed.
-Lemma always_own γ a : core a ≡ a → (□ own γ a) ⊣⊢ own γ a.
-Proof. by intros <-; rewrite always_own_core. Qed.
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
   rewrite /own ownG_valid /to_globalF.
@@ -53,9 +49,9 @@ Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
-Proof. unfold own; apply _. Qed.
-Global Instance own_core_persistent γ a : Persistent (own γ (core a)).
-Proof. by rewrite /Persistent always_own_core. Qed.
+Proof. rewrite /own; apply _. Qed.
+Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
+Proof. rewrite /own; apply _. Qed.
 
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)

program_logic/global_functor.v

@@ -41,12 +41,10 @@ Lemma to_globalF_op γ a1 a2 :
 Proof.
   by rewrite /to_globalF iprod_op_singleton map_op_singleton cmra_transport_op.
 Qed.
-Lemma to_globalF_core γ a : core (to_globalF γ a) ≡ to_globalF γ (core a).
-Proof.
-  by rewrite /to_globalF
-    iprod_core_singleton map_core_singleton cmra_transport_core.
-Qed.
-Global Instance to_globalF_timeless γ m : Timeless m → Timeless (to_globalF γ m).
+Global Instance to_globalF_timeless γ m: Timeless m → Timeless (to_globalF γ m).
+Proof. rewrite /to_globalF; apply _. Qed.
+Global Instance to_globalF_persistent γ m :
+  Persistent m → Persistent (to_globalF γ m).
 Proof. rewrite /to_globalF; apply _. Qed.
 End to_globalF.
 

program_logic/invariants.v

@@ -23,7 +23,7 @@ Implicit Types Φ : val Λ → iProp Λ Σ.
 Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
 Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
 
-Global Instance inv_persistent N P : Persistent (inv N P).
+Global Instance inv_persistent N P : PersistentP (inv N P).
 Proof. rewrite /inv; apply _. Qed.
 
 Lemma always_inv N P : (□ inv N P) ⊣⊢ inv N P.
@@ -96,5 +96,4 @@ Proof.
   intros. rewrite -(pvs_mask_weaken N) //.
   by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
 Qed.
-
 End inv.

program_logic/ownership.v

@@ -25,15 +25,8 @@ Proof.
   apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
   by apply Next_contractive=> j ?; rewrite (HPQ j).
 Qed.
-Lemma always_ownI i P : (□ ownI i P) ⊣⊢ ownI i P.
-Proof.
-  apply uPred.always_ownM.
-  by rewrite Res_core !cmra_core_unit map_core_singleton.
-Qed.
-Global Instance ownI_persistent i P : Persistent (ownI i P).
-Proof. by rewrite /Persistent always_ownI. Qed.
-Lemma ownI_sep_dup i P : ownI i P ⊣⊢ (ownI i P ★ ownI i P).
-Proof. apply (uPred.always_sep_dup _). Qed.
+Global Instance ownI_persistent i P : PersistentP (ownI i P).
+Proof. rewrite /ownI. apply _. Qed.
 
 (* physical state *)
 Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Λ Σ) ⊢ False.
@@ -52,25 +45,16 @@ Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ (ownG m1 ★ ownG m2).
 Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
 Global Instance ownG_mono : Proper (flip (≼) ==> (⊢)) (@ownG Λ Σ).
 Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
-Lemma always_ownG_core m : (□ ownG (core m)) ⊣⊢ ownG (core m).
-Proof.
-  apply uPred.always_ownM.
-  by rewrite Res_core !cmra_core_unit -{2}(cmra_core_idemp m).
-Qed.
-Lemma always_ownG m : core m ≡ m → (□ ownG m) ⊣⊢ ownG m.
-Proof. by intros <-; rewrite always_ownG_core. Qed.
 Lemma ownG_valid m : ownG m ⊢ ✓ m.
-Proof.
-  rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
-Qed.
+Proof. rewrite /ownG uPred.ownM_valid res_validI /=; auto with I. Qed.
 Lemma ownG_valid_r m : ownG m ⊢ (ownG m ★ ✓ m).
 Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Lemma ownG_empty : True ⊢ (ownG ∅ : iProp Λ Σ).
 Proof. apply uPred.ownM_empty. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
-Global Instance ownG_core_persistent m : Persistent (ownG (core m)).
-Proof. by rewrite /Persistent always_ownG_core. Qed.
+Global Instance ownG_persistent m : Persistent m → PersistentP (ownG m).
+Proof. rewrite /ownG; apply _. Qed.
 
 (* inversion lemmas *)
 Lemma ownI_spec n r i P :

program_logic/pviewshifts.v

@@ -146,10 +146,10 @@ Lemma pvs_strip_pvs E P Q : P ⊢ (|={E}=> Q) → (|={E}=> P) ⊢ (|={E}=> Q).
 Proof. move=>->. by rewrite pvs_trans'. Qed.
 Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊢ (|={E1,E2}=> P ★ Q).
 Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
-Lemma pvs_always_l E1 E2 P Q `{!Persistent P} :
+Lemma pvs_always_l E1 E2 P Q `{!PersistentP P} :
   (P ∧ |={E1,E2}=> Q) ⊢ (|={E1,E2}=> P ∧ Q).
 Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
-Lemma pvs_always_r E1 E2 P Q `{!Persistent Q} :
+Lemma pvs_always_r E1 E2 P Q `{!PersistentP Q} :
   ((|={E1,E2}=> P) ∧ Q) ⊢ (|={E1,E2}=> P ∧ Q).
 Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
 Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=> Q).

program_logic/resources.v

@@ -153,6 +153,8 @@ Lemma lookup_wld_op_r n r1 r2 i P :
 Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
 Global Instance Res_timeless eσ m : Timeless m → Timeless (@Res Λ A M ∅ eσ m).
 Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
+Global Instance Res_persistent w m: Persistent m → Persistent (@Res Λ A M w ∅ m).
+Proof. constructor; apply (persistent _). Qed.
 
 (** Internalized properties *)
 Lemma res_equivI {M'} r1 r2 :

program_logic/saved_one_shot.v

@@ -9,8 +9,7 @@ Definition oneShotGF (F : cFunctor) : gFunctor :=
 Instance inGF_oneShotG  `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
 Proof. apply: inGF_inG. Qed.
 
-Definition one_shot_pending `{oneShotG Λ Σ F}
-    (γ : gname) : iPropG Λ Σ :=
+Definition one_shot_pending `{oneShotG Λ Σ F} (γ : gname) : iPropG Λ Σ :=
   own γ OneShotPending.
 Definition one_shot_own `{oneShotG Λ Σ F}
     (γ : gname) (x : F (iPropG Λ Σ)) : iPropG Λ Σ :=
@@ -23,9 +22,8 @@ Section one_shot.
   Implicit Types x y : F (iPropG Λ Σ).
   Implicit Types γ : gname.
 
-  Global Instance ne_shot_own_persistent γ x :
-    Persistent (one_shot_own γ x).
-  Proof. by rewrite /Persistent always_own. Qed.
+  Global Instance ne_shot_own_persistent γ x : PersistentP (one_shot_own γ x).
+  Proof. rewrite /one_shot_own; apply _. Qed.
 
   Lemma one_shot_alloc_strong N (G : gset gname) :
     True ⊢ pvs N N (∃ γ, ■ (γ ∉ G) ∧ one_shot_pending γ).

program_logic/saved_prop.v

@@ -20,9 +20,8 @@ Section saved_prop.
   Implicit Types x y : F (iPropG Λ Σ).
   Implicit Types γ : gname.
 
-  Global Instance saved_prop_persistent γ x :
-    Persistent (saved_prop_own γ x).
-  Proof. by rewrite /Persistent always_own. Qed.
+  Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
+  Proof. rewrite /saved_prop_own; apply _. Qed.
 
   Lemma saved_prop_alloc_strong N x (G : gset gname) :
     True ⊢ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x).

program_logic/sts.v

@@ -42,7 +42,7 @@ Section definitions.
   Global Instance sts_ctx_proper N :
     Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
   Proof. solve_proper. Qed.
-  Global Instance sts_ctx_persistent N φ : Persistent (sts_ctx N φ).
+  Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).