Add unpersist laws for authorative parts of frag

iris/algebra/auth.v

@@ -332,6 +332,10 @@ Section auth.
   Qed.
   Lemma auth_update_auth_persist dq a : ●{dq} a ~~> ●□ a.
   Proof. apply view_update_auth_persist. Qed.
+  Lemma auth_updateP_auth_unpersist a : ●□ a ~~>: λ k, ∃ q, k = ●{#q} a.
+  Proof. apply view_updateP_auth_unpersist. Qed.
+  Lemma auth_updateP_both_unpersist a b : ●□ a ⋅ ◯ b ~~>: λ k, ∃ q, k = ●{#q} a ⋅ ◯ b.
+  Proof. apply view_updateP_both_unpersist. Qed.
 
   Lemma auth_update_dfrac_alloc dq a b `{!CoreId b} :
     b ≼ a → ●{dq} a ~~> ●{dq} a ⋅ ◯ b.

iris/algebra/lib/dfrac_agree.v

@@ -123,6 +123,14 @@ Section lemmas.
     simpl. apply dfrac_discard_update.
   Qed.
 
+  Lemma dfrac_agree_unpersist a :
+    to_dfrac_agree DfracDiscarded a ~~>: λ k, ∃ q, k = to_dfrac_agree (DfracOwn q) a.
+  Proof.
+    rewrite /to_dfrac_agree. eapply prod_updateP; first apply dfrac_undiscard_update.
+    { by eapply cmra_update_updateP. }
+    naive_solver.
+  Qed.
+
 End lemmas.
 
 Definition dfrac_agreeRF (F : oFunctor) : rFunctor :=

iris/algebra/lib/gmap_view.v

@@ -407,6 +407,10 @@ Section lemmas.
     gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
   Proof. apply view_update_auth_persist. Qed.
 
+  Lemma gmap_view_auth_unpersist m :
+    gmap_view_auth DfracDiscarded m ~~>: λ a, ∃ q, a = gmap_view_auth (DfracOwn q) m.
+  Proof. apply view_updateP_auth_unpersist. Qed.
+
   Lemma gmap_view_frag_persist k dq v :
     gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
   Proof.

iris/algebra/lib/mono_Z.v

@@ -118,6 +118,9 @@ Section mono_Z.
     eapply cmra_update_op_proper; last done.
     eapply auth_update_auth_persist.
   Qed.
+  Lemma mono_Z_auth_unpersist n :
+    ●MZ□ n ~~>: λ k, ∃ q, k = ●MZ{# q} n.
+  Proof. eapply auth_updateP_both_unpersist. Qed.
 End mono_Z.
 
 Global Typeclasses Opaque mono_Z_auth mono_Z_lb.

iris/algebra/lib/mono_list.v

@@ -178,6 +178,9 @@ Section mono_list_props.
     rewrite /mono_list_auth. apply cmra_update_op; [|done].
     by apply auth_update_auth_persist.
   Qed.
+  Lemma mono_list_auth_unpersist l :
+    ●ML□ l ~~>: λ k, ∃ q, k = ●ML{#q} l.
+  Proof. eapply auth_updateP_both_unpersist. Qed.
 End mono_list_props.
 
 Definition mono_listURF (F : oFunctor) : urFunctor :=

iris/algebra/lib/mono_nat.v

@@ -114,6 +114,9 @@ Section mono_nat.
     eapply cmra_update_op_proper; last done.
     eapply auth_update_auth_persist.
   Qed.
+  Lemma mono_nat_auth_unpersist n :
+    ●MN□ n ~~>: λ k, ∃ q, k = ●MN{# q} n.
+  Proof. eapply auth_updateP_both_unpersist. Qed.
 End mono_nat.
 
 Global Typeclasses Opaque mono_nat_auth mono_nat_lb.

iris/algebra/view.v

@@ -531,11 +531,39 @@ Section cmra.
     intros Hup. rewrite -(right_id _ _ (●V a)) -(right_id _ _ (●V a')).
     apply view_update=> n bf. rewrite !left_id. apply Hup.
   Qed.
+
+  Local Lemma view_updateP_auth_dfrac dq P a :
+    dq ~~>: P →
+    ●V{dq} a ~~>: λ k, ∃ dq', k = ●V{dq'} a ∧ P dq'.
+  Proof.
+    intros Hupd. apply cmra_total_updateP.
+    move=> n [[[dq' ag]|] bf] [Hv ?].
+    - destruct (Hupd n (Some dq') Hv) as (dr&Hdr&Heq).
+      eexists. split; first by eexists. done.
+    - destruct (Hupd n None Hv) as (dr&Hdr&Heq).
+      eexists. split; first by eexists. done.
+  Qed.
+
   Lemma view_update_auth_persist dq a : ●V{dq} a ~~> ●V□ a.
   Proof.
-    apply cmra_total_update.
-    move=> n [[[dq' ag]|] bf] [Hv ?]; last done. split; last done.
-    by apply (dfrac_discard_update dq _ (Some dq')).
+    eapply (cmra_update_lift_updateP (λ dq, view_auth dq a)).
+    { intros; by apply view_updateP_auth_dfrac. }
+    { apply dfrac_discard_update. }
+  Qed.
+  Lemma view_updateP_auth_unpersist a : ●V□ a ~~>: λ k, ∃ q, k = ●V{#q} a.
+  Proof.
+    eapply cmra_updateP_weaken.
+    { eapply view_updateP_auth_dfrac, dfrac_undiscard_update. }
+    naive_solver.
+  Qed.
+
+  Lemma view_updateP_both_unpersist a b : ●V□ a ⋅ ◯V b ~~>: λ k, ∃ q, k = ●V{#q} a ⋅ ◯V b.
+  Proof.
+    eapply cmra_updateP_weaken.
+    { eapply cmra_updateP_op'.
+      { eapply view_updateP_auth_unpersist. }
+      by eapply cmra_update_updateP. }
+    naive_solver.
   Qed.
 
   Lemma view_updateP_frag b P :