Exclusive typeclass for CMRA elements

algebra/cmra.v

@@ -122,6 +122,11 @@ Infix "⋅?" := opM (at level 50, left associativity) : C_scope.
 Class Persistent {A : cmraT} (x : A) := persistent : pcore x ≡ Some x.
 Arguments persistent {_} _ {_}.
 
+(** * Exclusive elements (i.e., elements that cannot have a frame). *)
+Class Exclusive {A : cmraT} (x : A) :=
+  exclusiveN_r : ∀ n y, ✓{n} (x ⋅ y) → False.
+Arguments exclusiveN_r {_} _ {_} _ _ _.
+
 (** * CMRAs whose core is total *)
 (** The function [core] may return a dummy when used on CMRAs without total
 core. *)
@@ -337,6 +342,15 @@ Qed.
 Lemma persistent_dup x `{!Persistent x} : x ≡ x ⋅ x.
 Proof. by apply cmra_pcore_dup' with x. Qed.
 
+(** ** Exclusive elements *)
+Lemma exclusiveN_l x `{!Exclusive x} :
+  ∀ (n : nat) (y : A), ✓{n} (y ⋅ x) → False.
+Proof. intros ??. rewrite comm. by apply exclusiveN_r. Qed.
+Lemma exclusive_r x `{!Exclusive x} : ∀ (y : A), ✓ (x ⋅ y) → False.
+Proof. by intros ? ?%cmra_valid_validN%(exclusiveN_r _ 0). Qed.
+Lemma exclusive_l x `{!Exclusive x} : ∀ (y : A), ✓ (y ⋅ x) → False.
+Proof. by intros ? ?%cmra_valid_validN%(exclusiveN_l _ 0). Qed.
+
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
 Proof. intros [z ->]. by exists z. Qed.
@@ -518,6 +532,10 @@ Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.
 Global Instance local_update_id : 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 ??? H ?%H. 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.
@@ -541,6 +559,9 @@ Proof.
   - 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)) →
@@ -941,6 +962,13 @@ 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).
+  Proof. by intros ??[][?%exclusiveN_r]. Qed.
+  Global Instance pair_exclusive_r x y :
+    Exclusive y → Exclusive (x,y).
+  Proof. by intros ??[][??%exclusiveN_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.

algebra/csum.v

@@ -234,6 +234,11 @@ Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
 Global Instance Cinr_persistent b : Persistent b → Persistent (Cinr b).
 Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
 
+Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a).
+Proof. by move=> H n[]? =>[/H||]. Qed.
+Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
+Proof. by move=> H n[]? =>[|/H|]. Qed.
+
 (** Internalized properties *)
 Lemma csum_equivI {M} (x y : csum A B) :
   (x ≡ y) ⊣⊢ (match x, y with

algebra/excl.v

@@ -114,16 +114,9 @@ Lemma excl_validI {M} (x : excl A) :
   ✓ x ⊣⊢ (if x is ExclBot then False else True : uPred M).
 Proof. uPred.unseal. by destruct x. Qed.
 
-(** ** Local updates *)
-Global Instance excl_local_update y :
-  LocalUpdate (λ _, True) (λ _, y).
-Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed.
-
-(** Updates *)
-Lemma excl_update a y : ✓ y → Excl a ~~> y.
-Proof. destruct y=> ? n [z|]; eauto. Qed.
-Lemma excl_updateP (P : excl A → Prop) a y : ✓ y → P y → Excl a ~~>: P.
-Proof. destruct y=> ?? n [z|]; eauto. Qed.
+(** Exclusive *)
+Global Instance excl_exclusive x : Exclusive x.
+Proof. by destruct x; intros n []. Qed.
 
 (** Option excl *)
 Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.

algebra/frac.v

@@ -143,14 +143,6 @@ Proof.
   intros [q a]; destruct 1; split; auto using cmra_discrete_valid.
 Qed.
 
-Lemma frac_validN_inv_l n x y : ✓{n} (x ⋅ y) → frac_perm x ≠ 1%Qp.
-Proof.
-  intros [Hq _] Hx; simpl in *; destruct (Qcle_not_lt _ _ Hq).
-  by rewrite Hx -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
-Qed.
-Lemma frac_valid_inv_l x y : ✓ (x ⋅ y) → frac_perm x ≠ 1%Qp.
-Proof. intros. by apply frac_validN_inv_l with 0 y, cmra_valid_validN. Qed.
-
 (** Internalized properties *)
 Lemma frac_equivI {M} (x y : frac A) :
   (x ≡ y) ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M).
@@ -159,10 +151,14 @@ Lemma frac_validI {M} (x : frac A) :
   ✓ x ⊣⊢ (■ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M).
 Proof. by uPred.unseal. Qed.
 
+(** Exclusive *)
+Global Instance frac_full_exclusive a : Exclusive (Frac 1 a).
+Proof.
+  move => ?[[??]?][/Qcle_not_lt[]]; simpl in *.
+  by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
+Qed.
+
 (** ** Local updates *)
-Global Instance frac_local_update_full p a :
-  LocalUpdate (λ x, frac_perm x = 1%Qp) (λ _, Frac p a).
-Proof. split; first by intros ???. by intros n x y ? ?%frac_validN_inv_l. Qed.
 Global Instance frac_local_update `{!LocalUpdate Lv L} :
   LocalUpdate (λ x, Lv (frac_car x)) (frac_map L).
 Proof.
@@ -171,11 +167,6 @@ Proof.
 Qed.
 
 (** Updates *)
-Lemma frac_update_full (a1 a2 : A) : ✓ a2 → Frac 1 a1 ~~> Frac 1 a2.
-Proof.
-  move=> ? n [y|]; last (intros; by apply cmra_valid_validN).
-  by intros ?%frac_validN_inv_l.
-Qed.
 Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 → Frac p a1 ~~> Frac p a2.
 Proof.
   intros Ha n mz [??]; split; first by destruct mz.

heap_lang/heap.v

@@ -89,7 +89,7 @@ Section heap.
   Proof.
     intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
     - rewrite !lookup_op !lookup_singleton.
-      by case: (h !! l)=> [x|] // /frac_valid_inv_l.
+      by case: (h !! l)=> [x|] // /Some_valid/exclusive_r.
     - by rewrite !lookup_op !lookup_singleton_ne.
   Qed.
   Hint Resolve heap_store_valid.
@@ -180,7 +180,8 @@ Section heap.
     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; naive_solver.
+    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ".
+    iPureIntro. eauto with typeclass_instances.
   Qed.
 
   Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
@@ -208,6 +209,7 @@ Section heap.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
     rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
-    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
+    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ".
+    iPureIntro.  eauto with typeclass_instances.
   Qed.
 End heap.

program_logic/boxes.v

@@ -74,7 +74,7 @@ Lemma box_own_auth_update E γ b1 b2 b3 :
 Proof.
   rewrite /box_own_prop -!own_op.
   apply own_update, prod_update; simpl; last reflexivity.
-  by apply (auth_local_update (λ _, Excl' b3)).
+  apply (auth_local_update (λ _, Excl' b3)). apply _. done.
 Qed.
 
 Lemma box_own_agree γ Q1 Q2 :