Add general/missing lemmas about updateP

iris/algebra/updates.v

@@ -202,6 +202,27 @@ Section iso_cmra.
   Proof. eauto using iso_cmra_updateP. Qed.
 End iso_cmra.
 
+Section update_lift_cmra.
+  Context {A B : cmra}.
+  Implicit Types a : A.
+  Implicit Types b : B.
+
+  (** This lemma shows that if [f] maps non-deterministic updates from [B] to [A]
+  (i.e., [cmra_updateP] / [~~>:]), then [f] also maps deterministic updates from
+  [B] to [A] (i.e., [cmra_update] / [~~>]) *)
+  Lemma cmra_update_lift_updateP (f : B → A) b b' :
+    (∀ P, b ~~>: P → f b ~~>: λ a', ∃ b', a' = f b' ∧ P b') →
+    b ~~> b' →
+    f b ~~> f b'.
+  Proof.
+    intros Hgen Hupd.
+    eapply cmra_update_updateP, cmra_updateP_weaken.
+    { eapply Hgen, cmra_update_updateP, Hupd. }
+    naive_solver.
+  Qed.
+
+End update_lift_cmra.
+
 (** * Product *)
 Section prod.
   Context {A B : cmra}.

iris/algebra/view.v

@@ -483,14 +483,30 @@ Section cmra.
   Proof. rewrite view_both_dfrac_included. naive_solver. Qed.
 
   (** Updates *)
+
+  Lemma view_updateP a b Pab :
+    (∀ n bf, rel n a (b ⋅ bf) → ∃ a' b', Pab a' b' ∧ rel n a' (b' ⋅ bf)) →
+    ●V a ⋅ ◯V b ~~>: λ k, ∃ a' b', k = ●V a' ⋅ ◯V b' ∧ Pab a' b'.
+  Proof.
+    intros Hup; apply cmra_total_updateP=> n [[[dq ag]|] bf] [/=].
+    { by intros []%(exclusiveN_l _ _). }
+    intros _ (a0 & <-%(inj to_agree) & Hrel).
+    rewrite !left_id in Hrel. apply Hup in Hrel as (a' & b' & Hab' & Hrel).
+    eexists; split.
+    - naive_solver.
+    - split; simpl; [done|].
+      exists a'; split; [done|]. by rewrite left_id.
+  Qed.
+
   Lemma view_update a b a' b' :
     (∀ n bf, rel n a (b ⋅ bf) → rel n a' (b' ⋅ bf)) →
     ●V a ⋅ ◯V b ~~> ●V a' ⋅ ◯V b'.
   Proof.
-    intros Hup; apply cmra_total_update=> n [[[dq ag]|] bf] [/=].
-    { by intros []%(exclusiveN_l _ _). }
-    intros _ (a0 & <-%(inj to_agree) & Hrel). split; simpl; [done|].
-    exists a'; split; [done|]. revert Hrel. rewrite !left_id. apply Hup.
+    intros Hup.
+    eapply cmra_update_updateP, cmra_updateP_weaken.
+    { eapply view_updateP with (Pab := λ a b, a = a' ∧ b = b').
+      naive_solver. }
+    { naive_solver. }
   Qed.
 
   Lemma view_update_alloc a a' b' :
@@ -522,6 +538,13 @@ Section cmra.
     by apply (dfrac_discard_update dq _ (Some dq')).
   Qed.
 
+  Lemma view_updateP_frag b P :
+    (∀ a n bf, rel n a (b ⋅ bf) → ∃ b', P b' ∧ rel n a (b' ⋅ bf)) →
+    ◯V b ~~>: λ k, ∃ b', k = ◯V b' ∧ P b'.
+  Proof.
+    rewrite !cmra_total_updateP view_validN_eq=> ? n [[[dq ag]|] bf]; naive_solver.
+  Qed.
+
   Lemma view_update_frag b b' :
     (∀ a n bf, rel n a (b ⋅ bf) → rel n a (b' ⋅ bf)) →
     ◯V b ~~> ◯V b'.