From 61af23a790384c46323fb910fc10d2e4a09e2256 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jul 2016 00:52:59 +0200
Subject: [PATCH] FP update for auth without frame.

---
 algebra/auth.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/algebra/auth.v b/algebra/auth.v
index c473c83b6..d9fa09e15 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -183,8 +183,7 @@ Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 Lemma auth_update a af b :
-  a ~l~> b @ Some af →
-  ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
+  a ~l~> b @ Some af → ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
 Proof.
   intros [Hab Hab']; apply cmra_total_update.
   move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
@@ -192,6 +191,11 @@ Proof.
   exists bf2. rewrite -assoc.
   apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
 Qed.
+Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ● a ⋅ ◯ a ~~> ● b ⋅ ◯ b.
+Proof.
+  intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
+  by apply auth_update.
+Qed.
 End cmra.
 
 Arguments authR : clear implicits.
-- 
GitLab