From 465dd9f45b6d39a93195a2edbab9088d715443af Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 May 2018 22:30:47 +0200
Subject: [PATCH] Some results about `frac_auth` by Danny and Ales.

---
 theories/algebra/frac_auth.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 814bf3224..d55fea490 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -105,4 +105,17 @@ Section frac_auth.
   Proof.
     intros. by apply auth_update, option_local_update, prod_local_update_2.
   Qed.
+
+  Lemma frac_auth_update_alloc q a b c :
+    (∀ n : nat, ✓{n} a → ✓{n} (c ⋅ a)) →
+    ●! a ⋅ ◯!{q} b ~~> ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b).
+  Proof. intros ?. by apply frac_auth_update, op_local_update. Qed.
+
+  Lemma frac_auth_dealloc q a b c `{!Cancelable c} :
+    ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b) ~~> ●! a ⋅ ◯!{q} b.
+  Proof.
+    apply frac_auth_update.
+    move=> n [x|] /= Hvalid Heq; split; eauto using cmra_validN_op_r.
+    eapply (cancelableN c); by rewrite ?assoc.
+  Qed.
 End frac_auth.
-- 
GitLab