Better setoid-rewriting for updates.

iris/algebra/lib/gmap_view.v

@@ -359,11 +359,9 @@ Section lemmas.
   Proof.
     induction m' as [|k v m' ? IH] using map_ind.
     { rewrite right_id_L big_opM_empty right_id //. }
-    rewrite big_opM_insert //. etrans.
-    - rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc.
-      eapply cmra_update_op; [eapply IH|reflexivity].
-    - etrans; first by eapply gmap_view_delete.
-      rewrite -delete_difference. done.
+    rewrite big_opM_insert //.
+    rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc IH gmap_view_delete.
+    rewrite -delete_difference. done.
   Qed.
 
   Lemma gmap_view_update m k v v' :
@@ -388,18 +386,16 @@ Section lemmas.
     rewrite dom_insert_L in Hdom.
     assert (k ∈ dom (gset K) m1) as Hindom by set_solver.
     apply elem_of_dom in Hindom as [v' Hlookup].
-    rewrite big_opM_insert //. etrans; last etrans.
-    - rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc.
-      eapply cmra_update_op; [eapply (IH (delete k m1))|reflexivity].
-      rewrite dom_delete_L Hdom.
-      apply not_elem_of_dom in Hnotdom. set_solver -Hdom.
-    - rewrite -assoc [_ ⋅ gmap_view_frag _ _ _]comm assoc.
-      eapply cmra_update_op; last reflexivity.
-      eapply (gmap_view_update _ _ v v').
-    - rewrite (big_opM_delete _ m1 k v') // -assoc.
-      eapply cmra_update_op; last done.
-      rewrite insert_union_r; last by rewrite lookup_delete.
-      rewrite union_delete_insert //.
+    rewrite big_opM_insert //.
+    rewrite [gmap_view_frag _ _ _ ⋅ _]comm assoc.
+    rewrite (IH (delete k m1)); last first.
+    { rewrite dom_delete_L Hdom.
+      apply not_elem_of_dom in Hnotdom. set_solver -Hdom. }
+    rewrite -assoc [_ ⋅ gmap_view_frag _ _ _]comm assoc.
+    rewrite (gmap_view_update _ _ _ v').
+    rewrite (big_opM_delete _ m1 k v') // -assoc.
+    rewrite insert_union_r; last by rewrite lookup_delete.
+    rewrite union_delete_insert //.
   Qed.
 
   Lemma gmap_view_persist k dq v :

iris/algebra/updates.v

@@ -52,6 +52,8 @@ Lemma cmra_update_exclusive `{!Exclusive x} y:
 Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
 
 (** Updates form a preorder. *)
+Global Instance cmra_update_rewrite_relation :
+  RewriteRelation (@cmra_update A) := {}.
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof.
   split.
@@ -59,7 +61,16 @@ Proof.
   - intros x y z. rewrite !cmra_update_updateP.
     eauto using cmra_updateP_compose with subst.
 Qed.
-Global Instance cmra_update_rewrite_relation : RewriteRelation (@cmra_update A) := {}.
+Global Instance cmra_update_proper_update :
+  Proper (flip cmra_update ==> cmra_update ==> impl) (@cmra_update A).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
+Qed.
+Global Instance cmra_update_flip_proper_update :
+  Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update A).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
+Qed.
 
 Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
   x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
@@ -81,6 +92,13 @@ Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
 
+Global Instance cmra_update_op_proper :
+  Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
+Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.
+Global Instance cmra_update_op_flip_proper :
+  Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
+Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.
+
 Lemma cmra_update_op_l x y : x ⋅ y ~~> x.
 Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
 Lemma cmra_update_op_r x y : x ⋅ y ~~> y.