Merge branch 'robbert/local_updates'

_CoqProject

@@ -78,7 +78,6 @@ program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
 program_logic/saved_prop.v
-program_logic/auth.v
 program_logic/sts.v
 program_logic/namespaces.v
 program_logic/boxes.v

algebra/auth.v

@@ -200,26 +200,20 @@ Proof. by rewrite /op /auth_op /= left_id. Qed.
 Lemma auth_auth_valid a : ✓ a → ✓ (● a).
 Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
 
-Lemma auth_update a af b :
-  a ~l~> b @ Some af → ● (a ⋅ af) ⋅ ◯ a ~~> ● (b ⋅ af) ⋅ ◯ b.
+Lemma auth_update a b a' b' :
+  (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
 Proof.
-  intros [Hab Hab']; apply cmra_total_update.
-  move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
-  move: Ha; rewrite !left_id=> Hm; split; auto.
-  exists bf2. rewrite -assoc.
-  apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
+  intros Hup; apply cmra_total_update.
+  move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *.
+  move: Ha; rewrite !left_id -assoc=> Ha.
+  destruct (Hup n (Some (bf1 ⋅ bf2))); auto.
+  split; last done. exists bf2. by rewrite -assoc.
 Qed.
 
-Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ● a ⋅ ◯ a ~~> ● b ⋅ ◯ b.
-Proof.
-  intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
-  by apply auth_update.
-Qed.
-Lemma auth_update_no_frag af b : ∅ ~l~> b @ Some af → ● af ~~> ● (b ⋅ af) ⋅ ◯ b.
-Proof.
-  intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ (● _)).
-  by apply auth_update.
-Qed.
+Lemma auth_update_alloc a a' b' : (a,∅) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
+Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
+Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',∅) → ● a ⋅ ◯ b ~~> ● a'.
+Proof. intros. rewrite -(right_id _ _ (● a')). by apply auth_update. Qed.
 End cmra.
 
 Arguments authR : clear implicits.

algebra/coPset.v

@@ -48,11 +48,11 @@ Section coPset.
   Lemma coPset_update X Y : X ~~> Y.
   Proof. done. Qed.
 
-  Lemma coPset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf.
+  Lemma coPset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
-    intros; apply local_update_total; split; [done|]; simpl.
-    intros mZ _. rewrite !coPset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
+    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
+    split. done. rewrite coPset_op_union. set_solver.
   Qed.
 End coPset.
 

algebra/csum.v

@@ -300,31 +300,22 @@ Proof. eauto using csum_updateP_l. Qed.
 Lemma csum_updateP'_r (P : B → Prop) b :
   b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
 Proof. eauto using csum_updateP_r. Qed.
-Lemma csum_local_update_l (a1 a2 : A) af :
-  (∀ af', af = Cinl <$> af' → a1 ~l~> a2 @ af') → Cinl a1 ~l~> Cinl a2 @ af.
+
+Lemma csum_local_update_l (a1 a2 a1' a2' : A) :
+  (a1,a2) ~l~> (a1',a2') → (Cinl a1,Cinl a2) ~l~> (Cinl a1',Cinl a2').
 Proof.
-  intros Ha. split; destruct af as [[af'| |]|]=>//=.
-  - by eapply (Ha (Some af')).
-  - by eapply (Ha None).
-  - destruct (Ha (Some af') (reflexivity _)) as [_ Ha'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Ha' n (Some mz)). by apply (Ha' n None).
-  - destruct (Ha None (reflexivity _)) as [_ Ha'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Ha' n (Some mz)). by apply (Ha' n None).
+  intros Hup n mf ? Ha1; simpl in *.
+  destruct (Hup n (mf ≫= maybe Cinl)); auto.
+  { by destruct mf as [[]|]; inversion_clear Ha1. }
+  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
-Lemma csum_local_update_r (b1 b2 : B) bf :
-  (∀ bf', bf = Cinr <$> bf' → b1 ~l~> b2 @ bf') → Cinr b1 ~l~> Cinr b2 @ bf.
+Lemma csum_local_update_r (b1 b2 b1' b2' : B) :
+  (b1,b2) ~l~> (b1',b2') → (Cinr b1,Cinr b2) ~l~> (Cinr b1',Cinr b2').
 Proof.
-  intros Hb. split; destruct bf as [[|bf'|]|]=>//=.
-  - by eapply (Hb (Some bf')).
-  - by eapply (Hb None).
-  - destruct (Hb (Some bf') (reflexivity _)) as [_ Hb'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Hb' n (Some mz)). by apply (Hb' n None).
-  - destruct (Hb None (reflexivity _)) as [_ Hb'].
-    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
-    by apply (Hb' n (Some mz)). by apply (Hb' n None).
+  intros Hup n mf ? Ha1; simpl in *.
+  destruct (Hup n (mf ≫= maybe Cinr)); auto.
+  { by destruct mf as [[]|]; inversion_clear Ha1. }
+  split. done. by destruct mf as [[]|]; inversion_clear Ha1; constructor.
 Qed.
 End cmra.
 

algebra/gmap.v

@@ -378,50 +378,63 @@ Section freshness.
   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.
+Lemma alloc_local_update m1 m2 i x :
+  m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
 Proof.
-  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.
-
-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.
-
-Lemma alloc_singleton_local_update m i x mf :
-  (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf.
+  rewrite cmra_valid_validN=> Hi ?.
+  apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  split; auto using insert_validN.
+  intros j; destruct (decide (i = j)) as [->|].
+  - move: (Hm j); rewrite Hi symmetry_iff dist_None lookup_op op_None=>-[_ Hj].
+    by rewrite lookup_op !lookup_insert Hj.
+  - rewrite Hm lookup_insert_ne // !lookup_op lookup_insert_ne //.
+Qed.
+
+Lemma alloc_singleton_local_update m i x :
+  m !! i = None → ✓ x → (m,∅) ~l~> (<[i:=x]>m, {[ i:=x ]}).
+Proof. apply alloc_local_update. Qed.
+
+Lemma insert_local_update m1 m2 i x y x' y' :
+  m1 !! i = Some x → m2 !! i = Some y →
+  (x, y) ~l~> (x', y') →
+  (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
 Proof.
-  rewrite lookup_opM op_None=> -[Hi Hif] ?.
-  rewrite insert_singleton_op // comm. apply alloc_local_update.
-  intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
-  - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi.
-    by apply cmra_valid_validN.
-  - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id.
+  intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
+  { move: (Hmv i). by rewrite Hi1. }
+  { move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). }
+  split; auto using insert_validN.
+  rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|].
+  - by rewrite lookup_insert lookup_op lookup_insert Some_op_opM.
+  - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne.
+Qed.
+
+Lemma singleton_local_update m i x y x' y' :
+  m !! i = Some x →
+  (x, y) ~l~> (x', y') →
+  (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
+Proof.
+  intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
+  eapply insert_local_update; eauto using lookup_insert.
 Qed.
 
-Lemma alloc_unit_singleton_local_update i x mf :
-  mf ≫= (!! i) = None → ✓ x → (∅:gmap K A) ~l~> {[ i := x ]} @ mf.
+Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
+  m2 !! i = Some x → (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
+  intros Hi. apply local_update_unital=> n mf Hmv Hm; simpl in *.
+  split; auto using delete_validN.
+  rewrite Hm=> j; destruct (decide (i = j)) as [<-|].
+  - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None.
+    apply eq_None_not_Some=> -[y Hi'].
+    move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l.
+  - by rewrite lookup_op !lookup_delete_ne // lookup_op. 
 Qed.
 
-Lemma delete_local_update m i x `{!Exclusive x} mf :
-  m !! i = Some x → m ~l~> delete i m @ mf.
+Lemma delete_singleton_local_update m i x `{!Exclusive x} :
+  (m, {[ i := x ]}) ~l~> (delete i m, ∅).
 Proof.
-  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.
+  rewrite -(delete_singleton i x).
+  eapply delete_local_update; eauto using lookup_singleton.
 Qed.
 End properties.
 

algebra/gset.v

@@ -47,16 +47,15 @@ Section gset.
   Lemma gset_update X Y : X ~~> Y.
   Proof. done. Qed.
 
-  Lemma gset_local_update X Y mXf : X ⊆ Y → X ~l~> Y @ mXf.
+  Lemma gset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
   Proof.
     intros (Z&->&?)%subseteq_disjoint_union_L.
-    intros; apply local_update_total; split; [done|]; simpl.
-    intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
+    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
+    split. done. rewrite gset_op_union. set_solver.
   Qed.
 
   Global Instance gset_persistent X : Persistent X.
   Proof. by apply persistent_total; rewrite gset_core_self. Qed.
-
 End gset.
 
 Arguments gsetR _ {_ _}.
@@ -72,6 +71,8 @@ Arguments GSetBot {_ _ _}.
 Section gset_disj.
   Context `{Countable K}.
   Arguments op _ _ !_ !_ /.
+  Arguments cmra_op _ !_ !_ /.
+  Arguments ucmra_op _ !_ !_ /.
 
   Canonical Structure gset_disjC := leibnizC (gset_disj K).
 
@@ -174,35 +175,45 @@ Section gset_disj.
     Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
   End fresh_updates.
 
-  Lemma gset_disj_dealloc_local_update X Y Xf :
-    GSet X ~l~> GSet (X ∖ Y) @ Some (GSet Xf).
+  Lemma gset_disj_dealloc_local_update X Y :
+    (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), ∅).
+  Proof.
+    apply local_update_total_valid=> _ _ /gset_disj_included HYX.
+    rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=.
+    rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done].
+    by rewrite difference_union_distr_l_L
+      difference_diag_L !left_id_L difference_disjoint_L.
+  Qed.
+  Lemma gset_disj_dealloc_empty_local_update X Z :
+    (GSet Z ⋅ GSet X, GSet Z) ~l~> (GSet X,∅).
   Proof.
-    apply local_update_total; split; simpl.
-    { rewrite !gset_disj_valid_op; set_solver. }
-    intros mZ ?%gset_disj_valid_op. rewrite gset_disj_union //.
-    destruct mZ as [[Z|]|]; simpl; try done.
-    - rewrite {1}/op {1}/cmra_op /=. destruct (decide _); simpl; try done.
-      intros [=]. do 2 f_equal. by apply union_cancel_l_L with X.
-    - intros [=]. assert (Xf = ∅) as -> by set_solver. by rewrite right_id.
+    apply local_update_total_valid=> /gset_disj_valid_op HZX _ _.
+    assert (X = (Z ∪ X) ∖ Z) as HX by set_solver.
+    rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update.
   Qed.
-  Lemma gset_disj_dealloc_empty_local_update X Xf :
-    GSet X ~l~> GSet ∅ @ Some (GSet Xf).
+  Lemma gset_disj_dealloc_op_local_update X Y Z :
+    (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y) ~l~> (GSet X,GSet Y).
   Proof.
-    rewrite -(difference_diag_L X). apply gset_disj_dealloc_local_update.
+    rewrite -{2}(left_id ∅ _ (GSet Y)).
+    apply op_local_update_frame, gset_disj_dealloc_empty_local_update.
   Qed.
 
-  Lemma gset_disj_alloc_local_update X i Xf :
-    i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
+  Lemma gset_disj_alloc_op_local_update X Y Z :
+    Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet Z ⋅ GSet X, GSet Z ⋅ GSet Y).
+  Proof.
+    intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op.
+  Qed.
+  Lemma gset_disj_alloc_local_update X Y Z :
+    Z ⊥ X → (GSet X,GSet Y) ~l~> (GSet (Z ∪ X), GSet (Z ∪ Y)).
   Proof.
-    intros ??; apply local_update_total; split; simpl.
-    - rewrite !gset_disj_valid_op; set_solver.
-    - intros mZ ?%gset_disj_valid_op HXf.
-      rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
+    intros. apply local_update_total_valid=> _ _ /gset_disj_included ?.
+    rewrite -!gset_disj_union //; last set_solver.
+    auto using gset_disj_alloc_op_local_update.
   Qed.
-  Lemma gset_disj_alloc_empty_local_update i Xf :
-    i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf).
+  Lemma gset_disj_alloc_empty_local_update X Z :
+    Z ⊥ X → (GSet X, GSet ∅) ~l~> (GSet (Z ∪ X), GSet Z).
   Proof.
-    intros. rewrite -(right_id_L _ _ {[i]}).
+    intros. rewrite -{2}(right_id_L _ union Z).
     apply gset_disj_alloc_local_update; set_solver.
   Qed.
 End gset_disj.

algebra/list.v

@@ -398,6 +398,7 @@ Section properties.
     rewrite !cmra_update_updateP=> ?; eauto using list_middle_updateP with subst.
   Qed.
 
+(* FIXME
   Lemma list_middle_local_update l1 l2 x y ml :
     x ~l~> y @ ml ≫= (!! length l1) →
     l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
@@ -421,6 +422,7 @@ Section properties.
   Lemma list_singleton_local_update i x y ml :
     x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
   Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
+*)
 End properties.
 
 (** Functor *)

algebra/local_updates.v

 From iris.algebra Require Export cmra.
 
 (** * Local updates *)
-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'
-}.
-Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
+Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
+  ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
 Instance: Params (@local_update) 1.
+Infix "~l~>" := local_update (at level 70).
 
 Section updates.
-Context {A : cmraT}.
-Implicit Types x y : A.
+  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 local_update_proper :
+    Proper ((≡) ==> (≡) ==> iff) (@local_update A).
+  Proof. unfold local_update. by repeat intro; setoid_subst. Qed.
 
-Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
-Proof.
-  split.
-  - intros x; by split.
-  - intros x1 x2 x3 [??] [??]; split; eauto.
-Qed.
+  Global Instance local_update_preorder : PreOrder (@local_update A).
+  Proof. split; unfold local_update; red; naive_solver. 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.
+  Lemma exclusive_local_update `{!Exclusive y} x x' : ✓ x' → (x,y) ~l~> (x',x').
+  Proof.
+    intros ? n mz Hxv Hx; simpl in *.
+    move: Hxv; rewrite Hx; move=> /exclusiveN_opM=> ->; split; auto.
+    by apply cmra_valid_validN.
+  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.
+  Lemma op_local_update x y z :
+    (∀ n, ✓{n} x → ✓{n} (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
+  Proof.
+    intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
+    by rewrite Hx -cmra_opM_assoc.
+  Qed.
+  Lemma op_local_update_discrete `{!CMRADiscrete A} x y z :
+    (✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
+  Proof.
+    intros; apply op_local_update=> n. by rewrite -!(cmra_discrete_valid_iff n).
+  Qed.
 
-Lemma alloc_local_update x y mz :
-  (∀ n, ✓{n} (x ⋅? mz) → ✓{n} (x ⋅ y ⋅? mz)) → x ~l~> x ⋅ y @ mz.
-Proof.
-  split; first done.
-  intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
-Qed.
+  Lemma op_local_update_frame x y x' y' yf :
+    (x,y) ~l~> (x',y') → (x,y ⋅ yf) ~l~> (x', y' ⋅ yf).
+  Proof.
+    intros Hup n mz Hxv Hx; simpl in *.
+    destruct (Hup n (Some (yf ⋅? mz))); [done|by rewrite /= -cmra_opM_assoc|].
+    by rewrite cmra_opM_assoc.
+  Qed.
 
-Lemma local_update_total `{CMRADiscrete A} x y mz :
-  x ~l~> y @ mz ↔
-    (✓ (x ⋅? mz) → ✓ (y ⋅? mz)) ∧
-    (∀ mz', ✓ (x ⋅? mz) → x ⋅? mz ≡ x ⋅? mz' → y ⋅? mz ≡ y ⋅? mz').
-Proof.
-  split.
-  - destruct 1. split; intros until 0;
-      rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto.
-  - intros [??]; split; intros until 0;
-      rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto.
-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.
+    rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
+    setoid_rewrite <-(λ n, timeless_iff n x).
+    setoid_rewrite <-(λ n, timeless_iff n x'). naive_solver eauto using 0.
+  Qed.
+
+  Lemma local_update_valid0 x y x' y' :
+    (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) →
+    (x,y) ~l~> (x',y').
+  Proof.
+    intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
+    - by apply (cmra_validN_le n); last lia.
+    - apply (cmra_validN_le n); last lia.
+      move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
+    - destruct mz as [z|].
+      + right. exists z. apply dist_le with n; auto with lia.
+      + left. apply dist_le with n; auto with lia.
+  Qed.
+  Lemma local_update_valid `{!CMRADiscrete A} x y x' y' :
+    (✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+  Proof.
+    rewrite !(cmra_discrete_valid_iff 0)
+      (cmra_discrete_included_iff 0) (timeless_iff 0).
+    apply local_update_valid0.
+  Qed.
+
+  Lemma local_update_total_valid0 `{!CMRATotal A} x y x' y' :
+    (✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+  Proof.
+    intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
+    by rewrite Hx.
+  Qed.
+  Lemma local_update_total_valid `{!CMRATotal A, !CMRADiscrete A} x y x' y' :
+    (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+  Proof.
+    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
+    apply local_update_total_valid0.
+  Qed.
 End updates.
 
+Section updates_unital.
+  Context {A : ucmraT}.
+  Implicit Types x y : A.
+
+  Lemma local_update_unital x y x' y' :
+    (x,y) ~l~> (x',y') ↔ ∀ n z,
+      ✓{n} x → x ≡{n}≡ y ⋅ z → ✓{n} x' ∧ x' ≡{n}≡ y' ⋅ z.
+  Proof.
+    split.
+    - intros Hup n z. apply (Hup _ (Some z)).
+    - intros Hup n [z|]; simpl; [by auto|].
+      rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto.
+  Qed.
+
+  Lemma local_update_unital_discrete `{!CMRADiscrete A} (x y x' y' : A) :
+    (x,y) ~l~> (x',y') ↔ ∀ z, ✓ x → x ≡ y ⋅ z → ✓ x' ∧ x' ≡ y' ⋅ z.
+  Proof.
+    rewrite local_update_discrete. split.
+    - intros Hup z. apply (Hup (Some z)).
+    - intros Hup [z|]; simpl; [by auto|].
+      rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto.
+  Qed.
+End updates_unital.
+
 (** * Product *)
-Lemma prod_local_update {A B : cmraT} (x y : A * B) mz :
-  x.1 ~l~> y.1 @ fst <$> mz → x.2 ~l~> y.2 @ snd <$> mz →
-  x ~l~> y @ mz.
+Lemma prod_local_update {A B : cmraT} (x y x' y' : A * B) :
+  (x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →
+  (x,y) ~l~> (x',y').
 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.
+  intros Hup1 Hup2 n mz [??] [??]; simpl in *.
+  destruct (Hup1 n (fst <$> mz)); [done|by destruct mz|].
+  destruct (Hup2 n (snd <$> mz)); [done|by destruct mz|].
+  by destruct mz.
 Qed.
 
+Lemma prod_local_update' {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 x2' y2' : B) :
+  (x1,y1) ~l~> (x1',y1') → (x2,y2) ~l~> (x2',y2') →
+  ((x1,x2),(y1,y2)) ~l~> ((x1',x2'),(y1',y2')).
+Proof. intros. by apply prod_local_update. Qed.
+Lemma prod_local_update_1 {A B : cmraT} (x1 y1 x1' y1' : A) (x2 y2 : B) :
+  (x1,y1) ~l~> (x1',y1') → ((x1,x2),(y1,y2)) ~l~> ((x1',x2),(y1',y2)).
+Proof. intros. by apply prod_local_update. Qed.
+Lemma prod_local_update_2 {A B : cmraT} (x1 y1 : A) (x2 y2 x2' y2' : B) :