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

algebra/agree.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
@@ -129,6 +129,12 @@ Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
 Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
 Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
+
+(** Internalized properties *)
+Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b)%I ≡ (a ≡ b : uPred M)%I.
+Proof. split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
+Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
+Proof. by intros r n _ ?; apply: agree_op_inv. Qed.
 End agree.
 
 Arguments agreeC : clear implicits.

algebra/auth.v

 From algebra Require Export excl.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -131,6 +131,18 @@ Qed.
 Canonical Structure authRA : cmraT :=
   CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
 
+(** Internalized properties *)
+Lemma auth_equivI {M} (x y : auth A) :
+  (x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I.
+Proof. done. Qed.
+Lemma auth_validI {M} (x : auth A) :
+  (✓ x)%I ≡ (match authoritative x with
+             | Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
+             | ExclUnit => ✓ own x
+             | ExclBot => False
+             end : uPred M)%I.
+Proof. by destruct x as [[]]. Qed.
+
 (** The notations ◯ and ● only work for CMRAs with an empty element. So, in
 what follows, we assume we have an empty element. *)
 Context `{Empty A, !CMRAIdentity A}.

algebra/excl.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -138,6 +138,18 @@ Proof.
   by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
 Qed.
 
+(** Internalized properties *)
+Lemma excl_equivI {M} (x y : excl A) :
+  (x ≡ y)%I ≡ (match x, y with
+               | Excl a, Excl b => a ≡ b
+               | ExclUnit, ExclUnit | ExclBot, ExclBot => True
+               | _, _ => False
+               end : uPred M)%I.
+Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
+Lemma excl_validI {M} (x : excl A) :
+  (✓ x)%I ≡ (if x is ExclBot then False else True : uPred M)%I.
+Proof. by destruct x. Qed.
+
 (** ** Local updates *)
 Global Instance excl_local_update b :
   LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).

algebra/fin_maps.v

 From algebra Require Export cmra option.
 From prelude Require Export gmap.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
@@ -85,6 +85,7 @@ Arguments mapC _ {_ _} _.
 (* CMRA *)
 Section cmra.
 Context `{Countable K} {A : cmraT}.
+Implicit Types m : gmap K A.
 
 Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
@@ -160,6 +161,12 @@ Proof.
   * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   * apply map_empty_timeless.
 Qed.
+
+(** Internalized properties *)
+Lemma map_equivI {M} m1 m2 : (m1 ≡ m2)%I ≡ (∀ i, m1 !! i ≡ m2 !! i : uPred M)%I.
+Proof. done. Qed.
+Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
+Proof. done. Qed.
 End cmra.
 
 Arguments mapRA _ {_ _} _.

algebra/iprod.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
@@ -169,6 +169,12 @@ Section iprod_cmra.
     * by apply _.
   Qed.
 
+  (** Internalized properties *)
+  Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I.
+  Proof. done. Qed.
+  Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I.
+  Proof. done. Qed.
+
   (** Properties of iprod_insert. *)
   Context `{∀ x x' : A, Decision (x = x')}.
 

algebra/option.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 
 (* COFE *)
 Section cofe.
@@ -121,6 +121,7 @@ Canonical Structure optionRA :=
 Global Instance option_cmra_identity : CMRAIdentity optionRA.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
 
+(** Misc *)
 Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
 Proof.
   destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
@@ -130,6 +131,17 @@ 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.
 
+(** Internalized properties *)
+Lemma option_equivI {M} (x y : option A) :
+  (x ≡ y)%I ≡ (match x, y with
+               | Some a, Some b => a ≡ b | None, None => True | _, _ => False
+               end : uPred M)%I.
+Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
+Lemma option_validI {M} (x : option A) :
+  (✓ x)%I ≡ (match x with Some a => ✓ a | None => True end : uPred M)%I.
+Proof. by destruct x. Qed.
+
+(** Updates *)
 Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
   x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
 Proof.

algebra/upred.v

@@ -521,6 +521,9 @@ Proof.
   * by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
   * by apply impl_intro_l; rewrite left_id.
 Qed.
+Lemma iff_refl Q P : Q ⊑ (P ↔ P).
+Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
+
 Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I.
 Proof.
   apply (anti_symm (⊑)); first auto.
@@ -790,7 +793,7 @@ Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
-(* Own and valid *)
+(* Own *)
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
 Proof.
@@ -813,17 +816,28 @@ Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
 Proof. intros x n ??. by exists x; simpl. Qed.
 Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
 Proof. intros x n ??; by  exists x; rewrite left_id. Qed.
+
+(* Valid *)
 Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
 Proof. intros x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
 Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
 Proof. intros Ha x n ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
-  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊑ ✓ b.
-Proof. by intros ? x n ?; simpl; auto. Qed.
 Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
 Proof. done. Qed.
+Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
+Proof. intros r n _; apply cmra_validN_op_l. Qed.
+
+Lemma prod_equivI {A B : cofeT} (x y : A * B) :
+  (x ≡ y)%I ≡ (x.1 ≡ y.1 ∧ x.2 ≡ y.2 : uPred M)%I.
+Proof. done. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) :
+  (✓ x)%I ≡ (✓ x.1 ∧ ✓ x.2 : uPred M)%I.
+Proof. done. Qed.
+Lemma later_equivI {A : cofeT} (x y : later A) :
+  (x ≡ y)%I ≡ (▷ (later_car x ≡ later_car y) : uPred M)%I.
+Proof. done. Qed.
 
 (* Own and valid derived *)
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
@@ -989,5 +1003,5 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve always_mono : I.
 Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
 Hint Immediate True_intro False_elim : I.
-
+Hint Immediate iff_refl : I.
 End uPred.

program_logic/auth.v

-From algebra Require Export auth functor.
+From algebra Require Export auth.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
-Section auth.
-  Context {A : cmraT} `{Empty A, !CMRAIdentity A} `{!∀ a : A, Timeless a}.
-  Context {Λ : language} {Σ : iFunctorG} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
-  Context (N : namespace) (φ : A → iPropG Λ Σ).
+Class AuthInG Λ Σ (i : gid) (A : cmraT) `{Empty A} := {
+  auth_inG :> InG Λ Σ i (authRA A);
+  auth_identity :> CMRAIdentity A;
+  auth_timeless (a : A) :> Timeless a;
+}.
+
+Definition auth_inv {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
+  (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := (∃ a, (■✓a ∧ own i γ (● a)) ★ φ a)%I.
+Definition auth_own {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
+  (γ : gname) (a : A) : iPropG Λ Σ := own i γ (◯ a).
+Definition auth_ctx {Λ Σ A} (i : gid) `{AuthInG Λ Σ i A}
+    (γ : gname) (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+  inv N (auth_inv i γ φ).
+Instance: Params (@auth_inv) 7.
+Instance: Params (@auth_own) 7.
+Instance: Params (@auth_ctx) 8.
 
+Section auth.
+  Context `{AuthInG Λ Σ AuthI A}.
+  Context (φ : A → iPropG Λ Σ) {φ_ne : ∀ n, Proper (dist n ==> dist n) φ}.
+  Implicit Types N : namespace.
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
-  (* TODO: Need this to be proven somewhere. *)
-  Hypothesis auth_valid :
-    forall a b, (✓ Auth (Excl a) b : iPropG Λ Σ) ⊑ (∃ b', a ≡ b ⋅ b').
-
-  Definition auth_inv (γ : gname) : iPropG Λ Σ :=
-    (∃ a, (■✓a ∧ own AuthI γ (● a)) ★ φ a)%I.
-  Definition auth_own (γ : gname) (a : A) : iPropG Λ Σ := own AuthI γ (◯ a).
-  Definition auth_ctx (γ : gname) : iPropG Λ Σ := inv N (auth_inv γ).
+  Local Instance φ_proper : Proper ((≡) ==> (≡)) φ := ne_proper _.
 
-  Lemma auth_alloc a :
-    ✓a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ ∧ auth_own γ a).
+  Lemma auth_alloc N a :
+    ✓ a → φ a ⊑ pvs N N (∃ γ, auth_ctx AuthI γ N φ ∧ auth_own AuthI γ a).
   Proof.
     intros Ha. rewrite -(right_id True%I (★)%I (φ _)).
     rewrite (own_alloc AuthI (Auth (Excl a) a) N) //; [].
     rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    transitivity (▷auth_inv γ ★ auth_own γ a)%I.
+    transitivity (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ a)%I.
     { rewrite /auth_inv -later_intro -(exist_intro a).
       rewrite const_equiv // left_id.
       rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
@@ -36,26 +45,24 @@ Section auth.
     by rewrite always_and_sep_l.
   Qed.
 
-  Lemma auth_empty γ E :
-    True ⊑ pvs E E (auth_own γ ∅).
+  Lemma auth_empty γ E : True ⊑ pvs E E (auth_own AuthI γ ∅).
   Proof. by rewrite own_update_empty /auth_own. Qed.
 
-  Context {φ_ne : ∀ n, Proper (dist n ==> dist n) φ}.
-  Local Instance φ_proper : Proper ((≡) ==> (≡)) φ := ne_proper _.
-
   Lemma auth_opened E a γ :
-    (▷auth_inv γ ★ auth_own γ a) ⊑ pvs E E (∃ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
+    (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ a)
+    ⊑ pvs E E (∃ a', ■✓(a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
     rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
     rewrite later_sep [(▷(_ ∧ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
     rewrite always_and_sep_l -!assoc. apply const_elim_sep_l=>Hv.
     rewrite /auth_own [(▷φ _ ★ _)%I]comm assoc -own_op.
-    rewrite own_valid_r auth_valid sep_exist_l sep_exist_r /=. apply exist_elim=>a'.
-    rewrite [∅ ⋅ _]left_id -(exist_intro a').
+    rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
+    apply exist_elim=>a'.
+    rewrite left_id -(exist_intro a').
     apply (eq_rewrite b (a ⋅ a')
               (λ x, ■✓x ★ ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
     { by move=>n ? ? /timeless_iff ->. }
-    { apply sep_elim_l', sep_elim_r'. done. (* FIXME why does "eauto using I not work? *) }
+    { apply sep_elim_l', sep_elim_r'. done. (* FIXME why does "eauto using I" not work? *) }
     rewrite const_equiv // left_id comm.
     apply sep_mono; first done.
     by rewrite sep_elim_l.
@@ -63,8 +70,8 @@ Section auth.
 
   Lemma auth_closing E `{!LocalUpdate Lv L} a a' γ :
     Lv a → ✓ (L a ⋅ a') →
-    (▷φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
-    ⊑ pvs E E (▷auth_inv γ ★ auth_own γ (L a)).
+    (▷ φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
+    ⊑ pvs E E (▷ auth_inv AuthI γ φ ★ auth_own AuthI γ (L a)).
   Proof.
     intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a ⋅ a')).
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
@@ -77,11 +84,11 @@ Section auth.
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
   Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
-        `{!LocalUpdate Lv L} E P (Q : X → iPropG Λ Σ) γ a :
+        `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
     nclose N ⊆ E →
-    P ⊑ auth_ctx γ →
-    P ⊑ (auth_own γ a ★ (∀ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') -★
-        FSA (E ∖ nclose N) (λ x, ■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own γ (L a) -★ Q x)))) →
+    P ⊑ auth_ctx AuthI γ N φ →
+    P ⊑ (auth_own AuthI γ a ★ (∀ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') -★
+        FSA (E ∖ nclose N) (λ x, ■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ (auth_own AuthI γ (L a) -★ Q x)))) →
     P ⊑ FSA E Q.
   Proof.
     rewrite /auth_ctx=>HN Hinv Hinner.

program_logic/ghost_ownership.v

@@ -34,11 +34,6 @@ Implicit Types a : A.
 (** * Properties of to_globalC *)
 Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF i γ).
 Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
-Lemma to_globalF_validN n γ a : ✓{n} to_globalF i γ a ↔ ✓{n} a.
-Proof.
-  by rewrite /to_globalF
-    iprod_singleton_validN map_singleton_validN cmra_transport_validN.
-Qed.
 Lemma to_globalF_op γ a1 a2 :
   to_globalF i γ (a1 ⋅ a2) ≡ to_globalF i γ a1 ⋅ to_globalF i γ a2.
 Proof.
@@ -75,7 +70,10 @@ Lemma always_own_unit γ a : (□ own i γ (unit a))%I ≡ own i γ (unit a).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
 Lemma own_valid γ a : own i γ a ⊑ ✓ a.
 Proof.
-  rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalF_validN.
+  rewrite /own ownG_valid /to_globalF.
+  rewrite iprod_validI (forall_elim i) iprod_lookup_singleton.
+  rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
+  by destruct inG.
 Qed.
 Lemma own_valid_r γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.

program_logic/ownership.v

@@ -55,9 +55,11 @@ Proof.
   apply uPred.always_ownM.
   by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
 Qed.
-Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
-Proof. by rewrite /ownG uPred.ownM_valid; apply uPred.valid_mono=> n [? []]. Qed.
-Lemma ownG_valid_r m : (ownG m) ⊑ (ownG m ★ ✓ m).
+Lemma ownG_valid m : ownG m ⊑ ✓ m.
+Proof.
+  rewrite /ownG uPred.ownM_valid res_validI /= option_validI; auto with I.
+Qed.
+Lemma ownG_valid_r m : ownG m ⊑ (ownG m ★ ✓ m).
 Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.

program_logic/resources.v

 From algebra Require Export fin_maps agree excl functor.
+From algebra Require Import upred.
 From program_logic Require Export language.
 
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
@@ -154,20 +155,23 @@ Proof.
 Qed.
 Lemma lookup_wld_op_r n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
-Proof.
-  rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l.
-Qed.
+Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
 Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
 Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
+
+(** Internalized properties *)
+Lemma res_equivI {M} r1 r2 :
+  (r1 ≡ r2)%I ≡ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M)%I.
+Proof. split. by destruct 1. by intros (?&?&?); constructor. Qed.
+Lemma res_validI {M} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M)%I.
+Proof. done. Qed.
 End res.
 
 Arguments resC : clear implicits.
 Arguments resRA : clear implicits.
 
 Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
-  Res (agree_map f <$> wld r)
-      (pst r)
-      (ifunctor_map Σ f <$> gst r).
+  Res (agree_map f <$> wld r) (pst r) (ifunctor_map Σ f <$> gst r).
 Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
   (∀ n, Proper (dist n ==> dist n) f) →
   ∀ n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).

program_logic/saved_prop.v

+From algebra Require Export agree.
+From program_logic Require Export ghost_ownership.
+Import uPred.
+
+Class SavedPropInG Λ Σ (i : gid) :=
+  saved_prop_inG :> InG Λ Σ i (agreeRA (laterC (iPreProp Λ (globalF Σ)))).
+
+Definition saved_prop_own {Λ Σ} (i : gid) `{SavedPropInG Λ Σ i}
+    (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
+  own i γ (to_agree (Next (iProp_unfold P))).
+Instance: Params (@saved_prop_own) 5.
+
+Section stored_prop.
+  Context `{SavedPropInG Λ Σ SPI}.
+  Implicit Types P Q : iPropG Λ Σ.
+  Implicit Types γ : gname.
+
+  Lemma saved_prop_alloc N P :
+    True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P).
+  Proof. by apply own_alloc. Qed.
+
+  Lemma saved_prop_twice γ P Q :
+    (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ↔ Q).
+  Proof.
+    rewrite /saved_prop_own -own_op own_valid agree_validI.
+    rewrite agree_equivI later_equivI /=; apply later_mono.
+    rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
+    apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
+      iProp_fold (iProp_unfold P) ↔ iProp_fold Q')%I); solve_ne || auto with I.
+  Qed.
+End stored_prop.