From 40d953c6806493cd831719b4d2bbf0a74cc4f6a5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 11:35:52 +0100
Subject: [PATCH] show some more local updates for the option type

---
 theories/algebra/cmra.v          |  1 +
 theories/algebra/local_updates.v | 29 +++++++++++++++++++++++++----
 2 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index a8aeb26dc..3f02ee64c 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1257,6 +1257,7 @@ Section option.
   Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 
   Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
+  Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.
   Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
   Lemma Some_core `{CMRATotal A} a : Some (core a) = core (Some a).
   Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 267ef1883..7ea069d64 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -145,14 +145,35 @@ Lemma prod_local_update_2 {A B : cmraT} (x1 y1 : A) (x2 y2 x2' y2' : B) :
 Proof. intros. by apply prod_local_update. Qed.
 
 (** * Option *)
+(* TODO: Investigate whether we can use these in proving the very similar local
+   updates on finmaps. *)
 Lemma option_local_update {A : cmraT} (x y x' y' : A) :
   (x, y) ~l~> (x',y') →
   (Some x, Some y) ~l~> (Some x', Some y').
 Proof.
-  intros Hup n mmz Hxv Hx; simpl in *.
-  destruct (Hup n (mjoin mmz)); first done.
-  { destruct mmz as [[?|]|]; inversion_clear Hx; auto. }
-  split; first done. destruct mmz as [[?|]|]; constructor; auto.
+  intros Hup. apply local_update_unital=>n mz Hxv Hx; simpl in *.
+  destruct (Hup n mz); first done.
+  { destruct mz as [?|]; inversion_clear Hx; auto. }
+  split; first done. destruct mz as [?|]; constructor; auto.
+Qed.
+
+Lemma alloc_option_local_update {A : cmraT} (x : A) y :
+  ✓ x →
+  (None, y) ~l~> (Some x, Some x).
+Proof.
+  move=>Hx. apply local_update_unital=> n z _ /= Heq. split.
+  { rewrite Some_validN. apply cmra_valid_validN. done. }
+  destruct z as [z|]; last done. destruct y; inversion Heq.
+Qed.
+
+Lemma delete_option_local_update {A : cmraT} (x y : A) :
+  Exclusive y →
+  (Some x, Some y) ~l~> (None, None).
+Proof.
+  move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
+  destruct z as [z|]; last done. exfalso.
+  move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
+  eapply cmra_validN_le. eapply Hy. omega.
 Qed.
 
 (** * Natural numbers  *)
-- 
GitLab