Make local updates relational.

algebra/auth.v

@@ -179,42 +179,15 @@ Proof. done. Qed.
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
-Lemma auth_update a a' b b' :
-  (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
-  ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'.
+Lemma auth_update a af b :
+  a ~l~> b @ Some af →
+  ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
 Proof.
-  intros Hab; apply cmra_total_update.
+  intros [Hab Hab']; apply cmra_total_update.
   move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
-  destruct (Hab n (bf1 ⋅ bf2)) as [Ha' ?]; auto.
-  { by rewrite Ha left_id assoc. }
-  split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
-Qed.
-
-Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
-  Lv a → ✓ L a' →
-  ● a' ⋅ ◯ a ~~> ● L a' ⋅ ◯ L a.
-Proof.
-  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
-  by rewrite EQ (local_updateN L) // -EQ.
-Qed.
-
-Lemma auth_update_op_l a a' b :
-  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
-Proof. by intros; apply (auth_local_update _). Qed.
-Lemma auth_update_op_r a a' b :
-  ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b).
-Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed.
-
-(* This does not seem to follow from auth_local_update.
-   The trouble is that given ✓ (L a ⋅ a'), Lv a
-   we need ✓ (a ⋅ a'). I think this should hold for every local update,
-   but adding an extra axiom to local updates just for this is silly. *)
-Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' :
-  Lv a → ✓ (L a ⋅ a') →
-  ● (a ⋅ a') ⋅ ◯ a ~~> ● (L a ⋅ a') ⋅ ◯ L a.
-Proof.
-  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
-  by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
+  move: Ha; rewrite !left_id=> Hm; split; auto.
+  exists bf2. rewrite -assoc.
+  apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
 Qed.
 End cmra.
 

algebra/cmra.v

@@ -326,6 +326,8 @@ Lemma exclusive_l x `{!Exclusive x} y : ✓ (x ⋅ y) → False.
 Proof. by move /cmra_valid_validN /(_ 0) /exclusive0_l. Qed.
 Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
+Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
+Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed.
 
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
@@ -965,6 +967,8 @@ Section option.
   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.
+  Lemma Some_op_opM x my : Some x ⋅ my = Some (x ⋅? my).
+  Proof. by destruct my. Qed.
 
   Lemma option_included (mx my : option A) :
     mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ (x ≼ y ∨ x ≡ y).

algebra/gmap.v

@@ -184,7 +184,10 @@ Section properties.
 Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
 Implicit Types i : K.
-Implicit Types a : A.
+Implicit Types x y : A.
+
+Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
+Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
 
 Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
@@ -281,82 +284,108 @@ Proof. apply insert_updateP'. Qed.
 Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
 Proof. apply insert_update. Qed.
 
-Section freshness.
-Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
-  ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
+Lemma delete_update m i : m ~~> delete i m.
 Proof.
-  intros ? HQ. apply cmra_total_updateP.
-  intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
-  assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
-  { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
-  exists (<[i:=x]>m); split.
-  { by apply HQ; last done; apply not_elem_of_dom. }
-  rewrite insert_singleton_opN; last by apply not_elem_of_dom.
-  rewrite -assoc -insert_singleton_opN;
-    last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
-  by apply insert_validN; [apply cmra_valid_validN|].
+  apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst.
+  - move: (Hm j). rewrite !lookup_op lookup_delete left_id.
+    apply cmra_validN_op_r.
+  - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
 Qed.
-Lemma alloc_updateP (Q : gmap K A → Prop) m x :
-  ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
-Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed.
-Lemma alloc_updateP_strong' m x (I : gset K) :
-  ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
-Proof. eauto using alloc_updateP_strong. Qed.
-Lemma alloc_updateP' m x :
-  ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
-Proof. eauto using alloc_updateP. Qed.
-
-Lemma singleton_updateP_unit (P : A → Prop) (Q : gmap K A → Prop) u i :
-  ✓ u → LeftId (≡) u (⋅) →
-  u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
-Proof.
-  intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
-  destruct (Hx n (gf !! i)) as (y&?&Hy).
-  { move:(Hg i). rewrite !left_id.
-    case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
-    intros; by apply cmra_valid_validN. }
-  exists {[ i := y ]}; split; first by auto.
-  intros i'; destruct (decide (i' = i)) as [->|].
-  - rewrite lookup_op lookup_singleton.
-    move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
-  - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
-Qed.
-Lemma singleton_updateP_unit' (P: A → Prop) u i :
-  ✓ u → LeftId (≡) u (⋅) →
-  u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-Proof. eauto using singleton_updateP_unit. Qed.
-Lemma singleton_update_unit u i (y : A) :
-  ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
+
+Section freshness.
+  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
+  Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
+    ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
+  Proof.
+    intros ? HQ. apply cmra_total_updateP.
+    intros n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
+    assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
+    { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
+    exists (<[i:=x]>m); split.
+    { by apply HQ; last done; apply not_elem_of_dom. }
+    rewrite insert_singleton_opN; last by apply not_elem_of_dom.
+    rewrite -assoc -insert_singleton_opN;
+      last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
+    by apply insert_validN; [apply cmra_valid_validN|].
+  Qed.
+  Lemma alloc_updateP (Q : gmap K A → Prop) m x :
+    ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
+  Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed.
+  Lemma alloc_updateP_strong' m x (I : gset K) :
+    ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP_strong. Qed.
+  Lemma alloc_updateP' m x :
+    ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
+  Proof. eauto using alloc_updateP. Qed.
+
+  Lemma singleton_updateP_unit (P : A → Prop) (Q : gmap K A → Prop) u i :
+    ✓ u → LeftId (≡) u (⋅) →
+    u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
+  Proof.
+    intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
+    destruct (Hx n (gf !! i)) as (y&?&Hy).
+    { move:(Hg i). rewrite !left_id.
+      case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
+      intros; by apply cmra_valid_validN. }
+    exists {[ i := y ]}; split; first by auto.
+    intros i'; destruct (decide (i' = i)) as [->|].
+    - rewrite lookup_op lookup_singleton.
+      move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
+    - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
+  Qed.
+  Lemma singleton_updateP_unit' (P: A → Prop) u i :
+    ✓ u → LeftId (≡) u (⋅) →
+    u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
+  Proof. eauto using singleton_updateP_unit. Qed.
+  Lemma singleton_update_unit u i (y : A) :
+    ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
+  Proof.
+    rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
+  Qed.
+End freshness.
+
+Lemma insert_local_update m i x y mf :
+  x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf.
 Proof.
-  rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
+  intros [Hxy Hxy']; split.
+  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
+    + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy.
+    + by rewrite !lookup_opM !lookup_insert_ne.
+  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
+    destruct (decide (i = j)); subst.
+    + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'.
+    + by rewrite !lookup_opM !lookup_insert_ne.
 Qed.
-End freshness.
 
-(* Allocation is a local update: Just use composition with a singleton map. *)
+Lemma singleton_local_update i x y mf :
+  x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
+Proof. apply insert_local_update. Qed.
 
-Global Instance delete_local_update :
-  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Exclusive x) (delete i).
+Lemma alloc_singleton_local_update i x mf :
+  mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
 Proof.
-  split; first apply _.
-  intros n m1 m2 (x&Hix&Hv) Hm j; destruct (decide (i = j)) as [<-|].
-  - rewrite lookup_delete !lookup_op lookup_delete.
-    case Hiy: (m2 !! i)=> [y|]; last constructor.
-    destruct (Hv y); apply cmra_validN_le with n; last omega.
-    move: (Hm i). by rewrite lookup_op Hix Hiy.
-  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
+  intros Hi. split.
+  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
+    + intros _; rewrite !lookup_opM !lookup_insert !Some_op_opM Hi /=.
+      by apply cmra_valid_validN.
+    + by rewrite !lookup_opM !lookup_insert_ne.
+  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
+    destruct (decide (i = j)); subst.
+    + intros _. rewrite !lookup_opM !lookup_insert !Hi !lookup_empty !left_id_L.
+      by intros <-.
+    + by rewrite !lookup_opM !lookup_insert_ne.
 Qed.
 
-(* Applying a local update at a position we own is a local update. *)
-Global Instance alter_local_update `{!LocalUpdate Lv L} i :
-  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Lv x) (alter L i).
+Lemma delete_local_update m i x `{!Exclusive x} mf :
+  m !! i = Some x → m ~l~> delete i m @ mf.
 Proof.
-  split; first apply _.
-  intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
-  - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
-    move: (Hm j); rewrite lookup_op Hix.
-    case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L).
-  - by rewrite lookup_op !lookup_alter_ne // lookup_op.
+  intros Hx; split; [intros n; apply delete_update|].
+  intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
+  destruct (decide (i = j)); subst.
+  + rewrite !lookup_opM !lookup_delete Hx=> ? Hj.
+    rewrite (exclusiveN_Some_l n x (mf ≫= lookup j)) //.
+    by rewrite (exclusiveN_Some_l n x (mf' ≫= lookup j)) -?Hj.
+  + by rewrite !lookup_opM !lookup_delete_ne.
 Qed.
 End properties.
 

algebra/list.v

@@ -246,6 +246,9 @@ Section properties.
   Local Arguments op _ _ !_ !_ / : simpl nomatch.
   Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
 
+  Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)).
+  Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
+
   Lemma list_op_app l1 l2 l3 :
     length l2 ≤ length l1 → (l1 ++ l3) ⋅ l2 = (l1 ⋅ l2) ++ l3.
   Proof.
@@ -337,17 +340,25 @@ Section properties.
     rewrite !cmra_update_updateP => H; eauto using list_middle_updateP with subst.
   Qed.
 
-  (* Applying a local update at a position we own is a local update. *)
-  Global Instance list_alter_local_update `{LocalUpdate A Lv L} i :
-    LocalUpdate (λ L, ∃ x, L !! i = Some x ∧ Lv x) (alter L i).
+  Lemma list_middle_local_update l1 l2 x y ml :
+    x ~l~> y @ ml ≫= (!! length l1) →
+    l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
   Proof.
-    split; [apply _|]; intros n l1 l2 (x&Hi1&?) Hm; apply list_dist_lookup=> j.
-    destruct (decide (j = i)); subst; last first.
-    { by rewrite list_lookup_op !list_lookup_alter_ne // list_lookup_op. }
-    rewrite list_lookup_op !list_lookup_alter list_lookup_op Hi1.
-    destruct (l2 !! i) as [y|] eqn:Hi2; rewrite Hi2; constructor; auto.
-    eapply (local_updateN L), (list_lookup_validN_Some _ _ i); eauto.
-    by rewrite list_lookup_op Hi1 Hi2.
+    intros [Hxy Hxy']; split.
+    - intros n; rewrite !list_lookup_validN=> Hl i; move: (Hl i).
+      destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
+      + by rewrite !list_lookup_opM !lookup_app_l.
+      + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM; apply (Hxy n).
+      + rewrite !(cons_middle _ l1 l2) !assoc.
+        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
+    - intros n mk; rewrite !list_lookup_validN !list_dist_lookup => Hl Hl' i.
+      move: (Hl i) (Hl' i).
+      destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
+      + by rewrite !list_lookup_opM !lookup_app_l.
+      + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM !inj_iff.
+        apply (Hxy' n).
+      + rewrite !(cons_middle _ l1 l2) !assoc.
+        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
   Qed.
 End properties.
 

algebra/updates.v

 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
+Record local_update {A : cmraT} (mz : option A) (x y : A) := {
+  local_update_valid n : ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz);
+  local_update_go n mz' :
+    ✓{n} (x ⋅? mz) → x ⋅? mz ≡{n}≡ x ⋅? mz' → y ⋅? mz ≡{n}≡ y ⋅? mz'
 }.
-Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
+Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
+Instance: Params (@local_update) 1.
 
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
@@ -25,6 +25,13 @@ Section cmra.
 Context {A : cmraT}.
 Implicit Types x y : A.
 
+Global Instance local_update_proper :
+  Proper ((≡) ==> (≡) ==> (≡) ==> iff) (@local_update A).
+Proof.
+  cut (Proper ((≡) ==> (≡) ==> (≡) ==> impl) (@local_update A)).
+  { intros Hproper; split; by apply Hproper. }
+  intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto.
+Qed.
 Global Instance cmra_updateP_proper :
   Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP A).
 Proof.
@@ -38,25 +45,35 @@ Proof.
 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.
+Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
 Proof.
-  by rewrite cmra_valid_validN equiv_dist=>?? n; apply (local_updateN L).
+  split.
+  - intros x; by split.
+  - intros x1 x2 x3 [??] [??]; split; eauto.
 Qed.
 
-Global Instance op_local_update x : LocalUpdate (λ _, True) (op x).
-Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
+Lemma exclusive_local_update `{!Exclusive x} y mz : ✓ y → x ~l~> y @ mz.
+Proof.
+  split; intros n.
+  - move=> /exclusiveN_opM ->. by apply cmra_valid_validN.
+  - intros mz' ? Hmz.
+    by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz.
+Qed.
 
-Global Instance id_local_update : LocalUpdate (λ _, True) (@id A).
-Proof. split; auto with typeclass_instances. Qed.
+Lemma op_local_update x1 x2 y mz :
+  x1 ~l~> x2 @ Some (y ⋅? mz) → x1 ⋅ y ~l~> x2 ⋅ y @ mz.
+Proof.
+  intros [Hv1 H1]; split.
+  - intros n. rewrite !cmra_opM_assoc. move=> /Hv1 /=; auto.
+  - intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto.
+Qed.
 
-Global Instance exclusive_local_update y :
-  LocalUpdate Exclusive (λ _, y) | 1000.
-Proof. split. apply _. by intros ?????%exclusiveN_l. Qed.
+Lemma alloc_local_update x y mz : ✓ (x ⋅ y ⋅? mz) → x ~l~> x ⋅ y @ mz.
+Proof.
+  split.
+  - intros n _. by apply cmra_valid_validN.
+  - intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
+Qed.
 
 (** ** Frame preserving updates *)
 Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
@@ -137,19 +154,7 @@ Section total_updates.
 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.
-
+(** * Transport *)
 Section cmra_transport.
   Context {A B : cmraT} (H : A = B).
   Notation T := (cmra_transport H).
@@ -166,6 +171,17 @@ Section prod.
   Context {A B : cmraT}.
   Implicit Types x : A * B.
 
+  Lemma prod_local_update x y mz :
+    x.1 ~l~> y.1 @ fst <$> mz → x.2 ~l~> y.2 @ snd <$> mz →
+    x ~l~> y @ mz.
+  Proof.
+    intros [Hv1 H1] [Hv2 H2]; split.
+    - intros n [??]; destruct mz; split; auto.
+    - intros n mz' [??] [??].
+      specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')).
+      destruct mz, mz'; split; naive_solver.
+  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.
@@ -182,16 +198,6 @@ Section prod.
     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 *)
@@ -199,19 +205,13 @@ 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).
+  Lemma option_local_update x y mmz :
+    x ~l~> y @ mjoin mmz →
+    Some x ~l~> Some y @ mmz.
   Proof.
-    split; first apply _.
-    intros n [x|] [z|]; constructor; by eauto using (local_updateN (λ _, y)).
+    intros [Hv H]; split; first destruct mmz as [[?|]|]; auto.
+    intros n mmz'. specialize (H n (mjoin mmz')).
+    destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto.
   Qed.
 
   Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
@@ -226,7 +226,5 @@ Section option.
     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.
+  Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
 End option.

heap_lang/heap.v

@@ -77,8 +77,7 @@ Section heap.
   Lemma to_heap_insert l v σ :
     to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ).
   Proof. by rewrite /to_heap -fmap_insert. Qed.
-  Lemma of_heap_None h l :
-    ✓ h → of_heap h !! l = None → h !! l = None.
+  Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None.
   Proof.
     move=> /(_ l). rewrite /of_heap lookup_omap.
     by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto.
@@ -130,7 +129,8 @@ Section heap.
     rewrite -auth_own_op op_singleton pair_op dec_agree_ne //.
     apply (anti_symm (⊢)); last by apply const_elim_l.
     rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
-    rewrite option_validI prod_validI frac_validI discrete_valid. by apply const_elim_r.
+    rewrite option_validI prod_validI frac_validI discrete_valid.
+    by apply const_elim_r.
   Qed.
 
   Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
@@ -139,19 +139,18 @@ Section heap.
   (** Weakest precondition *)
   Lemma wp_alloc N E e v Φ :
     to_val e = Some v → nclose N ⊆ E →
-    heap_ctx N ★ ▷ (∀ l, l ↦ v -★ Φ (LitV $ LitLoc l)) ⊢ WP Alloc e @ E {{ Φ }}.
+    heap_ctx N ★ ▷ (∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
     iPvs (auth_empty heap_name) as "Hheap".
-    iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
-    iFrame "Hinv Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id.
+    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
+    iFrame "Hinv Hheap". iIntros {h}. rewrite left_id.
     iIntros "[% Hheap]". rewrite /heap_inv.
     iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
-    iIntros {l} "[% Hheap]". iExists (op {[ l := (1%Qp, DecAgree v) ]}), _, _.
-    rewrite [{[ _ := _ ]} ⋅ ∅]right_id.
+    iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
-    iFrame "Hheap". iSplit.
-    { iPureIntro; split; first done. by apply (insert_valid h). }
+    iFrame "Hheap". iSplit; first iPureIntro.
+    { by apply alloc_singleton_local_update; first apply of_heap_None. }
     iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
   Qed.
 
@@ -161,12 +160,12 @@ Section heap.
     ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
     iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
-      heap_name {[ l := (q, DecAgree v) ]}); simpl; eauto.
+    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
-    rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
-    iIntros "$"; eauto.
+    rewrite of_heap_singleton_op //. iFrame "Hl".
+    iIntros "> Hown". iExists _; iSplit; first done.
+    rewrite of_heap_singleton_op //. by iFrame.
   Qed.
 
   Lemma wp_store N E l v' e v Φ :
@@ -175,13 +174,13 @@ Section heap.
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
     iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
-    iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, (1%Qp, DecAgree v)) l) _
-      N _ heap_name {[ l := (1%Qp, DecAgree v') ]}); simpl; eauto.
+    iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
-    rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
-    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ".
-    iPureIntro. eauto 10 with typeclass_instances.
+    rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
+    iIntros "> Hown". iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
+    { iPureIntro; by apply singleton_local_update, exclusive_local_update. }
+    rewrite of_heap_singleton_op //; eauto. by iFrame.
   Qed.
 
   Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
@@ -190,12 +189,12 @@ Section heap.
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.