diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 2356a14c53371fed5682ab8e3f160c39e42c4b93..9908c2fc2b54cd670760a2e257c5d7d39616abb3 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -131,7 +131,7 @@ Proof.
- destruct (elem_of_agree x1); naive_solver.
Qed.
-Definition agree_cmra_mixin : CMRAMixin (agree A).
+Definition agree_cmra_mixin : CmraMixin (agree A).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- intros n x; rewrite !agree_validN_def; eauto using dist_S.
@@ -142,14 +142,14 @@ Proof.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
-Canonical Structure agreeR : cmraT := CMRAT (agree A) agree_cmra_mixin.
+Canonical Structure agreeR : cmraT := CmraT (agree A) agree_cmra_mixin.
-Global Instance agree_total : CMRATotal agreeR.
-Proof. rewrite /CMRATotal; eauto. Qed.
+Global Instance agree_cmra_total : CmraTotal agreeR.
+Proof. rewrite /CmraTotal; eauto. Qed.
Global Instance agree_persistent (x : agree A) : Persistent x.
Proof. by constructor. Qed.
-Global Instance agree_cmra_discrete : OFEDiscrete A → CMRADiscrete agreeR.
+Global Instance agree_cmra_discrete : OfeDiscrete A → CmraDiscrete agreeR.
Proof.
intros HD. split.
- intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _); auto.
@@ -267,7 +267,7 @@ Section agree_map.
- intros (a&->&?). exists (f a). rewrite -Hfg; eauto.
Qed.
- Global Instance agree_map_morphism : CMRAMorphism (agree_map f).
+ Global Instance agree_map_morphism : CmraMorphism (agree_map f).
Proof using Hf.
split; first apply _.
- intros n x. rewrite !agree_validN_def=> Hv b b' /=.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index f297946554c7fb7239b4d264b5178728eb5bf0a7..8fa2c404204f22aaad33107758621a81ca36694f 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -52,7 +52,7 @@ Qed.
Global Instance Auth_discrete a b :
Discrete a → Discrete b → Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
-Global Instance auth_ofe_discrete : OFEDiscrete A → OFEDiscrete authC.
+Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete authC.
Proof. intros ? [??]; apply _. Qed.
Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
@@ -113,7 +113,7 @@ Proof.
destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
Qed.
-Lemma auth_valid_discrete `{CMRADiscrete A} x :
+Lemma auth_valid_discrete `{CmraDiscrete A} x :
✓ x ↔ match authoritative x with
| Excl' a => auth_own x ≼ a ∧ ✓ a
| None => ✓ auth_own x
@@ -125,18 +125,18 @@ Proof.
Qed.
Lemma auth_validN_2 n a b : ✓{n} (◠a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
Proof. by rewrite auth_validN_eq /= left_id. Qed.
-Lemma auth_valid_discrete_2 `{CMRADiscrete A} a b : ✓ (◠a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Lemma auth_valid_discrete_2 `{CmraDiscrete A} a b : ✓ (◠a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
Proof. by rewrite auth_valid_discrete /= left_id. Qed.
Lemma authoritative_valid x : ✓ x → ✓ authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_valid `{CMRADiscrete A} x : ✓ x → ✓ auth_own x.
+Lemma auth_own_valid `{CmraDiscrete A} x : ✓ x → ✓ auth_own x.
Proof.
rewrite auth_valid_discrete.
destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
Qed.
-Lemma auth_cmra_mixin : CMRAMixin (auth A).
+Lemma auth_cmra_mixin : CmraMixin (auth A).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -166,9 +166,9 @@ Proof.
as (b1&b2&?&?&?); auto using auth_own_validN.
by exists (Auth ea1 b1), (Auth ea2 b2).
Qed.
-Canonical Structure authR := CMRAT (auth A) auth_cmra_mixin.
+Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
-Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
+Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete authR.
Proof.
split; first apply _.
intros [[[?|]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
@@ -178,14 +178,14 @@ Proof.
Qed.
Instance auth_empty : Unit (auth A) := Auth ε ε.
-Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
+Lemma auth_ucmra_mixin : UcmraMixin (auth A).
Proof.
split; simpl.
- rewrite auth_valid_eq /=. apply ucmra_unit_valid.
- by intros x; constructor; rewrite /= left_id.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
-Canonical Structure authUR := UCMRAT (auth A) auth_ucmra_mixin.
+Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin.
Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
@@ -274,7 +274,7 @@ Proof.
apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
Qed.
Instance auth_map_cmra_morphism {A B : ucmraT} (f : A → B) :
- CMRAMorphism f → CMRAMorphism (auth_map f).
+ CmraMorphism f → CmraMorphism (auth_map f).
Proof.
split; try apply _.
- intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 7c1067fca0b64998c24b6438c9c85b24bd86538e..e2221626d94a4e2d3d4ad18caf6cee35d8b300c0 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -41,7 +41,7 @@ Hint Extern 0 (_ ≼{_} _) => reflexivity.
Section mixin.
Local Set Primitive Projections.
- Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
+ Record CmraMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
(* setoids *)
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n x y cx :
@@ -65,7 +65,7 @@ Section mixin.
End mixin.
(** Bundeled version *)
-Structure cmraT := CMRAT' {
+Structure cmraT := CmraT' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
@@ -74,14 +74,14 @@ Structure cmraT := CMRAT' {
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
- cmra_mixin : CMRAMixin cmra_car;
+ cmra_mixin : CmraMixin cmra_car;
_ : Type
}.
-Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
-(* Given [m : CMRAMixin A], the notation [CMRAT A m] provides a smart
+Arguments CmraT' _ {_ _ _ _ _ _} _ _ _.
+(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
-Notation CMRAT A m := (CMRAT' A (ofe_mixin_of A%type) m A) (only parsing).
+Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m A) (only parsing).
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
@@ -100,7 +100,7 @@ Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeC.
-Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac → A) : CMRAMixin Ac := cmra_mixin Ac.
+Definition cmra_mixin_of' A {Ac : cmraT} (f : Ac → A) : CmraMixin Ac := cmra_mixin Ac.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
@@ -171,8 +171,8 @@ Instance: Params (@IdFree) 1.
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
core. *)
-Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
-Hint Mode CMRATotal ! : typeclass_instances.
+Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
+Hint Mode CmraTotal ! : typeclass_instances.
Class Core (A : Type) := core : A → A.
Hint Mode Core ! : typeclass_instances.
@@ -185,13 +185,13 @@ Arguments core' _ _ _ /.
Class Unit (A : Type) := ε : A.
Arguments ε {_ _}.
-Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Unit A} := {
+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' {
+Structure ucmraT := UcmraT' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
@@ -201,13 +201,13 @@ Structure ucmraT := UCMRAT' {
ucmra_validN : ValidN ucmra_car;
ucmra_unit : Unit ucmra_car;
ucmra_ofe_mixin : OfeMixin ucmra_car;
- ucmra_cmra_mixin : CMRAMixin ucmra_car;
- ucmra_mixin : UCMRAMixin ucmra_car;
+ ucmra_cmra_mixin : CmraMixin ucmra_car;
+ ucmra_mixin : UcmraMixin ucmra_car;
_ : Type;
}.
-Arguments UCMRAT' _ {_ _ _ _ _ _ _} _ _ _ _.
-Notation UCMRAT A m :=
- (UCMRAT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
+Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _ _.
+Notation UcmraT A m :=
+ (UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
@@ -223,7 +223,7 @@ 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 :=
- CMRAT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
+ CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
Canonical Structure ucmra_cmraR.
(** Lifting properties from the mixin *)
@@ -239,14 +239,14 @@ Section ucmra_mixin.
End ucmra_mixin.
(** * Discrete CMRAs *)
-Class CMRADiscrete (A : cmraT) := {
- cmra_discrete_ofe_discrete :> OFEDiscrete A;
+Class CmraDiscrete (A : cmraT) := {
+ cmra_discrete_ofe_discrete :> OfeDiscrete A;
cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
}.
-Hint Mode CMRADiscrete ! : typeclass_instances.
+Hint Mode CmraDiscrete ! : typeclass_instances.
(** * Morphisms *)
-Class CMRAMorphism {A B : cmraT} (f : A → B) := {
+Class CmraMorphism {A B : cmraT} (f : A → B) := {
cmra_morphism_ne :> NonExpansive f;
cmra_morphism_validN n x : ✓{n} x → ✓{n} f x;
cmra_morphism_pcore x : pcore (f x) ≡ f <$> pcore x;
@@ -464,7 +464,7 @@ Qed.
(** ** Total core *)
Section total_core.
Local Set Default Proof Using "Type*".
- Context `{CMRATotal A}.
+ Context `{CmraTotal A}.
Lemma cmra_core_l x : core x ⋅ x ≡ x.
Proof.
@@ -549,12 +549,12 @@ Proof.
Qed.
(** ** Discrete *)
-Lemma cmra_discrete_valid_iff `{CMRADiscrete A} n x : ✓ x ↔ ✓{n} x.
+Lemma cmra_discrete_valid_iff `{CmraDiscrete A} n x : ✓ x ↔ ✓{n} x.
Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
-Lemma cmra_discrete_included_iff `{OFEDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
+Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
@@ -565,7 +565,7 @@ Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
Proof. unfold Cancelable. intros x x' EQ. by setoid_rewrite EQ. Qed.
Lemma cancelable x `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z.
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
-Lemma discrete_cancelable x `{CMRADiscrete A}:
+Lemma discrete_cancelable x `{CmraDiscrete A}:
(∀ y z, ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z → y ≡ z) → Cancelable x.
Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
@@ -595,7 +595,7 @@ Lemma id_free_r x `{!IdFree x} y : ✓x → x ⋅ y ≡ x → False.
Proof. move=> /cmra_valid_validN ? /equiv_dist. eauto. Qed.
Lemma id_free_l x `{!IdFree x} y : ✓x → y ⋅ x ≡ x → False.
Proof. rewrite comm. eauto using id_free_r. Qed.
-Lemma discrete_id_free x `{CMRADiscrete A}:
+Lemma discrete_id_free x `{CmraDiscrete A}:
(∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x.
Proof.
intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
@@ -627,7 +627,7 @@ Section ucmra.
Global Instance ucmra_unit_persistent : Persistent (ε:A).
Proof. apply ucmra_pcore_unit. Qed.
- Global Instance cmra_unit_total : CMRATotal A.
+ Global Instance cmra_unit_cmra_total : CmraTotal A.
Proof.
intros x. destruct (cmra_pcore_mono' ε x ε) as (cx&->&?);
eauto using ucmra_unit_least, (persistent (ε:A)).
@@ -639,7 +639,7 @@ Section ucmra.
Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
End ucmra.
-Hint Immediate cmra_unit_total.
+Hint Immediate cmra_unit_cmra_total.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
@@ -672,7 +672,7 @@ Section cmra_leibniz.
(** ** Total core *)
Section total_core.
- Context `{CMRATotal A}.
+ Context `{CmraTotal A}.
Lemma cmra_core_r_L x : x â‹… core x = x.
Proof. unfold_leibniz. apply cmra_core_r. Qed.
@@ -718,7 +718,7 @@ Section cmra_total.
Context (extend : ∀ n (x y1 y2 : A),
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2).
- Lemma cmra_total_mixin : CMRAMixin A.
+ Lemma cmra_total_mixin : CmraMixin A.
Proof using Type*.
split; auto.
- intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
@@ -732,12 +732,12 @@ Section cmra_total.
End cmra_total.
(** * Properties about morphisms *)
-Instance cmra_morphism_id {A : cmraT} : CMRAMorphism (@id A).
+Instance cmra_morphism_id {A : cmraT} : CmraMorphism (@id A).
Proof. split=>//=. apply _. intros. by rewrite option_fmap_id. Qed.
-Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CMRAMorphism f} :
+Instance cmra_morphism_proper {A B : cmraT} (f : A → B) `{!CmraMorphism f} :
Proper ((≡) ==> (≡)) f := ne_proper _.
Instance cmra_morphism_compose {A B C : cmraT} (f : A → B) (g : B → C) :
- CMRAMorphism f → CMRAMorphism g → CMRAMorphism (g ∘ f).
+ CmraMorphism f → CmraMorphism g → CmraMorphism (g ∘ f).
Proof.
split.
- apply _.
@@ -748,7 +748,7 @@ Qed.
Section cmra_morphism.
Local Set Default Proof Using "Type*".
- Context {A B : cmraT} (f : A → B) `{!CMRAMorphism f}.
+ Context {A B : cmraT} (f : A → B) `{!CmraMorphism f}.
Lemma cmra_morphism_core x : core (f x) ≡ f (core x).
Proof. unfold core, core'. rewrite cmra_morphism_pcore. by destruct (pcore x). Qed.
Lemma cmra_morphism_monotone x y : x ≼ y → f x ≼ f y.
@@ -771,7 +771,7 @@ Structure rFunctor := RFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
rFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
- CMRAMorphism (rFunctor_map fg)
+ CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_ne rFunctor_mor.
Instance: Params (@rFunctor_map) 5.
@@ -804,7 +804,7 @@ Structure urFunctor := URFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
urFunctor_mor {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
- CMRAMorphism (urFunctor_map fg)
+ CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_ne urFunctor_mor.
Instance: Params (@urFunctor_map) 5.
@@ -876,7 +876,7 @@ Section discrete.
Existing Instances discrete_dist.
Instance discrete_validN : ValidN A := λ n x, ✓ x.
- Definition discrete_cmra_mixin : CMRAMixin A.
+ Definition discrete_cmra_mixin : CmraMixin A.
Proof.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ 0).
@@ -884,15 +884,15 @@ Section discrete.
Qed.
Instance discrete_cmra_discrete :
- CMRADiscrete (CMRAT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A).
+ CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A).
Proof. split. apply _. done. Qed.
End discrete.
(** A smart constructor for the discrete RA over a carrier [A]. It uses
-[discrete_ofe_equivalence_of A] to make sure the same [Equivalence] proof is
+[ofe_discrete_equivalence_of A] to make sure the same [Equivalence] proof is
used as when constructing the OFE. *)
Notation discreteR A ra_mix :=
- (CMRAT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
+ (CmraT A (discrete_cmra_mixin (discrete_ofe_equivalence_of A%type) ra_mix))
(only parsing).
Section ra_total.
@@ -927,16 +927,16 @@ Section unit.
Instance unit_validN : ValidN () := λ n x, True.
Instance unit_pcore : PCore () := λ x, Some x.
Instance unit_op : Op () := λ x y, ().
- Lemma unit_cmra_mixin : CMRAMixin ().
+ Lemma unit_cmra_mixin : CmraMixin ().
Proof. apply discrete_cmra_mixin, ra_total_mixin; by eauto. Qed.
- Canonical Structure unitR : cmraT := CMRAT unit unit_cmra_mixin.
+ Canonical Structure unitR : cmraT := CmraT unit unit_cmra_mixin.
Instance unit_unit : Unit () := ().
- Lemma unit_ucmra_mixin : UCMRAMixin ().
+ Lemma unit_ucmra_mixin : UcmraMixin ().
Proof. done. Qed.
- Canonical Structure unitUR : ucmraT := UCMRAT unit unit_ucmra_mixin.
+ Canonical Structure unitUR : ucmraT := UcmraT unit unit_ucmra_mixin.
- Global Instance unit_cmra_discrete : CMRADiscrete unitR.
+ Global Instance unit_cmra_discrete : CmraDiscrete unitR.
Proof. done. Qed.
Global Instance unit_persistent (x : ()) : Persistent x.
Proof. by constructor. Qed.
@@ -963,13 +963,13 @@ Section nat.
Qed.
Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
- Global Instance nat_cmra_discrete : CMRADiscrete natR.
+ Global Instance nat_cmra_discrete : CmraDiscrete natR.
Proof. apply discrete_cmra_discrete. Qed.
Instance nat_unit : Unit nat := 0.
- Lemma nat_ucmra_mixin : UCMRAMixin nat.
+ Lemma nat_ucmra_mixin : UcmraMixin nat.
Proof. split; apply _ || done. Qed.
- Canonical Structure natUR : ucmraT := UCMRAT nat nat_ucmra_mixin.
+ Canonical Structure natUR : ucmraT := UcmraT nat nat_ucmra_mixin.
Global Instance nat_cancelable (x : nat) : Cancelable x.
Proof. by intros ???? ?%Nat.add_cancel_l. Qed.
@@ -1001,12 +1001,12 @@ Section mnat.
Qed.
Canonical Structure mnatR : cmraT := discreteR mnat mnat_ra_mixin.
- Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
+ Global Instance mnat_cmra_discrete : CmraDiscrete mnatR.
Proof. apply discrete_cmra_discrete. Qed.
- Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
+ Lemma mnat_ucmra_mixin : UcmraMixin mnat.
Proof. split; apply _ || done. Qed.
- Canonical Structure mnatUR : ucmraT := UCMRAT mnat mnat_ucmra_mixin.
+ Canonical Structure mnatUR : ucmraT := UcmraT mnat mnat_ucmra_mixin.
Global Instance mnat_persistent (x : mnat) : Persistent x.
Proof. by constructor. Qed.
@@ -1030,7 +1030,7 @@ Section positive.
Qed.
Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
- Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
+ Global Instance pos_cmra_discrete : CmraDiscrete positiveR.
Proof. apply discrete_cmra_discrete. Qed.
Global Instance pos_cancelable (x : positive) : Cancelable x.
@@ -1078,7 +1078,7 @@ Section prod.
intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
Qed.
- Definition prod_cmra_mixin : CMRAMixin (A * B).
+ Definition prod_cmra_mixin : CmraMixin (A * B).
Proof.
split; try apply _.
- by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
@@ -1107,19 +1107,19 @@ Section prod.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
by exists (z11,z21), (z12,z22).
Qed.
- Canonical Structure prodR := CMRAT (prod A B) prod_cmra_mixin.
+ Canonical Structure prodR := CmraT (prod A B) prod_cmra_mixin.
Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
Proof. done. Qed.
- Global Instance prod_cmra_total : CMRATotal A → CMRATotal B → CMRATotal prodR.
+ Global Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
Proof.
intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
exists (ca,cb); by simplify_option_eq.
Qed.
Global Instance prod_cmra_discrete :
- CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodR.
+ CmraDiscrete A → CmraDiscrete B → CmraDiscrete prodR.
Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
Global Instance pair_persistent x y :
@@ -1147,14 +1147,14 @@ Section prod_unit.
Context {A B : ucmraT}.
Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := (ε, ε).
- Lemma prod_ucmra_mixin : UCMRAMixin (A * B).
+ Lemma prod_ucmra_mixin : UcmraMixin (A * B).
Proof.
split.
- split; apply ucmra_unit_valid.
- by split; rewrite /=left_id.
- rewrite prod_pcore_Some'; split; apply (persistent _).
Qed.
- Canonical Structure prodUR := UCMRAT (prod A B) prod_ucmra_mixin.
+ Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ε) ⋅ (ε, y).
Proof. by rewrite pair_op left_id right_id. Qed.
@@ -1167,7 +1167,7 @@ End prod_unit.
Arguments prodUR : clear implicits.
Instance prod_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
- CMRAMorphism f → CMRAMorphism g → CMRAMorphism (prod_map f g).
+ CmraMorphism f → CmraMorphism g → CmraMorphism (prod_map f g).
Proof.
split; first apply _.
- by intros n x [??]; split; simpl; apply cmra_morphism_validN.
@@ -1245,7 +1245,7 @@ Section option.
Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
Definition Some_validN a n : ✓{n} Some a ↔ ✓{n} a := reflexivity _.
Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
- Lemma Some_core `{CMRATotal A} a : Some (core a) = core (Some a).
+ Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Lemma Some_op_opM x my : Some x â‹… my = Some (x â‹…? my).
Proof. by destruct my. Qed.
@@ -1280,7 +1280,7 @@ Section option.
+ exists (Some z); by constructor.
Qed.
- Lemma option_cmra_mixin : CMRAMixin (option A).
+ Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -1312,15 +1312,15 @@ Section option.
+ by exists None, (Some x); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
- Canonical Structure optionR := CMRAT (option A) option_cmra_mixin.
+ Canonical Structure optionR := CmraT (option A) option_cmra_mixin.
- Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
+ Global Instance option_cmra_discrete : CmraDiscrete A → CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
Instance option_unit : Unit (option A) := None.
- Lemma option_ucmra_mixin : UCMRAMixin optionR.
+ Lemma option_ucmra_mixin : UcmraMixin optionR.
Proof. split. done. by intros []. done. Qed.
- Canonical Structure optionUR := UCMRAT (option A) option_ucmra_mixin.
+ Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
(** Misc *)
Lemma op_None mx my : mx ⋅ my = None ↔ mx = None ∧ my = None.
@@ -1353,9 +1353,9 @@ Section option.
Lemma Some_included_2 x y : x ≼ y → Some x ≼ Some y.
Proof. rewrite Some_included; eauto. Qed.
- Lemma Some_includedN_total `{CMRATotal A} n x y : Some x ≼{n} Some y ↔ x ≼{n} y.
+ Lemma Some_includedN_total `{CmraTotal A} n x y : Some x ≼{n} Some y ↔ x ≼{n} y.
Proof. rewrite Some_includedN. split. by intros [->|?]. eauto. Qed.
- Lemma Some_included_total `{CMRATotal A} x y : Some x ≼ Some y ↔ x ≼ y.
+ Lemma Some_included_total `{CmraTotal A} x y : Some x ≼ Some y ↔ x ≼ y.
Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
Lemma Some_includedN_exclusive n x `{!Exclusive x} y :
@@ -1392,26 +1392,26 @@ Section option_prod.
Lemma Some_pair_includedN n (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) ≼{n} Some (x2,y2) → Some x1 ≼{n} Some x2 ∧ Some y1 ≼{n} Some y2.
Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.
- Lemma Some_pair_includedN_total_1 `{CMRATotal A} n (x1 x2 : A) (y1 y2 : B) :
+ Lemma Some_pair_includedN_total_1 `{CmraTotal A} n (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) ≼{n} Some (x2,y2) → x1 ≼{n} x2 ∧ Some y1 ≼{n} Some y2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ x1). Qed.
- Lemma Some_pair_includedN_total_2 `{CMRATotal B} n (x1 x2 : A) (y1 y2 : B) :
+ Lemma Some_pair_includedN_total_2 `{CmraTotal B} n (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) ≼{n} Some (x2,y2) → Some x1 ≼{n} Some x2 ∧ y1 ≼{n} y2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ y1). Qed.
Lemma Some_pair_included (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ Some y1 ≼ Some y2.
Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
- Lemma Some_pair_included_total_1 `{CMRATotal A} (x1 x2 : A) (y1 y2 : B) :
+ Lemma Some_pair_included_total_1 `{CmraTotal A} (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) ≼ Some (x2,y2) → x1 ≼ x2 ∧ Some y1 ≼ Some y2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total x1). Qed.
- Lemma Some_pair_included_total_2 `{CMRATotal B} (x1 x2 : A) (y1 y2 : B) :
+ Lemma Some_pair_included_total_2 `{CmraTotal B} (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ y1 ≼ y2.
Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total y1). Qed.
End option_prod.
-Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CMRAMorphism f} :
- CMRAMorphism (fmap f : option A → option B).
+Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
+ CmraMorphism (fmap f : option A → option B).
Proof.
split; first apply _.
- intros n [x|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 2de9c50670f01b84735c1f23b1f240053955ffec..224f2d33da6233ad2f92f82244f65c48111b04ec 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -39,12 +39,12 @@ Section coPset.
Qed.
Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
- Global Instance coPset_cmra_discrete : CMRADiscrete coPsetR.
+ Global Instance coPset_cmra_discrete : CmraDiscrete coPsetR.
Proof. apply discrete_cmra_discrete. Qed.
- Lemma coPset_ucmra_mixin : UCMRAMixin coPset.
+ Lemma coPset_ucmra_mixin : UcmraMixin coPset.
Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
- Canonical Structure coPsetUR := UCMRAT coPset coPset_ucmra_mixin.
+ Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
Lemma coPset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
@@ -112,10 +112,10 @@ Section coPset_disj.
Qed.
Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
- Global Instance coPset_disj_cmra_discrete : CMRADiscrete coPset_disjR.
+ Global Instance coPset_disj_cmra_discrete : CmraDiscrete coPset_disjR.
Proof. apply discrete_cmra_discrete. Qed.
- Lemma coPset_disj_ucmra_mixin : UCMRAMixin coPset_disj.
+ Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
- Canonical Structure coPset_disjUR := UCMRAT coPset_disj coPset_disj_ucmra_mixin.
+ Canonical Structure coPset_disjUR := UcmraT coPset_disj coPset_disj_ucmra_mixin.
End coPset_disj.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index c1536c960b5e9b39db4037370399465b2286ccc0..596d9522b37fbab8228e2a2d570d5d9ae4d12b38 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -96,7 +96,8 @@ Next Obligation.
+ rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
Qed.
-Global Instance csum_ofe_discrete : OFEDiscrete A → OFEDiscrete B → OFEDiscrete csumC.
+Global Instance csum_ofe_discrete :
+ OfeDiscrete A → OfeDiscrete B → OfeDiscrete csumC.
Proof. by inversion_clear 3; constructor; apply (discrete _). Qed.
Global Instance csum_leibniz :
LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv (csumC A B).
@@ -202,7 +203,7 @@ Proof.
+ exists (Cinr c); by constructor.
Qed.
-Lemma csum_cmra_mixin : CMRAMixin (csum A B).
+Lemma csum_cmra_mixin : CmraMixin (csum A B).
Proof.
split.
- intros [] n; destruct 1; constructor; by ofe_subst.
@@ -246,10 +247,10 @@ Proof.
exists (Cinr z1), (Cinr z2). by repeat constructor.
+ by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
Qed.
-Canonical Structure csumR := CMRAT (csum A B) csum_cmra_mixin.
+Canonical Structure csumR := CmraT (csum A B) csum_cmra_mixin.
Global Instance csum_cmra_discrete :
- CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR.
+ CmraDiscrete A → CmraDiscrete B → CmraDiscrete csumR.
Proof.
split; first apply _.
by move=>[a|b|] HH /=; try apply cmra_discrete_valid.
@@ -357,7 +358,7 @@ Arguments csumR : clear implicits.
(* Functor *)
Instance csum_map_cmra_morphism {A A' B B' : cmraT} (f : A → A') (g : B → B') :
- CMRAMorphism f → CMRAMorphism g → CMRAMorphism (csum_map f g).
+ CmraMorphism f → CmraMorphism g → CmraMorphism (csum_map f g).
Proof.
split; try apply _.
- intros n [a|b|]; simpl; auto using cmra_morphism_validN.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 8a64ae6f854ce5386b31469224f5a6c706806e66..551e47fd7edebb46ad1b170d78c5604208d9bacd 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -50,9 +50,9 @@ Qed.
Canonical Structure dec_agreeR : cmraT :=
discreteR (dec_agree A) dec_agree_ra_mixin.
-Global Instance dec_agree_cmra_discrete : CMRADiscrete dec_agreeR.
+Global Instance dec_agree_cmra_discrete : CmraDiscrete dec_agreeR.
Proof. apply discrete_cmra_discrete. Qed.
-Global Instance dec_agree_total : CMRATotal dec_agreeR.
+Global Instance dec_agree_cmra_total : CmraTotal dec_agreeR.
Proof. intros x. by exists x. Qed.
(* Some properties of this CMRA *)
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index 8c2799cc1f623195a80f4e56c8e032615ac5d4b7..73b4d0b99f6ad0501fa45fac4a69e580df99ab0e 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -1,7 +1,7 @@
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type".
-Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
+Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
(* setoids *)
mixin_dra_equivalence : Equivalence ((≡) : relation A);
mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
@@ -24,16 +24,16 @@ Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
mixin_dra_core_mono x y :
∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
}.
-Structure draT := DRAT {
+Structure draT := DraT {
dra_car :> Type;
dra_equiv : Equiv dra_car;
dra_core : Core dra_car;
dra_disjoint : Disjoint dra_car;
dra_op : Op dra_car;
dra_valid : Valid dra_car;
- dra_mixin : DRAMixin dra_car
+ dra_mixin : DraMixin dra_car
}.
-Arguments DRAT _ {_ _ _ _ _} _.
+Arguments DraT _ {_ _ _ _ _} _.
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
@@ -177,10 +177,10 @@ Qed.
Canonical Structure validityR : cmraT :=
discreteR (validity A) validity_ra_mixin.
-Global Instance validity_cmra_disrete : CMRADiscrete validityR.
+Global Instance validity_disrete_cmra : CmraDiscrete validityR.
Proof. apply discrete_cmra_discrete. Qed.
-Global Instance validity_cmra_total : CMRATotal validityR.
-Proof. rewrite /CMRATotal; eauto. Qed.
+Global Instance validity_cmra_total : CmraTotal validityR.
+Proof. rewrite /CmraTotal; eauto. Qed.
Lemma validity_update x y :
(∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index b5f99ab6c08e8f6b72183b9c247535591b901980..b73aaa01e635b775c07fb9e40d0a71903b410877 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -59,7 +59,7 @@ Proof.
- by intros []; constructor.
Qed.
-Global Instance excl_ofe_discrete : OFEDiscrete A → OFEDiscrete exclC.
+Global Instance excl_ofe_discrete : OfeDiscrete A → OfeDiscrete exclC.
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
@@ -77,7 +77,7 @@ Instance excl_validN : ValidN (excl A) := λ n x,
Instance excl_pcore : PCore (excl A) := λ _, None.
Instance excl_op : Op (excl A) := λ x y, ExclBot.
-Lemma excl_cmra_mixin : CMRAMixin (excl A).
+Lemma excl_cmra_mixin : CmraMixin (excl A).
Proof.
split; try discriminate.
- by intros n []; destruct 1; constructor.
@@ -89,9 +89,9 @@ Proof.
- by intros n [?|] [?|].
- intros n x [?|] [?|] ?; inversion_clear 1; eauto.
Qed.
-Canonical Structure exclR := CMRAT (excl A) excl_cmra_mixin.
+Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
-Global Instance excl_cmra_discrete : OFEDiscrete A → CMRADiscrete exclR.
+Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
Proof. split. apply _. by intros []. Qed.
(** Internalized properties *)
@@ -142,7 +142,7 @@ Instance excl_map_ne {A B : ofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Instance excl_map_cmra_morphism {A B : ofeT} (f : A → B) :
- NonExpansive f → CMRAMorphism (excl_map f).
+ NonExpansive f → CmraMorphism (excl_map f).
Proof. split; try done; try apply _. by intros n [a|]. Qed.
Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f).
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 5a296f36d4a6ed641c82a376adbe85474c655690..c83f701175df6a20c8c4487f3df0831f45b659fd 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -26,7 +26,7 @@ Proof.
Qed.
Canonical Structure fracR := discreteR frac frac_ra_mixin.
-Global Instance frac_cmra_discrete : CMRADiscrete fracR.
+Global Instance frac_cmra_discrete : CmraDiscrete fracR.
Proof. apply discrete_cmra_discrete. Qed.
End frac.
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 09294255e5aa2b1c251212ebf63f1463a2afcae4..b1aebd8db68441c4c7aa5c06c82d6d119f9f9f2a 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -58,13 +58,13 @@ Section frac_auth.
Lemma frac_auth_includedN n q a b : ✓{n} (â—! a â‹… â—¯!{q} b) → Some b ≼{n} Some a.
Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
- Lemma frac_auth_included `{CMRADiscrete A} q a b :
+ Lemma frac_auth_included `{CmraDiscrete A} q a b :
✓ (â—! a â‹… â—¯!{q} b) → Some b ≼ Some a.
Proof. by rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
- Lemma frac_auth_includedN_total `{CMRATotal A} n q a b :
+ Lemma frac_auth_includedN_total `{CmraTotal A} n q a b :
✓{n} (â—! a â‹… â—¯!{q} b) → b ≼{n} a.
Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
- Lemma frac_auth_included_total `{CMRADiscrete A, CMRATotal A} q a b :
+ Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b :
✓ (â—! a â‹… â—¯!{q} b) → b ≼ a.
Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 310f2598e2f85a0dc0b2d52f5a631e4c16a8c974..a32c84576eb84027289b590c0e54ebc8dd1d5bd4 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -37,7 +37,7 @@ Next Obligation.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
-Global Instance gmap_ofe_discrete : OFEDiscrete A → OFEDiscrete gmapC.
+Global Instance gmap_ofe_discrete : OfeDiscrete A → OfeDiscrete gmapC.
Proof. intros ? m m' ? i. by apply (discrete _). Qed.
(* why doesn't this go automatic? *)
Global Instance gmapC_leibniz: LeibnizEquiv A → LeibnizEquiv gmapC.
@@ -127,7 +127,7 @@ Proof.
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
-Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
+Lemma gmap_cmra_mixin : CmraMixin (gmap K A).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -171,19 +171,19 @@ Proof.
* by rewrite lookup_partial_alter.
* by rewrite lookup_partial_alter_ne // Hm2' lookup_delete_ne.
Qed.
-Canonical Structure gmapR := CMRAT (gmap K A) gmap_cmra_mixin.
+Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin.
-Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
+Global Instance gmap_cmra_discrete : CmraDiscrete A → CmraDiscrete gmapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
-Lemma gmap_ucmra_mixin : UCMRAMixin (gmap K A).
+Lemma gmap_ucmra_mixin : UcmraMixin (gmap K A).
Proof.
split.
- by intros i; rewrite lookup_empty.
- by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
- constructor=> i. by rewrite lookup_omap lookup_empty.
Qed.
-Canonical Structure gmapUR := UCMRAT (gmap K A) gmap_ucmra_mixin.
+Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
(** Internalized properties *)
Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
@@ -477,7 +477,7 @@ Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A → B) n :
Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
Instance gmap_fmap_cmra_morphism `{Countable K} {A B : cmraT} (f : A → B)
- `{!CMRAMorphism f} : CMRAMorphism (fmap f : gmap K A → gmap K B).
+ `{!CmraMorphism f} : CmraMorphism (fmap f : gmap K A → gmap K B).
Proof.
split; try apply _.
- by intros n m ? i; rewrite lookup_fmap; apply (cmra_morphism_validN _).
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 029f0bfcf301661662a10e9c81eec9be392ec211..6013bdbeabdb69d1f8fdc9984f4aabf3d83c8914 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -38,12 +38,12 @@ Section gset.
Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
- Global Instance gset_cmra_discrete : CMRADiscrete gsetR.
+ Global Instance gset_cmra_discrete : CmraDiscrete gsetR.
Proof. apply discrete_cmra_discrete. Qed.
- Lemma gset_ucmra_mixin : UCMRAMixin (gset K).
+ Lemma gset_ucmra_mixin : UcmraMixin (gset K).
Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
- Canonical Structure gsetUR := UCMRAT (gset K) gset_ucmra_mixin.
+ Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
Lemma gset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
@@ -123,12 +123,12 @@ Section gset_disj.
Qed.
Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.
- Global Instance gset_disj_cmra_discrete : CMRADiscrete gset_disjR.
+ Global Instance gset_disj_cmra_discrete : CmraDiscrete gset_disjR.
Proof. apply discrete_cmra_discrete. Qed.
- Lemma gset_disj_ucmra_mixin : UCMRAMixin (gset_disj K).
+ Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
- Canonical Structure gset_disjUR := UCMRAT (gset_disj K) gset_disj_ucmra_mixin.
+ Canonical Structure gset_disjUR := UcmraT (gset_disj K) gset_disj_ucmra_mixin.
Arguments op _ _ _ _ : simpl never.
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 9b116b172fdecfd5591d40b8db8b9bc1bcb366b6..1f896d7814e99aeca219959f4e9694709d2c526f 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -100,7 +100,7 @@ Section iprod_cmra.
intros [h ?]%finite_choice. by exists h.
Qed.
- Lemma iprod_cmra_mixin : CMRAMixin (iprod B).
+ Lemma iprod_cmra_mixin : CmraMixin (iprod B).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -126,21 +126,21 @@ Section iprod_cmra.
exists (y1,y2); eauto. }
exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
Qed.
- Canonical Structure iprodR := CMRAT (iprod B) iprod_cmra_mixin.
+ Canonical Structure iprodR := CmraT (iprod B) iprod_cmra_mixin.
Instance iprod_unit : Unit (iprod B) := λ x, ε.
Definition iprod_lookup_empty x : ε x = ε := eq_refl.
- Lemma iprod_ucmra_mixin : UCMRAMixin (iprod B).
+ Lemma iprod_ucmra_mixin : UcmraMixin (iprod B).
Proof.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite iprod_lookup_op left_id.
- constructor=> x. apply persistent_core, _.
Qed.
- Canonical Structure iprodUR := UCMRAT (iprod B) iprod_ucmra_mixin.
+ Canonical Structure iprodUR := UcmraT (iprod B) iprod_ucmra_mixin.
- Global Instance iprod_empty_discrete :
+ Global Instance iprod_unit_discrete :
(∀ i, Discrete (ε : B i)) → Discrete (ε : iprod B).
Proof. intros ? f Hf x. by apply: discrete. Qed.
@@ -284,7 +284,7 @@ Instance iprod_map_ne `{Finite A} {B1 B2 : A → ofeT} (f : ∀ x, B1 x → B2 x
Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
Instance iprod_map_cmra_morphism
`{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
- (∀ x, CMRAMorphism (f x)) → CMRAMorphism (iprod_map f).
+ (∀ x, CmraMorphism (f x)) → CmraMorphism (iprod_map f).
Proof.
split; first apply _.
- intros n g Hg x; rewrite /iprod_map; apply (cmra_morphism_validN (f _)), Hg.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 6a647027fbddde744f200d5d90e64be2d28491ca..5afced0d314e9b3b5921c3ea62978c1826231fde 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -77,7 +77,7 @@ Next Obligation.
by rewrite Hcn.
Qed.
-Global Instance list_ofe_discrete : OFEDiscrete A → OFEDiscrete listC.
+Global Instance list_ofe_discrete : OfeDiscrete A → OfeDiscrete listC.
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
Global Instance nil_discrete : Discrete (@nil A).
@@ -186,7 +186,7 @@ Section cmra.
+ exists (core x :: l3); constructor; by rewrite ?cmra_core_r.
Qed.
- Definition list_cmra_mixin : CMRAMixin (list A).
+ Definition list_cmra_mixin : CmraMixin (list A).
Proof.
apply cmra_total_mixin.
- eauto.
@@ -219,19 +219,19 @@ Section cmra.
(cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
Qed.
- Canonical Structure listR := CMRAT (list A) list_cmra_mixin.
+ Canonical Structure listR := CmraT (list A) list_cmra_mixin.
Global Instance list_unit : Unit (list A) := [].
- Definition list_ucmra_mixin : UCMRAMixin (list A).
+ Definition list_ucmra_mixin : UcmraMixin (list A).
Proof.
split.
- constructor.
- by intros l.
- by constructor.
Qed.
- Canonical Structure listUR := UCMRAT (list A) list_ucmra_mixin.
+ Canonical Structure listUR := UcmraT (list A) list_ucmra_mixin.
- Global Instance list_cmra_discrete : CMRADiscrete A → CMRADiscrete listR.
+ Global Instance list_cmra_discrete : CmraDiscrete A → CmraDiscrete listR.
Proof.
split; [apply _|]=> l; rewrite list_lookup_valid list_lookup_validN=> Hl i.
by apply cmra_discrete_valid.
@@ -436,7 +436,7 @@ End properties.
(** Functor *)
Instance list_fmap_cmra_morphism {A B : ucmraT} (f : A → B)
- `{!CMRAMorphism f} : CMRAMorphism (fmap f : list A → list B).
+ `{!CmraMorphism f} : CmraMorphism (fmap f : list A → list B).
Proof.
split; try apply _.
- intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 8667cbe679c71571e1c9cdbf7f304abdf86e5c67..3b4a36ff495fd90af3843b8f09f610997c9bdf1f 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -31,7 +31,7 @@ Section updates.
intros Hv n mz Hxv Hx; simpl in *; split; [by auto|].
by rewrite Hx -cmra_opM_assoc.
Qed.
- Lemma op_local_update_discrete `{!CMRADiscrete A} x y z :
+ Lemma op_local_update_discrete `{!CmraDiscrete A} x y z :
(✓ x → ✓ (z ⋅ x)) → (x,y) ~l~> (z ⋅ x, z ⋅ y).
Proof.
intros; apply op_local_update=> n. by rewrite -!(cmra_discrete_valid_iff n).
@@ -52,7 +52,7 @@ Section updates.
apply (cancelableN x); first done. by rewrite -cmra_opM_assoc.
Qed.
- Lemma local_update_discrete `{!CMRADiscrete A} (x y x' y' : A) :
+ Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
(x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
Proof.
rewrite /local_update /=. setoid_rewrite <-cmra_discrete_valid_iff.
@@ -72,7 +72,7 @@ Section updates.
+ right. exists z. apply dist_le with n; auto with lia.
+ left. apply dist_le with n; auto with lia.
Qed.
- Lemma local_update_valid `{!CMRADiscrete A} x y x' y' :
+ Lemma local_update_valid `{!CmraDiscrete A} x y x' y' :
(✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
Proof.
rewrite !(cmra_discrete_valid_iff 0)
@@ -80,13 +80,13 @@ Section updates.
apply local_update_valid0.
Qed.
- Lemma local_update_total_valid0 `{!CMRATotal A} x y x' y' :
+ Lemma local_update_total_valid0 `{!CmraTotal A} x y x' y' :
(✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
Proof.
intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
by rewrite Hx.
Qed.
- Lemma local_update_total_valid `{!CMRATotal A, !CMRADiscrete A} x y x' y' :
+ Lemma local_update_total_valid `{!CmraTotal A, !CmraDiscrete A} x y x' y' :
(✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
Proof.
rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
@@ -108,7 +108,7 @@ Section updates_unital.
rewrite -(right_id ε op y) -(right_id ε op y'). auto.
Qed.
- Lemma local_update_unital_discrete `{!CMRADiscrete A} (x y x' y' : A) :
+ Lemma local_update_unital_discrete `{!CmraDiscrete A} (x y x' y' : A) :
(x,y) ~l~> (x',y') ↔ ∀ z, ✓ x → x ≡ y ⋅ z → ✓ x' ∧ x' ≡ y' ⋅ z.
Proof.
rewrite local_update_discrete. split.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index e4defa69a3b2adbfa58b96c092b2219f58e498ad..9997c5c4bae25b969a73c9ff488296b0ca942d1e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -63,7 +63,7 @@ Arguments ofe_mixin : simpl never.
(** When declaring instances of subclasses of OFE (like CMRAs and unital CMRAs)
we need Coq to *infer* the canonical OFE instance of a given type and take the
mixin out of it. This makes sure we do not use two different OFE instances in
-different places (see for example the constructors [CMRAT] and [UCMRAT] in the
+different places (see for example the constructors [CmraT] and [UcmraT] in the
file [cmra.v].)
In order to infer the OFE instance, we use the definition [ofe_mixin_of'] which
@@ -105,8 +105,7 @@ Arguments discrete {_} _ {_} _ _.
Hint Mode Discrete + ! : typeclass_instances.
Instance: Params (@Discrete) 1.
-Class OFEDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
-Hint Mode OFEDiscrete ! : typeclass_instances.
+Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
(** OFEs with a completion *)
Record chain (A : ofeT) := {
@@ -651,7 +650,7 @@ Section unit.
Global Program Instance unit_cofe : Cofe unitC := { compl x := () }.
Next Obligation. by repeat split; try exists 0. Qed.
- Global Instance unit_ofe_discrete : OFEDiscrete unitC.
+ Global Instance unit_ofe_discrete : OfeDiscrete unitC.
Proof. done. Qed.
End unit.
@@ -684,7 +683,8 @@ Section product.
Global Instance prod_discrete (x : A * B) :
Discrete (x.1) → Discrete (x.2) → Discrete x.
Proof. by intros ???[??]; split; apply (discrete _). Qed.
- Global Instance prod_ofe_discrete : OFEDiscrete A → OFEDiscrete B → OFEDiscrete prodC.
+ Global Instance prod_ofe_discrete :
+ OfeDiscrete A → OfeDiscrete B → OfeDiscrete prodC.
Proof. intros ?? [??]; apply _. Qed.
End product.
@@ -866,7 +866,8 @@ Section sum.
Proof. inversion_clear 2; constructor; by apply (discrete _). Qed.
Global Instance inr_discrete (y : B) : Discrete y → Discrete (inr y).
Proof. inversion_clear 2; constructor; by apply (discrete _). Qed.
- Global Instance sum_ofe_discrete : OFEDiscrete A → OFEDiscrete B → OFEDiscrete sumC.
+ Global Instance sum_ofe_discrete :
+ OfeDiscrete A → OfeDiscrete B → OfeDiscrete sumC.
Proof. intros ?? [?|?]; apply _. Qed.
End sum.
@@ -921,7 +922,7 @@ Section discrete_ofe.
- done.
Qed.
- Global Instance discrete_ofe_discrete : OFEDiscrete (OfeT A discrete_ofe_mixin).
+ Global Instance discrete_ofe_discrete : OfeDiscrete (OfeT A discrete_ofe_mixin).
Proof. by intros x y. Qed.
Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
@@ -990,7 +991,7 @@ Section option.
destruct (c n); naive_solver.
Qed.
- Global Instance option_ofe_discrete : OFEDiscrete A → OFEDiscrete optionC.
+ Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionC.
Proof. destruct 2; constructor; by apply (discrete _). Qed.
Global Instance Some_ne : NonExpansive (@Some A).
@@ -1224,7 +1225,7 @@ Section sigma.
Global Instance sig_discrete (x : sig P) : Discrete (`x) → Discrete x.
Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (discrete _). Qed.
- Global Instance sig_ofe_discrete : OFEDiscrete A → OFEDiscrete sigC.
+ Global Instance sig_ofe_discrete : OfeDiscrete A → OfeDiscrete sigC.
Proof. intros ??. apply _. Qed.
End sigma.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 0ef2608f45d5126ae9b65931113e454ded8e3460..9af05124e77df42fa22e04df6c0bbc855f03281d 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -8,13 +8,13 @@ Local Arguments core _ _ !_ /.
(** * Definition of STSs *)
Module sts.
-Structure stsT := STS {
+Structure stsT := Sts {
state : Type;
token : Type;
prim_step : relation state;
tok : state → set token;
}.
-Arguments STS {_ _} _ _.
+Arguments Sts {_ _} _ _.
Arguments prim_step {_} _ _.
Arguments tok {_} _.
Notation states sts := (set (state sts)).
@@ -177,7 +177,7 @@ Arguments frag {_} _ _.
End sts.
Notation stsT := sts.stsT.
-Notation STS := sts.STS.
+Notation Sts := sts.Sts.
(** * STSs form a disjoint RA *)
Section sts_dra.
@@ -232,7 +232,7 @@ Proof.
- by destruct 1; constructor.
- destruct 1; inversion_clear 1; constructor; etrans; eauto.
Qed.
-Lemma sts_dra_mixin : DRAMixin (car sts).
+Lemma sts_dra_mixin : DraMixin (car sts).
Proof.
split.
- apply _.
@@ -266,7 +266,7 @@ Proof.
unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
end; auto with sts.
Qed.
-Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
+Canonical Structure stsDR : draT := DraT (car sts) sts_dra_mixin.
End sts_dra.
(** * The STS Resource Algebra *)
@@ -442,11 +442,11 @@ End stsRA.
(** STSs without tokens: Some stuff is simpler *)
Module sts_notok.
-Structure stsT := STS {
+Structure stsT := Sts {
state : Type;
prim_step : relation state;
}.
-Arguments STS {_} _.
+Arguments Sts {_} _.
Arguments prim_step {_} _ _.
Notation states sts := (set (state sts)).
@@ -454,7 +454,7 @@ Definition stsT_token := Empty_set.
Definition stsT_tok {sts : stsT} (_ : state sts) : set stsT_token := ∅.
Canonical Structure sts_notok (sts : stsT) : sts.stsT :=
- sts.STS (@prim_step sts) stsT_tok.
+ sts.Sts (@prim_step sts) stsT_tok.
Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
Section sts.
@@ -486,7 +486,7 @@ End sts.
End sts_notok.
Notation sts_notokT := sts_notok.stsT.
-Notation STS_NoTok := sts_notok.STS.
+Notation Sts_NoTok := sts_notok.Sts.
Section sts_notokRA.
Context {sts : sts_notokT}.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 20bbe63b8851ca8584534ba7056efc3cdb3f9646..169b78a66aea71c24160702ae82502477cf9fb16 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -87,7 +87,7 @@ Qed.
(** ** Frame preserving updates for total CMRAs *)
Section total_updates.
Local Set Default Proof Using "Type*".
- Context `{CMRATotal A}.
+ Context `{CmraTotal A}.
Lemma cmra_total_updateP x (P : A → Prop) :
x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
@@ -100,7 +100,7 @@ Section total_updates.
Lemma cmra_total_update x y : x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.
- Context `{CMRADiscrete A}.
+ Context `{CmraDiscrete A}.
Lemma cmra_discrete_updateP (x : A) (P : A → Prop) :
x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index f8cfc7b0b1dabe5b6ae1ffee9c5a087dec9cbc1f..7250ce400546401f18b69a2a24d32c92b87d0401 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -29,7 +29,7 @@ Section ofe.
intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
constructor. by apply discrete. change (v ≡ v'). by apply discrete.
Qed.
- Global Instance vec_ofe_discrete m : OFEDiscrete A → OFEDiscrete (vecC m).
+ Global Instance vec_ofe_discrete m : OfeDiscrete A → OfeDiscrete (vecC m).
Proof. intros ? v. induction v; apply _. Qed.
End ofe.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 521b4598996fde95af37f36ff0230dcb2cad4048..7d16acabc2e1a6224b8eae828858df4f6def8dcb 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -801,7 +801,7 @@ Global Instance pure_timeless φ : TimelessP (⌜φ⌠: uPred M)%I.
Proof.
rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
Qed.
-Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
+Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
TimelessP (✓ a : uPred M)%I.
Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed.
Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index a46400ae92ae9902edfae933fc43ff3a7794bc90..dbabe9361c168e31dccf4cc2fe27230786649df0 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -9,11 +9,11 @@ Import uPred.
(* The CMRA we need. *)
Class authG Σ (A : ucmraT) := AuthG {
auth_inG :> inG Σ (authR A);
- auth_discrete :> CMRADiscrete A;
+ auth_cmra_discrete :> CmraDiscrete A;
}.
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
-Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
+Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
Proof. solve_inG. Qed.
Section definitions.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 3a180f3e1c6b9e742ff6cab9046c91141df3ce0f..4a6159998d90515a39563e82930ad9ff9ae712d7 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -561,7 +561,7 @@ Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y)
Proof. by unseal. Qed.
(* Discrete *)
-Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
Proof.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 4888c302f4d5a661b95e3c5894050e76a43d2d81..801608cd705f7fd80e77f93296d92d0dc5947fe6 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -93,13 +93,13 @@ Qed.
(** functor *)
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
- `{!CMRAMorphism f} (P : uPred M1) :
+ `{!CmraMorphism f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
Next Obligation. naive_solver eauto using uPred_closed, cmra_morphism_validN. Qed.
Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
- `{!CMRAMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
+ `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
intros x1 x2 Hx; split=> n' y ??.
split; apply Hx; auto using cmra_morphism_validN.
@@ -107,17 +107,17 @@ Qed.
Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
Proof. by split=> n x ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
- `{!CMRAMorphism f, !CMRAMorphism g} (P : uPred M3):
+ `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
Proof. by split=> n x Hx. Qed.
Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
- `{!CMRAMorphism f} `{!CMRAMorphism g}:
+ `{!CmraMorphism f} `{!CmraMorphism g}:
(∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CMRAMorphism f} :
+Definition uPredC_map {M1 M2 : ucmraT} (f : M2 -n> M1) `{!CmraMorphism f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
Lemma uPredC_map_ne {M1 M2 : ucmraT} (f g : M2 -n> M1)
- `{!CMRAMorphism f, !CMRAMorphism g} n :
+ `{!CmraMorphism f, !CmraMorphism g} n :
f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
Proof.
by intros Hfg P; split=> n' y ??;
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 18f94ea6914281e03acd6c5b4ae25b747d32e3b9..ea43fb10b9a93040c2ebea221fbaf09d50179f37 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -44,7 +44,7 @@ Proof. done. Qed.
Global Instance into_pure_eq {A : ofeT} (a b : A) :
Discrete a → @IntoPure M (a ≡ b) (a ≡ b).
Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
-Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
+Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
@IntoPure M (✓ a) (✓ a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 5896d63912131dc0e63bc5e214243e58859f496c..9ecd34931ad5d887492af49a7f5bfb8c08260b51 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -152,15 +152,15 @@ Section M.
Qed.
Canonical Structure M_R : cmraT := discreteR M M_ra_mixin.
- Global Instance M_cmra_discrete : CMRADiscrete M_R.
+ Global Instance M_discrete : CmraDiscrete M_R.
Proof. apply discrete_cmra_discrete. Qed.
- Definition M_ucmra_mixin : UCMRAMixin M.
+ Definition M_ucmra_mixin : UcmraMixin M.
Proof.
split; try (done || apply _).
intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
Qed.
- Canonical Structure M_UR : ucmraT := UCMRAT M M_ucmra_mixin.
+ Canonical Structure M_UR : ucmraT := UcmraT M M_ucmra_mixin.
Global Instance frag_persistent n : Persistent (Frag n).
Proof. by constructor. Qed.