From 71c10187c9c4dc6cc8dfa7622bdf4af9678ea36d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 27 Jan 2017 16:08:05 +0100
Subject: [PATCH] Cancelable and IdFree typeclasses.

Cancelable elements are a new way of proving local updates, by
removing some cancellable element of the global state, provided that
we own it and we are willing to lose this ownership.

Identity-free elements are an auxiliary that is necessary to prove that
[Some x] is cancelable.

For technical reasons, these two notions are not defined exactly like
what one might expect, but also take into account validity. Otherwise,
an exclusive element would not be cancelable or idfree, which is
rather confusing.
---
 theories/algebra/agree.v         |  31 +++++++--
 theories/algebra/cmra.v          | 115 +++++++++++++++++++++++++++++--
 theories/algebra/csum.v          |  34 ++++++++-
 theories/algebra/frac.v          |  10 ++-
 theories/algebra/gmap.v          |  38 +++++++++-
 theories/algebra/local_updates.v |  13 ++++
 6 files changed, 224 insertions(+), 17 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 3a38ffa34..f0cd0c5bc 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -271,7 +271,7 @@ Qed.
 
 Instance: ∀ x : agree A, NonExpansive (op x).
 Proof.
-  intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=. 
+  intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=.
   rewrite !app_comm_cons. apply: list_setequiv_app.
 Qed.
 Instance: NonExpansive2 (@op (agree A) _).
@@ -353,7 +353,7 @@ Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
 
 Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
-Proof. intros a b [Hxy%list_setincl_singleton_rev _]. done. Qed. 
+Proof. intros a b [Hxy%list_setincl_singleton_rev _]. done. Qed.
 Global Instance to_agree_inj : Inj (≡) (≡) (to_agree).
 Proof.
   intros a b ?. apply equiv_dist=>n. apply to_agree_injN. by apply equiv_dist.
@@ -387,14 +387,35 @@ Proof.
   - intros Hab. rewrite Hab. eexists. symmetry. eapply agree_idemp.
 Qed.
 
-Lemma to_agree_comp_valid (a b : A) : ✓ (to_agree a ⋅ to_agree b) ↔ a ≡ b.
+Lemma to_agree_comp_validN n (a b : A) :
+  ✓{n} (to_agree a ⋅ to_agree b) ↔ a ≡{n}≡ b.
 Proof.
   split.
-  - (* TODO: can this be derived from other stuff?  Otherwise, should probably become sth. generic about list_agrees. *)
+  - (* TODO: can this be derived from other stuff?  Otherwise, should probably
+       become sth. generic about list_agrees. *)
     intros Hv. apply Hv; simpl; set_solver.
   - intros ->. rewrite agree_idemp. done.
 Qed.
 
