From 13e7b1b54bb2273447fe44f8af4d95fa0f9397de Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 28 Jul 2016 14:10:57 +0200
Subject: [PATCH] FP update for auth without fragment.

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

diff --git a/algebra/auth.v b/algebra/auth.v
index d9fa09e15..301268fbd 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -191,11 +191,17 @@ 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.
+Lemma auth_update_no_frag af b : ∅ ~l~> b @ Some af → ● af ~~> ● (b ⋅ af) ⋅ ◯ b.
+Proof.
+  intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ (● _)).
+  by apply auth_update.
+Qed.
 End cmra.
 
 Arguments authR : clear implicits.
-- 
GitLab