From 22e1622c91257da9b219e68083c0aa76563ae492 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Jul 2019 10:44:50 +0200
Subject: [PATCH] provide a lemma to update only the authoritative part,
 ignoring the fragments entirely

---
 theories/algebra/auth.v    | 6 ++++++
 theories/algebra/updates.v | 8 +++++---
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 4e1e9ddde..646676291 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -366,6 +366,12 @@ Qed.
 Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
 Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
 
+Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a'.
+Proof.
+  intros. etrans; first exact: auth_update_alloc.
+  exact: cmra_update_op_l.
+Qed.
+
 Lemma auth_update_core_id a b `{!CoreId b} :
   b ≼ a → ● a ~~> ● a ⋅ ◯ b.
 Proof.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 790017571..4e1f96c72 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -47,6 +47,11 @@ Qed.
 Lemma cmra_updateP_weaken (P Q : A → Prop) x :
   x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
 Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
+Lemma cmra_update_exclusive `{!Exclusive x} y:
+  ✓ y → x ~~> y.
+Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
+
+(** Updates form a preorder. *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof.
   split.
@@ -54,9 +59,6 @@ Proof.
   - intros x y z. rewrite !cmra_update_updateP.
     eauto using cmra_updateP_compose with subst.
 Qed.
-Lemma cmra_update_exclusive `{!Exclusive x} y:
-  ✓ y → x ~~> y.
-Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. 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)) →
-- 
GitLab