From 6b5909efb4b895e2949f33fc0b34204b61bbc155 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 30 May 2016 23:28:04 +0200
Subject: [PATCH] Local updates for option.

---
 algebra/cmra.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 5c8a685e9..00537cb75 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1143,6 +1143,21 @@ Section option.
   Proof. intros. destruct mx; apply _. Qed.
 
   (** Updates *)
+  Global Instance option_local_fmap_update L Lv :
+    LocalUpdate Lv L →
+    LocalUpdate (λ mx, if mx is Some x then Lv x else False) (fmap L).
+  Proof.
+    split; first apply _.
+    intros n [x|] [z|]; constructor; by eauto using (local_updateN L).
+  Qed.
+  Global Instance option_local_const_update Lv y :
+    LocalUpdate Lv (λ _, y) →
+    LocalUpdate (λ mx, if mx is Some x then Lv x else False) (λ _, Some y).
+  Proof.
+    split; first apply _.
+    intros n [x|] [z|]; constructor; by eauto using (local_updateN (λ _, y)).
+  Qed.
+
   Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
     x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
   Proof.
-- 
GitLab