rename CMRA identity -> CMRA unit

algebra/auth.v

@@ -156,12 +156,12 @@ Proof. uPred.unseal. by destruct x as [[]]. Qed.
 
 (** The notations ◯ and ● only work for CMRAs with an empty element. So, in
 what follows, we assume we have an empty element. *)
-Context `{Empty A, !CMRAIdentity A}.
+Context `{Empty A, !CMRAUnit A}.
 
-Global Instance auth_cmra_identity : CMRAIdentity authR.
+Global Instance auth_cmra_unit : CMRAUnit authR.
 Proof.
   split; simpl.
-  - by apply (@cmra_empty_valid A _).
+  - by apply (@cmra_unit_valid A _).
   - by intros x; constructor; rewrite /= left_id.
   - apply _.
 Qed.

algebra/cmra.v

@@ -124,15 +124,15 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
 End cmra_mixin.
 
-(** * CMRAs with a global identity element *)
+(** * CMRAs with a unit element *)
 (** We use the notation ∅ because for most instances (maps, sets, etc) the
-`empty' element is the global identity. *)
-Class CMRAIdentity (A : cmraT) `{Empty A} := {
-  cmra_empty_valid : ✓ ∅;
-  cmra_empty_left_id :> LeftId (≡) ∅ (⋅);
-  cmra_empty_timeless :> Timeless ∅
+`empty' element is the unit. *)
+Class CMRAUnit (A : cmraT) `{Empty A} := {
+  cmra_unit_valid : ✓ ∅;
+  cmra_unit_left_id :> LeftId (≡) ∅ (⋅);
+  cmra_unit_timeless :> Timeless ∅
 }.
-Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅.
+Instance cmra_unit_inhabited `{CMRAUnit A} : Inhabited A := populate ∅.
 
 (** * Discrete CMRAs *)
 Class CMRADiscrete (A : cmraT) := {
@@ -347,20 +347,20 @@ Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
   (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
 Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
 
-(** ** RAs with an empty element *)
-Section identity.
-  Context `{Empty A, !CMRAIdentity A}.
-  Lemma cmra_empty_validN n : ✓{n} ∅.
-  Proof. apply cmra_valid_validN, cmra_empty_valid. Qed.
-  Lemma cmra_empty_leastN n x : ∅ ≼{n} x.
+(** ** RAs with a unit element *)
+Section unit.
+  Context `{Empty A, !CMRAUnit A}.
+  Lemma cmra_unit_validN n : ✓{n} ∅.
+  Proof. apply cmra_valid_validN, cmra_unit_valid. Qed.
+  Lemma cmra_unit_leastN n x : ∅ ≼{n} x.
   Proof. by exists x; rewrite left_id. Qed.
-  Lemma cmra_empty_least x : ∅ ≼ x.
+  Lemma cmra_unit_least x : ∅ ≼ x.
   Proof. by exists x; rewrite left_id. Qed.
-  Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅).
+  Global Instance cmra_unit_right_id : RightId (≡) ∅ (⋅).
   Proof. by intros x; rewrite (comm op) left_id. Qed.
-  Lemma cmra_core_empty : core ∅ ≡ ∅.
+  Lemma cmra_core_unit : core ∅ ≡ ∅.
   Proof. by rewrite -{2}(cmra_core_l ∅) right_id. Qed.
-End identity.
+End unit.
 
 (** ** Local updates *)
 Global Instance local_update_proper Lv (L : A → A) :
@@ -422,13 +422,13 @@ Qed.
 Lemma cmra_update_id x : x ~~> x.
 Proof. intro. auto. Qed.
 
-Section identity_updates.
-  Context `{Empty A, !CMRAIdentity A}.
-  Lemma cmra_update_empty x : x ~~> ∅.
+Section unit_updates.
+  Context `{Empty A, !CMRAUnit A}.
+  Lemma cmra_update_unit x : x ~~> ∅.
   Proof. intros n z; rewrite left_id; apply cmra_validN_op_r. Qed.
-  Lemma cmra_update_empty_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
-  Proof. split; [intros; trans ∅|]; auto using cmra_update_empty. Qed.
-End identity_updates.
+  Lemma cmra_update_unit_alt y : ∅ ~~> y ↔ ∀ x, x ~~> y.
+  Proof. split; [intros; trans ∅|]; auto using cmra_update_unit. Qed.
+End unit_updates.
 End cmra.
 
 (** * Properties about monotone functions *)
@@ -531,7 +531,7 @@ Section unit.
   Proof. by split. Qed.
   Canonical Structure unitR : cmraT :=
     Eval cbv [unitC discreteR cofe_car] in discreteR unit_ra.
-  Global Instance unit_cmra_identity : CMRAIdentity unitR.
+  Global Instance unit_cmra_unit : CMRAUnit unitR.
   Global Instance unit_cmra_discrete : CMRADiscrete unitR.
   Proof. by apply discrete_cmra_discrete. Qed.
 End unit.
@@ -582,11 +582,11 @@ Section prod.
       by exists ((z1.1,z2.1),(z1.2,z2.2)).
   Qed.
   Canonical Structure prodR : cmraT := CMRAT prod_cofe_mixin prod_cmra_mixin.
-  Global Instance prod_cmra_identity `{Empty A, Empty B} :
-    CMRAIdentity A → CMRAIdentity B → CMRAIdentity prodR.
+  Global Instance prod_cmra_unit `{Empty A, Empty B} :
+    CMRAUnit A → CMRAUnit B → CMRAUnit prodR.
   Proof.
     split.
-    - split; apply cmra_empty_valid.
+    - split; apply cmra_unit_valid.
     - by split; rewrite /=left_id.
     - by intros ? [??]; split; apply (timeless _).
   Qed.

algebra/cmra_big_op.v

@@ -11,7 +11,7 @@ Instance: Params (@big_opM) 5.
 
 (** * Properties about big ops *)
 Section big_op.
-Context `{CMRAIdentity A}.
+Context `{CMRAUnit A}.
 
 (** * Big ops *)
 Lemma big_op_nil : big_op (@nil A) = ∅.

algebra/cmra_tactics.v

@@ -3,7 +3,7 @@ From algebra Require Import cmra_big_op.
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
-  Context `{CMRAIdentity A}.
+  Context `{CMRAUnit A}.
 
   Inductive expr :=
     | EVar : nat → expr

algebra/excl.v

@@ -128,7 +128,7 @@ Proof.
       end; destruct y1, y2; inversion_clear Hx; repeat constructor.
 Qed.
 Canonical Structure exclR : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
-Global Instance excl_cmra_identity : CMRAIdentity exclR.
+Global Instance excl_cmra_unit : CMRAUnit exclR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
 Proof. split. apply _. by intros []. Qed.

algebra/fin_maps.v

@@ -159,7 +159,7 @@ Proof.
       by symmetry; apply option_op_positive_dist_r with (m1 !! i).
 Qed.
 Canonical Structure mapR : cmraT := CMRAT map_cofe_mixin map_cmra_mixin.
-Global Instance map_cmra_identity : CMRAIdentity mapR.
+Global Instance map_cmra_unit : CMRAUnit mapR.
 Proof.
   split.
   - by intros i; rewrite lookup_empty.
@@ -194,7 +194,7 @@ Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
 Lemma map_singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
 Proof.
-  split; [|by intros; apply map_insert_validN, cmra_empty_validN].
+  split; [|by intros; apply map_insert_validN, cmra_unit_validN].
   by move=>/(_ i); simplify_map_eq.
 Qed.
 Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
@@ -232,7 +232,7 @@ Proof.
   - intros (y&Hi&?); rewrite map_includedN_spec=>j.
     destruct (decide (i = j)); simplify_map_eq.
     + rewrite Hi. by apply (includedN_preserving _), cmra_included_includedN.
-    + apply: cmra_empty_leastN.
+    + apply: cmra_unit_leastN.
 Qed.
 Lemma map_dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
 Proof.
@@ -268,14 +268,14 @@ Proof. apply map_insert_updateP'. Qed.
 Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
 Proof. apply map_insert_update. Qed.
 
-Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
+Lemma map_singleton_updateP_empty `{Empty A, !CMRAUnit A}
     (P : A → Prop) (Q : gmap K A → Prop) i :
   ∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
 Proof.
   intros Hx HQ n gf Hg.
   destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy).
   { move:(Hg i). rewrite !left_id.
-    case _: (gf !! i); simpl; auto using cmra_empty_validN. }
+    case _: (gf !! i); simpl; auto using cmra_unit_validN. }
   exists {[ i := y ]}; split; first by auto.
   intros i'; destruct (decide (i' = i)) as [->|].
   - rewrite lookup_op lookup_singleton.
