From e29ce6f1ea706d0121276915cfddc04f87a961d3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 1 May 2021 10:30:09 +0200
Subject: [PATCH] make cmra_update a rewritable relation

---
 iris/algebra/lib/gmap_view.v | 9 ++++-----
 iris/algebra/updates.v       | 1 +
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index 2776c2d73..2926e636c 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -331,7 +331,7 @@ Section lemmas.
   Proof.
     intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
     { rewrite big_opM_empty left_id_L right_id. done. }
-    etrans; first by apply IH.
+    rewrite IH //.
     rewrite big_opM_insert // assoc.
     apply cmra_update_op; last done.
     rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); last done.
@@ -370,10 +370,9 @@ Section lemmas.
     gmap_view_auth 1 m â‹… gmap_view_frag k (DfracOwn 1) v ~~>
       gmap_view_auth 1 (<[k := v']> m) â‹… gmap_view_frag k (DfracOwn 1) v'.
   Proof.
-    etrans; first by eapply gmap_view_delete. etrans.
-    - eapply (gmap_view_alloc _ k (DfracOwn 1) v'); last done.
-      rewrite lookup_delete //.
-    - rewrite insert_delete. done.
+    rewrite gmap_view_delete.
+    rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
+    rewrite insert_delete //.
   Qed.
 
   Lemma gmap_view_update_big m m0 m1 :
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 75250e3e5..46f38b557 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -59,6 +59,7 @@ 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) := {}.
 
 Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
   x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
-- 
GitLab