RAs with empty (global unit) element.

iris/auth.v

@@ -9,6 +9,7 @@ Arguments own {_} _.
 Notation "∘ x" := (Auth ExclUnit x) (at level 20).
 Notation "∙ x" := (Auth (Excl x) ∅) (at level 20).
 
+Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
 Instance auth_valid `{Valid A, Included A} : Valid (auth A) := λ x,
   valid (authorative x) ∧ excl_above (own x) (authorative x).
 Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
@@ -44,7 +45,9 @@ Proof.
     by apply excl_above_weaken with (own x ⋅ own y)
       (authorative x ⋅ authorative y); try apply ra_included_l.
   * split; simpl; apply ra_included_l.
-  * by intros ?? [??]; split; simpl; apply ra_op_difference.
+  * by intros ?? [??]; split; simpl; apply ra_op_minus.
 Qed.
+Instance auth_ra_empty `{RA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
+Proof. split. done. by intros x; constructor; simpl; rewrite (left_id _ _). Qed.
 Lemma auth_frag_op `{RA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b.
-Proof. done. Qed.
+Proof. done. Qed.
\ No newline at end of file

iris/cmra.v

@@ -24,7 +24,7 @@ Class CMRA A `{Equiv A, Compl A,
   cmra_unit_weaken x y : unit x ≼ unit (x ⋅ y);
   cmra_valid_op_l n x y : validN n (x ⋅ y) → validN n x;
   cmra_included_l x y : x ≼ x ⋅ y;
-  cmra_op_difference x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+  cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
 }.
 Class CMRAExtend A `{Equiv A, Dist A, Op A, ValidN A} :=
   cmra_extend_op x y1 y2 n :

iris/excl.v

@@ -4,20 +4,22 @@ Local Arguments included _ _ !_ !_ /.
 
 Inductive excl (A : Type) :=
   | Excl : A → excl A
-  | ExclUnit : excl A
+  | ExclUnit : Empty (excl A)
   | ExclBot : excl A.
 Arguments Excl {_} _.
 Arguments ExclUnit {_}.
 Arguments ExclBot {_}.
+Existing Instance ExclUnit.
 
 Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
   | Excl_equiv (x y : A) : x ≡ y → Excl x ≡ Excl y
-  | ExclUnit_equiv : ExclUnit ≡ ExclUnit
+  | ExclUnit_equiv : ∅ ≡ ∅
   | ExclBot_equiv : ExclBot ≡ ExclBot.
 Existing Instance excl_equiv.
 Instance excl_valid {A} : Valid (excl A) := λ x,
   match x with Excl _ | ExclUnit => True | ExclBot => False end.
-Instance excl_unit {A} : Unit (excl A) := λ _, ExclUnit.
+Instance excl_empty {A} : Empty (excl A) := ExclUnit.
+Instance excl_unit {A} : Unit (excl A) := λ _, ∅.
 Instance excl_op {A} : Op (excl A) := λ x y,
   match x, y with
   | Excl x, ExclUnit | ExclUnit, Excl x => Excl x
@@ -60,6 +62,8 @@ Proof.
   * by intros [?| |] [?| |]; simpl; try constructor.
   * by intros [?| |] [?| |] ?; try constructor.
 Qed.
+Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A).
+Proof. split. done. by intros []. Qed.
 Lemma excl_update {A} (x : A) y : valid y → Excl x ⇝ y.
 Proof. by destruct y; intros ? [?| |]. Qed.
 
@@ -73,4 +77,4 @@ Section excl_above.
     destruct x as [a'| |], y as [b'| |]; simpl; intros ??; try done.
     by intros Hab; rewrite Hab; transitivity b.
   Qed.
-End excl_above.
+End excl_above.
\ No newline at end of file

iris/ra.v

@@ -37,7 +37,11 @@ Class RA A `{Equiv A, Valid A, Unit A, Op A, Included A, Minus A} : Prop := {
   ra_unit_weaken x y : unit x ≼ unit (x ⋅ y);
   ra_valid_op_l x y : valid (x ⋅ y) → valid x;
   ra_included_l x y : x ≼ x ⋅ y;
-  ra_op_difference x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+  ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+}.
+Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := {
+  ra_empty_valid : valid ∅;
+  ra_empty_l :> LeftId (≡) ∅ (⋅)
 }.
 
 (** Updates *)
@@ -72,7 +76,7 @@ Proof. by rewrite (commutative _ x), ra_unit_l. Qed.
 (** ** Order *)
 Lemma ra_included_spec x y : x ≼ y ↔ ∃ z, y ≡ x ⋅ z.
 Proof.
-  split; [by exists (y ⩪ x); rewrite ra_op_difference|].
+  split; [by exists (y ⩪ x); rewrite ra_op_minus|].
   intros [z Hz]; rewrite Hz; apply ra_included_l.
 Qed.
 Global Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> iff) (≼).
@@ -106,4 +110,14 @@ Qed.
 (** ** Properties of [(⇝)] relation *)
 Global Instance ra_update_preorder : PreOrder ra_update.
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
+
+(** ** RAs with empty element *)
+Context `{Empty A, !RAEmpty A}.
+
+Global Instance ra_empty_r : RightId (≡) ∅ (⋅).
+Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed.
+Lemma ra_unit_empty x : unit ∅ ≡ ∅.
+Proof. by rewrite <-(ra_unit_l ∅) at 2; rewrite (right_id _ _). Qed.
+Lemma ra_empty_least x : ∅ ≼ x.
+Proof. by rewrite ra_included_spec; exists x; rewrite (left_id _ _). Qed.
 End ra.