@@ -283,7 +283,7 @@ Proof.
     by rewrite right_id.
   - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
 Qed.
-Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A → Prop) i :
+Lemma map_singleton_updateP_empty' `{Empty A, !CMRAUnit A} (P: A → Prop) i :
   ∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
 Proof. eauto using map_singleton_updateP_empty. Qed.
 

algebra/frac.v

@@ -172,7 +172,7 @@ Proof.
     + exfalso; inversion_clear Hx'.
 Qed.
 Canonical Structure fracR : cmraT := CMRAT frac_cofe_mixin frac_cmra_mixin.
-Global Instance frac_cmra_identity : CMRAIdentity fracR.
+Global Instance frac_cmra_unit : CMRAUnit fracR.
 Proof. split. done. by intros []. apply _. Qed.
 Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR.
 Proof.
@@ -238,7 +238,7 @@ Proof.
   split; try apply _.
   - intros n [p a|]; destruct 1; split; auto using validN_preserving.
   - intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
-      inversion Hx; setoid_subst; try apply: cmra_empty_least; auto.
+      inversion Hx; setoid_subst; try apply: cmra_unit_least; auto.
     destruct (included_preserving f a1 (a1 ⋅ a3)) as [b ?].
     { by apply cmra_included_l. }
     by exists (Frac q3 b); constructor.

