From b51af294fc64d7dff95325a1960e2cf94bb1a0da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Sep 2017 12:22:34 +0200
Subject: [PATCH] =?UTF-8?q?Use=20=CE=B5=20for=20CMRA=20unit.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For obsolete reasons, that no longer seem to apply, we used ∅ as the
unit.
---
 theories/algebra/auth.v                 |  8 ++--
 theories/algebra/cmra.v                 | 59 +++++++++++++------------
 theories/algebra/coPset.v               |  5 ++-
 theories/algebra/gmap.v                 |  6 ++-
 theories/algebra/gset.v                 | 11 ++---
 theories/algebra/iprod.v                | 18 ++++----
 theories/algebra/list.v                 | 10 ++---
 theories/algebra/local_updates.v        | 10 ++---
 theories/base_logic/derived.v           |  6 +--
 theories/base_logic/double_negation.v   |  4 +-
 theories/base_logic/lib/auth.v          |  4 +-
 theories/base_logic/lib/boxes.v         |  4 +-
 theories/base_logic/lib/na_invariants.v |  6 +--
 theories/base_logic/lib/own.v           |  8 ++--
 theories/base_logic/lib/wsat.v          |  8 ++--
 theories/base_logic/primitive.v         |  2 +-
 theories/base_logic/soundness.v         |  2 +-
 theories/heap_lang/lib/ticket_lock.v    |  8 ++--
 theories/tests/ipm_paper.v              |  2 +-
 19 files changed, 93 insertions(+), 88 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c49bfa240..0ac73f70e 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -12,7 +12,7 @@ Instance: Params (@Auth) 1.
 Instance: Params (@authoritative) 1.
 Instance: Params (@auth_own) 1.
 Notation "â—¯ a" := (Auth None a) (at level 20).
-Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
+Notation "● a" := (Auth (Excl' a) ε) (at level 20).
 
 (* COFE *)
 Section cofe.
@@ -177,7 +177,7 @@ Proof.
   - by rewrite -cmra_discrete_valid_iff.
 Qed.
 
-Instance auth_empty : Empty (auth A) := Auth ∅ ∅.
+Instance auth_empty : Unit (auth A) := Auth ε ε.
 Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
 Proof.
   split; simpl.
@@ -226,9 +226,9 @@ Proof.
   split; last done. exists bf2. by rewrite -assoc.
 Qed.
 
-Lemma auth_update_alloc a a' b' : (a,∅) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
+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'.
+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.
 
 Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index cc67b0541..49cc8080a 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -179,12 +179,13 @@ Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
 Arguments core' _ _ _ /.
 
 (** * CMRAs with a unit element *)
-(** We use the notation ∅ because for most instances (maps, sets, etc) the
-`empty' element is the unit. *)
-Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
-  mixin_ucmra_unit_valid : ✓ ∅;
-  mixin_ucmra_unit_left_id : LeftId (≡) ∅ (⋅);
-  mixin_ucmra_pcore_unit : pcore ∅ ≡ Some ∅
+Class Unit (A : Type) := ε : A.
+Arguments ε {_ _}.
+
+Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
+  mixin_ucmra_unit_valid : ✓ ε;
+  mixin_ucmra_unit_left_id : LeftId (≡) ε (⋅);
+  mixin_ucmra_pcore_unit : pcore ε ≡ Some ε
 }.
 
 Structure ucmraT := UCMRAT' {
@@ -195,7 +196,7 @@ Structure ucmraT := UCMRAT' {
   ucmra_op : Op ucmra_car;
   ucmra_valid : Valid ucmra_car;
   ucmra_validN : ValidN ucmra_car;
-  ucmra_empty : Empty ucmra_car;
+  ucmra_unit : Unit ucmra_car;
   ucmra_ofe_mixin : OfeMixin ucmra_car;
   ucmra_cmra_mixin : CMRAMixin ucmra_car;
   ucmra_mixin : UCMRAMixin ucmra_car;
@@ -215,7 +216,7 @@ Arguments ucmra_ofe_mixin : simpl never.
 Arguments ucmra_cmra_mixin : simpl never.
 Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmraT.
-Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
+Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
 Coercion ucmra_ofeC (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
 Canonical Structure ucmra_ofeC.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
@@ -226,11 +227,11 @@ Canonical Structure ucmra_cmraR.
 Section ucmra_mixin.
   Context {A : ucmraT}.
   Implicit Types x y : A.
-  Lemma ucmra_unit_valid : ✓ (∅ : A).
+  Lemma ucmra_unit_valid : ✓ (ε : A).
   Proof. apply (mixin_ucmra_unit_valid _ (ucmra_mixin A)). Qed.
-  Global Instance ucmra_unit_left_id : LeftId (≡) ∅ (@op A _).
+  Global Instance ucmra_unit_left_id : LeftId (≡) ε (@op A _).
   Proof. apply (mixin_ucmra_unit_left_id _ (ucmra_mixin A)). Qed.
-  Lemma ucmra_pcore_unit : pcore (∅:A) ≡ Some ∅.
+  Lemma ucmra_pcore_unit : pcore (ε:A) ≡ Some ε.
   Proof. apply (mixin_ucmra_pcore_unit _ (ucmra_mixin A)). Qed.
 End ucmra_mixin.
 
@@ -610,27 +611,27 @@ Section ucmra.
   Context {A : ucmraT}.
   Implicit Types x y z : A.
 
-  Lemma ucmra_unit_validN n : ✓{n} (∅:A).
+  Lemma ucmra_unit_validN n : ✓{n} (ε:A).
   Proof. apply cmra_valid_validN, ucmra_unit_valid. Qed.
-  Lemma ucmra_unit_leastN n x : ∅ ≼{n} x.
+  Lemma ucmra_unit_leastN n x : ε ≼{n} x.
   Proof. by exists x; rewrite left_id. Qed.
-  Lemma ucmra_unit_least x : ∅ ≼ x.
+  Lemma ucmra_unit_least x : ε ≼ x.
   Proof. by exists x; rewrite left_id. Qed.
-  Global Instance ucmra_unit_right_id : RightId (≡) ∅ (@op A _).
+  Global Instance ucmra_unit_right_id : RightId (≡) ε (@op A _).
   Proof. by intros x; rewrite (comm op) left_id. Qed.
-  Global Instance ucmra_unit_persistent : Persistent (∅:A).
+  Global Instance ucmra_unit_persistent : Persistent (ε:A).
   Proof. apply ucmra_pcore_unit. Qed.
 
   Global Instance cmra_unit_total : CMRATotal A.
   Proof.
-    intros x. destruct (cmra_pcore_mono' ∅ x ∅) as (cx&->&?);
-      eauto using ucmra_unit_least, (persistent (∅:A)).
+    intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
+      eauto using ucmra_unit_least, (persistent (ε:A)).
   Qed.
-  Global Instance empty_cancelable : Cancelable (∅:A).
+  Global Instance empty_cancelable : Cancelable (ε:A).
   Proof. intros ???. by rewrite !left_id. Qed.
 
   (* For big ops *)
-  Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ∅ |}.
+  Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
 End ucmra.
 
 Hint Immediate cmra_unit_total.
@@ -688,9 +689,9 @@ Section ucmra_leibniz.
   Context {A : ucmraT} `{!LeibnizEquiv A}.
   Implicit Types x y z : A.
 
-  Global Instance ucmra_unit_left_id_L : LeftId (=) ∅ (@op A _).
+  Global Instance ucmra_unit_left_id_L : LeftId (=) ε (@op A _).
   Proof. intros x. unfold_leibniz. by rewrite left_id. Qed.
-  Global Instance ucmra_unit_right_id_L : RightId (=) ∅ (@op A _).
+  Global Instance ucmra_unit_right_id_L : RightId (=) ε (@op A _).
   Proof. intros x. unfold_leibniz. by rewrite right_id. Qed.
 End ucmra_leibniz.
 
@@ -925,7 +926,7 @@ Section unit.
   Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
   Canonical Structure unitR : cmraT := CMRAT unit unit_cmra_mixin.
 
-  Instance unit_empty : Empty () := ().
+  Instance unit_unit : Unit () := ().
   Lemma unit_ucmra_mixin : UCMRAMixin ().
   Proof. done. Qed.
   Canonical Structure unitUR : ucmraT := UCMRAT unit unit_ucmra_mixin.
@@ -960,7 +961,7 @@ Section nat.
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Instance nat_empty : Empty nat := 0.
+  Instance nat_unit : Unit nat := 0.
   Lemma nat_ucmra_mixin : UCMRAMixin nat.
   Proof. split; apply _ || done. Qed.
   Canonical Structure natUR : ucmraT := UCMRAT nat nat_ucmra_mixin.
@@ -972,6 +973,7 @@ End nat.
 Definition mnat := nat.
 
 Section mnat.
+  Instance mnat_unit : Unit mnat := 0.
   Instance mnat_valid : Valid mnat := λ x, True.
   Instance mnat_validN : ValidN mnat := λ n x, True.
   Instance mnat_pcore : PCore mnat := Some.
@@ -997,7 +999,6 @@ Section mnat.
   Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Instance mnat_empty : Empty mnat := 0.
   Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
   Proof. split; apply _ || done. Qed.
   Canonical Structure mnatUR : ucmraT := UCMRAT mnat mnat_ucmra_mixin.
@@ -1140,7 +1141,7 @@ Arguments prodR : clear implicits.
 Section prod_unit.
   Context {A B : ucmraT}.
 
-  Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
+  Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
   Lemma prod_ucmra_mixin : UCMRAMixin (A * B).
   Proof.
     split.
@@ -1150,11 +1151,11 @@ Section prod_unit.
   Qed.
   Canonical Structure prodUR := UCMRAT (prod A B) prod_ucmra_mixin.
 
-  Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
+  Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ε) ⋅ (ε, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
 
   Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
-    (x, y) = (x, ∅) ⋅ (∅, y).
+    (x, y) = (x, ε) ⋅ (ε, y).
   Proof. unfold_leibniz. apply pair_split. Qed.
 End prod_unit.
 
@@ -1311,7 +1312,7 @@ Section option.
   Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
   Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
 
-  Instance option_empty : Empty (option A) := None.
+  Instance option_unit : Unit (option A) := None.
   Lemma option_ucmra_mixin : UCMRAMixin optionR.
   Proof. split. done. by intros []. done. Qed.
   Canonical Structure optionUR := UCMRAT (option A) option_ucmra_mixin.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 1f65be0b0..2de9c5067 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -12,6 +12,7 @@ Section coPset.
   Canonical Structure coPsetC := discreteC coPset.
 
   Instance coPset_valid : Valid coPset := λ _, True.
+  Instance coPset_unit : Unit coPset := (∅ : coPset).
   Instance coPset_op : Op coPset := union.
   Instance coPset_pcore : PCore coPset := Some.
 
@@ -70,13 +71,13 @@ Section coPset_disj.
 
   Instance coPset_disj_valid : Valid coPset_disj := λ X,
     match X with CoPset _ => True | CoPsetBot => False end.
-  Instance coPset_disj_empty : Empty coPset_disj := CoPset ∅.
+  Instance coPset_disj_unit : Unit coPset_disj := CoPset ∅.
   Instance coPset_disj_op : Op coPset_disj := λ X Y,
     match X, Y with
     | CoPset X, CoPset Y => if decide (X ⊥ Y) then CoPset (X ∪ Y) else CoPsetBot
     | _, _ => CoPsetBot
     end.
-  Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ∅.
+  Instance coPset_disj_pcore : PCore coPset_disj := λ _, Some ε.
 
   Ltac coPset_disj_solve :=
     repeat (simpl || case_decide);
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 7513358c6..ca815b69c 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -100,6 +100,7 @@ Section cmra.
 Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
 
+Instance gmap_unit : Unit (gmap K A) := (∅ : gmap K A).
 Instance gmap_op : Op (gmap K A) := merge op.
 Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
 Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
@@ -218,8 +219,9 @@ Lemma insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
 Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
 Proof.
-  split; [|by intros; apply insert_validN, ucmra_unit_validN].
-  by move=>/(_ i); simplify_map_eq.
+  split.
+  - move=>/(_ i); by simplify_map_eq.
+  - intros. apply insert_validN. done. apply: ucmra_unit_validN.
 Qed.
 Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
 Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 28ccc0186..029f0bfcf 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -11,6 +11,7 @@ Section gset.
   Canonical Structure gsetC := discreteC (gset K).
 
   Instance gset_valid : Valid (gset K) := λ _, True.
+  Instance gset_unit : Unit (gset K) := (∅ : gset K).
   Instance gset_op : Op (gset K) := union.
   Instance gset_pcore : PCore (gset K) := λ X, Some X.
 
@@ -82,13 +83,13 @@ Section gset_disj.
 
   Instance gset_disj_valid : Valid (gset_disj K) := λ X,
     match X with GSet _ => True | GSetBot => False end.
-  Instance gset_disj_empty : Empty (gset_disj K) := GSet ∅.
+  Instance gset_disj_unit : Unit (gset_disj K) := GSet ∅.
   Instance gset_disj_op : Op (gset_disj K) := λ X Y,
     match X, Y with
     | GSet X, GSet Y => if decide (X ⊥ Y) then GSet (X ∪ Y) else GSetBot
     | _, _ => GSetBot
     end.
-  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ∅.
+  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ε.
 
   Ltac gset_disj_solve :=
     repeat (simpl || case_decide);
@@ -183,7 +184,7 @@ Section gset_disj.
   End fresh_updates.
 
   Lemma gset_disj_dealloc_local_update X Y :
-    (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), ∅).
+    (GSet X, GSet Y) ~l~> (GSet (X ∖ Y), GSet ∅).
   Proof.
     apply local_update_total_valid=> _ _ /gset_disj_included HYX.
     rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=.
@@ -192,7 +193,7 @@ Section gset_disj.
       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,∅).
+    (GSet Z ⋅ GSet X, GSet Z) ~l~> (GSet X, GSet ∅).
   Proof.
     apply local_update_total_valid=> /gset_disj_valid_op HZX _ _.
     assert (X = (Z ∪ X) ∖ Z) as HX by set_solver.
@@ -201,7 +202,7 @@ Section gset_disj.
   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 -{2}(left_id ∅ _ (GSet Y)).
+    rewrite -{2}(left_id ε _ (GSet Y)).
     apply op_local_update_frame, gset_disj_dealloc_empty_local_update.
   Qed.
 
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 991ed5183..60fb8fea4 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -128,8 +128,8 @@ Section iprod_cmra.
   Qed.
   Canonical Structure iprodR := CMRAT (iprod B) iprod_cmra_mixin.
 
-  Instance iprod_empty : Empty (iprod B) := λ x, ∅.
-  Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl.
+  Instance iprod_unit : Unit (iprod B) := λ x, ε.
+  Definition iprod_lookup_empty x : ε x = ε := eq_refl.
 
   Lemma iprod_ucmra_mixin : UCMRAMixin (iprod B).
   Proof.
@@ -141,7 +141,7 @@ Section iprod_cmra.
   Canonical Structure iprodUR := UCMRAT (iprod B) iprod_ucmra_mixin.
 
   Global Instance iprod_empty_timeless :
-    (∀ i, Timeless (∅ : B i)) → Timeless (∅ : iprod B).
+    (∀ i, Timeless (ε : B i)) → Timeless (ε : iprod B).
   Proof. intros ? f Hf x. by apply: timeless. Qed.
 
   (** Internalized properties *)
@@ -179,7 +179,7 @@ Arguments iprodR {_ _ _} _.
 Arguments iprodUR {_ _ _} _.
 
 Definition iprod_singleton `{Finite A} {B : A → ucmraT} 
-  (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
+  (x : A) (y : B x) : iprod B := iprod_insert x y ε.
 Instance: Params (@iprod_singleton) 5.
 
 Section iprod_singleton.
@@ -195,11 +195,11 @@ Section iprod_singleton.
   Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y.
   Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
   Lemma iprod_lookup_singleton_ne x x' (y : B x) :
-    x ≠ x' → (iprod_singleton x y) x' = ∅.
+    x ≠ x' → (iprod_singleton x y) x' = ε.
   Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
 
   Global Instance iprod_singleton_timeless x (y : B x) :
-    (∀ i, Timeless (∅ : B i)) →  Timeless y → Timeless (iprod_singleton x y).
+    (∀ i, Timeless (ε : B i)) →  Timeless y → Timeless (iprod_singleton x y).
   Proof. apply _. Qed.
 
   Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
@@ -243,7 +243,7 @@ Section iprod_singleton.
   Proof. eauto using iprod_insert_update. Qed.
 
   Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
-    ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q.
+    ε ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ε ~~>: Q.
   Proof.
     intros Hx HQ; apply cmra_total_updateP.
     intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
@@ -253,10 +253,10 @@ Section iprod_singleton.
     - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
   Qed.
   Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
-    ∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
+    ε ~~>: P → ε ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
   Proof. eauto using iprod_singleton_updateP_empty. Qed.
   Lemma iprod_singleton_update_empty x (y : B x) :
-    ∅ ~~> y → ∅ ~~> iprod_singleton x y.
+    ε ~~> y → ε ~~> iprod_singleton x y.
   Proof.
     rewrite !cmra_update_updateP;
       eauto using iprod_singleton_updateP_empty with subst.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 978d1909d..7e3e8618d 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -221,7 +221,7 @@ Section cmra.
   Qed.
   Canonical Structure listR := CMRAT (list A) list_cmra_mixin.
 
-  Global Instance empty_list : Empty (list A) := [].
+  Global Instance list_unit : Unit (list A) := [].
   Definition list_ucmra_mixin : UCMRAMixin (list A).
   Proof.
     split.
@@ -254,7 +254,7 @@ Arguments listR : clear implicits.
 Arguments listUR : clear implicits.
 
 Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
-  replicate n ∅ ++ [x].
+  replicate n ε ++ [x].
 
 Section properties.
   Context {A : ucmraT}.
@@ -298,7 +298,7 @@ Section properties.
   Global Instance list_singletonM_proper i :
     Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
 
-  Lemma elem_of_list_singletonM i z x : z ∈ ({[i := x]} : list A) → z = ∅ ∨ z = x.
+  Lemma elem_of_list_singletonM i z x : z ∈ ({[i := x]} : list A) → z = ε ∨ z = x.
   Proof.
     rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
   Qed.
@@ -306,7 +306,7 @@ Section properties.
   Proof. induction i; by f_equal/=. Qed.
   Lemma list_lookup_singletonM_ne i j x :
     i ≠ j →
-    ({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ∅.
+    ({[ i := x ]} : list A) !! j = None ∨ ({[ i := x ]} : list A) !! j = Some ε.
   Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
   Lemma list_singletonM_validN n i x : ✓{n} ({[ i := x ]} : list A) ↔ ✓{n} x.
   Proof.
@@ -351,7 +351,7 @@ Section properties.
     x ~~>: P → (∀ y, P y → Q [y]) → [x] ~~>: Q.
   Proof.
     rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv.
-    destruct (Hup n (from_option id ∅ (lf !! 0))) as (y&?&Hv').
+    destruct (Hup n (from_option id ε (lf !! 0))) as (y&?&Hv').
     { move: (Hv 0). by destruct lf; rewrite /= ?right_id. }
     exists [y]; split; first by auto.
     apply list_lookup_validN=> i.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index cdb86b1aa..0884225f3 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -105,7 +105,7 @@ Section updates_unital.
     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.
+      rewrite -(right_id ε op y) -(right_id ε op y'). auto.
   Qed.
 
   Lemma local_update_unital_discrete `{!CMRADiscrete A} (x y x' y' : A) :
@@ -114,12 +114,12 @@ Section updates_unital.
     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.
+      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.
+  Lemma cancel_local_update_unit 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 *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8ec056b86..a703ad7d5 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -758,8 +758,8 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
 Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
 Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
-Lemma ownM_empty' : uPred_ownM ∅ ⊣⊢ True.
-Proof. apply (anti_symm _); first by auto. apply ownM_empty. Qed.
+Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
+Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
 Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   intros; apply (anti_symm _); first by apply:always_elim.
@@ -990,6 +990,6 @@ Global Instance uPred_except_0_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply except_0_sep. apply except_0_True. Qed.
 Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
-Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_empty'. Qed.
+Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 End derived.
 End uPred.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 72977057e..38754d614 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -307,7 +307,7 @@ Proof.
   case (decide (n' < n)).
   - intros. move: laterN_small. unseal. naive_solver.
   - intros. assert (n ≤ n'). omega. 
-    exfalso. specialize (Hupd n' ∅).
+    exfalso. specialize (Hupd n' ε).
     eapply Hdne. intros Hfal.
     eapply laterN_big; eauto. 
     unseal. rewrite right_id in Hupd *; naive_solver.
@@ -323,7 +323,7 @@ Proof.
   - rewrite /uPred_nnupd. unseal=> k P x Hx Hf1 Hf2.
     eapply Hf1. intros Hf3.
     eapply (laterN_big (S k) (S k)); eauto.
-    specialize (Hf3 (S k) (S k) ∅). rewrite right_id in Hf3 *. unseal.
+    specialize (Hf3 (S k) (S k) ε). rewrite right_id in Hf3 *. unseal.
     intros Hf3. eapply Hf3; eauto.
     intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
     unseal. 
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index f425cfd6f..a46400ae9 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -119,8 +119,8 @@ Section auth.
     iMod (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
   Qed.
 
-  Lemma auth_empty γ : (|==> auth_own γ ∅)%I.
-  Proof. by rewrite /auth_own -own_empty. Qed.
+  Lemma auth_empty γ : (|==> auth_own γ ε)%I.
+  Proof. by rewrite /auth_own -own_unit. Qed.
 
   Lemma auth_acc E γ a :
     ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t,
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 9ff7a6d4d..d41ce60ff 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -23,10 +23,10 @@ Section box_defs.
   Definition slice_name := gname.
 
   Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool))) : iProp Σ :=
-    own γ (a, (∅:option (agree (later (iPreProp Σ))))).
+    own γ (a, None).
 
   Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
-    own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
+    own γ (ε, Some (to_agree (Next (iProp_unfold P)))).
 
   Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
     (∃ b, box_own_auth γ (● Excl' b) ∗ if b then P else True)%I.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index bb351a767..2f20a514e 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -19,11 +19,11 @@ Section defs.
   Context `{invG Σ, na_invG Σ}.
 
   Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
-    own p (CoPset E, ∅).
+    own p (CoPset E, GSet ∅).
 
   Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
     (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
-          inv N (P ∗ own p (∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
+          inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
 End defs.
 
 Instance: Params (@na_inv) 3.
@@ -68,7 +68,7 @@ Section proofs.
   Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
   Proof.
     iIntros "HP".
-    iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
+    iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
       apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset))).
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 7743e5d46..4049d8dc2 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -119,7 +119,7 @@ Lemma own_alloc_strong a (G : gset gname) :
 Proof.
   intros Ha.
   rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
-  - rewrite /uPred_valid ownM_empty.
+  - rewrite /uPred_valid ownM_unit.
     eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
       naive_solver.
@@ -167,11 +167,11 @@ Arguments own_update {_ _} [_] _ _ _ _.
 Arguments own_update_2 {_ _} [_] _ _ _ _ _.
 Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
-Lemma own_empty A `{inG Σ (A:ucmraT)} γ : (|==> own γ ∅)%I.
+Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
 Proof.
-  rewrite /uPred_valid ownM_empty !own_eq /own_def.
+  rewrite /uPred_valid ownM_unit !own_eq /own_def.
   apply bupd_ownM_update, iprod_singleton_update_empty.
-  apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done.
+  apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.
 Qed.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3fc0558cb..ce126984a 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -53,7 +53,7 @@ Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
 Lemma ownE_empty : (|==> ownE ∅)%I.
-Proof. by rewrite /uPred_valid (own_empty (coPset_disjUR) enabled_name). Qed.
+Proof. by rewrite /uPred_valid (own_unit (coPset_disjUR) enabled_name). Qed.
 Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
 Lemma ownE_disjoint E1 E2 : ownE E1 ∗ ownE E2 ⊢ ⌜E1 ⊥ E2⌝.
@@ -68,7 +68,7 @@ Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
 Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
 
 Lemma ownD_empty : (|==> ownD ∅)%I.
-Proof. by rewrite /uPred_valid (own_empty (gset_disjUR positive) disabled_name). Qed.
+Proof. by rewrite /uPred_valid (own_unit (gset_disjUR positive) disabled_name). Qed.
 Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
 Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
 Lemma ownD_disjoint E1 E2 : ownD E1 ∗ ownD E2 ⊢ ⌜E1 ⊥ E2⌝.
@@ -126,7 +126,7 @@ Lemma ownI_alloc φ P :
   wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌝ ∗ wsat ∗ ownI i P.
 Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
-  iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
+  iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
   iMod (own_updateP with "[$]") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
@@ -148,7 +148,7 @@ Lemma ownI_alloc_open φ P :
   wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
 Proof.
   iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
-  iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
+  iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
   iMod (own_updateP with "[$]") as "HD".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
     intros E. destruct (Hfresh (E ∪ dom _ I))
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index ce9ac390d..c3e4052d4 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -491,7 +491,7 @@ Lemma always_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
 Proof.
   split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
 Qed.
-Lemma ownM_empty : uPred_valid (M:=M) (uPred_ownM ∅).
+Lemma ownM_unit : uPred_valid (M:=M) (uPred_ownM ε).
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
 Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
 Proof.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index 105cb7503..e2c764eee 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -12,7 +12,7 @@ Proof.
   { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
     eapply H; try unseal; by eauto using ucmra_unit_validN. }
   unseal. induction n as [|n IH]=> x Hx Hupd; auto.
-  destruct (Hupd (S n) ∅) as (x'&?&?); rewrite ?right_id; auto.
+  destruct (Hupd (S n) ε) as (x'&?&?); rewrite ?right_id; auto.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 5de499428..56c0e6706 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -43,16 +43,16 @@ Section proof.
     (∃ o n : nat,
       lo ↦ #o ∗ ln ↦ #n ∗
       own γ (● (Excl' o, GSet (seq_set 0 n))) ∗
-      ((own γ (◯ (Excl' o, ∅)) ∗ R) ∨ own γ (◯ (∅, GSet {[ o ]}))))%I.
+      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))))%I.
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     (∃ lo ln : loc,
        ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R))%I.
 
   Definition issued (γ : gname) (x : nat) : iProp Σ :=
-    own γ (◯ (∅, GSet {[ x ]}))%I.
+    own γ (◯ (ε, GSet {[ x ]}))%I.
 
-  Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
+  Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, GSet ∅)))%I.
 
   Global Instance lock_inv_ne γ lo ln :
     NonExpansive (lock_inv γ lo ln).
@@ -75,7 +75,7 @@ Section proof.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
-    iMod (own_alloc (● (Excl' 0%nat, ∅) ⋅ ◯ (Excl' 0%nat, ∅))) as (γ) "[Hγ Hγ']".
+    iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
     { by rewrite -auth_both_op. }
     iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
     { iNext. rewrite /lock_inv.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 352345458..5896d6391 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -136,7 +136,7 @@ Section M.
     end.
   Instance M_pcore : PCore M := λ x,
     Some match x with Auth j | Frag j => Frag j | _ => Bot end.
-  Instance M_empty : Empty M := Frag 0.
+  Instance M_unit : Unit M := Frag 0.
 
   Definition M_ra_mixin : RAMixin M.
   Proof.
-- 
GitLab