Add separation logic unpersist update laws

iris/base_logic/lib/gen_heap.v

@@ -189,6 +189,11 @@ Section gen_heap.
   Lemma pointsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
   Proof. rewrite pointsto_unseal. apply ghost_map_elem_persist. Qed.
 
+  (** Recover fractional ownership for read-only element. *)
+  Lemma pointsto_unpersist l v :
+    l ↦□ v ==∗ ∃ q, l ↦{# q} v.
+  Proof. rewrite pointsto_unseal. apply ghost_map_elem_unpersist. Qed.
+
   (** Framing support *)
   Global Instance frame_pointsto p l v q1 q2 q :
     FrameFractionalQp q1 q2 q →

iris/base_logic/lib/ghost_map.v

@@ -137,6 +137,17 @@ Section lemmas.
     k ↪[γ]{dq} v ==∗ k ↪[γ]□ v.
   Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
 
+  (** Recover fractional ownership for read-only element. *)
+  Lemma ghost_map_elem_unpersist k γ v :
+    k ↪[γ]□ v ==∗ ∃ q, k ↪[γ]{# q} v.
+  Proof.
+    unseal. iIntros "H".
+    iMod (own_updateP with "H") as "H";
+      first by apply gmap_view_frag_unpersist.
+    iDestruct "H" as (? (q&->)) "H".
+    iIntros "!>". iExists q. done.
+  Qed.
+
   (** * Lemmas about [ghost_map_auth] *)
   Lemma ghost_map_alloc_strong P m :
     pred_infinite P →

iris/base_logic/lib/saved_prop.v

@@ -108,6 +108,17 @@ Section saved_anything.
     iApply own_update. apply dfrac_agree_persist.
   Qed.
 
+  (** Recover fractional ownership for read-only element. *)
+  Lemma saved_anything_unpersist γ v :
+    saved_anything_own γ DfracDiscarded v ==∗ ∃ q, saved_anything_own γ (DfracOwn q) v.
+  Proof.
+    iIntros "H".
+    iMod (own_updateP with "H") as "H";
+      first by apply dfrac_agree_unpersist.
+    iDestruct "H" as (? (q&->)) "H".
+    iIntros "!>". iExists q. done.
+  Qed.
+
   (** Updates *)
   Lemma saved_anything_update y γ x :
     saved_anything_own γ (DfracOwn 1) x ==∗ saved_anything_own γ (DfracOwn 1) y.
@@ -193,6 +204,11 @@ Section saved_prop.
     saved_prop_own γ dq P ==∗ saved_prop_own γ DfracDiscarded P.
   Proof. apply saved_anything_persist. Qed.
 
+  (** Recover fractional ownership for read-only element. *)
+  Lemma saved_prop_unpersist γ v :
+    saved_prop_own γ DfracDiscarded v ==∗ ∃ q, saved_prop_own γ (DfracOwn q) v.
+  Proof. apply saved_anything_unpersist. Qed.
+
   (** Updates *)
   Lemma saved_prop_update Q γ P :
     saved_prop_own γ (DfracOwn 1) P ==∗ saved_prop_own γ (DfracOwn 1) Q.
@@ -272,6 +288,11 @@ Section saved_pred.
     saved_pred_own γ dq Φ ==∗ saved_pred_own γ DfracDiscarded Φ.
   Proof. apply saved_anything_persist. Qed.
 
+  (** Recover fractional ownership for read-only element. *)
+  Lemma saved_pred_unpersist γ Φ:
+    saved_pred_own γ DfracDiscarded Φ ==∗ ∃ q, saved_pred_own γ (DfracOwn q) Φ.
+  Proof. apply saved_anything_unpersist. Qed.
+
   (** Updates *)
   Lemma saved_pred_update Ψ γ Φ :
     saved_pred_own γ (DfracOwn 1) Φ ==∗ saved_pred_own γ (DfracOwn 1) Ψ.

iris_heap_lang/primitive_laws.v

@@ -233,6 +233,8 @@ Proof. apply pointsto_ne. Qed.
 
 Lemma pointsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
 Proof. apply pointsto_persist. Qed.
+Lemma pointsto_unpersist l v : l ↦□ v ==∗ ∃ q, l ↦{#q} v.
+Proof. apply pointsto_unpersist. Qed.
 
 Global Instance inv_pointsto_own_proper l v :
   Proper (pointwise_relation _ iff ==> (≡)) (inv_pointsto_own l v).