From 9d629ec84309f35aa83c206c57e6dc645b2cb769 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 16:33:23 +0100
Subject: [PATCH] Frame preserving updates for op.

---
 modures/cmra.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/modures/cmra.v b/modures/cmra.v
index d0abf150a..4c4310475 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -327,6 +327,20 @@ Proof.
 Qed.
 Lemma ra_updateP_weaken (P Q : A → Prop) x : x ⇝: P → (∀ y, P y → Q y) → x ⇝: Q.
 Proof. eauto using ra_updateP_compose, ra_updateP_id. Qed.
+
+Lemma ra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
+  x1 ⇝: P1 → x2 ⇝: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ⇝: Q.
+Proof.
+  intros Hx1 Hx2 Hy z n ?.
+  destruct (Hx1 (x2 â‹… z) n) as (y1&?&?); first by rewrite associative.
+  destruct (Hx2 (y1 â‹… z) n) as (y2&?&?);
+    first by rewrite associative (commutative _ x2) -associative.
+  exists (y1 â‹… y2); split; last rewrite (commutative _ y1) -associative; auto.
+Qed.
+Lemma ra_update_op x1 x2 y1 y2 : x1 ⇝ y1 → x2 ⇝ y2 → x1 ⋅ x2 ⇝ y1 ⋅ y2.
+Proof.
+  rewrite !cmra_update_updateP; eauto using ra_updateP_op with congruence.
+Qed.
 End cmra.
 
 Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.
-- 
GitLab