+Lemma to_agree_comp_valid (a b : A) : ✓ (to_agree a ⋅ to_agree b) ↔ a ≡ b.
+Proof.
+  rewrite cmra_valid_validN equiv_dist. by setoid_rewrite to_agree_comp_validN.
+Qed.
+
+Global Instance agree_cancelable (x : agree A) : Cancelable x.
+Proof.
+  intros n y z Hv Heq.
+  destruct (to_agree_uninjN n x) as [x' EQx]; first by eapply cmra_validN_op_l.
+  destruct (to_agree_uninjN n y) as [y' EQy]; first by eapply cmra_validN_op_r.
+  destruct (to_agree_uninjN n z) as [z' EQz].
+  { eapply (cmra_validN_op_r n x z). by rewrite -Heq. }
+  assert (Hx'y' : x' ≡{n}≡ y').
+  { apply to_agree_comp_validN. by rewrite EQx EQy. }
+  assert (Hx'z' : x' ≡{n}≡ z').
+  { apply to_agree_comp_validN. by rewrite EQx EQz -Heq. }
+  by rewrite -EQy -EQz -Hx'y' -Hx'z'.
+Qed.
+
 (** Internalized properties *)
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
 Proof.
@@ -425,7 +446,7 @@ Section agree_map.
   Proof using Hyps.
     intros n x y Hxy.
     change (list_setequiv (dist n)(f <$> (agree_list x))(f <$> (agree_list y))).
-    eapply list_setequiv_fmap; last exact Hxy. apply _. 
+    eapply list_setequiv_fmap; last exact Hxy. apply _.
   Qed.
   Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _.
 
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3f1c99a10..c60bfe6c2 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -137,6 +137,18 @@ Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → Fal
 Arguments exclusive0_l {_} _ {_} _ _.
 Hint Mode Exclusive + ! : typeclass_instances.
 
+(** * Cancelable elements. *)
+Class Cancelable {A : cmraT} (x : A) :=
+  cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
+Arguments cancelableN {_} _ {_} _ _ _ _.
+Hint Mode Cancelable + ! : typeclass_instances.
+
+(** * Identity-free elements. *)
+Class IdFree {A : cmraT} (x : A) :=
+  id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
+Arguments id_free0_r {_} _ {_} _ _.
+Hint Mode IdFree + ! : typeclass_instances.
+
 (** * CMRAs whose core is total *)
 (** The function [core] may return a dummy when used on CMRAs without total
 core. *)
@@ -310,11 +322,11 @@ Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
 Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
 Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r x cx : pcore x = Some cx → x ⋅ cx ≡ x.
-Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed. 
+Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed. 
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
 Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed. 
+Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
 Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
@@ -526,6 +538,60 @@ Proof.
   split; first by apply cmra_included_includedN.
   intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
 Qed.
+
+(** Cancelable elements  *)
+Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
+Proof. unfold Cancelable. intros ?? EQ. by setoid_rewrite EQ. Qed.
+Lemma cancelable x `{!Cancelable x} y z :
+  ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
+Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
+Lemma discrete_cancelable x `{CMRADiscrete A}:
+  (∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
+Proof. intros ????. rewrite -!timeless_iff -cmra_discrete_valid_iff. auto. Qed.
+Global Instance cancelable_op x y :
+  Cancelable x → Cancelable y → Cancelable (x ⋅ y).
+Proof.
+  intros ???????. apply (cancelableN y), (cancelableN x).
+  - eapply cmra_validN_op_r. by rewrite assoc.
+  - by rewrite assoc.
+  - by rewrite !assoc.
+Qed.
+Global Instance exclusive_cancelable (x : A) : Exclusive x → Cancelable x.
+Proof. intros ???? []%(exclusiveN_l _ x). Qed.
+
+(** Id-free elements  *)
+Global Instance id_free_ne : Proper (dist n ==> iff) (@IdFree A).
+Proof.
+  unfold IdFree. intros ??? EQ%(dist_le _ 0); last lia.
+  split; intros ??; (rewrite -EQ || rewrite EQ); eauto.
+Qed.
+Global Instance id_free_proper : Proper (equiv ==> iff) (@IdFree A).
+Proof.
+  unfold IdFree. intros ?? EQ.
+  split; intros ??; (rewrite -EQ || rewrite EQ); eauto.
+Qed.
+Lemma id_freeN_r n n' x `{!IdFree x} y : ✓{n}x → x ⋅ y ≡{n'}≡ x → False.
+Proof. eauto using cmra_validN_le, dist_le with lia. Qed.
+Lemma id_freeN_l n n' x `{!IdFree x} y : ✓{n}x → y ⋅ x ≡{n'}≡ x → False.
+Proof. rewrite comm. eauto using id_freeN_r. Qed.
+Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
+Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
+Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
+Proof. rewrite comm. eauto using id_free_r. Qed.
+Lemma discrete_id_free x `{CMRADiscrete A}:
+  (∀ y, ✓x → x ⋅ y ≡ x → False) → IdFree x.
+Proof. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
+Global Instance id_free_op_r x y :
+  IdFree y → Cancelable x → IdFree (x ⋅ y).
+Proof.
+  intros ???? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
+  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
+Qed.
+Global Instance id_free_op_l x y :
+  IdFree x → Cancelable y → IdFree (x ⋅ y).
+Proof. intros. rewrite comm. apply _. Qed.
+Global Instance exclusive_id_free x : Exclusive x → IdFree x.
+Proof. intros ? z ? Hid. apply (exclusiveN_l 0 x z). by rewrite Hid. Qed.
 End cmra.
 
 (** * Properties about CMRAs with a unit element **)
@@ -549,6 +615,8 @@ Section ucmra.
     intros x. destruct (cmra_pcore_mono' ∅ x ∅) as (cx&->&?);
       eauto using ucmra_unit_least, (persistent (∅:A)).
   Qed.
+  Global Instance empty_cancelable : Cancelable (∅:A).
+  Proof. intros ???. by rewrite !left_id. Qed.
 End ucmra.
 Hint Immediate cmra_unit_total.
 
@@ -650,7 +718,7 @@ Instance cmra_monotone_compose {A B C : cmraT} (f : A → B) (g : B → C) :
   CMRAMonotone f → CMRAMonotone g → CMRAMonotone (g ∘ f).
 Proof.
   split.
-  - apply _. 
+  - apply _.
   - move=> n x Hx /=. by apply cmra_monotone_validN, cmra_monotone_validN.
   - move=> x y Hxy /=. by apply cmra_monotone, cmra_monotone.
 Qed.
@@ -674,7 +742,7 @@ Instance cmra_homomorphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
   CMRAHomomorphism f → CMRAHomomorphism g → CMRAHomomorphism (g ∘ f).
 Proof.
   split.
-  - apply _. 
+  - apply _.
   - move=> x y /=. rewrite -(cmra_homomorphism g).
     by apply (ne_proper _), cmra_homomorphism.
 Qed.
@@ -700,7 +768,7 @@ Structure rFunctor := RFunctor {
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
   rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
-    CMRAMonotone (rFunctor_map fg) 
+    CMRAMonotone (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mono.
 Instance: Params (@rFunctor_map) 5.
@@ -868,6 +936,8 @@ Section unit.
   Proof. done. Qed.
   Global Instance unit_persistent (x : ()) : Persistent x.
   Proof. by constructor. Qed.
+  Global Instance unit_cancelable (x : ()) : Cancelable x.
+  Proof. by constructor. Qed.
 End unit.
 
 (** ** Natural numbers *)
@@ -901,6 +971,9 @@ Section nat.
 
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. constructor; apply _ || done. Qed.
+
+  Global Instance nat_cancelable (x : nat) : Cancelable x.
+  Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
 End nat.
 
 Definition mnat := nat.
@@ -964,6 +1037,13 @@ Section positive.
 
   Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
   Proof. constructor; apply _ || done. Qed.
+  Global Instance pos_cancelable (x : positive) : Cancelable x.
+  Proof. intros ?????. by eapply Pos.add_reg_l, leibniz_equiv. Qed.
+  Global Instance pos_id_free (x : positive) : IdFree x.
+  Proof.
+    intros ???. edestruct Pos.add_no_neutral. rewrite Pos.add_comm.
+    by apply leibniz_equiv.
+  Qed.
 End positive.
 
 (** ** Product *)
@@ -1055,6 +1135,15 @@ Section prod.
   Proof. by intros ?[][?%exclusive0_l]. Qed.
   Global Instance pair_exclusive_r x y : Exclusive y → Exclusive (x,y).
   Proof. by intros ?[][??%exclusive0_l]. Qed.
+
+  Global Instance pair_cancelable x y :
+    Cancelable x → Cancelable y → Cancelable (x,y).
+  Proof. intros ???[][][][]. constructor; simpl in *; by eapply cancelableN. Qed.
+
+  Global Instance pair_id_free_l x y : IdFree x → IdFree (x,y).
+  Proof. move=>? [??] [? _] [/=? _]. eauto. Qed.
+  Global Instance pair_id_free_r x y : IdFree y → IdFree (x,y).
+  Proof. move=>? [??] [_ ?] [_ /=?]. eauto. Qed.
 End prod.
 
 Arguments prodR : clear implicits.
@@ -1259,6 +1348,20 @@ Section option.
 
   Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
   Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
+
+  Global Instance cancelable_Some x :
+    IdFree x → Cancelable x → Cancelable (Some x).
+  Proof.
+    intros Hirr ?? [y|] [z|] ? EQ; inversion_clear EQ.
+    - constructor. by apply (cancelableN x).
+    - edestruct Hirr.
+      + eapply (cmra_validN_op_l 0 x y), (cmra_validN_le n). done. lia.
+      + eapply dist_le. done. lia.
+    - edestruct Hirr.
+      + eapply (cmra_validN_le n). done. lia.
+      + eapply dist_le. done. lia.
+    - done.
+  Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 4fb69bd32..fde21171b 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -181,9 +181,21 @@ Lemma csum_included x y :
                       ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
 Proof.
   split.
-  - intros [z Hy]; destruct x as [a|b|], z as [a'|b'|]; inversion_clear Hy; auto.
-    + right; left; eexists _, _; split_and!; eauto. eexists; eauto.
-    + right; right; eexists _, _; split_and!; eauto. eexists; eauto.
+  - unfold included. intros [[a'|b'|] Hy]; destruct x as [a|b|];
+      inversion_clear Hy; eauto 10.
+  - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
+    + destruct x; exists CsumBot; constructor.
+    + exists (Cinl c); by constructor.
+    + exists (Cinr c); by constructor.
+Qed.
+
+Lemma csum_includedN n x y :
+  x ≼{n} y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼{n} a')
+                         ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼{n} b').
+Proof.
+  split.
+  - unfold includedN. intros [[a'|b'|] Hy]; destruct x as [a|b|];
+      inversion_clear Hy; eauto 10.
   - intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
     + destruct x; exists CsumBot; constructor.
     + exists (Cinl c); by constructor.
@@ -254,6 +266,22 @@ Proof. by move=> H[]? =>[/H||]. Qed.
 Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
 Proof. by move=> H[]? =>[|/H|]. Qed.
 
+Global Instance Cinl_cancelable a : Cancelable a → Cancelable (Cinl a).
+Proof.
+  move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
+  constructor. by eapply (cancelableN a).
+Qed.
+Global Instance Cinr_cancelable b : Cancelable b → Cancelable (Cinr b).
+Proof.
+  move=> ?? [y|y|] [z|z|] ? EQ //; inversion_clear EQ.
+  constructor. by eapply (cancelableN b).
+Qed.
+
+Global Instance Cinl_id_free a : IdFree a → IdFree (Cinl a).
+Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
+Global Instance Cinr_id_free b : IdFree b → IdFree (Cinr b).
+Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
+
 Global Instance Cinl_cmra_homomorphism : CMRAHomomorphism Cinl.
 Proof. split. apply _. done. Qed.
 Global Instance Cinr_cmra_homomorphism : CMRAHomomorphism Cinr.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 6ba732e05..d00e7d9c4 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -31,11 +31,19 @@ Qed.
 Canonical Structure fracR := discreteR frac frac_ra_mixin.
 End frac.
 
-(** Exclusive *)
 Global Instance frac_full_exclusive : Exclusive 1%Qp.
 Proof.
   move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
 Qed.
 
+Global Instance frac_cancelable (q : frac) : Cancelable q.
+Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+
+Global Instance frac_id_free (q : frac) : IdFree q.
+Proof.
+  intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
+  eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
+Qed.
+
 Lemma frac_op': ∀ (p q: Qp), (p ⋅ q) = (p + q)%Qp.
 Proof. done. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index bf43c4666..36bd80ee9 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -156,7 +156,7 @@ Proof.
       + intros _. by rewrite lookup_op !lookup_delete Hi.
       + by rewrite !lookup_op lookup_insert_ne // !lookup_delete_ne. }
     destruct (cmra_extend n (Some x) (m1 !! i) (m2 !! i)) as (y1&y2&?&?&?).
-    { move: Hmv=> /(_ i). by rewrite lookup_insert. } 
+    { move: Hmv=> /(_ i). by rewrite lookup_insert. }
     { move: Hm=> /(_ i). by rewrite lookup_insert lookup_op. }
     exists (partial_alter (λ _, y1) i m1'), (partial_alter (λ _, y2) i m2').
     split_and!.
@@ -288,6 +288,17 @@ Proof.
     + by rewrite lookup_op lookup_singleton_ne// lookup_partial_alter_ne// left_id.
 Qed.
 
+Global Instance singleton_cancelable i x :
+  Cancelable (Some x) → Cancelable {[ i := x ]}.
+Proof.
+  intros ???? Hv EQ j. specialize (EQ j). specialize (Hv j).
+  rewrite !lookup_op in EQ, Hv. destruct (decide (i = j)).
+  - subst. rewrite lookup_singleton in EQ, Hv.
+    by eapply cancelableN.
+  - rewrite lookup_singleton_ne // in EQ, Hv.
+    by rewrite ->!(left_id None _) in EQ.
+Qed.
+
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
   x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
 Proof.
@@ -435,7 +446,7 @@ Proof.
   - 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. 
+  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
 Qed.
 
 Lemma delete_singleton_local_update m i x `{!Exclusive x} :
@@ -444,6 +455,29 @@ Proof.
   rewrite -(delete_singleton i x).
   eapply delete_local_update; eauto using lookup_singleton.
 Qed.
+
+Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
+  m1 !! i ≡ mx → m2 !! i ≡ mx →
+  (m1, m2) ~l~> (delete i m1, delete i m2).
+Proof.
+  intros EQ1 EQ2.
+  destruct mx as [x|], (m1 !! i) as [m1i|] eqn:?, (m2 !! i) as [m2i|] eqn:?;
+    inversion_clear EQ1; inversion_clear EQ2.
+  - rewrite -{1}(insert_id m1 i m1i) // -{1}(insert_id m2 i m2i) //
+            -(insert_delete m1) -(insert_delete m2) !insert_singleton_op;
+    try by apply lookup_delete.
+    assert (m1i ≡ x) as -> by done. assert (m2i ≡ x) as -> by done.
+    apply cancel_local_update, _.
+  - rewrite !delete_notin //.
+Qed.
+
+Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :
+  m !! i ≡ Some x → (m, {[ i := x ]}) ~l~> (delete i m, ∅).
+Proof.
+  intros. rewrite -(delete_singleton i x).
+  apply (delete_local_update_cancelable m _ i (Some x));
+    [done|by rewrite lookup_singleton].
+Qed.
 End properties.
 
 (** Functor *)
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index e465e9e68..1c96c435d 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -45,6 +45,13 @@ Section updates.
     by rewrite cmra_opM_assoc.
   Qed.
 
+  Lemma cancel_local_update x y z `{!Cancelable x} :
+    (x â‹… y, x â‹… z) ~l~> (y, z).
+  Proof.
+    intros ? f ? Heq. split; first by eapply cmra_validN_op_r.
+    apply (cancelableN x); first done. by rewrite -cmra_opM_assoc.
+  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.
@@ -109,6 +116,12 @@ Section updates_unital.
     - intros Hup [z|]; simpl; [by auto|].
       rewrite -(right_id ∅ op y) -(right_id ∅ op y'). auto.
   Qed.
+
+  Lemma cancel_local_update_empty x y `{!Cancelable x} :
+    (x ⋅ y, x) ~l~> (y, ∅).
+  Proof.
+    rewrite -{2}(right_id ∅ op x). by apply cancel_local_update.
+  Qed.
 End updates_unital.
 
 (** * Product *)
-- 
GitLab