algebra/iprod.v

@@ -160,11 +160,11 @@ Section iprod_cmra.
       split_and?; intros x; apply (proj2_sig (g x)).
   Qed.
   Canonical Structure iprodR : cmraT := CMRAT iprod_cofe_mixin iprod_cmra_mixin.
-  Global Instance iprod_cmra_identity `{∀ x, Empty (B x)} :
-    (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodR.
+  Global Instance iprod_cmra_unit `{∀ x, Empty (B x)} :
+    (∀ x, CMRAUnit (B x)) → CMRAUnit iprodR.
   Proof.
     intros ?; split.
-    - intros x; apply cmra_empty_valid.
+    - intros x; apply cmra_unit_valid.
     - by intros f x; rewrite iprod_lookup_op left_id.
     - by apply _.
   Qed.
@@ -201,14 +201,14 @@ Section iprod_cmra.
   Qed.
 
   (** Properties of iprod_singleton. *)
-  Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}.
+  Context `{∀ x, Empty (B x), ∀ x, CMRAUnit (B x)}.
 
   Lemma iprod_singleton_validN n x (y: B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
   Proof.
     split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
     move=>Hx x'; destruct (decide (x = x')) as [->|];
       rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
-    by apply cmra_empty_validN.
+    by apply cmra_unit_validN.
   Qed.
 
   Lemma iprod_core_singleton x (y : B x) :
@@ -216,7 +216,7 @@ Section iprod_cmra.
   Proof.
     by move=>x'; destruct (decide (x = x')) as [->|];
       rewrite iprod_lookup_core ?iprod_lookup_singleton
-      ?iprod_lookup_singleton_ne // cmra_core_empty.
+      ?iprod_lookup_singleton_ne // cmra_core_unit.
   Qed.
 
   Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :

algebra/option.v

@@ -119,7 +119,7 @@ Proof.
     + exists (None,None); repeat constructor.
 Qed.
 Canonical Structure optionR := CMRAT option_cofe_mixin option_cmra_mixin.
-Global Instance option_cmra_identity : CMRAIdentity optionR.
+Global Instance option_cmra_unit : CMRAUnit optionR.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
 Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
 Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
@@ -164,10 +164,10 @@ Lemma option_update x y : x ~~> y → Some x ~~> Some y.
 Proof.
   rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
 Qed.
-Lemma option_update_None `{Empty A, !CMRAIdentity A} : ∅ ~~> Some ∅.
+Lemma option_update_None `{Empty A, !CMRAUnit A} : ∅ ~~> Some ∅.
 Proof.
   intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
-    auto using cmra_empty_validN.
+    auto using cmra_unit_validN.
 Qed.
 End cmra.
 Arguments optionR : clear implicits.

algebra/upred.v

@@ -499,11 +499,11 @@ Proof.
   unseal; intros Hab Ha; split=> n x ??.
   apply HΨ with n a; auto. by symmetry; apply Hab with x. by apply Ha.
 Qed.
-Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
+Lemma eq_equiv `{Empty M, !CMRAUnit M} {A : cofeT} (a b : A) :
   True ⊑ (a ≡ b) → a ≡ b.
 Proof.
   unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
