From edfbdd5fd57f8e6b95f1d0517d11b989bcab6766 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Fri, 1 May 2020 09:34:21 +0200
Subject: [PATCH] Readd core_id_local_update

---
 theories/algebra/local_updates.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 78cf25133..93f185ff3 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -59,6 +59,14 @@ Section updates.
     destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
   Qed.
 
+  Lemma core_id_local_update x y z `{!CoreId y} :
+    y ≼ x → (x, z) ~l~> (x, z ⋅ y).
+  Proof.
+    intros Hincl n mf ? Heq; simpl in *; split; first done.
+    rewrite [x]core_id_extract // Heq. destruct mf as [f|]; last done.
+    simpl. rewrite -assoc [f â‹… y]comm assoc //.
+  Qed.
+
   Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
     (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
   Proof.
-- 
GitLab