From 4397cde322554fced90a9038dcf45843c71fadd5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jun 2016 00:48:14 +0200
Subject: [PATCH] Move update stuff to its own file (it used to be in cmra.v).

---
 _CoqProject       |   1 +
 algebra/auth.v    |   2 +-
 algebra/cmra.v    | 207 +----------------------------------------
 algebra/csum.v    |   2 +-
 algebra/dra.v     |   2 +-
 algebra/gmap.v    |   2 +-
 algebra/iprod.v   |   2 +-
 algebra/list.v    |   2 +-
 algebra/updates.v | 232 ++++++++++++++++++++++++++++++++++++++++++++++
 9 files changed, 241 insertions(+), 211 deletions(-)
 create mode 100644 algebra/updates.v

diff --git a/_CoqProject b/_CoqProject
index 076f36f34..7aee7017a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -56,6 +56,7 @@ algebra/upred_big_op.v
 algebra/frac.v
 algebra/csum.v
 algebra/list.v
+algebra/updates.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/hoare_lifting.v
diff --git a/algebra/auth.v b/algebra/auth.v
index e974e056f..8ab3307cd 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export excl.
+From iris.algebra Require Export excl updates.
 From iris.algebra Require Import upred.
 Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index d42344ead..fbda788c4 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -217,26 +217,6 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 Arguments validN_preserving {_ _} _ {_} _ _ _.
 Arguments included_preserving {_ _} _ {_} _ _ _.
 
-(** * Local updates *)
-(** The idea is that lemams taking this class will usually have L explicit,
-    and leave Lv implicit - it will be inferred by the typeclass machinery. *)
-Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := {
-  local_update_ne n :> Proper (dist n ==> dist n) L;
-  local_updateN n x y : Lv x → ✓{n} (x ⋅ y) → L (x ⋅ y) ≡{n}≡ L x ⋅ y
-}.
-Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
-
-(** * Frame preserving updates *)
-Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
-  ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
-Instance: Params (@cmra_updateP) 1.
-Infix "~~>:" := cmra_updateP (at level 70).
-
-Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
-  ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
-Infix "~~>" := cmra_update (at level 70).
-Instance: Params (@cmra_update) 1.
-
 (** * Properties **)
 Section cmra.
 Context {A : cmraT}.
@@ -296,17 +276,6 @@ Global Instance cmra_opM_ne n : Proper (dist n ==> dist n ==> dist n) (@opM A).
 Proof. destruct 2; by cofe_subst. Qed.
 Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
 Proof. destruct 2; by setoid_subst. Qed.
-Global Instance cmra_updateP_proper :
-  Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
-Proof.
-  rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP;
-    split=> ? n mz; setoid_subst; naive_solver.
-Qed.
-Global Instance cmra_update_proper :
-  Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
-Proof.
-  rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
-Qed.
 
 (** ** Op *)
 Lemma cmra_opM_assoc x y mz : (x ⋅ y) ⋅? mz ≡ x ⋅ (y ⋅? mz).
@@ -523,104 +492,6 @@ Proof.
   split; first by apply cmra_included_includedN.
   intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
 Qed.
