Simplify the definition of Exclusive. Use it for gmap.

algebra/cmra.v

@@ -123,9 +123,8 @@ 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 {_} _ {_} _ _ _.
+Class Exclusive {A : cmraT} (x : A) := exclusive0_r : ∀ y, ✓{0} (x ⋅ y) → False.
+Arguments exclusive0_r {_} _ {_} _ _.
 
 (** * CMRAs whose core is total *)
 (** The function [core] may return a dummy when used on CMRAs without total
@@ -343,6 +342,9 @@ Lemma persistent_dup x `{!Persistent x} : x ≡ x ⋅ x.
 Proof. by apply cmra_pcore_dup' with x. Qed.
 
 (** ** Exclusive elements *)
+Lemma exclusiveN_r x `{!Exclusive x} :
+  ∀ (n : nat) (y : A), ✓{n} (x ⋅ y) → False.
+Proof. intros ???%cmra_validN_le%exclusive0_r; auto with arith. Qed.
 Lemma exclusiveN_l x `{!Exclusive x} :
   ∀ (n : nat) (y : A), ✓{n} (y ⋅ x) → False.
 Proof. intros ??. rewrite comm. by apply exclusiveN_r. Qed.
@@ -534,7 +536,7 @@ 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.
+Proof. split. apply _. by intros ?????%exclusiveN_r. Qed.
 
 (** ** Updates *)
 Lemma cmra_update_updateP x y : x ~~> y ↔ x ~~>: (y =).
@@ -964,10 +966,10 @@ Section prod.
 
   Global Instance pair_exclusive_l x y :
     Exclusive x → Exclusive (x,y).
-  Proof. by intros ??[][?%exclusiveN_r]. Qed.
+  Proof. by intros ?[][?%exclusive0_r]. Qed.
   Global Instance pair_exclusive_r x y :
     Exclusive y → Exclusive (x,y).
-  Proof. by intros ??[][??%exclusiveN_r]. Qed.
+  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.

algebra/csum.v

@@ -235,9 +235,9 @@ 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.
+Proof. by move=> H[]? =>[/H||]. Qed.
 Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
-Proof. by move=> H n[]? =>[|/H|]. Qed.
+Proof. by move=> H[]? =>[|/H|]. Qed.
 
 (** Internalized properties *)
 Lemma csum_equivI {M} (x y : csum A B) :

algebra/frac.v

@@ -154,7 +154,7 @@ Proof. by uPred.unseal. Qed.
 (** Exclusive *)
 Global Instance frac_full_exclusive a : Exclusive (Frac 1 a).
 Proof.
-  move => ?[[??]?][/Qcle_not_lt[]]; simpl in *.
+  move => [[??]?][/Qcle_not_lt[]]; simpl in *.
   by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
 Qed.
 

algebra/gmap.v

@@ -336,7 +336,7 @@ End freshness.
 (* Allocation is a local update: Just use composition with a singleton map. *)
 
 Global Instance gmap_delete_update :
-  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ ∀ y, ¬ ✓{0} (x ⋅ y)) (delete i).
+  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Exclusive x) (delete i).
 Proof.
   split; first apply _.
   intros n m1 m2 (x&Hix&Hv) Hm j; destruct (decide (i = j)) as [<-|].