-  apply cmra_valid_validN, cmra_empty_valid.
+  apply cmra_valid_validN, cmra_unit_valid.
 Qed.
 Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
 Proof.
@@ -1002,7 +1002,7 @@ Lemma always_ownM (a : M) : core a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM
 Proof. by intros <-; rewrite always_ownM_core. Qed.
 Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
 Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
-Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
+Lemma ownM_empty `{Empty M, !CMRAUnit M} : True ⊑ uPred_ownM ∅.
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
 
 (* Valid *)

program_logic/auth.v

@@ -5,14 +5,14 @@ Import uPred.
 (* The CMRA we need. *)
 Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_inG :> inG Λ Σ (authR A);
-  auth_identity :> CMRAIdentity A;
+  auth_identity :> CMRAUnit A;
   auth_timeless :> CMRADiscrete A;
 }.
 (* The Functor we need. *)
 Definition authGF (A : cmraT) : gFunctor := GFunctor (constRF (authR A)).
 (* Show and register that they match. *)
 Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
-  `{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
+  `{CMRAUnit A, CMRADiscrete A} : authG Λ Σ A.
 Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Section definitions.

program_logic/ghost_ownership.v

@@ -19,10 +19,10 @@ Implicit Types a : A.
 Instance inG_empty `{Empty A} :
   Empty (Σ inG_id (iPreProp Λ (globalF Σ))) := cmra_transport inG_prf ∅.
 Instance inG_empty_spec `{Empty A} :
-  CMRAIdentity A → CMRAIdentity (Σ inG_id (iPreProp Λ (globalF Σ))).
+  CMRAUnit A → CMRAUnit (Σ inG_id (iPreProp Λ (globalF Σ))).
 Proof.
   split.
-  - apply cmra_transport_valid, cmra_empty_valid.
+  - apply cmra_transport_valid, cmra_unit_valid.
   - intros x; rewrite /empty /inG_empty; destruct inG_prf. by rewrite left_id.
   - apply _.
 Qed.
@@ -52,7 +52,7 @@ Lemma own_valid_r γ a : own γ a ⊑ (own γ a ★ ✓ a).
 Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊑ (✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
-Lemma own_empty `{CMRAIdentity A} γ : True ⊑ own γ ∅.
+Lemma own_empty `{CMRAUnit A} γ : True ⊑ own γ ∅.
 Proof.
   rewrite ownG_empty /own. apply equiv_spec, ownG_proper.
   (* FIXME: rewrite to_globalF_empty. *)
@@ -99,13 +99,13 @@ Proof.
   by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
 Qed.
 
-Lemma own_empty `{Empty A, !CMRAIdentity A} γ E :
+Lemma own_empty `{Empty A, !CMRAUnit A} γ E :
   True ⊑ (|={E}=> own γ ∅).
 Proof.
   rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
   eapply iprod_singleton_updateP_empty;
       first by eapply map_singleton_updateP_empty', cmra_transport_updateP',
-               cmra_update_updateP, cmra_update_empty.
+               cmra_update_updateP, cmra_update_unit.
   naive_solver.
 Qed.
 End global.

program_logic/model.v

@@ -10,7 +10,7 @@ Structure iFunctor := IFunctor {
   iFunctor_F :> rFunctor;
   iFunctor_contractive : rFunctorContractive iFunctor_F;
   iFunctor_empty (A : cofeT) : Empty (iFunctor_F A);
-  iFunctor_identity (A : cofeT) : CMRAIdentity (iFunctor_F A);
+  iFunctor_identity (A : cofeT) : CMRAUnit (iFunctor_F A);
 }.
 Arguments IFunctor _ {_ _ _}.
 Existing Instances iFunctor_contractive iFunctor_empty iFunctor_identity.

program_logic/ownership.v

@@ -28,7 +28,7 @@ Qed.
 Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.
 Proof.
   apply uPred.always_ownM.
-  by rewrite Res_core !cmra_core_empty map_core_singleton.
+  by rewrite Res_core !cmra_core_unit map_core_singleton.
 Qed.
 Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
 Proof. by rewrite /AlwaysStable always_ownI. Qed.
@@ -55,7 +55,7 @@ Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
 Lemma always_ownG_core m : (□ ownG (core m))%I ≡ ownG (core m).
 Proof.
   apply uPred.always_ownM.
-  by rewrite Res_core !cmra_core_empty -{2}(cmra_core_idemp m).
+  by rewrite Res_core !cmra_core_unit -{2}(cmra_core_idemp m).
 Qed.
 Lemma always_ownG m : core m ≡ m → (□ ownG m)%I ≡ ownG m.
 Proof. by intros <-; rewrite always_ownG_core. Qed.
@@ -82,17 +82,17 @@ Proof.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
     by apply Some_dist, symmetry, agree_valid_includedN,
       (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
-  - intros ?; split_and?; try apply cmra_empty_leastN; eauto.
+  - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
 Qed.
 Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl σ.
 Proof.
   intros (?&?&?). rewrite /ownP; uPred.unseal.
   rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
-  rewrite (timeless_iff n). naive_solver (apply cmra_empty_leastN).
+  rewrite (timeless_iff n). naive_solver (apply cmra_unit_leastN).
 Qed.
 Lemma ownG_spec n r m : (ownG m) n r ↔ m ≼{n} gst r.
 Proof.
   rewrite /ownG; uPred.unseal.
-  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
+  rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_unit_leastN).
 Qed.
 End ownership.

program_logic/resources.v

@@ -124,10 +124,10 @@ Proof.
     by exists (Res w σ m, Res w' σ' m').
 Qed.
 Canonical Structure resR : cmraT := CMRAT res_cofe_mixin res_cmra_mixin.
-Global Instance res_cmra_identity `{CMRAIdentity M} : CMRAIdentity resR.
+Global Instance res_cmra_unit `{CMRAUnit M} : CMRAUnit resR.
 Proof.
   split.
-  - split_and!; apply cmra_empty_valid.
+  - split_and!; apply cmra_unit_valid.
   - by split; rewrite /= left_id.
   - apply _.
 Qed.

program_logic/viewshifts.v

@@ -117,7 +117,7 @@ Proof. by intros; apply vs_alt, own_updateP. Qed.
 Lemma vs_update E γ a a' : a ~~> a' → own γ a ={E}=> own γ a'.
 Proof. by intros; apply vs_alt, own_update. Qed.
 
-Lemma vs_own_empty `{Empty A, !CMRAIdentity A} E γ :
+Lemma vs_own_empty `{Empty A, !CMRAUnit A} E γ :
   True ={E}=> own γ ∅.
 Proof. by intros; eapply vs_alt, own_empty. Qed.