-
-(** ** Local updates *)
-Global Instance local_update_proper Lv (L : A → A) :
-  LocalUpdate Lv L → Proper ((≡) ==> (≡)) L.
-Proof. intros; apply (ne_proper _). Qed.
-
-Lemma local_update L `{!LocalUpdate Lv L} x y :
-  Lv x → ✓ (x ⋅ y) → L (x ⋅ y) ≡ L x ⋅ y.
-Proof.
-  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
-Qed.
-
-Global Instance op_local_update x : LocalUpdate (λ _, True) (op x).
-Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
-
-Global Instance id_local_update : LocalUpdate (λ _, True) (@id A).
-Proof. split; auto with typeclass_instances. Qed.
-
-Global Instance exclusive_local_update y :
-  LocalUpdate Exclusive (λ _, y) | 1000.
-Proof. split. apply _. by intros ?????%exclusiveN_r. Qed.
-
-(** ** Updates *)
-Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
-Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
-Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
-Proof. intros ? n mz ?; eauto. Qed.
-Lemma cmra_updateP_compose (P Q : A → Prop) x :
-  x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
-Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
-Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q.
-Proof.
-  rewrite cmra_update_updateP.
-  intros; apply cmra_updateP_compose with (y =); naive_solver.
-Qed.
-Lemma cmra_updateP_weaken (P Q : A → Prop) x :
-  x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
-Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
-Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
-Proof.
-  split.
-  - intros x. by apply cmra_update_updateP, cmra_updateP_id.
-  - intros x y z. rewrite !cmra_update_updateP.
-    eauto using cmra_updateP_compose with subst.
-Qed.
-Lemma cmra_update_exclusive `{!Exclusive x} y:
-  ✓ y → x ~~> y.
-Proof. move=>??[z|]=>[/exclusiveN_r[]|_]. by apply cmra_valid_validN. Qed.
-
-Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
-  x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
-  x1 â‹… x2 ~~>: Q.
-Proof.
-  intros Hx1 Hx2 Hy n mz ?.
-  destruct (Hx1 n (Some (x2 â‹…? mz))) as (y1&?&?).
-  { by rewrite /= -cmra_opM_assoc. }
-  destruct (Hx2 n (Some (y1 â‹…? mz))) as (y2&?&?).
-  { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. }
-  exists (y1 â‹… y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto.
-Qed.
-Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
-  x1 ~~>: P1 → x2 ~~>: P2 →
-  x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
-Proof. eauto 10 using cmra_updateP_op. Qed.
-Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2.
-Proof.
-  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
-Qed.
-
-Section total_updates.
-  Context `{CMRATotal A}.
-
-  Lemma cmra_total_updateP x (P : A → Prop) :
-    x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
-  Proof.
-    split=> Hup; [intros n z; apply (Hup n (Some z))|].
-    intros n [z|] ?; simpl; [by apply Hup|].
-    destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r.
-    eauto using cmra_validN_op_l.
-  Qed.
-  Lemma cmra_total_update x y : x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
-  Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.
-
-  Context `{CMRADiscrete A}.
-
-  Lemma cmra_discrete_updateP (x : A) (P : A → Prop) :
-    x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
-  Proof.
-    rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
-    naive_solver eauto using 0.
-  Qed.
-  Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
-    x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
-  Proof.
-    rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
-    naive_solver eauto using 0.
-  Qed.
-End total_updates.
 End cmra.
 
 (** * Properties about CMRAs with a unit element **)
@@ -646,13 +517,6 @@ Section ucmra.
     intros x. destruct (cmra_pcore_preserving' ∅ x ∅) as (cx&->&?);
       eauto using ucmra_unit_least, (persistent ∅).
   Qed.
-
-  Lemma ucmra_update_unit x : x ~~> ∅.
-  Proof.
-    apply cmra_total_update=> n z. rewrite left_id; apply cmra_validN_op_r.
-  Qed.
-  Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
-  Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed.
 End ucmra.
 Hint Immediate cmra_unit_total.
 
@@ -793,12 +657,6 @@ Section cmra_transport.
   Proof. by destruct H. Qed.
   Global Instance cmra_transport_persistent x : Persistent x → Persistent (T x).
   Proof. by destruct H. Qed.
-  Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
-    x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
-  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
-  Lemma cmra_transport_updateP' (P : A → Prop) x :
-    x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
-  Proof. eauto using cmra_transport_updateP. Qed.
 End cmra_transport.
 
 (** * Instances *)
@@ -1009,39 +867,10 @@ Section prod.
     Persistent x → Persistent y → Persistent (x,y).
   Proof. by rewrite /Persistent prod_pcore_Some'. Qed.
 
-  Global Instance pair_exclusive_l x y :
-    Exclusive x → Exclusive (x,y).
+  Global Instance pair_exclusive_l x y : Exclusive x → Exclusive (x,y).
   Proof. by intros ?[][?%exclusive0_r]. Qed.
-  Global Instance pair_exclusive_r x y :
-    Exclusive y → Exclusive (x,y).
+  Global Instance pair_exclusive_r x y : Exclusive y → Exclusive (x,y).
   Proof. by intros ?[][??%exclusive0_r]. Qed.
-
-  Lemma prod_updateP P1 P2 (Q : A * B → Prop)  x :
-    x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
-  Proof.
-    intros Hx1 Hx2 HP n mz [??]; simpl in *.
-    destruct (Hx1 n (fst <$> mz)) as (a&?&?); first by destruct mz.
-    destruct (Hx2 n (snd <$> mz)) as (b&?&?); first by destruct mz.
-    exists (a,b); repeat split; destruct mz; auto.
-  Qed.
-  Lemma prod_updateP' P1 P2 x :
-    x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
-  Proof. eauto using prod_updateP. Qed.
-  Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
-  Proof.
-    rewrite !cmra_update_updateP.
-    destruct x, y; eauto using prod_updateP with subst.
-  Qed.
-
-  Global Instance prod_local_update
-      (LA : A → A) `{!LocalUpdate LvA LA} (LB : B → B) `{!LocalUpdate LvB LB} :
-    LocalUpdate (λ x, LvA (x.1) ∧ LvB (x.2)) (prod_map LA LB).
-  Proof.
-    constructor.
-    - intros n x y [??]; constructor; simpl; by apply local_update_ne.
-    - intros n ?? [??] [??];
-        constructor; simpl in *; eapply local_updateN; eauto.
-  Qed.
 End prod.
 
 Arguments prodR : clear implicits.
@@ -1216,38 +1045,6 @@ Section option.
   Global Instance option_persistent (mx : option A) :
     (∀ x : A, Persistent x) → Persistent mx.
   Proof. intros. destruct mx; apply _. Qed.
-
-  (** Updates *)
-  Global Instance option_fmap_local_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_const_local_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.
-    intros Hx Hy; apply cmra_total_updateP=> n [y|] ?.
-    { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. }
-    destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto.
-    by exists (Some y'); auto.
-  Qed.
-  Lemma option_updateP' (P : A → Prop) x :
-    x ~~>: P → Some x ~~>: from_option P False.
-  Proof. eauto using option_updateP. Qed.
-  Lemma option_update x y : x ~~> y → Some x ~~> Some y.
-  Proof.
-    rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
-  Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/algebra/csum.v b/algebra/csum.v
index aaf319b2a..9bc08217b 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra updates.
 From iris.algebra Require Import upred.
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
diff --git a/algebra/dra.v b/algebra/dra.v
index e4e46c1eb..ce053438c 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra updates.
 
 Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 4df688a30..58749181f 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra updates.
 From iris.prelude Require Export gmap.
 From iris.algebra Require Import upred.
 
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 26cdb338f..06fc17e01 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra updates.
 From iris.algebra Require Import upred.
 From iris.prelude Require Import finite.
 
diff --git a/algebra/list.v b/algebra/list.v
index cd927b133..558e4032b 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra updates.
 From iris.prelude Require Export list.
 From iris.algebra Require Import upred.
 
diff --git a/algebra/updates.v b/algebra/updates.v
new file mode 100644
index 000000000..900c0dcd6
--- /dev/null
+++ b/algebra/updates.v
@@ -0,0 +1,232 @@
+From iris.algebra Require Export cmra.
+
+(** * Local updates *)
+(** The idea is that lemams taking this class will usually have L explicit,
+    and leave Lv implicit - it will be inferred by the typeclass machinery. *)
+Class LocalUpdate {A : cmraT} (Lv : A → Prop) (L : A → A) := {
+  local_update_ne n :> Proper (dist n ==> dist n) L;
+  local_updateN n x y : Lv x → ✓{n} (x ⋅ y) → L (x ⋅ y) ≡{n}≡ L x ⋅ y
+}.
+Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
+
+(** * Frame preserving updates *)
+Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
+  ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
+Instance: Params (@cmra_updateP) 1.
+Infix "~~>:" := cmra_updateP (at level 70).
+
+Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
+  ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
+Infix "~~>" := cmra_update (at level 70).
+Instance: Params (@cmra_update) 1.
+
+(** ** CMRAs *)
+Section cmra.
+Context {A : cmraT}.
+Implicit Types x y : A.
+
+Global Instance cmra_updateP_proper :
+  Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
+Proof.
+  rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP;
+    split=> ? n mz; setoid_subst; naive_solver.
+Qed.
+Global Instance cmra_update_proper :
+  Proper ((≡) ==> (≡) ==> iff) (@cmra_update A).
+Proof.
+  rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
+Qed.
+
+(** ** Local updates *)
+Global Instance local_update_proper (L : A → A) Lv :
+  LocalUpdate Lv L → Proper ((≡) ==> (≡)) L.
+Proof. intros; apply (ne_proper _). Qed.
+
+Lemma local_update (L : A → A) `{!LocalUpdate Lv L} x y :
+  Lv x → ✓ (x ⋅ y) → L (x ⋅ y) ≡ L x ⋅ y.
+Proof.
+  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
+Qed.
+
+Global Instance op_local_update x : LocalUpdate (λ _, True) (op x).
+Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
+
+Global Instance id_local_update : LocalUpdate (λ _, True) (@id A).
+Proof. split; auto with typeclass_instances. Qed.
+
+Global Instance exclusive_local_update y :
+  LocalUpdate Exclusive (λ _, y) | 1000.
+Proof. split. apply _. by intros ?????%exclusiveN_r. Qed.
+
+(** ** Frame preserving updates *)
+Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
+Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.
+Lemma cmra_updateP_id (P : A → Prop) x : P x → x ~~>: P.
+Proof. intros ? n mz ?; eauto. Qed.
+Lemma cmra_updateP_compose (P Q : A → Prop) x :
+  x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
+Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
+Lemma cmra_updateP_compose_l (Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q.
+Proof.
+  rewrite cmra_update_updateP.
+  intros; apply cmra_updateP_compose with (y =); naive_solver.
+Qed.
+Lemma cmra_updateP_weaken (P Q : A → Prop) x :
+  x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
+Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
+Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
+Proof.
+  split.
+  - intros x. by apply cmra_update_updateP, cmra_updateP_id.
+  - intros x y z. rewrite !cmra_update_updateP.
+    eauto using cmra_updateP_compose with subst.
+Qed.
+Lemma cmra_update_exclusive `{!Exclusive x} y:
+  ✓ y → x ~~> y.
+Proof. move=>??[z|]=>[/exclusiveN_r[]|_]. by apply cmra_valid_validN. Qed.
+
+Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
+  x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
+  x1 â‹… x2 ~~>: Q.
+Proof.
+  intros Hx1 Hx2 Hy n mz ?.
+  destruct (Hx1 n (Some (x2 â‹…? mz))) as (y1&?&?).
+  { by rewrite /= -cmra_opM_assoc. }
+  destruct (Hx2 n (Some (y1 â‹…? mz))) as (y2&?&?).
+  { by rewrite /= -cmra_opM_assoc (comm _ x2) cmra_opM_assoc. }
+  exists (y1 â‹… y2); split; last rewrite (comm _ y1) cmra_opM_assoc; auto.
+Qed.
+Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
+  x1 ~~>: P1 → x2 ~~>: P2 →
+  x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
+Proof. eauto 10 using cmra_updateP_op. Qed.
+Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2.
+Proof.
+  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
+Qed.
+
+(** ** Frame preserving updates for total CMRAs *)
+Section total_updates.
+  Context `{CMRATotal A}.
+
+  Lemma cmra_total_updateP x (P : A → Prop) :
+    x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
+  Proof.
+    split=> Hup; [intros n z; apply (Hup n (Some z))|].
+    intros n [z|] ?; simpl; [by apply Hup|].
+    destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r.
+    eauto using cmra_validN_op_l.
+  Qed.
+  Lemma cmra_total_update x y : x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
+  Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.
+
+  Context `{CMRADiscrete A}.
+
+  Lemma cmra_discrete_updateP (x : A) (P : A → Prop) :
+    x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
+  Proof.
+    rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
+    naive_solver eauto using 0.
+  Qed.
+  Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
+    x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
+  Proof.
+    rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
+    naive_solver eauto using 0.
+  Qed.
+End total_updates.
+End cmra.
+
+(** ** CMRAs with a unit *)
+Section ucmra.
+  Context {A : ucmraT}.
+  Implicit Types x y : A.
+
+  Lemma ucmra_update_unit x : x ~~> ∅.
+  Proof.
+    apply cmra_total_update=> n z. rewrite left_id; apply cmra_validN_op_r.
+  Qed.
+  Lemma ucmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
+  Proof. split; [intros; trans ∅|]; auto using ucmra_update_unit. Qed.
+End ucmra.
+
+Section cmra_transport.
+  Context {A B : cmraT} (H : A = B).
+  Notation T := (cmra_transport H).
+  Lemma cmra_transport_updateP (P : A → Prop) (Q : B → Prop) x :
+    x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
+  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.
+  Lemma cmra_transport_updateP' (P : A → Prop) x :
+    x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
+  Proof. eauto using cmra_transport_updateP. Qed.
+End cmra_transport.
+
+(** * Product *)
+Section prod.
+  Context {A B : cmraT}.
+  Implicit Types x : A * B.
+
+  Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
+    x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
+  Proof.
+    intros Hx1 Hx2 HP n mz [??]; simpl in *.
+    destruct (Hx1 n (fst <$> mz)) as (a&?&?); first by destruct mz.
+    destruct (Hx2 n (snd <$> mz)) as (b&?&?); first by destruct mz.
+    exists (a,b); repeat split; destruct mz; auto.
+  Qed.
+  Lemma prod_updateP' P1 P2 x :
+    x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
+  Proof. eauto using prod_updateP. Qed.
+  Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
+  Proof.
+    rewrite !cmra_update_updateP.
+    destruct x, y; eauto using prod_updateP with subst.
+  Qed.
+
+  Global Instance prod_local_update
+      (LA : A → A) `{!LocalUpdate LvA LA} (LB : B → B) `{!LocalUpdate LvB LB} :
+    LocalUpdate (λ x, LvA (x.1) ∧ LvB (x.2)) (prod_map LA LB).
+  Proof.
+    constructor.
+    - intros n x y [??]; constructor; simpl; by apply local_update_ne.
+    - intros n ?? [??] [??];
+        constructor; simpl in *; eapply local_updateN; eauto.
+  Qed.
+End prod.
+
+(** * Option *)
+Section option.
+  Context {A : cmraT}.
+  Implicit Types x y : A.
+
+  Global Instance option_fmap_local_update (L : A → A) 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_const_local_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.
+    intros Hx Hy; apply cmra_total_updateP=> n [y|] ?.
+    { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. }
+    destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto.
+    by exists (Some y'); auto.
+  Qed.
+  Lemma option_updateP' (P : A → Prop) x :
+    x ~~>: P → Some x ~~>: from_option P False.
+  Proof. eauto using option_updateP. Qed.
+  Lemma option_update x y : x ~~> y → Some x ~~> Some y.
+  Proof.
+    rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
+  Qed.
+End option.
-- 
GitLab