From be858230883f44b829ea6b382305a40418375621 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Sep 2020 21:31:58 +0200
Subject: [PATCH] Add lemma `view_update_frag`.

---
 theories/algebra/view.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 24bac65b3..f18259973 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -389,12 +389,21 @@ Section cmra.
     intros Hup. rewrite -(right_id _ _ (●V a')).
     apply view_update=> n bf. rewrite left_id. apply Hup.
   Qed.
+
   Lemma view_update_auth a a' b' :
-    (∀ n bf, rel n a bf → rel n a' bf) → ●V a ~~> ●V a'.
+    (∀ n bf, rel n a bf → rel n a' bf) →
+    ●V a ~~> ●V a'.
   Proof.
     intros Hup. rewrite -(right_id _ _ (●V a)) -(right_id _ _ (●V a')).
     apply view_update=> n bf. rewrite !left_id. apply Hup.
   Qed.
+  Lemma view_update_frag b b' :
+    (∀ a n bf, rel n a (b ⋅ bf) → rel n a (b' ⋅ bf)) →
+    b ~~> b' →
+    â—¯V b ~~> â—¯V b'.
+  Proof.
+    rewrite !cmra_total_update view_validN_eq=> ?? n [[[q ag]|] bf]; naive_solver.
+  Qed.
 
   Lemma view_update_alloc_frac q a b :
     (∀ n bf, rel n a bf → rel n a (b ⋅ bf)) →
-- 
GitLab