diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 846d12bbf5a9871b8f45c5b1859d82d1b5c842ce..2a6b94f843a2ed2088fbe2878ae405a9aa8e29fa 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,19 +142,19 @@ 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_persistent (x : agree A) : Persistent x.
+Global Instance agree_cmra_total : CmraTotal agreeR.
+Proof. rewrite /CmraTotal; eauto. Qed.
+Global Instance agree_core_id (x : agree A) : CoreId x.
Proof. by constructor. Qed.
-Global Instance agree_discrete : Discrete 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 <-(timeless_iff_0 _ _); auto.
+ - intros x y [H H'] n; split=> a; setoid_rewrite <-(discrete_iff_0 _ _); auto.
- intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??.
- apply timeless_iff_0; auto.
+ apply discrete_iff_0; auto.
Qed.
Program Definition to_agree (a : A) : agree A :=
@@ -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 0ac73f70e4c73610c06d49fdb4a36f928667f0e5..992400cac2f4e44a79c8b626d6ed7bf786df4e37 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -49,10 +49,10 @@ Proof.
(λ x, (authoritative x, auth_own x))); by repeat intro.
Qed.
-Global Instance Auth_timeless a b :
- Timeless a → Timeless b → Timeless (Auth a b).
-Proof. by intros ?? [??] [??]; split; apply: timeless. Qed.
-Global Instance auth_discrete : Discrete A → Discrete authC.
+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.
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,17 +178,17 @@ 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 _).
+ - do 2 constructor; simpl; apply (core_id_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.
+Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
+Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
@@ -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 85c785d24d6ff2e084411bfd2781874d4d2bebc2..b6c22f5ba318be9dae79d2b19d144a26013b32f1 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).
@@ -142,11 +142,11 @@ Definition opM {A : cmraT} (x : A) (my : option A) :=
match my with Some y => x â‹… y | None => x end.
Infix "â‹…?" := opM (at level 50, left associativity) : C_scope.
-(** * Persistent elements *)
-Class Persistent {A : cmraT} (x : A) := persistent : pcore x ≡ Some x.
-Arguments persistent {_} _ {_}.
-Hint Mode Persistent + ! : typeclass_instances.
-Instance: Params (@Persistent) 1.
+(** * CoreId elements *)
+Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
+Arguments core_id {_} _ {_}.
+Hint Mode CoreId + ! : typeclass_instances.
+Instance: Params (@CoreId) 1.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
@@ -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 :> Discrete 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;
@@ -316,7 +316,7 @@ Proof. destruct 2; by ofe_subst. Qed.
Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
Proof. destruct 2; by setoid_subst. Qed.
-Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent A).
+Global Instance CoreId_proper : Proper ((≡) ==> iff) (@CoreId A).
Proof. solve_proper. Qed.
Global Instance Exclusive_proper : Proper ((≡) ==> iff) (@Exclusive A).
Proof. intros x y Hxy. rewrite /Exclusive. by setoid_rewrite Hxy. Qed.
@@ -361,8 +361,8 @@ Proof.
intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
-(** ** Persistent elements *)
-Lemma persistent_dup x `{!Persistent x} : x ≡ x ⋅ x.
+(** ** CoreId elements *)
+Lemma core_id_dup x `{!CoreId x} : x ≡ x ⋅ x.
Proof. by apply cmra_pcore_dup' with x. Qed.
(** ** Exclusive elements *)
@@ -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.
@@ -498,19 +498,19 @@ Section total_core.
Lemma cmra_core_valid x : ✓ x → ✓ core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
- Lemma persistent_total x : Persistent x ↔ core x ≡ x.
+ Lemma core_id_total x : CoreId x ↔ core x ≡ x.
Proof.
- split; [intros; by rewrite /core /= (persistent x)|].
- rewrite /Persistent /core /=.
+ split; [intros; by rewrite /core /= (core_id x)|].
+ rewrite /CoreId /core /=.
destruct (cmra_total x) as [? ->]. by constructor.
Qed.
- Lemma persistent_core x `{!Persistent x} : core x ≡ x.
- Proof. by apply persistent_total. Qed.
+ Lemma core_id_core x `{!CoreId x} : core x ≡ x.
+ Proof. by apply core_id_total. Qed.
- Global Instance cmra_core_persistent x : Persistent (core x).
+ Global Instance cmra_core_core_id x : CoreId (core x).
Proof.
destruct (cmra_total x) as [cx Hcx].
- rewrite /Persistent /core /= Hcx /=. eauto using cmra_pcore_idemp.
+ rewrite /CoreId /core /= Hcx /=. eauto using cmra_pcore_idemp.
Qed.
Lemma cmra_included_core x : core x ≼ x.
@@ -530,34 +530,34 @@ Section total_core.
Qed.
End total_core.
-(** ** Timeless *)
-Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
+(** ** Discrete *)
+Lemma cmra_discrete_included_l x y : Discrete x → ✓{0} y → x ≼{0} y → x ≼ y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
- by exists z'; rewrite Hy (timeless x z).
+ by exists z'; rewrite Hy (discrete x z).
Qed.
-Lemma cmra_timeless_included_r x y : Timeless y → x ≼{0} y → x ≼ y.
-Proof. intros ? [x' ?]. exists x'. by apply (timeless y). Qed.
-Lemma cmra_op_timeless x1 x2 :
- ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
+Lemma cmra_discrete_included_r x y : Discrete y → x ≼{0} y → x ≼ y.
+Proof. intros ? [x' ?]. exists x'. by apply (discrete y). Qed.
+Lemma cmra_op_discrete x1 x2 :
+ ✓ (x1 ⋅ x2) → Discrete x1 → Discrete x2 → Discrete (x1 ⋅ x2).
Proof.
intros ??? z Hz.
destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
{ rewrite -?Hz. by apply cmra_valid_validN. }
- by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
+ by rewrite Hz' (discrete x1 y1) // (discrete x2 y2).
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 `{Discrete 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 ->%(timeless_iff _ _)]; eauto using cmra_included_l.
+ intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
(** Cancelable elements *)
@@ -565,9 +565,9 @@ 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 -!timeless_iff -cmra_discrete_valid_iff. auto. Qed.
+Proof. intros ????. rewrite -!discrete_iff -cmra_discrete_valid_iff. auto. Qed.
Global Instance cancelable_op x y :
Cancelable x → Cancelable y → Cancelable (x ⋅ y).
Proof.
@@ -595,9 +595,11 @@ 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. repeat intro. eauto using cmra_discrete_valid, cmra_discrete, timeless. Qed.
+Proof.
+ intros Hx y ??. apply (Hx y), (discrete _); eauto using cmra_discrete_valid.
+Qed.
Global Instance id_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y).
Proof.
intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
@@ -622,13 +624,13 @@ Section ucmra.
Proof. by exists x; rewrite left_id. Qed.
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_core_id : CoreId (ε: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)).
+ eauto using ucmra_unit_least, (core_id (ε:A)).
Qed.
Global Instance empty_cancelable : Cancelable (ε:A).
Proof. intros ???. by rewrite !left_id. Qed.
@@ -637,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.
@@ -664,13 +666,13 @@ Section cmra_leibniz.
Lemma cmra_pcore_dup_L x cx : pcore x = Some cx → cx = cx ⋅ cx.
Proof. unfold_leibniz. apply cmra_pcore_dup'. Qed.
- (** ** Persistent elements *)
- Lemma persistent_dup_L x `{!Persistent x} : x = x â‹… x.
- Proof. unfold_leibniz. by apply persistent_dup. Qed.
+ (** ** CoreId elements *)
+ Lemma core_id_dup_L x `{!CoreId x} : x = x â‹… x.
+ Proof. unfold_leibniz. by apply core_id_dup. Qed.
(** ** 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.
@@ -680,10 +682,10 @@ Section cmra_leibniz.
Proof. unfold_leibniz. apply cmra_core_idemp. Qed.
Lemma cmra_core_dup_L x : core x = core x â‹… core x.
Proof. unfold_leibniz. apply cmra_core_dup. Qed.
- Lemma persistent_total_L x : Persistent x ↔ core x = x.
- Proof. unfold_leibniz. apply persistent_total. Qed.
- Lemma persistent_core_L x `{!Persistent x} : core x = x.
- Proof. by apply persistent_total_L. Qed.
+ Lemma core_id_total_L x : CoreId x ↔ core x = x.
+ Proof. unfold_leibniz. apply core_id_total. Qed.
+ Lemma core_id_core_L x `{!CoreId x} : core x = x.
+ Proof. by apply core_id_total_L. Qed.
End total_core.
End cmra_leibniz.
@@ -716,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 /=.
@@ -730,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 _.
@@ -746,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.
@@ -769,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.
@@ -802,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.
@@ -843,9 +845,9 @@ Section cmra_transport.
Proof. by destruct H. Qed.
Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x.
Proof. by destruct H. Qed.
- Global Instance cmra_transport_timeless x : Timeless x → Timeless (T x).
+ Global Instance cmra_transport_discrete x : Discrete x → Discrete (T x).
Proof. by destruct H. Qed.
- Global Instance cmra_transport_persistent x : Persistent x → Persistent (T x).
+ Global Instance cmra_transport_core_id x : CoreId x → CoreId (T x).
Proof. by destruct H. Qed.
End cmra_transport.
@@ -874,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).
@@ -882,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.
@@ -925,18 +927,18 @@ 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.
+ Global Instance unit_core_id (x : ()) : CoreId x.
Proof. by constructor. Qed.
Global Instance unit_cancelable (x : ()) : Cancelable x.
Proof. by constructor. Qed.
@@ -961,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.
@@ -999,14 +1001,14 @@ 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.
+ Global Instance mnat_core_id (x : mnat) : CoreId x.
Proof. by constructor. Qed.
End mnat.
@@ -1028,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.
@@ -1076,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.
@@ -1105,24 +1107,24 @@ 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 :
- Persistent x → Persistent y → Persistent (x,y).
- Proof. by rewrite /Persistent prod_pcore_Some'. Qed.
+ Global Instance pair_core_id x y :
+ CoreId x → CoreId y → CoreId (x,y).
+ Proof. by rewrite /CoreId prod_pcore_Some'. Qed.
Global Instance pair_exclusive_l x y : Exclusive x → Exclusive (x,y).
Proof. by intros ?[][?%exclusive0_l]. Qed.
@@ -1145,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 _).
+ - rewrite prod_pcore_Some'; split; apply (core_id _).
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.
@@ -1165,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.
@@ -1243,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.
@@ -1278,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.
@@ -1310,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.
@@ -1326,10 +1328,10 @@ Section option.
Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
- Global Instance Some_persistent (x : A) : Persistent x → Persistent (Some x).
+ Global Instance Some_core_id (x : A) : CoreId x → CoreId (Some x).
Proof. by constructor. Qed.
- Global Instance option_persistent (mx : option A) :
- (∀ x : A, Persistent x) → Persistent mx.
+ Global Instance option_core_id (mx : option A) :
+ (∀ x : A, CoreId x) → CoreId mx.
Proof. intros. destruct mx; apply _. Qed.
Lemma exclusiveN_Some_l n x `{!Exclusive x} my :
@@ -1351,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 :
@@ -1390,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 41643dfc98abf09ecccaa6dcc5784fd7ba1d183d..f330344a0cdb00d86ee640574af8a206a360d019 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -96,16 +96,17 @@ Next Obligation.
+ rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
Qed.
-Global Instance csum_discrete : Discrete A → Discrete B → Discrete csumC.
-Proof. by inversion_clear 3; constructor; apply (timeless _). Qed.
+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).
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
-Global Instance Cinl_timeless a : Timeless a → Timeless (Cinl a).
-Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
-Global Instance Cinr_timeless b : Timeless b → Timeless (Cinr b).
-Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
+Global Instance Cinl_discrete a : Discrete a → Discrete (Cinl a).
+Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
+Global Instance Cinr_discrete b : Discrete b → Discrete (Cinr b).
+Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
End cofe.
Arguments csumC : clear implicits.
@@ -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,19 +247,19 @@ 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.
Qed.
-Global Instance Cinl_persistent a : Persistent a → Persistent (Cinl a).
-Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
-Global Instance Cinr_persistent b : Persistent b → Persistent (Cinr b).
-Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
+Global Instance Cinl_core_id a : CoreId a → CoreId (Cinl a).
+Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
+Global Instance Cinr_core_id b : CoreId b → CoreId (Cinr b).
+Proof. rewrite /CoreId /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a).
Proof. by move=> H[]? =>[/H||]. Qed.
@@ -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..ccb061003a11268da2e5b9a0a00005785188da77 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -50,13 +50,13 @@ 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 *)
-Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
+Global Instance dec_agree_core_id (x : dec_agreeR) : CoreId x.
Proof. by constructor. Qed.
Lemma dec_agree_ne a b : a ≠b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
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 1c71576e7004518a3f745da96d5981d45d24aa1c..b73aaa01e635b775c07fb9e40d0a71903b410877 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -59,14 +59,14 @@ Proof.
- by intros []; constructor.
Qed.
-Global Instance excl_discrete : Discrete A → Discrete exclC.
-Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
+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.
-Global Instance Excl_timeless a : Timeless a → Timeless (Excl a).
-Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
-Global Instance ExclBot_timeless : Timeless (@ExclBot A).
+Global Instance Excl_discrete a : Discrete a → Discrete (Excl a).
+Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
+Global Instance ExclBot_discrete : Discrete (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
(* CMRA *)
@@ -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 : Discrete 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 3107f83315202e05eb579e07c5a39c0b402a34fe..3f65239d370aa0d8241d9e0dc3ac7f9d6de51de1 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -34,10 +34,10 @@ Section frac_auth.
Global Instance frac_auth_frag_proper q : Proper ((≡) ==> (≡)) (@frac_auth_frag A q).
Proof. solve_proper. Qed.
- Global Instance frac_auth_auth_timeless a : Timeless a → Timeless (â—! a).
- Proof. intros; apply Auth_timeless; apply _. Qed.
- Global Instance frac_auth_frag_timeless a : Timeless a → Timeless (◯! a).
- Proof. intros; apply Auth_timeless, Some_timeless; apply _. Qed.
+ Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (â—! a).
+ Proof. intros; apply Auth_discrete; apply _. Qed.
+ Global Instance frac_auth_frag_discrete a : Discrete a → Discrete (◯! a).
+ Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (â—! a â‹… â—¯! a).
Proof. done. Qed.
@@ -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.
@@ -94,10 +94,10 @@ Section frac_auth.
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
- Persistent a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
+ CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
- by rewrite -frag_auth_op -persistent_dup.
+ by rewrite -frag_auth_op -core_id_dup.
Qed.
Lemma frac_auth_update q a b a' b' :
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 2c31f3ee618e91f794a3c0bca0d6693f9597784f..a09b287e85b6afdfd71b15e2226985ae528e6e50 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -37,8 +37,8 @@ Next Obligation.
by rewrite conv_compl /=; apply reflexive_eq.
Qed.
-Global Instance gmap_discrete : Discrete A → Discrete gmapC.
-Proof. intros ? m m' ? i. by apply (timeless _). Qed.
+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.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
@@ -70,27 +70,27 @@ Proof.
[by constructor|by apply lookup_ne].
Qed.
-Global Instance gmap_empty_timeless : Timeless (∅ : gmap K A).
+Global Instance gmap_empty_discrete : Discrete (∅ : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
inversion_clear Hm; constructor.
Qed.
-Global Instance gmap_lookup_timeless m i : Timeless m → Timeless (m !! i).
+Global Instance gmap_lookup_discrete m i : Discrete m → Discrete (m !! i).
Proof.
- intros ? [x|] Hx; [|by symmetry; apply: timeless].
+ intros ? [x|] Hx; [|by symmetry; apply: discrete].
assert (m ≡{0}≡ <[i:=x]> m)
by (by symmetry in Hx; inversion Hx; ofe_subst; rewrite insert_id).
- by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
+ by rewrite (discrete m (<[i:=x]>m)) // lookup_insert.
Qed.
-Global Instance gmap_insert_timeless m i x :
- Timeless x → Timeless m → Timeless (<[i:=x]>m).
+Global Instance gmap_insert_discrete m i x :
+ Discrete x → Discrete m → Discrete (<[i:=x]>m).
Proof.
intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
- { by apply: timeless; rewrite -Hm lookup_insert. }
- by apply: timeless; rewrite -Hm lookup_insert_ne.
+ { by apply: discrete; rewrite -Hm lookup_insert. }
+ by apply: discrete; rewrite -Hm lookup_insert_ne.
Qed.
-Global Instance gmap_singleton_timeless i x :
- Timeless x → Timeless ({[ i := x ]} : gmap K A) := _.
+Global Instance gmap_singleton_discrete i x :
+ Discrete x → Discrete ({[ i := x ]} : gmap K A) := _.
End cofe.
Arguments 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).
@@ -250,14 +250,14 @@ Lemma op_singleton (i : K) (x y : A) :
{[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
-Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m.
+Global Instance gmap_core_id m : (∀ x : A, CoreId x) → CoreId m.
Proof.
- intros; apply persistent_total=> i.
- rewrite lookup_core. apply (persistent_core _).
+ intros; apply core_id_total=> i.
+ rewrite lookup_core. apply (core_id_core _).
Qed.
-Global Instance gmap_singleton_persistent i (x : A) :
- Persistent x → Persistent {[ i := x ]}.
-Proof. intros. by apply persistent_total, core_singleton'. Qed.
+Global Instance gmap_singleton_core_id i (x : A) :
+ CoreId x → CoreId {[ i := x ]}.
+Proof. intros. by apply core_id_total, core_singleton'. Qed.
Lemma singleton_includedN n m i x :
{[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ Some x ≼{n} Some y.
@@ -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..6842ddfb2cad1438af2b3be20b2ecd902525b680 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.
@@ -58,8 +58,8 @@ Section gset.
split. done. rewrite gset_op_union. set_solver.
Qed.
- Global Instance gset_persistent X : Persistent X.
- Proof. by apply persistent_total; rewrite gset_core_self. Qed.
+ Global Instance gset_core_id X : CoreId X.
+ Proof. by apply core_id_total; rewrite gset_core_self. Qed.
End gset.
Arguments gsetC _ {_ _}.
@@ -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 60fb8fea49074d4db4f0502b755ecd2c76f652f7..e3051d27f9b7e4d4fc730c14eb8ac68afde98794 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -61,22 +61,22 @@ Section iprod_cofe.
x ≠x' → (iprod_insert x y f) x' = f x'.
Proof. by rewrite /iprod_insert; destruct (decide _). Qed.
- Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x).
+ Global Instance iprod_lookup_discrete f x : Discrete f → Discrete (f x).
Proof.
intros ? y ?.
cut (f ≡ iprod_insert x y f).
{ by move=> /(_ x)->; rewrite iprod_lookup_insert. }
- apply (timeless _)=> x'; destruct (decide (x = x')) as [->|];
+ apply (discrete _)=> x'; destruct (decide (x = x')) as [->|];
by rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
Qed.
- Global Instance iprod_insert_timeless f x y :
- Timeless f → Timeless y → Timeless (iprod_insert x y f).
+ Global Instance iprod_insert_discrete f x y :
+ Discrete f → Discrete y → Discrete (iprod_insert x y f).
Proof.
intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
- rewrite iprod_lookup_insert.
- apply: timeless. by rewrite -(Heq x') iprod_lookup_insert.
+ apply: discrete. by rewrite -(Heq x') iprod_lookup_insert.
- rewrite iprod_lookup_insert_ne //.
- apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne.
+ apply: discrete. by rewrite -(Heq x') iprod_lookup_insert_ne.
Qed.
End iprod_cofe.
@@ -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,23 +126,23 @@ 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, _.
+ - constructor=> x. apply core_id_core, _.
Qed.
- Canonical Structure iprodUR := UCMRAT (iprod B) iprod_ucmra_mixin.
+ Canonical Structure iprodUR := UcmraT (iprod B) iprod_ucmra_mixin.
- Global Instance iprod_empty_timeless :
- (∀ i, Timeless (ε : B i)) → Timeless (ε : iprod B).
- Proof. intros ? f Hf x. by apply: timeless. Qed.
+ Global Instance iprod_unit_discrete :
+ (∀ i, Discrete (ε : B i)) → Discrete (ε : iprod B).
+ Proof. intros ? f Hf x. by apply: discrete. Qed.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
@@ -198,8 +198,8 @@ Section iprod_singleton.
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).
+ Global Instance iprod_singleton_discrete x (y : B x) :
+ (∀ i, Discrete (ε : B i)) → Discrete y → Discrete (iprod_singleton x y).
Proof. apply _. Qed.
Lemma iprod_singleton_validN n x (y : B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
@@ -215,12 +215,12 @@ Section iprod_singleton.
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite iprod_lookup_core ?iprod_lookup_singleton
- ?iprod_lookup_singleton_ne // (persistent_core ∅).
+ ?iprod_lookup_singleton_ne // (core_id_core ∅).
Qed.
- Global Instance iprod_singleton_persistent x (y : B x) :
- Persistent y → Persistent (iprod_singleton x y).
- Proof. by rewrite !persistent_total iprod_core_singleton=> ->. Qed.
+ Global Instance iprod_singleton_core_id x (y : B x) :
+ CoreId y → CoreId (iprod_singleton x y).
+ Proof. by rewrite !core_id_total iprod_core_singleton=> ->. Qed.
Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
@@ -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 5f42e37e0e6ee17f7ee4180133df99044878b5b1..ed4736a1875450294db3b1b7474a06c9357e0fe8 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -77,13 +77,13 @@ Next Obligation.
by rewrite Hcn.
Qed.
-Global Instance list_discrete : Discrete A → Discrete listC.
-Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
+Global Instance list_ofe_discrete : OfeDiscrete A → OfeDiscrete listC.
+Proof. induction 2; constructor; try apply (discrete _); auto. Qed.
-Global Instance nil_timeless : Timeless (@nil A).
+Global Instance nil_discrete : Discrete (@nil A).
Proof. inversion_clear 1; constructor. Qed.
-Global Instance cons_timeless x l : Timeless x → Timeless l → Timeless (x :: l).
-Proof. intros ??; inversion_clear 1; constructor; by apply timeless. Qed.
+Global Instance cons_discrete x l : Discrete x → Discrete l → Discrete (x :: l).
+Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
End cofe.
Arguments listC : clear implicits.
@@ -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,28 +219,28 @@ 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.
Qed.
- Global Instance list_persistent l : (∀ x : A, Persistent x) → Persistent l.
+ Global Instance list_core_id l : (∀ x : A, CoreId x) → CoreId l.
Proof.
intros ?; constructor; apply list_equiv_lookup=> i.
- by rewrite list_lookup_core (persistent_core (l !! i)).
+ by rewrite list_lookup_core (core_id_core (l !! i)).
Qed.
(** Internalized properties *)
@@ -329,7 +329,7 @@ Section properties.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
Proof.
rewrite /singletonM /list_singletonM.
- by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅).
+ by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
Qed.
Lemma list_op_singletonM i (x y : A) :
{[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
@@ -342,9 +342,9 @@ Section properties.
Proof.
rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
Qed.
- Global Instance list_singleton_persistent i (x : A) :
- Persistent x → Persistent {[ i := x ]}.
- Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
+ Global Instance list_singleton_core_id i (x : A) :
+ CoreId x → CoreId {[ i := x ]}.
+ Proof. by rewrite !core_id_total list_core_singletonM=> ->. Qed.
(* Update *)
Lemma list_singleton_updateP (P : A → Prop) (Q : list A → Prop) x :
@@ -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 0884225f3b561241b8e7107bb7d48be3fae563a2..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,12 +52,12 @@ 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.
- setoid_rewrite <-(λ n, timeless_iff n x).
- setoid_rewrite <-(λ n, timeless_iff n x'). naive_solver eauto using 0.
+ setoid_rewrite <-(λ n, discrete_iff n x).
+ setoid_rewrite <-(λ n, discrete_iff n x'). naive_solver eauto using 0.
Qed.
Lemma local_update_valid0 x y x' y' :
@@ -72,21 +72,21 @@ 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)
- (cmra_discrete_included_iff 0) (timeless_iff 0).
+ (cmra_discrete_included_iff 0) (discrete_iff 0).
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 09992145e4c8b7a37df90e332cdc880d8143e516..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
@@ -99,16 +99,13 @@ End ofe_mixin.
Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
-(** Discrete OFEs and Timeless elements *)
-(* TODO: On paper, We called these "discrete elements". I think that makes
- more sense. *)
-Class Timeless {A : ofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
-Arguments timeless {_} _ {_} _ _.
-Hint Mode Timeless + ! : typeclass_instances.
-Instance: Params (@Timeless) 1.
+(** Discrete OFEs and discrete OFE elements *)
+Class Discrete {A : ofeT} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
+Arguments discrete {_} _ {_} _ _.
+Hint Mode Discrete + ! : typeclass_instances.
+Instance: Params (@Discrete) 1.
-Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
-Hint Mode Discrete ! : typeclass_instances.
+Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
(** OFEs with a completion *)
Record chain (A : ofeT) := {
@@ -165,8 +162,8 @@ Section ofe.
Qed.
Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
- Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless A).
- Proof. intros x y Hxy. rewrite /Timeless. by setoid_rewrite Hxy. Qed.
+ Global Instance Discrete_proper : Proper ((≡) ==> iff) (@Discrete A).
+ Proof. intros x y Hxy. rewrite /Discrete. by setoid_rewrite Hxy. Qed.
Lemma dist_le n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y.
Proof. induction 2; eauto using dist_S. Qed.
@@ -188,13 +185,13 @@ Section ofe.
apply chain_cauchy. omega.
Qed.
- Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
+ Lemma discrete_iff n (x : A) `{!Discrete x} y : x ≡ y ↔ x ≡{n}≡ y.
Proof.
- split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
+ split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
Qed.
- Lemma timeless_iff_0 n (x : A) `{!Timeless x} y : x ≡{0}≡ y ↔ x ≡{n}≡ y.
+ Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x ≡{0}≡ y ↔ x ≡{n}≡ y.
Proof.
- split=> ?. by apply equiv_dist, (timeless _). eauto using dist_le with lia.
+ split=> ?. by apply equiv_dist, (discrete _). eauto using dist_le with lia.
Qed.
End ofe.
@@ -273,7 +270,7 @@ Section limit_preserving.
Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P).
Proof. intros c HP. apply (HP 0). Qed.
- Lemma limit_preserving_timeless (P : A → Prop) :
+ Lemma limit_preserving_discrete (P : A → Prop) :
Proper (dist 0 ==> impl) P → LimitPreserving P.
Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.
@@ -653,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_discrete_cofe : Discrete unitC.
+ Global Instance unit_ofe_discrete : OfeDiscrete unitC.
Proof. done. Qed.
End unit.
@@ -683,10 +680,11 @@ Section product.
apply (conv_compl n (chain_map snd c)).
Qed.
- Global Instance prod_timeless (x : A * B) :
- Timeless (x.1) → Timeless (x.2) → Timeless x.
- Proof. by intros ???[??]; split; apply (timeless _). Qed.
- Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC.
+ 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.
Proof. intros ?? [??]; apply _. Qed.
End product.
@@ -864,11 +862,12 @@ Section sum.
- rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
Qed.
- Global Instance inl_timeless (x : A) : Timeless x → Timeless (inl x).
- Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
- Global Instance inr_timeless (y : B) : Timeless y → Timeless (inr y).
- Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
- Global Instance sum_discrete_ofe : Discrete A → Discrete B → Discrete sumC.
+ Global Instance inl_discrete (x : A) : Discrete x → Discrete (inl x).
+ 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.
Proof. intros ?? [?|?]; apply _. Qed.
End sum.
@@ -923,7 +922,7 @@ Section discrete_ofe.
- done.
Qed.
- Global Instance discrete_discrete_ofe : Discrete (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) :=
@@ -992,8 +991,8 @@ Section option.
destruct (c n); naive_solver.
Qed.
- Global Instance option_discrete : Discrete A → Discrete optionC.
- Proof. destruct 2; constructor; by apply (timeless _). Qed.
+ Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionC.
+ Proof. destruct 2; constructor; by apply (discrete _). Qed.
Global Instance Some_ne : NonExpansive (@Some A).
Proof. by constructor. Qed.
@@ -1005,10 +1004,10 @@ Section option.
Proper (dist n ==> R) f → Proper (R ==> dist n ==> R) (from_option f).
Proof. destruct 3; simpl; auto. Qed.
- Global Instance None_timeless : Timeless (@None A).
+ Global Instance None_discrete : Discrete (@None A).
Proof. inversion_clear 1; constructor. Qed.
- Global Instance Some_timeless x : Timeless x → Timeless (Some x).
- Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
+ Global Instance Some_discrete x : Discrete x → Discrete (Some x).
+ Proof. by intros ?; inversion_clear 1; constructor; apply discrete. Qed.
Lemma dist_None n mx : mx ≡{n}≡ None ↔ mx = None.
Proof. split; [by inversion_clear 1|by intros ->]. Qed.
@@ -1224,9 +1223,9 @@ Section sigma.
Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigC.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
- Global Instance sig_timeless (x : sig P) : Timeless (`x) → Timeless x.
- Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (timeless _). Qed.
- Global Instance sig_discrete_ofe : Discrete A → Discrete sigC.
+ 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.
Proof. intros ??. apply _. Qed.
End sigma.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 0ef2608f45d5126ae9b65931113e454ded8e3460..638ceca69c54f5d5ef1e3e47aa48321e90a5b8c4 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 *)
@@ -391,7 +391,7 @@ Proof.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
-Global Instance sts_frag_peristent S : Persistent (sts_frag S ∅).
+Global Instance sts_frag_core_id S : CoreId (sts_frag S ∅).
Proof.
constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
Qed.
@@ -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 5f1b29130dea34af2d5077c10cbbdeda92776f4e..7250ce400546401f18b69a2a24d32c92b87d0401 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -21,15 +21,15 @@ Section ofe.
- intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= vec_to_list_length.
Qed.
- Global Instance vnil_timeless : Timeless (@vnil A).
+ Global Instance vnil_discrete : Discrete (@vnil A).
Proof. intros v _. by inv_vec v. Qed.
- Global Instance vcons_timeless n x (v : vec A n) :
- Timeless x → Timeless v → Timeless (x ::: v).
+ Global Instance vcons_discrete n x (v : vec A n) :
+ Discrete x → Discrete v → Discrete (x ::: v).
Proof.
intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1.
- constructor. by apply timeless. change (v ≡ v'). by apply timeless.
+ constructor. by apply discrete. change (v ≡ v'). by apply discrete.
Qed.
- Global Instance vec_discrete_cofe m : Discrete A → Discrete (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/base_logic.v b/theories/base_logic/base_logic.v
index 701ff8357f9f8c43d9e446f76024b94a6c0fc15f..58a5a0098d6391f1f112526469741343ba2f8a84 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -11,7 +11,7 @@ End uPred.
Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
-Hint Resolve always_mono : I.
+Hint Resolve persistently_mono : I.
Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl internal_eq_refl' : I.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 9b9daea32a22a5a4ff0b6ca3b520d6d444b436e9..6079c922a11989c852610650be32d332e05ad851 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -117,16 +117,16 @@ Section list.
▷^n ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ▷^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
- Lemma big_sepL_always Φ l :
+ Lemma big_sepL_persistently Φ l :
(□ [∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □ Φ k x).
Proof. apply (big_opL_commute _). Qed.
- Lemma big_sepL_always_if p Φ l :
+ Lemma big_sepL_persistently_if p Φ l :
□?p ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, □?p Φ k x).
Proof. apply (big_opL_commute _). Qed.
Lemma big_sepL_forall Φ l :
- (∀ k x, PersistentP (Φ k x)) →
+ (∀ k x, Persistent (Φ k x)) →
([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌠→ Φ k x).
Proof.
intros HΦ. apply (anti_symm _).
@@ -134,7 +134,7 @@ Section list.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
{ rewrite big_sepL_nil; auto with I. }
- rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
+ rewrite big_sepL_cons. rewrite -and_sep_l; apply and_intro.
- by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
- rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
@@ -143,30 +143,30 @@ Section list.
□ (∀ k x, ⌜l !! k = Some x⌠→ Φ k x → Ψ k x) ∧ ([∗ list] k↦x ∈ l, Φ k x)
⊢ [∗ list] k↦x ∈ l, Ψ k x.
Proof.
- rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
- setoid_rewrite always_impl; setoid_rewrite always_pure.
+ rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
+ setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
- by rewrite -always_wand_impl always_elim wand_elim_l.
+ by rewrite persistently_impl_wand persistently_elim wand_elim_l.
Qed.
Global Instance big_sepL_nil_persistent Φ :
- PersistentP ([∗ list] k↦x ∈ [], Φ k x).
+ Persistent ([∗ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_sepL_persistent Φ l :
- (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x).
+ (∀ k x, Persistent (Φ k x)) → Persistent ([∗ list] k↦x ∈ l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Global Instance big_sepL_persistent_id Ps :
- TCForall PersistentP Ps → PersistentP ([∗] Ps).
+ TCForall Persistent Ps → Persistent ([∗] Ps).
Proof. induction 1; simpl; apply _. Qed.
Global Instance big_sepL_nil_timeless Φ :
- TimelessP ([∗ list] k↦x ∈ [], Φ k x).
+ Timeless ([∗ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_sepL_timeless Φ l :
- (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x).
+ (∀ k x, Timeless (Φ k x)) → Timeless ([∗ list] k↦x ∈ l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Global Instance big_sepL_timeless_id Ps :
- TCForall TimelessP Ps → TimelessP ([∗] Ps).
+ TCForall Timeless Ps → Timeless ([∗] Ps).
Proof. induction 1; simpl; apply _. Qed.
End list.
@@ -307,23 +307,23 @@ Section gmap.
▷^n ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ▷^n Φ k x).
Proof. apply (big_opM_commute _). Qed.
- Lemma big_sepM_always Φ m :
+ Lemma big_sepM_persistently Φ m :
(□ [∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □ Φ k x).
Proof. apply (big_opM_commute _). Qed.
- Lemma big_sepM_always_if p Φ m :
+ Lemma big_sepM_persistently_if p Φ m :
□?p ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, □?p Φ k x).
Proof. apply (big_opM_commute _). Qed.
Lemma big_sepM_forall Φ m :
- (∀ k x, PersistentP (Φ k x)) →
+ (∀ k x, Persistent (Φ k x)) →
([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, ⌜m !! k = Some x⌠→ Φ k x).
Proof.
intros. apply (anti_symm _).
{ apply forall_intro=> k; apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
- rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
+ rewrite big_sepM_insert // -and_sep_l. apply and_intro.
- rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_True // True_impl.
- rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
@@ -336,23 +336,23 @@ Section gmap.
□ (∀ k x, ⌜m !! k = Some x⌠→ Φ k x → Ψ k x) ∧ ([∗ map] k↦x ∈ m, Φ k x)
⊢ [∗ map] k↦x ∈ m, Ψ k x.
Proof.
- rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
- setoid_rewrite always_impl; setoid_rewrite always_pure.
+ rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
+ setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
- by rewrite -always_wand_impl always_elim wand_elim_l.
+ by rewrite persistently_impl_wand persistently_elim wand_elim_l.
Qed.
Global Instance big_sepM_empty_persistent Φ :
- PersistentP ([∗ map] k↦x ∈ ∅, Φ k x).
+ Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_persistent Φ m :
- (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ map] k↦x ∈ m, Φ k x).
+ (∀ k x, Persistent (Φ k x)) → Persistent ([∗ map] k↦x ∈ m, Φ k x).
Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
Global Instance big_sepM_nil_timeless Φ :
- TimelessP ([∗ map] k↦x ∈ ∅, Φ k x).
+ Timeless ([∗ map] k↦x ∈ ∅, Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_timeless Φ m :
- (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ map] k↦x ∈ m, Φ k x).
+ (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x).
Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
End gmap.
@@ -460,22 +460,22 @@ Section gset.
▷^n ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ▷^n Φ y).
Proof. apply (big_opS_commute _). Qed.
- Lemma big_sepS_always Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
+ Lemma big_sepS_persistently Φ X : □ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □ Φ y).
Proof. apply (big_opS_commute _). Qed.
- Lemma big_sepS_always_if q Φ X :
+ Lemma big_sepS_persistently_if q Φ X :
□?q ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, □?q Φ y).
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_forall Φ X :
- (∀ x, PersistentP (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌠→ Φ x).
+ (∀ x, Persistent (Φ x)) → ([∗ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌠→ Φ x).
Proof.
intros. apply (anti_symm _).
{ apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
induction X as [|x X ? IH] using collection_ind_L.
{ rewrite big_sepS_empty; auto. }
- rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
+ rewrite big_sepS_insert // -and_sep_l. apply and_intro.
- by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
- rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
@@ -484,21 +484,21 @@ Section gset.
Lemma big_sepS_impl Φ Ψ X :
□ (∀ x, ⌜x ∈ X⌠→ Φ x → Ψ x) ∧ ([∗ set] x ∈ X, Φ x) ⊢ [∗ set] x ∈ X, Ψ x.
Proof.
- rewrite always_and_sep_l always_forall.
- setoid_rewrite always_impl; setoid_rewrite always_pure.
+ rewrite persistently_and_sep_l persistently_forall.
+ setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
- by rewrite -always_wand_impl always_elim wand_elim_l.
+ by rewrite persistently_impl_wand persistently_elim wand_elim_l.
Qed.
- Global Instance big_sepS_empty_persistent Φ : PersistentP ([∗ set] x ∈ ∅, Φ x).
+ Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed.
Global Instance big_sepS_persistent Φ X :
- (∀ x, PersistentP (Φ x)) → PersistentP ([∗ set] x ∈ X, Φ x).
+ (∀ x, Persistent (Φ x)) → Persistent ([∗ set] x ∈ X, Φ x).
Proof. rewrite /big_opS. apply _. Qed.
- Global Instance big_sepS_nil_timeless Φ : TimelessP ([∗ set] x ∈ ∅, Φ x).
+ Global Instance big_sepS_nil_timeless Φ : Timeless ([∗ set] x ∈ ∅, Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed.
Global Instance big_sepS_timeless Φ X :
- (∀ x, TimelessP (Φ x)) → TimelessP ([∗ set] x ∈ X, Φ x).
+ (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x).
Proof. rewrite /big_opS. apply _. Qed.
End gset.
@@ -571,22 +571,22 @@ Section gmultiset.
▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
Proof. apply (big_opMS_commute _). Qed.
- Lemma big_sepMS_always Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
+ Lemma big_sepMS_persistently Φ X : □ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □ Φ y).
Proof. apply (big_opMS_commute _). Qed.
- Lemma big_sepMS_always_if q Φ X :
+ Lemma big_sepMS_persistently_if q Φ X :
□?q ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, □?q Φ y).
Proof. apply (big_opMS_commute _). Qed.
- Global Instance big_sepMS_empty_persistent Φ : PersistentP ([∗ mset] x ∈ ∅, Φ x).
+ Global Instance big_sepMS_empty_persistent Φ : Persistent ([∗ mset] x ∈ ∅, Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
Global Instance big_sepMS_persistent Φ X :
- (∀ x, PersistentP (Φ x)) → PersistentP ([∗ mset] x ∈ X, Φ x).
+ (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
Proof. rewrite /big_opMS. apply _. Qed.
- Global Instance big_sepMS_nil_timeless Φ : TimelessP ([∗ mset] x ∈ ∅, Φ x).
+ Global Instance big_sepMS_nil_timeless Φ : Timeless ([∗ mset] x ∈ ∅, Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
Global Instance big_sepMS_timeless Φ X :
- (∀ x, TimelessP (Φ x)) → TimelessP ([∗ mset] x ∈ X, Φ x).
+ (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
End big_op.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index aceaa62ea511e20c526ed728fa82c0ecdeb14f1b..0875fde43fa25d793102d7e9f5c55825ed4e1b4f 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -16,11 +16,11 @@ Notation "â–·? p P" := (uPred_laterN (Nat.b2n p) P)
(at level 20, p at level 9, P at level 20,
format "â–·? p P") : uPred_scope.
-Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
+Definition uPred_persistently_if {M} (p : bool) (P : uPred M) : uPred M :=
(if p then â–¡ P else P)%I.
-Instance: Params (@uPred_always_if) 2.
-Arguments uPred_always_if _ !_ _/.
-Notation "â–¡? p P" := (uPred_always_if p P)
+Instance: Params (@uPred_persistently_if) 2.
+Arguments uPred_persistently_if _ !_ _/.
+Notation "â–¡? p P" := (uPred_persistently_if p P)
(at level 20, p at level 9, P at level 20, format "â–¡? p P").
Definition uPred_except_0 {M} (P : uPred M) : uPred M := ▷ False ∨ P.
@@ -29,15 +29,15 @@ Notation "â—‡ P" := (uPred_except_0 P)
Instance: Params (@uPred_except_0) 1.
Typeclasses Opaque uPred_except_0.
-Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
+Class Timeless {M} (P : uPred M) := timelessP : ▷ P ⊢ ◇ P.
Arguments timelessP {_} _ {_}.
-Hint Mode TimelessP + ! : typeclass_instances.
-Instance: Params (@TimelessP) 1.
+Hint Mode Timeless + ! : typeclass_instances.
+Instance: Params (@Timeless) 1.
-Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
-Arguments persistentP {_} _ {_}.
-Hint Mode PersistentP + ! : typeclass_instances.
-Instance: Params (@PersistentP) 1.
+Class Persistent {M} (P : uPred M) := persistent : P ⊢ □ P.
+Arguments persistent {_} _ {_}.
+Hint Mode Persistent + ! : typeclass_instances.
+Instance: Params (@Persistent) 1.
Module uPred.
Section derived.
@@ -432,7 +432,7 @@ Qed.
Lemma sep_and P Q : (P ∗ Q) ⊢ (P ∧ Q).
Proof. auto. Qed.
-Lemma impl_wand P Q : (P → Q) ⊢ P -∗ Q.
+Lemma impl_wand_1 P Q : (P → Q) ⊢ P -∗ Q.
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Lemma pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ⌜φ⌠∗ Q ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
@@ -472,105 +472,105 @@ Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a,
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Always derived *)
-Hint Resolve always_mono always_elim.
-Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-Global Instance always_flip_mono' :
- Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
+Hint Resolve persistently_mono persistently_elim.
+Global Instance persistently_mono' : Proper ((⊢) ==> (⊢)) (@uPred_persistently M).
+Proof. intros P Q; apply persistently_mono. Qed.
+Global Instance persistently_flip_mono' :
+ Proper (flip (⊢) ==> flip (⊢)) (@uPred_persistently M).
+Proof. intros P Q; apply persistently_mono. Qed.
-Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof. intros <-. apply always_idemp_2. Qed.
-Lemma always_idemp P : □ □ P ⊣⊢ □ P.
-Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
+Lemma persistently_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros <-. apply persistently_idemp_2. Qed.
+Lemma persistently_idemp P : □ □ P ⊣⊢ □ P.
+Proof. apply (anti_symm _); auto using persistently_idemp_2. Qed.
-Lemma always_pure φ : â–¡ ⌜φ⌠⊣⊢ ⌜φâŒ.
+Lemma persistently_pure φ : â–¡ ⌜φ⌠⊣⊢ ⌜φâŒ.
Proof.
apply (anti_symm _); auto.
apply pure_elim'=> Hφ.
trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
- rewrite always_forall_2. auto using always_mono, pure_intro.
+ rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
+Lemma persistently_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
Proof.
- apply (anti_symm _); auto using always_forall_2.
+ apply (anti_symm _); auto using persistently_forall_2.
apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
+Lemma persistently_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
Proof.
- apply (anti_symm _); auto using always_exist_1.
+ apply (anti_symm _); auto using persistently_exist_1.
apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
-Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
-Proof. rewrite !and_alt always_forall. by apply forall_proper=> -[]. Qed.
-Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
-Proof. rewrite !or_alt always_exist. by apply exist_proper=> -[]. Qed.
-Lemma always_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
+Lemma persistently_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
+Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
+Lemma persistently_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
+Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
+Lemma persistently_impl P Q : □ (P → Q) ⊢ □ P → □ Q.
Proof.
- apply impl_intro_l; rewrite -always_and.
- apply always_mono, impl_elim with P; auto.
+ apply impl_intro_l; rewrite -persistently_and.
+ apply persistently_mono, impl_elim with P; auto.
Qed.
-Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
Proof.
- apply (anti_symm (⊢)); auto using always_elim.
+ apply (anti_symm (⊢)); auto using persistently_elim.
apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
{ intros n; solve_proper. }
- rewrite -(internal_eq_refl a) always_pure; auto.
+ rewrite -(internal_eq_refl a) persistently_pure; auto.
Qed.
-Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
-Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep_dup' P : □ P ⊣⊢ □ P ∗ □ P.
-Proof. by rewrite -always_and_sep_l' idemp. Qed.
+Lemma persistently_and_sep_l P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
+Proof. apply (anti_symm (⊢)); auto using persistently_and_sep_l_1. Qed.
+Lemma persistently_and_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ □ Q.
+Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
+Lemma persistently_sep_dup P : □ P ⊣⊢ □ P ∗ □ P.
+Proof. by rewrite -persistently_and_sep_l idemp. Qed.
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
+Lemma persistently_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ∗ Q).
Proof.
apply (anti_symm (⊢)); auto.
- rewrite -{1}always_idemp always_and always_and_sep_l'; auto.
+ rewrite -{1}persistently_idemp persistently_and persistently_and_sep_l; auto.
Qed.
-Lemma always_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
-Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
+Lemma persistently_sep P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Proof. by rewrite -persistently_and_sep -persistently_and_sep_l persistently_and. Qed.
-Lemma always_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
-Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_wand_impl P Q : □ (P -∗ Q) ⊣⊢ □ (P → Q).
+Lemma persistently_wand P Q : □ (P -∗ Q) ⊢ □ P -∗ □ Q.
+Proof. by apply wand_intro_r; rewrite -persistently_sep wand_elim_l. Qed.
+Lemma persistently_impl_wand P Q : □ (P → Q) ⊣⊢ □ (P -∗ Q).
Proof.
- apply (anti_symm (⊢)); [|by rewrite -impl_wand].
- apply always_intro', impl_intro_r.
- by rewrite always_and_sep_l' always_elim wand_elim_l.
+ apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
+ apply persistently_intro', impl_intro_r.
+ by rewrite persistently_and_sep_l persistently_elim wand_elim_l.
Qed.
-Lemma wand_impl_always P Q : ((□ P) -∗ Q) ⊣⊢ ((□ P) → Q).
+Lemma impl_wand_persistently P Q : (□ P → Q) ⊣⊢ (□ P -∗ Q).
Proof.
- apply (anti_symm (⊢)); [|by rewrite -impl_wand].
- apply impl_intro_l. by rewrite always_and_sep_l' wand_elim_r.
+ apply (anti_symm (⊢)); [by rewrite -impl_wand_1|].
+ apply impl_intro_l. by rewrite persistently_and_sep_l wand_elim_r.
Qed.
-Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
-Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
-Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
+Lemma persistently_entails_l P Q : (P ⊢ □ Q) → P ⊢ □ Q ∗ P.
+Proof. intros; rewrite -persistently_and_sep_l; auto. Qed.
+Lemma persistently_entails_r P Q : (P ⊢ □ Q) → P ⊢ P ∗ □ Q.
+Proof. intros; rewrite -persistently_and_sep_r; auto. Qed.
-Lemma always_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
+Lemma persistently_laterN n P : □ ▷^n P ⊣⊢ ▷^n □ P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite persistently_later IH. Qed.
Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ □ (P ∗ R → Q).
Proof.
apply (anti_symm (⊢)).
- rewrite -(right_id True%I uPred_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
- apply sep_mono_r. rewrite -always_pure. apply always_mono, impl_intro_l.
+ apply sep_mono_r. rewrite -persistently_pure. apply persistently_mono, impl_intro_l.
by rewrite wand_elim_r right_id.
- - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -always_and_sep_r'.
- by rewrite always_elim impl_elim_r.
+ - apply exist_elim=> R. apply wand_intro_l. rewrite assoc -persistently_and_sep_r.
+ by rewrite persistently_elim impl_elim_r.
Qed.
Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ □ (P ∧ R -∗ Q).
Proof.
apply (anti_symm (⊢)).
- rewrite -(right_id True%I uPred_and (P → Q)%I) -(exist_intro (P → Q)%I).
- apply and_mono_r. rewrite -always_pure. apply always_mono, wand_intro_l.
+ apply and_mono_r. rewrite -persistently_pure. apply persistently_mono, wand_intro_l.
by rewrite impl_elim_r right_id.
- - apply exist_elim=> R. apply impl_intro_l. rewrite assoc always_and_sep_r'.
- by rewrite always_elim wand_elim_r.
+ - apply exist_elim=> R. apply impl_intro_l. rewrite assoc persistently_and_sep_r.
+ by rewrite persistently_elim wand_elim_r.
Qed.
(* Later derived *)
@@ -671,33 +671,33 @@ Qed.
Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
-(* Conditional always *)
-Global Instance always_if_ne p : NonExpansive (@uPred_always_if M p).
+(* Conditional persistently *)
+Global Instance persistently_if_ne p : NonExpansive (@uPred_persistently_if M p).
Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
+Global Instance persistently_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_persistently_if M p).
Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
+Global Instance persistently_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_persistently_if M p).
Proof. solve_proper. Qed.
-Lemma always_if_elim p P : □?p P ⊢ P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : □ P ⊢ □?p P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-
-Lemma always_if_pure p φ : â–¡?p ⌜φ⌠⊣⊢ ⌜φâŒ.
-Proof. destruct p; simpl; auto using always_pure. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
-Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
-Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
-Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
-Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
-Proof. destruct p; simpl; auto using always_later. Qed.
-Lemma always_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
-Proof. destruct p; simpl; auto using always_laterN. Qed.
+Lemma persistently_if_elim p P : □?p P ⊢ P.
+Proof. destruct p; simpl; auto using persistently_elim. Qed.
+Lemma persistently_elim_if p P : □ P ⊢ □?p P.
+Proof. destruct p; simpl; auto using persistently_elim. Qed.
+
+Lemma persistently_if_pure p φ : â–¡?p ⌜φ⌠⊣⊢ ⌜φâŒ.
+Proof. destruct p; simpl; auto using persistently_pure. Qed.
+Lemma persistently_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Proof. destruct p; simpl; auto using persistently_and. Qed.
+Lemma persistently_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Proof. destruct p; simpl; auto using persistently_or. Qed.
+Lemma persistently_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
+Proof. destruct p; simpl; auto using persistently_exist. Qed.
+Lemma persistently_if_sep p P Q : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
+Proof. destruct p; simpl; auto using persistently_sep. Qed.
+Lemma persistently_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
+Proof. destruct p; simpl; auto using persistently_later. Qed.
+Lemma persistently_if_laterN p n P : □?p ▷^n P ⊣⊢ ▷^n □?p P.
+Proof. destruct p; simpl; auto using persistently_laterN. Qed.
(* True now *)
Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
@@ -727,7 +727,7 @@ Lemma except_0_sep P Q : ◇ (P ∗ Q) ⊣⊢ ◇ P ∗ ◇ Q.
Proof.
rewrite /uPred_except_0. apply (anti_symm _).
- apply or_elim; last by auto.
- by rewrite -!or_intro_l -always_pure -always_later -always_sep_dup'.
+ by rewrite -!or_intro_l -persistently_pure -persistently_later -persistently_sep_dup.
- rewrite sep_or_r sep_elim_l sep_or_l; auto.
Qed.
Lemma except_0_forall {A} (Φ : A → uPred M) : ◇ (∀ a, Φ a) ⊢ ∀ a, ◇ Φ a.
@@ -743,20 +743,20 @@ Proof.
Qed.
Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
-Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P.
-Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
-Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
-Proof. destruct p; simpl; auto using except_0_always. Qed.
+Lemma except_0_persistently P : ◇ □ P ⊣⊢ □ ◇ P.
+Proof. by rewrite /uPred_except_0 persistently_or persistently_later persistently_pure. Qed.
+Lemma except_0_persistently_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
+Proof. destruct p; simpl; auto using except_0_persistently. Qed.
Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
(* Own and valid derived *)
-Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
- intros; apply (anti_symm _); first by apply:always_elim.
- by rewrite {1}always_ownM_core persistent_core.
+ intros; apply (anti_symm _); first by apply:persistently_elim.
+ by rewrite {1}persistently_ownM_core core_id_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
@@ -764,10 +764,10 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. 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.
+Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
Proof.
- intros; apply (anti_symm _); first by apply:always_elim.
- apply:always_cmra_valid_1.
+ intros; apply (anti_symm _); first by apply:persistently_elim.
+ apply:persistently_cmra_valid_1.
Qed.
(** * Derived rules *)
@@ -794,147 +794,146 @@ Proof.
by rewrite -bupd_intro -or_intro_l.
Qed.
-(* Timeless instances *)
-Global Instance TimelessP_proper : Proper ((≡) ==> iff) (@TimelessP M).
+Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless M).
Proof. solve_proper. Qed.
-Global Instance pure_timeless φ : TimelessP (⌜φ⌠: uPred M)%I.
+Global Instance pure_timeless φ : Timeless (⌜φ⌠: uPred M)%I.
Proof.
- rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
+ rewrite /Timeless pure_alt later_exist_false. by setoid_rewrite later_True.
Qed.
-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).
-Proof. intros; rewrite /TimelessP except_0_and later_and; auto. Qed.
-Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
-Proof. intros; rewrite /TimelessP except_0_or later_or; auto. Qed.
-Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
+Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
+ Timeless (✓ a : uPred M)%I.
+Proof. rewrite /Timeless !discrete_valid. apply (timelessP _). Qed.
+Global Instance and_timeless P Q: Timeless P → Timeless Q → Timeless (P ∧ Q).
+Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
+Global Instance or_timeless P Q : Timeless P → Timeless Q → Timeless (P ∨ Q).
+Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
+Global Instance impl_timeless P Q : Timeless Q → Timeless (P → Q).
Proof.
- rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+ rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
apply or_mono, impl_intro_l; first done.
rewrite -{2}(löb Q); apply impl_intro_l.
rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed.
-Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∗ Q).
-Proof. intros; rewrite /TimelessP except_0_sep later_sep; auto. Qed.
-Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -∗ Q).
+Global Instance sep_timeless P Q: Timeless P → Timeless Q → Timeless (P ∗ Q).
+Proof. intros; rewrite /Timeless except_0_sep later_sep; auto. Qed.
+Global Instance wand_timeless P Q : Timeless Q → Timeless (P -∗ Q).
Proof.
- rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+ rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
apply or_mono, wand_intro_l; first done.
rewrite -{2}(löb Q); apply impl_intro_l.
rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
- rewrite -(always_pure) -always_later always_and_sep_l'.
- by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
+ rewrite -(persistently_pure) -persistently_later persistently_and_sep_l.
+ by rewrite assoc (comm _ _ P) -assoc -persistently_and_sep_l impl_elim_r wand_elim_r.
Qed.
Global Instance forall_timeless {A} (Ψ : A → uPred M) :
- (∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
+ (∀ x, Timeless (Ψ x)) → Timeless (∀ x, Ψ x).
Proof.
- rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
+ rewrite /Timeless=> HQ. rewrite later_false_excluded_middle.
apply or_mono; first done. apply forall_intro=> x.
rewrite -(löb (Ψ x)); apply impl_intro_l.
rewrite HQ /uPred_except_0 !and_or_r. apply or_elim; last auto.
by rewrite impl_elim_r (forall_elim x).
Qed.
Global Instance exist_timeless {A} (Ψ : A → uPred M) :
- (∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
+ (∀ x, Timeless (Ψ x)) → Timeless (∃ x, Ψ x).
Proof.
- rewrite /TimelessP=> ?. rewrite later_exist_false. apply or_elim.
+ rewrite /Timeless=> ?. rewrite later_exist_false. apply or_elim.
- rewrite /uPred_except_0; auto.
- apply exist_elim=> x. rewrite -(exist_intro x); auto.
Qed.
-Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
-Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
-Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
+Global Instance persistently_timeless P : Timeless P → Timeless (□ P).
+Proof. intros; rewrite /Timeless except_0_persistently -persistently_later; auto. Qed.
+Global Instance persistently_if_timeless p P : Timeless P → Timeless (□?p P).
Proof. destruct p; apply _. Qed.
Global Instance eq_timeless {A : ofeT} (a b : A) :
- Timeless a → TimelessP (a ≡ b : uPred M)%I.
-Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
-Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
+ Discrete a → Timeless (a ≡ b : uPred M)%I.
+Proof. intros. rewrite /Timeless !discrete_eq. apply (timelessP _). Qed.
+Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
Proof.
- intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
+ intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
apply except_0_mono. rewrite internal_eq_sym.
apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
Qed.
Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A) :
- (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx).
+ (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* Derived lemmas for persistence *)
-Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M).
+Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent M).
Proof. solve_proper. Qed.
-Global Instance limit_preserving_PersistentP {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
- NonExpansive Φ → LimitPreserving (λ x, PersistentP (Φ x)).
+Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
+ NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
-Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
-Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
-Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ∗ P.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
-Lemma always_impl_wand P `{!PersistentP P} Q : (P → Q) ⊣⊢ (P -∗ Q).
-Proof.
- apply (anti_symm _); auto using impl_wand.
- apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r.
+Lemma persistent_persistently P `{!Persistent P} : □ P ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); auto using persistently_elim. Qed.
+Lemma persistent_persistently_if p P `{!Persistent P} : □?p P ⊣⊢ P.
+Proof. destruct p; simpl; auto using persistent_persistently. Qed.
+Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ □ Q.
+Proof. rewrite -(persistent_persistently P); apply persistently_intro'. Qed.
+Lemma and_sep_l P Q `{!Persistent P} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(persistent_persistently P) persistently_and_sep_l. Qed.
+Lemma and_sep_r P Q `{!Persistent Q} : P ∧ Q ⊣⊢ P ∗ Q.
+Proof. by rewrite -(persistent_persistently Q) persistently_and_sep_r. Qed.
+Lemma sep_dup P `{!Persistent P} : P ⊣⊢ P ∗ P.
+Proof. by rewrite -(persistent_persistently P) -persistently_sep_dup. Qed.
+Lemma sep_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_l. Qed.
+Lemma sep_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. by rewrite -(persistent_persistently Q); apply persistently_entails_r. Qed.
+Lemma impl_wand P `{!Persistent P} Q : (P → Q) ⊣⊢ (P -∗ Q).
+Proof.
+ apply (anti_symm _); auto using impl_wand_1.
+ apply impl_intro_l. by rewrite and_sep_l wand_elim_r.
Qed.
(* Persistence *)
-Global Instance pure_persistent φ : PersistentP (⌜φ⌠: uPred M)%I.
-Proof. by rewrite /PersistentP always_pure. Qed.
+Global Instance pure_persistent φ : Persistent (⌜φ⌠: uPred M)%I.
+Proof. by rewrite /Persistent persistently_pure. Qed.
Global Instance pure_impl_persistent φ Q :
- PersistentP Q → PersistentP (⌜φ⌠→ Q)%I.
+ Persistent Q → Persistent (⌜φ⌠→ Q)%I.
Proof.
- rewrite /PersistentP pure_impl_forall always_forall. auto using forall_mono.
+ rewrite /Persistent pure_impl_forall persistently_forall. auto using forall_mono.
Qed.
Global Instance pure_wand_persistent φ Q :
- PersistentP Q → PersistentP (⌜φ⌠-∗ Q)%I.
+ Persistent Q → Persistent (⌜φ⌠-∗ Q)%I.
Proof.
- rewrite /PersistentP -always_impl_wand pure_impl_forall always_forall.
+ rewrite /Persistent -impl_wand pure_impl_forall persistently_forall.
auto using forall_mono.
Qed.
-Global Instance always_persistent P : PersistentP (â–¡ P).
-Proof. by intros; apply always_intro'. Qed.
+Global Instance persistently_persistent P : Persistent (â–¡ P).
+Proof. by intros; apply persistently_intro'. Qed.
Global Instance and_persistent P Q :
- PersistentP P → PersistentP Q → PersistentP (P ∧ Q).
-Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
+ Persistent P → Persistent Q → Persistent (P ∧ Q).
+Proof. by intros; rewrite /Persistent persistently_and; apply and_mono. Qed.
Global Instance or_persistent P Q :
- PersistentP P → PersistentP Q → PersistentP (P ∨ Q).
-Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
+ Persistent P → Persistent Q → Persistent (P ∨ Q).
+Proof. by intros; rewrite /Persistent persistently_or; apply or_mono. Qed.
Global Instance sep_persistent P Q :
- PersistentP P → PersistentP Q → PersistentP (P ∗ Q).
-Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
+ Persistent P → Persistent Q → Persistent (P ∗ Q).
+Proof. by intros; rewrite /Persistent persistently_sep; apply sep_mono. Qed.
Global Instance forall_persistent {A} (Ψ : A → uPred M) :
- (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
+ (∀ x, Persistent (Ψ x)) → Persistent (∀ x, Ψ x).
+Proof. by intros; rewrite /Persistent persistently_forall; apply forall_mono. Qed.
Global Instance exist_persistent {A} (Ψ : A → uPred M) :
- (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
+ (∀ x, Persistent (Ψ x)) → Persistent (∃ x, Ψ x).
+Proof. by intros; rewrite /Persistent persistently_exist; apply exist_mono. Qed.
Global Instance internal_eq_persistent {A : ofeT} (a b : A) :
- PersistentP (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_internal_eq. Qed.
+ Persistent (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
- PersistentP (✓ a : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
-Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
-Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
+ Persistent (✓ a : uPred M)%I.
+Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed.
+Global Instance later_persistent P : Persistent P → Persistent (▷ P).
+Proof. by intros; rewrite /Persistent persistently_later; apply later_mono. Qed.
+Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
Proof. induction n; apply _. Qed.
-Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
-Proof. intros. by rewrite /PersistentP always_ownM. Qed.
+Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a).
+Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
- (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
+ (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* For big ops *)
@@ -945,12 +944,12 @@ Global Instance uPred_or_monoid : Monoid (@uPred_or M) :=
Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
{| monoid_unit := True%I |}.
-Global Instance uPred_always_and_homomorphism :
- MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M).
-Proof. split; [split; try apply _|]. apply always_and. apply always_pure. Qed.
-Global Instance uPred_always_if_and_homomorphism b :
- MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M b).
-Proof. split; [split; try apply _|]. apply always_if_and. apply always_if_pure. Qed.
+Global Instance uPred_persistently_and_homomorphism :
+ MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently M).
+Proof. split; [split; try apply _|]. apply persistently_and. apply persistently_pure. Qed.
+Global Instance uPred_persistently_if_and_homomorphism b :
+ MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_persistently_if M b).
+Proof. split; [split; try apply _|]. apply persistently_if_and. apply persistently_if_pure. Qed.
Global Instance uPred_later_monoid_and_homomorphism :
MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_later M).
Proof. split; [split; try apply _|]. apply later_and. apply later_True. Qed.
@@ -961,12 +960,12 @@ Global Instance uPred_except_0_and_homomorphism :
MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_except_0 M).
Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qed.
-Global Instance uPred_always_or_homomorphism :
- MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M).
-Proof. split; [split; try apply _|]. apply always_or. apply always_pure. Qed.
-Global Instance uPred_always_if_or_homomorphism b :
- MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M b).
-Proof. split; [split; try apply _|]. apply always_if_or. apply always_if_pure. Qed.
+Global Instance uPred_persistently_or_homomorphism :
+ MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently M).
+Proof. split; [split; try apply _|]. apply persistently_or. apply persistently_pure. Qed.
+Global Instance uPred_persistently_if_or_homomorphism b :
+ MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_persistently_if M b).
+Proof. split; [split; try apply _|]. apply persistently_if_or. apply persistently_if_pure. Qed.
Global Instance uPred_later_monoid_or_homomorphism :
WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_later M).
Proof. split; try apply _. apply later_or. Qed.
@@ -977,12 +976,12 @@ Global Instance uPred_except_0_or_homomorphism :
WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_except_0 M).
Proof. split; try apply _. apply except_0_or. Qed.
-Global Instance uPred_always_sep_homomorphism :
- MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M).
-Proof. split; [split; try apply _|]. apply always_sep. apply always_pure. Qed.
-Global Instance uPred_always_if_sep_homomorphism b :
- MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M b).
-Proof. split; [split; try apply _|]. apply always_if_sep. apply always_if_pure. Qed.
+Global Instance uPred_persistently_sep_homomorphism :
+ MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently M).
+Proof. split; [split; try apply _|]. apply persistently_sep. apply persistently_pure. Qed.
+Global Instance uPred_persistently_if_sep_homomorphism b :
+ MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_persistently_if M b).
+Proof. split; [split; try apply _|]. apply persistently_if_sep. apply persistently_if_pure. Qed.
Global Instance uPred_later_monoid_sep_homomorphism :
MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_later M).
Proof. split; [split; try apply _|]. apply later_sep. apply later_True. Qed.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index a46400ae92ae9902edfae933fc43ff3a7794bc90..adcd5859d32af3cb3546104a78b12ca563529c9c 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.
@@ -30,9 +30,9 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
Proof. solve_proper. Qed.
- Global Instance auth_own_timeless a : TimelessP (auth_own a).
+ Global Instance auth_own_timeless a : Timeless (auth_own a).
Proof. apply _. Qed.
- Global Instance auth_own_persistent a : Persistent a → PersistentP (auth_own a).
+ Global Instance auth_own_core_id a : CoreId a → Persistent (auth_own a).
Proof. apply _. Qed.
Global Instance auth_inv_ne n :
@@ -51,7 +51,7 @@ Section definitions.
Proper (pointwise_relation T (≡) ==>
pointwise_relation T (⊣⊢) ==> (⊣⊢)) (auth_ctx N).
Proof. solve_proper. Qed.
- Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ).
+ Global Instance auth_ctx_persistent N f φ : Persistent (auth_ctx N f φ).
Proof. apply _. Qed.
End definitions.
@@ -78,7 +78,7 @@ Section auth.
FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
Proof. rewrite /IsOp /FromAnd=> ->. by rewrite auth_own_op. Qed.
Global Instance from_and_auth_own_persistent γ a b1 b2 :
- IsOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+ IsOp a b1 b2 → Or (CoreId b1) (CoreId b2) →
FromAnd true (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 91.
Proof.
intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 8cf543fd6a2afea91678e5bc70108dc236aba1dc..3d7a7ca77bfdd5f43e0ea1773ea9591f52e73bda 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -65,7 +65,7 @@ Proof. solve_contractive. Qed.
Global Instance slice_proper γ : Proper ((≡) ==> (≡)) (slice N γ).
Proof. apply ne_proper, _. Qed.
-Global Instance slice_persistent γ P : PersistentP (slice N γ P).
+Global Instance slice_persistent γ P : Persistent (slice N γ P).
Proof. apply _. Qed.
Global Instance box_contractive f : Contractive (box N f).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 83e3629d72766bd9640ffc8fa96ec5f6dbd5c8a2..3a4f1c92bf2e5d982c993bc94005c72697b9f979 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -24,7 +24,7 @@ Instance: Params (@cinv) 5.
Section proofs.
Context `{invG Σ, cinvG Σ}.
- Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
+ Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed.
Global Instance cinv_contractive N γ : Contractive (cinv N γ).
@@ -34,7 +34,7 @@ Section proofs.
Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ).
Proof. exact: ne_proper. Qed.
- Global Instance cinv_persistent N γ P : PersistentP (cinv N γ P).
+ Global Instance cinv_persistent N γ P : Persistent (cinv N γ P).
Proof. rewrite /cinv; apply _. Qed.
Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index f96e6edf2baa7848d6863ac9d8abd4121be1c930..e6d584217ca120eb903dcc557cd024f17b7b7f14 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -15,7 +15,7 @@ Import uPred.
*)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
- (∀ `(!PersistentP Q), ⌜P ⊢ Q⌠→ Q)%I.
+ (∀ `(!Persistent Q), ⌜P ⊢ Q⌠→ Q)%I.
Instance: Params (@coreP) 1.
Typeclasses Opaque coreP.
@@ -26,7 +26,7 @@ Section core.
Lemma coreP_intro P : P -∗ coreP P.
Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
- Global Instance coreP_persistent P : PersistentP (coreP P).
+ Global Instance coreP_persistent P : Persistent (coreP P).
Proof. rewrite /coreP. apply _. Qed.
Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
@@ -38,7 +38,7 @@ Section core.
Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
- Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
+ Lemma coreP_elim P : Persistent P → coreP P -∗ P.
Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
Lemma coreP_wand P Q :
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index d9f02cf5bec7003bbec19138ab250dc564968cdc..259eb66d28c31118b991225c71cdee14b0be16e1 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -12,7 +12,7 @@ Module savedprop. Section savedprop.
(** Saved Propositions and the update modality *)
Context (sprop : Type) (saved : sprop → iProp → iProp).
- Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
+ Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P).
Hypothesis sprop_alloc_dep :
∀ (P : sprop → iProp), (|==> (∃ i, saved i (P i)))%I.
Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
@@ -69,7 +69,7 @@ Module inv. Section inv.
(** We have invariants *)
Context (name : Type) (inv : name → iProp → iProp).
- Hypothesis inv_persistent : ∀ i P, PersistentP (inv i P).
+ Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
Hypothesis inv_open :
∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).
@@ -132,7 +132,7 @@ Module inv. Section inv.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : iProp) : iProp :=
∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
- Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
+ Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)).
Proof.
@@ -165,7 +165,7 @@ Module inv. Section inv.
(** And now we tie a bad knot. *)
Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope.
Definition A i : iProp := ∃ P, ¬P ∗ saved i P.
- Global Instance A_persistent i : PersistentP (A i) := _.
+ Global Instance A_persistent i : Persistent (A i) := _.
Lemma A_alloc : fupd M1 (∃ i, saved i (A i)).
Proof. by apply saved_alloc. Qed.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index fc505d702d42d078b694c975f12bee859205abb2..5e6bb63a35348fcbd87b03fe2d1a80e5bff65da9 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -13,7 +13,7 @@ Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
format "P ={ E1 , E2 }=> Q") : uPred_scope.
Context (vs_ne : ∀ E1 E2, NonExpansive2 (vs E1 E2)).
-Context (vs_persistent : ∀ E1 E2 P Q, PersistentP (P ={E1,E2}=> Q)).
+Context (vs_persistent : ∀ E1 E2 P Q, Persistent (P ={E1,E2}=> Q)).
Context (vs_impl : ∀ E P Q, □ (P → Q) ⊢ P ={E,E}=> Q).
Context (vs_transitive : ∀ E1 E2 E3 P Q R,
@@ -24,7 +24,7 @@ Context (vs_frame_r : ∀ E1 E2 P Q R, (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q
Context (vs_exists : ∀ {A} E1 E2 (Φ : A → uPred M) Q,
(∀ x, Φ x ={E1,E2}=> Q) ⊢ (∃ x, Φ x) ={E1,E2}=> Q).
Context (vs_persistent_intro_r : ∀ E1 E2 P Q R,
- PersistentP R →
+ Persistent R →
(R -∗ (P ={E1,E2}=> Q)) ⊢ P ∗ R ={E1,E2}=> Q).
Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index a94ea6989ed1ee7caf9790a6215928d8e3c639f7..179eac0fc705603bb9133a2a5613c9ca1a92be39 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -50,8 +50,8 @@ Section fractional.
(** Fractional and logical connectives *)
Global Instance persistent_fractional P :
- PersistentP P → Fractional (λ _, P).
- Proof. intros HP q q'. by apply uPred.always_sep_dup. Qed.
+ Persistent P → Fractional (λ _, P).
+ Proof. intros HP q q'. by apply uPred.sep_dup. Qed.
Global Instance fractional_sep Φ Ψ :
Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
@@ -134,7 +134,7 @@ Section fractional.
AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
IntoAnd p P P1 P2.
Proof.
- (* TODO: We need a better way to handle this boolean here; always
+ (* TODO: We need a better way to handle this boolean here; persistently
applying mk_into_and_sep (which only works after introducing all
assumptions) is rather annoying.
Ideally, it'd not even be possible to make the mistake that
@@ -148,7 +148,7 @@ Section fractional.
Proof. intros. apply mk_into_and_sep. rewrite [P]fractional_half //. Qed.
(* The instance [frame_fractional] can be tried at all the nodes of
- the proof search. The proof search then fails almost always on
+ the proof search. The proof search then fails almost persistently on
[AsFractional R Φ r], but the slowdown is still noticeable. For
that reason, we factorize the three instances that could have been
defined for that purpose into one. *)
@@ -179,6 +179,6 @@ Section fractional.
- rewrite fractional=><-<-. by rewrite assoc.
- rewrite fractional=><-<-=>_.
by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
- - move=>-[-> _]->. by rewrite uPred.always_if_elim -fractional Qp_div_2.
+ - move=>-[-> _]->. by rewrite uPred.persistently_if_elim -fractional Qp_div_2.
Qed.
End fractional.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 89914dc635f5dbd3fd2bf3e94a2c61cae981e9ae..2f27f2965702e536f18326ca77b9a1b208d5a944 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -82,7 +82,7 @@ Section gen_heap.
Implicit Types v : V.
(** General properties of mapsto *)
- Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).
+ Global Instance mapsto_timeless l q v : Timeless (l ↦{q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
Proof.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 467d60e224c5a82d5a0d5f02b635015bb8f73fde..1608c9a29e941181ae9db80c95ecf686113466dd 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -31,7 +31,7 @@ Proof. apply contractive_ne, _. Qed.
Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N).
Proof. apply ne_proper, _. Qed.
-Global Instance inv_persistent N P : PersistentP (inv N P).
+Global Instance inv_persistent N P : Persistent (inv N P).
Proof. rewrite inv_eq /inv; apply _. Qed.
Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
@@ -81,7 +81,7 @@ Proof.
iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
Qed.
-Lemma inv_open_timeless E N P `{!TimelessP P} :
+Lemma inv_open_timeless E N P `{!Timeless P} :
↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 95a378c30aa8827ddcf550230875418735cb816d..b0462acf5e89fbc7a224c260f94be3770b7dc2ae 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -83,7 +83,7 @@ Class subG (Σ1 Σ2 : gFunctors) := in_subG i : { j | Σ1 i = Σ2 j }.
(** Avoid trigger happy type class search: this line ensures that type class
search is only triggered if the arguments of [subG] do not contain evars. Since
-instance search for [subG] is restrained, instances should always have [subG] as
+instance search for [subG] is restrained, instances should persistently have [subG] as
their first parameter to avoid loops. For example, the instances [subG_authΣ]
and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode subG + + : typeclass_instances.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 2f20a514e2d7996ba685afc4e3af319c62b73422..385d17e64204d2e551b008ef10ae09e55a920c9a 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -32,7 +32,7 @@ Typeclasses Opaque na_own na_inv.
Section proofs.
Context `{invG Σ, na_invG Σ}.
- Global Instance na_own_timeless p E : TimelessP (na_own p E).
+ Global Instance na_own_timeless p E : Timeless (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
Global Instance na_inv_ne p N : NonExpansive (na_inv p N).
@@ -40,7 +40,7 @@ Section proofs.
Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
Proof. apply (ne_proper _). Qed.
- Global Instance na_inv_persistent p N P : PersistentP (na_inv p N P).
+ Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 4049d8dc2546c66cab4e488db1e7ee1b769e2bab..9381789f3f1b0956ee893cc142049b105123fd51 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -102,13 +102,13 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
+Proof. apply: uPred.sep_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
Proof. by rewrite comm -own_valid_r. Qed.
-Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
+Global Instance own_timeless γ a : Discrete a → Timeless (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
-Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
+Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
(** ** Allocation *)
@@ -193,7 +193,7 @@ Section proofmode_classes.
IsOp a b1 b2 → FromAnd false (own γ a) (own γ b1) (own γ b2).
Proof. intros. by rewrite /FromAnd -own_op -is_op. Qed.
Global Instance from_and_own_persistent γ a b1 b2 :
- IsOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+ IsOp a b1 b2 → Or (CoreId b1) (CoreId b2) →
FromAnd true (own γ a) (own γ b1) (own γ b2).
Proof.
intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 4002d1d821aedea8544a46a4bf9a2b83ba274531..4ce4a3ce2da7b3035353289cb0f9c695387c628c 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -23,7 +23,7 @@ Section saved_prop.
Implicit Types x y : F (iProp Σ).
Implicit Types γ : gname.
- Global Instance saved_prop_persistent γ x : PersistentP (saved_prop_own γ x).
+ Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
Proof. rewrite /saved_prop_own; apply _. Qed.
Lemma saved_prop_alloc_strong x (G : gset gname) :
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 047d10d32b0ebab956aa04ea9138683e9be6deb8..9effaf4d7c82c8a31163b9075fb40e2d83d752a2 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -43,11 +43,11 @@ Section definitions.
Global Instance sts_ctx_proper `{!invG Σ} N :
Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
Proof. solve_proper. Qed.
- Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
+ Global Instance sts_ctx_persistent `{!invG Σ} N φ : Persistent (sts_ctx N φ).
Proof. apply _. Qed.
- Global Instance sts_own_persistent s : PersistentP (sts_own s ∅).
+ Global Instance sts_own_persistent s : Persistent (sts_own s ∅).
Proof. apply _. Qed.
- Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅).
+ Global Instance sts_ownS_persistent S : Persistent (sts_ownS S ∅).
Proof. apply _. Qed.
End definitions.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index a4dd554853d18885448c34a163bdf11f3adbb836..e1b5bafc2b2deffed077f63079ad73ee372edc45 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -41,7 +41,7 @@ Proof. solve_proper. Qed.
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
Proof. iIntros "!# []". Qed.
-Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
+Lemma vs_timeless E P : Timeless P → ▷ P ={E}=> P.
Proof. by iIntros (?) "!# > ?". Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
@@ -81,5 +81,5 @@ Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
-Proof. rewrite uPred.wand_alt. by setoid_rewrite <-uPred.always_wand_impl. Qed.
+Proof. rewrite uPred.wand_alt. by setoid_rewrite uPred.persistently_impl_wand. Qed.
End vs.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index b270879e1d0dcf8b1bcb8764d981c7734b8f53c1..4a0fa26984a6b9a7f5dad445d1604319b409fe1d 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -49,7 +49,7 @@ Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
Proof. solve_contractive. Qed.
Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
Proof. solve_contractive. Qed.
-Global Instance ownI_persistent i P : PersistentP (ownI i P).
+Global Instance ownI_persistent i P : Persistent (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Lemma ownE_empty : (|==> ownE ∅)%I.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 08ed253eb83de83e70011c74c3af6048d98d0fc4..18d99c2017d88460b7af241a8ab1fea3856054ed 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -97,16 +97,16 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
-Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
+Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
-Definition uPred_always_aux : seal (@uPred_always_def). by eexists. Qed.
-Definition uPred_always {M} := unseal uPred_always_aux M.
-Definition uPred_always_eq :
- @uPred_always = @uPred_always_def := seal_eq uPred_always_aux.
+Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed.
+Definition uPred_persistently {M} := unseal uPred_persistently_aux M.
+Definition uPred_persistently_eq :
+ @uPred_persistently = @uPred_persistently_def := seal_eq uPred_persistently_aux.
Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
@@ -176,7 +176,7 @@ Notation "∀ x .. y , P" :=
Notation "∃ x .. y , P" :=
(uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I)
(at level 200, x binder, y binder, right associativity) : uPred_scope.
-Notation "â–¡ P" := (uPred_always P)
+Notation "â–¡ P" := (uPred_persistently P)
(at level 20, right associativity) : uPred_scope.
Notation "â–· P" := (uPred_later P)
(at level 20, right associativity) : uPred_scope.
@@ -198,7 +198,7 @@ Notation "P -∗ Q" := (P ⊢ Q)
Module uPred.
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
- uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
+ uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_persistently_eq,
uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq).
Ltac unseal := rewrite !unseal_eqs /=.
@@ -295,13 +295,13 @@ Proof.
Qed.
Global Instance later_proper' :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
-Global Instance always_ne : NonExpansive (@uPred_always M).
+Global Instance persistently_ne : NonExpansive (@uPred_persistently M).
Proof.
intros n P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
Qed.
-Global Instance always_proper :
- Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
+Global Instance persistently_proper :
+ Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_persistently M) := ne_proper _.
Global Instance ownM_ne : NonExpansive (@uPred_ownM M).
Proof.
intros n a b Ha.
@@ -422,22 +422,22 @@ Proof.
Qed.
(* Always *)
-Lemma always_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
Proof. intros HP; unseal; split=> n x ? /=. by apply HP, cmra_core_validN. Qed.
-Lemma always_elim P : □ P ⊢ P.
+Lemma persistently_elim P : □ P ⊢ P.
Proof.
unseal; split=> n x ? /=.
eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
Qed.
-Lemma always_idemp_2 P : □ P ⊢ □ □ P.
+Lemma persistently_idemp_2 P : □ P ⊢ □ □ P.
Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
-Lemma always_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
+Lemma persistently_forall_2 {A} (Ψ : A → uPred M) : (∀ a, □ Ψ a) ⊢ (□ ∀ a, Ψ a).
Proof. by unseal. Qed.
-Lemma always_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
+Lemma persistently_exist_1 {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊢ (∃ a, □ Ψ a).
Proof. by unseal. Qed.
-Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma persistently_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ∗ Q.
Proof.
unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
by rewrite cmra_core_l cmra_core_idemp.
@@ -475,7 +475,7 @@ Proof.
intros [|n'] x' ????; [|done].
eauto using uPred_closed, uPred_mono, cmra_included_includedN.
Qed.
-Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
+Lemma persistently_later P : □ ▷ P ⊣⊢ ▷ □ P.
Proof. by unseal. Qed.
(* Own *)
@@ -489,7 +489,7 @@ Proof.
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
-Lemma always_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
+Lemma persistently_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.
@@ -512,7 +512,7 @@ Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → uPred_valid (M:=M) (✓ a
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ ✓ a.
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ ✓ a.
Proof. by unseal. Qed.
Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
@@ -561,11 +561,11 @@ 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 timeless_eq {A : ofeT} (a b : A) : Timeless a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
+Lemma discrete_eq {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ bâŒ.
Proof.
- unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n).
+ unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (discrete_iff n).
Qed.
(* Option *)
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/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 79112c3fa39170854b808dce42c4a1716a7219fd..b9632c00c56c77d877d82dc6294721e44be25a74 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -29,7 +29,7 @@ Section mono_proof.
(∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
(** The main proofs. *)
- Global Instance mcounter_persistent l n : PersistentP (mcounter l n).
+ Global Instance mcounter_persistent l n : Persistent (mcounter l n).
Proof. apply _. Qed.
Lemma newcounter_mono_spec :
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 720dcc19aa4af6c4696ed456ae0167c6f797ac7d..a5d9966a25060e0ffdd20dc6bc361e9bf7ee8dae 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -14,8 +14,8 @@ Structure lock Σ `{!heapG Σ} := Lock {
locked (γ: name) : iProp Σ;
(* -- general properties -- *)
is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
- is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
- locked_timeless γ : TimelessP (locked γ);
+ is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
+ locked_timeless γ : Timeless (locked γ);
locked_exclusive γ : locked γ -∗ locked γ -∗ False;
(* -- operation specs -- *)
newlock_spec N (R : iProp Σ) :
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 007093dcda47bc7964077053434878a8f7799346..9abf0f6e7eff8755d4e0e5451fcc718090cb05a4 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -40,9 +40,9 @@ Section proof.
Proof. solve_proper. Qed.
(** The main proofs. *)
- Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+ Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
Proof. apply _. Qed.
- Global Instance locked_timeless γ : TimelessP (locked γ).
+ Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp Σ):
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index b5c0b7350e8c409bd972feace1b3113a0a3b771e..4d4d6cba841cbfb687b454444cb7562615f96ab7 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -59,9 +59,9 @@ Section proof.
Proof. solve_proper. Qed.
Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
Proof. solve_proper. Qed.
- Global Instance is_lock_persistent γ lk R : PersistentP (is_lock γ lk R).
+ Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
Proof. apply _. Qed.
- Global Instance locked_timeless γ : TimelessP (locked γ).
+ Global Instance locked_timeless γ : Timeless (locked γ).
Proof. apply _. Qed.
Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index bb4489e5eca99d6bb84ff329c5078b7e08cd34c6..f465765b473d5b432cc5bc96614bb96f61ff5a48 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -37,7 +37,7 @@ Global Instance ht_proper E :
Proof. solve_proper. Qed.
Lemma ht_mono E P P' Φ Φ' e :
(P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
-Proof. by intros; apply always_mono, wand_mono, wp_mono. Qed.
+Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
Global Instance ht_mono' E :
Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
Proof. solve_proper. Qed.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index f57fd0442c2b5b535a7b7656a22631ead9594720..1c3a8d3e34439ae1684659138937e0dd672729dd 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -75,7 +75,7 @@ Section lifting.
Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
- Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
+ Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
Proof. rewrite /ownP; apply _. Qed.
Lemma ownP_lift_step E Φ e1 :
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f51eb6f5d178f6620f12b686d3b1570c6e907370..e548668c04f1e2bbb649ec26228eabc86c801828 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -283,7 +283,7 @@ Section proofmode_classes.
ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
- (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
+ (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
atomic e →
ElimModal (|={E1,E2}=> P) P
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index beb33f1e1ec34c2b796db7ac13e27dc035ea7eee..234053f121ee02fc717e7ec1aa2e14b64be38c70 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -11,17 +11,17 @@ Implicit Types P Q R : uPred M.
(* FromAssumption *)
Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
-Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
+Proof. destruct p; by rewrite /FromAssumption /= ?persistently_elim. Qed.
Global Instance from_assumption_False p P : FromAssumption p False P | 1.
-Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
+Proof. destruct p; rewrite /FromAssumption /= ?persistently_pure; apply False_elim. Qed.
-Global Instance from_assumption_always_r P Q :
+Global Instance from_assumption_persistently_r P Q :
FromAssumption true P Q → FromAssumption true P (□ Q).
-Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
+Proof. rewrite /FromAssumption=><-. by rewrite persistent_persistently. Qed.
-Global Instance from_assumption_always_l p P Q :
+Global Instance from_assumption_persistently_l p P Q :
FromAssumption p P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Proof. rewrite /FromAssumption=><-. by rewrite persistently_elim. Qed.
Global Instance from_assumption_later p P Q :
FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
@@ -42,14 +42,14 @@ Proof. rewrite /FromAssumption=> <-. by rewrite forall_elim. Qed.
Global Instance into_pure_pure φ : @IntoPure M ⌜φ⌠φ.
Proof. done. Qed.
Global Instance into_pure_eq {A : ofeT} (a b : A) :
- Timeless a → @IntoPure M (a ≡ b) (a ≡ b).
-Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
-Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : 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) :
@IntoPure M (✓ a) (✓ a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
-Global Instance into_pure_always P φ : IntoPure P φ → IntoPure (□ P) φ.
-Proof. rewrite /IntoPure=> ->. by rewrite always_pure. Qed.
+Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (□ P) φ.
+Proof. rewrite /IntoPure=> ->. by rewrite persistently_pure. Qed.
Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
@@ -65,9 +65,7 @@ Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
-Proof.
- rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
-Qed.
+Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
Global Instance into_pure_exist {X : Type} (Φ : X → uPred M) (φ : X → Prop) :
(∀ x, @IntoPure M (Φ x) (φ x)) → @IntoPure M (∃ x, Φ x) (∃ x, φ x).
@@ -97,8 +95,8 @@ Proof.
rewrite -cmra_valid_intro //. auto with I.
Qed.
-Global Instance from_pure_always P φ : FromPure P φ → FromPure (□ P) φ.
-Proof. rewrite /FromPure=> <-. by rewrite always_pure. Qed.
+Global Instance from_pure_persistently P φ : FromPure P φ → FromPure (□ P) φ.
+Proof. rewrite /FromPure=> <-. by rewrite persistently_pure. Qed.
Global Instance from_pure_later P φ : FromPure P φ → FromPure (▷ P) φ.
Proof. rewrite /FromPure=> ->. apply later_intro. Qed.
Global Instance from_pure_laterN n P φ : FromPure P φ → FromPure (▷^n P) φ.
@@ -113,7 +111,7 @@ Global Instance from_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
Global Instance from_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∗ P2) (φ1 ∧ φ2).
-Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
+Proof. rewrite /FromPure pure_and and_sep_l. by intros -> ->. Qed.
Global Instance from_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
FromPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 ∨ P2) (φ1 ∨ φ2).
Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
@@ -122,9 +120,7 @@ Global Instance from_pure_pure_impl (φ1 φ2 : Prop) P1 P2 :
Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
Global Instance from_pure_pure_wand (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 → FromPure P2 φ2 → FromPure (P1 -∗ P2) (φ1 → φ2).
-Proof.
- rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
-Qed.
+Proof. rewrite /FromPure /IntoPure pure_impl impl_wand. by intros -> ->. Qed.
Global Instance from_pure_exist {X : Type} (Φ : X → uPred M) (φ : X → Prop) :
(∀ x, @FromPure M (Φ x) (φ x)) → @FromPure M (∃ x, Φ x) (∃ x, φ x).
@@ -139,14 +135,14 @@ Proof.
rewrite -Hx. apply pure_intro. done.
Qed.
-(* IntoPersistentP *)
-Global Instance into_persistentP_always_trans p P Q :
- IntoPersistentP true P Q → IntoPersistentP p (□ P) Q | 0.
-Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed.
-Global Instance into_persistentP_always P : IntoPersistentP true P P | 1.
+(* IntoPersistent *)
+Global Instance into_persistent_persistently_trans p P Q :
+ IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
+Proof. rewrite /IntoPersistent /==> ->. by rewrite persistent_persistently_if. Qed.
+Global Instance into_persistent_persistently P : IntoPersistent true P P | 1.
Proof. done. Qed.
-Global Instance into_persistentP_persistent P :
- PersistentP P → IntoPersistentP false P P | 100.
+Global Instance into_persistent_persistent P :
+ Persistent P → IntoPersistent false P P | 100.
Proof. done. Qed.
(* IntoLater *)
@@ -258,9 +254,9 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
-Global Instance from_later_always n P Q :
+Global Instance from_later_persistently n P Q :
FromLaterN n P Q → FromLaterN n (□ P) (□ Q).
-Proof. by rewrite /FromLaterN -always_laterN=> ->. Qed.
+Proof. by rewrite /FromLaterN -persistently_laterN=> ->. Qed.
Global Instance from_later_forall {A} n (Φ Ψ : A → uPred M) :
(∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
@@ -278,19 +274,19 @@ Global Instance wand_weaken_later p P Q P' Q' :
WandWeaken p P Q P' Q' → WandWeaken' p P Q (▷ P') (▷ Q').
Proof.
rewrite /WandWeaken' /WandWeaken=> ->.
- by rewrite always_if_later -later_wand -later_intro.
+ by rewrite persistently_if_later -later_wand -later_intro.
Qed.
Global Instance wand_weaken_laterN p n P Q P' Q' :
WandWeaken p P Q P' Q' → WandWeaken' p P Q (▷^n P') (▷^n Q').
Proof.
rewrite /WandWeaken' /WandWeaken=> ->.
- by rewrite always_if_laterN -laterN_wand -laterN_intro.
+ by rewrite persistently_if_laterN -laterN_wand -laterN_intro.
Qed.
Global Instance bupd_weaken_laterN p P Q P' Q' :
WandWeaken false P Q P' Q' → WandWeaken' p P Q (|==> P') (|==> Q').
Proof.
rewrite /WandWeaken' /WandWeaken=> ->.
- apply wand_intro_l. by rewrite always_if_elim bupd_wand_r.
+ apply wand_intro_l. by rewrite persistently_if_elim bupd_wand_r.
Qed.
Global Instance into_wand_wand p P P' Q Q' :
@@ -298,28 +294,28 @@ Global Instance into_wand_wand p P P' Q Q' :
Proof. done. Qed.
Global Instance into_wand_impl p P P' Q Q' :
WandWeaken p P Q P' Q' → IntoWand p (P → Q) P' Q'.
-Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed.
+Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand_1. Qed.
Global Instance into_wand_iff_l p P P' Q Q' :
WandWeaken p P Q P' Q' → IntoWand p (P ↔ Q) P' Q'.
-Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed.
+Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand_1. Qed.
Global Instance into_wand_iff_r p P P' Q Q' :
WandWeaken p Q P Q' P' → IntoWand p (P ↔ Q) Q' P'.
-Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
+Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
Global Instance into_wand_forall {A} p (Φ : A → uPred M) P Q x :
IntoWand p (Φ x) P Q → IntoWand p (∀ x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
-Global Instance into_wand_always p R P Q :
+Global Instance into_wand_persistently p R P Q :
IntoWand p R P Q → IntoWand p (□ R) P Q.
-Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
+Proof. rewrite /IntoWand=> ->. apply persistently_elim. Qed.
Global Instance into_wand_later p R P Q :
IntoWand p R P Q → IntoWand p (▷ R) (▷ P) (▷ Q).
-Proof. rewrite /IntoWand=> ->. by rewrite always_if_later -later_wand. Qed.
+Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_later -later_wand. Qed.
Global Instance into_wand_laterN p n R P Q :
IntoWand p R P Q → IntoWand p (▷^n R) (▷^n P) (▷^n Q).
-Proof. rewrite /IntoWand=> ->. by rewrite always_if_laterN -laterN_wand. Qed.
+Proof. rewrite /IntoWand=> ->. by rewrite persistently_if_laterN -laterN_wand. Qed.
Global Instance into_wand_bupd R P Q :
IntoWand false R P Q → IntoWand false (|==> R) (|==> P) (|==> Q).
@@ -339,19 +335,19 @@ Proof. by apply mk_from_and_and. Qed.
Global Instance from_and_sep P1 P2 : FromAnd false (P1 ∗ P2) P1 P2 | 100.
Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
- PersistentP P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
-Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
+ Persistent P1 → FromAnd true (P1 ∗ P2) P1 P2 | 9.
+Proof. intros. by rewrite /FromAnd and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
- PersistentP P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
-Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
+ Persistent P2 → FromAnd true (P1 ∗ P2) P1 P2 | 10.
+Proof. intros. by rewrite /FromAnd and_sep_r. Qed.
Global Instance from_and_pure p φ ψ : @FromAnd M p ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. apply mk_from_and_and. by rewrite pure_and. Qed.
-Global Instance from_and_always p P Q1 Q2 :
+Global Instance from_and_persistently p P Q1 Q2 :
FromAnd false P Q1 Q2 → FromAnd p (□ P) (□ Q1) (□ Q2).
Proof.
intros. apply mk_from_and_and.
- by rewrite always_and_sep_l' -always_sep -(from_and _ P).
+ by rewrite persistently_and_sep_l -persistently_sep -(from_and _ P).
Qed.
Global Instance from_and_later p P Q1 Q2 :
FromAnd p P Q1 Q2 → FromAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -370,7 +366,7 @@ Global Instance from_sep_ownM (a b1 b2 : M) :
FromAnd false (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromAnd -ownM_op -is_op. Qed.
Global Instance from_sep_ownM_persistent (a b1 b2 : M) :
- IsOp a b1 b2 → Or (Persistent b1) (Persistent b2) →
+ IsOp a b1 b2 → Or (CoreId b1) (CoreId b2) →
FromAnd true (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
intros ? Hper; apply mk_from_and_persistent; [destruct Hper; apply _|].
@@ -385,19 +381,19 @@ Global Instance from_and_big_sepL_cons {A} (Φ : nat → A → uPred M) x l :
FromAnd false ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
Proof. by rewrite /FromAnd big_sepL_cons. Qed.
Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
- PersistentP (Φ 0 x) →
+ Persistent (Φ 0 x) →
FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_cons and_sep_l. Qed.
Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
Proof. by rewrite /FromAnd big_opL_app. Qed.
Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M) l1 l2 :
- (∀ k y, PersistentP (Φ k y)) →
+ (∀ k y, Persistent (Φ k y)) →
FromAnd true ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
-Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
+Proof. intros. by rewrite /FromAnd big_opL_app and_sep_l. Qed.
(* FromOp *)
(* TODO: Worst case there could be a lot of backtracking on these instances,
@@ -406,11 +402,11 @@ Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
IsOp a b1 b2 → IsOp a' b1' b2' → IsOp' (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance is_op_pair_persistent_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
- Persistent a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
-Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
+ CoreId a → IsOp a' b1' b2' → IsOp' (a,a') (a,b1') (a,b2').
+Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
Global Instance is_op_pair_persistent_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
- Persistent a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
-Proof. constructor=> //=. by rewrite -persistent_dup. Qed.
+ CoreId a' → IsOp a b1 b2 → IsOp' (a,a') (b1,a') (b2,a').
+Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
IsOp a b1 b2 → IsOp' (Some a) (Some b1) (Some b2).
@@ -430,18 +426,18 @@ Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) ownM_op. Qed.
Global Instance into_and_and P Q : IntoAnd true (P ∧ Q) P Q.
Proof. done. Qed.
Global Instance into_and_and_persistent_l P Q :
- PersistentP P → IntoAnd false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoAnd /= always_and_sep_l. Qed.
+ Persistent P → IntoAnd false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoAnd /= and_sep_l. Qed.
Global Instance into_and_and_persistent_r P Q :
- PersistentP Q → IntoAnd false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoAnd /= always_and_sep_r. Qed.
+ Persistent Q → IntoAnd false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoAnd /= and_sep_r. Qed.
Global Instance into_and_pure p φ ψ : @IntoAnd M p ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ.
-Proof. apply mk_into_and_sep. by rewrite pure_and always_and_sep_r. Qed.
-Global Instance into_and_always p P Q1 Q2 :
+Proof. apply mk_into_and_sep. by rewrite pure_and and_sep_r. Qed.
+Global Instance into_and_persistently p P Q1 Q2 :
IntoAnd true P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
Proof.
- rewrite /IntoAnd=>->. destruct p; by rewrite ?always_and always_and_sep_r.
+ rewrite /IntoAnd=>->. destruct p; by rewrite ?persistently_and persistently_and_sep_r.
Qed.
Global Instance into_and_later p P Q1 Q2 :
IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
@@ -471,9 +467,9 @@ Proof. rewrite /IsApp=>->. apply mk_into_and_sep. by rewrite big_sepL_app. Qed.
(* Frame *)
Global Instance frame_here p R : Frame p R R True.
-Proof. by rewrite /Frame right_id always_if_elim. Qed.
+Proof. by rewrite /Frame right_id persistently_if_elim. Qed.
Global Instance frame_here_pure p φ Q : FromPure Q φ → Frame p ⌜φ⌠Q True.
-Proof. rewrite /FromPure /Frame=> ->. by rewrite always_if_elim right_id. Qed.
+Proof. rewrite /FromPure /Frame=> ->. by rewrite persistently_if_elim right_id. Qed.
Class MakeSep (P Q PQ : uPred M) := make_sep : P ∗ Q ⊣⊢ PQ.
Global Instance make_sep_true_l P : MakeSep True P P.
@@ -488,7 +484,7 @@ Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
Frame true R (P1 ∗ P2) Q' | 9.
Proof.
rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
- rewrite {1}(always_sep_dup (â–¡ R)). solve_sep_entails.
+ rewrite {1}(sep_dup (â–¡ R)). solve_sep_entails.
Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
@@ -563,7 +559,7 @@ Global Instance frame_later p R R' P Q Q' :
IntoLaterN 1 R' R → Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
- by rewrite always_if_later later_sep.
+ by rewrite persistently_if_later later_sep.
Qed.
Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ▷^n P ⊣⊢ lP.
@@ -576,20 +572,20 @@ Global Instance frame_laterN p n R R' P Q Q' :
IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-.
- by rewrite always_if_laterN laterN_sep.
+ by rewrite persistently_if_laterN laterN_sep.
Qed.
-Class MakeAlways (P Q : uPred M) := make_always : □ P ⊣⊢ Q.
-Global Instance make_always_true : MakeAlways True True.
-Proof. by rewrite /MakeAlways always_pure. Qed.
-Global Instance make_always_default P : MakeAlways P (â–¡ P) | 100.
+Class MakePersistently (P Q : uPred M) := make_persistently : □ P ⊣⊢ Q.
+Global Instance make_persistently_true : MakePersistently True True.
+Proof. by rewrite /MakePersistently persistently_pure. Qed.
+Global Instance make_persistently_default P : MakePersistently P (â–¡ P) | 100.
Proof. done. Qed.
-Global Instance frame_always R P Q Q' :
- Frame true R P Q → MakeAlways Q Q' → Frame true R (□ P) Q'.
+Global Instance frame_persistently R P Q Q' :
+ Frame true R P Q → MakePersistently Q Q' → Frame true R (□ P) Q'.
Proof.
- rewrite /Frame /MakeAlways=> <- <-.
- by rewrite always_sep /= always_always.
+ rewrite /Frame /MakePersistently=> <- <-.
+ by rewrite persistently_sep /= persistent_persistently.
Qed.
Class MakeExcept0 (P Q : uPred M) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -623,9 +619,9 @@ Global Instance from_or_bupd P Q1 Q2 :
Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
Global Instance from_or_pure φ ψ : @FromOr M ⌜φ ∨ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /FromOr pure_or. Qed.
-Global Instance from_or_always P Q1 Q2 :
+Global Instance from_or_persistently P Q1 Q2 :
FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
+Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
Global Instance from_or_later P Q1 Q2 :
FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.
@@ -641,9 +637,9 @@ Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
Proof. done. Qed.
Global Instance into_or_pure φ ψ : @IntoOr M ⌜φ ∨ ψ⌠⌜φ⌠⌜ψâŒ.
Proof. by rewrite /IntoOr pure_or. Qed.
-Global Instance into_or_always P Q1 Q2 :
+Global Instance into_or_persistently P Q1 Q2 :
IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite always_or. Qed.
+Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
Global Instance into_or_later P Q1 Q2 :
IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
@@ -665,9 +661,9 @@ Qed.
Global Instance from_exist_pure {A} (φ : A → Prop) :
@FromExist M A ⌜∃ x, φ x⌠(λ a, ⌜φ aâŒ)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
-Global Instance from_exist_always {A} P (Φ : A → uPred M) :
+Global Instance from_exist_persistently {A} P (Φ : A → uPred M) :
FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /FromExist=> <-. by rewrite always_exist. Qed.
+Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
Global Instance from_exist_later {A} P (Φ : A → uPred M) :
FromExist P Φ → FromExist (▷ P) (λ a, ▷ (Φ a))%I.
Proof.
@@ -688,6 +684,7 @@ Proof. done. Qed.
Global Instance into_exist_pure {A} (φ : A → Prop) :
@IntoExist M A ⌜∃ x, φ x⌠(λ a, ⌜φ aâŒ)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
+
Global Instance into_exist_and_pure P Q φ :
IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
Proof.
@@ -701,9 +698,9 @@ Proof.
apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.
-Global Instance into_exist_always {A} P (Φ : A → uPred M) :
+Global Instance into_exist_persistently {A} P (Φ : A → uPred M) :
IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
+Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
Global Instance into_exist_later {A} P (Φ : A → uPred M) :
IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
@@ -717,9 +714,9 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed.
(* IntoForall *)
Global Instance into_forall_forall {A} (Φ : A → uPred M) : IntoForall (∀ a, Φ a) Φ.
Proof. done. Qed.
-Global Instance into_forall_always {A} P (Φ : A → uPred M) :
+Global Instance into_forall_persistently {A} P (Φ : A → uPred M) :
IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
+Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
Global Instance into_forall_later {A} P (Φ : A → uPred M) :
IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
@@ -740,12 +737,12 @@ Global Instance from_forall_wand_pure P Q φ :
IntoPureT P φ → FromForall (P -∗ Q) (λ _ : φ, Q)%I.
Proof.
intros (φ'&->&?). rewrite /FromForall -pure_impl_forall.
- by rewrite always_impl_wand (into_pure P).
+ by rewrite impl_wand (into_pure P).
Qed.
-Global Instance from_forall_always {A} P (Φ : A → uPred M) :
+Global Instance from_forall_persistently {A} P (Φ : A → uPred M) :
FromForall P Φ → FromForall (□ P) (λ a, □ (Φ a))%I.
-Proof. rewrite /FromForall=> <-. by rewrite always_forall. Qed.
+Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
Global Instance from_forall_later {A} P (Φ : A → uPred M) :
FromForall P Φ → FromForall (▷ P) (λ a, ▷ (Φ a))%I.
Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
@@ -771,8 +768,8 @@ Proof.
rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.
-Global Instance elim_modal_always P Q : ElimModal (â–¡ P) P Q Q.
-Proof. intros. by rewrite /ElimModal always_elim wand_elim_r. Qed.
+Global Instance elim_modal_persistently P Q : ElimModal (â–¡ P) P Q Q.
+Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed.
Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
@@ -783,13 +780,13 @@ Proof.
by rewrite -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_timeless_bupd P Q :
- TimelessP P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
+ Timeless P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
Proof.
intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (timelessP P).
by rewrite -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_timeless_bupd' p P Q :
- TimelessP P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
+ Timeless P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
Proof.
destruct p; simpl; auto using elim_modal_timeless_bupd.
intros _ _. by rewrite /ElimModal wand_elim_r.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index caaa47f1784ba14068ee09c3031b249abaaaeb51..028fe94410b757b3ea6b83f188949f639c8296b2 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -15,7 +15,7 @@ Existing Instance Or_r | 10.
Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
from_assumption : □?p P ⊢ Q.
Arguments from_assumption {_} _ _ _ {_}.
-(* No need to restrict Hint Mode, we have a default instance that will always
+(* No need to restrict Hint Mode, we have a default instance that will persistently
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
@@ -54,10 +54,10 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌠⊢ P.
Arguments from_pure {_} _ _ {_}.
Hint Mode FromPure + ! - : typeclass_instances.
-Class IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
- into_persistentP : □?p P ⊢ □ Q.
-Arguments into_persistentP {_} _ _ _ {_}.
-Hint Mode IntoPersistentP + + ! - : typeclass_instances.
+Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
+ into_persistent : □?p P ⊢ □ Q.
+Arguments into_persistent {_} _ _ _ {_}.
+Hint Mode IntoPersistent + + ! - : typeclass_instances.
(* The class [IntoLaterN] has only two instances:
@@ -122,11 +122,11 @@ Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) :
(Q1 ∧ Q2 ⊢ P) → FromAnd p P Q1 Q2.
Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed.
Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
- Or (PersistentP Q1) (PersistentP Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
+ Or (Persistent Q1) (Persistent Q2) → (Q1 ∗ Q2 ⊢ P) → FromAnd true P Q1 Q2.
Proof.
intros [?|?] ?; rewrite /FromAnd.
- - by rewrite always_and_sep_l.
- - by rewrite always_and_sep_r.
+ - by rewrite and_sep_l.
+ - by rewrite and_sep_r.
Qed.
Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 50643dd05bb32f515983ff54e1e61a3fa1e245a8..923cb4fd383542ced465e307ce81b686b97eea3c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -140,7 +140,7 @@ Lemma envs_lookup_sound Δ i p P :
Proof.
rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- - rewrite (env_lookup_perm Γp) //= always_sep.
+ - rewrite (env_lookup_perm Γp) //= persistently_sep.
ecancel [□ [∗] _; □ P; [∗] Γs]%I; apply pure_intro.
destruct Hwf; constructor;
naive_solver eauto using env_delete_wf, env_delete_fresh.
@@ -152,11 +152,11 @@ Proof.
Qed.
Lemma envs_lookup_sound' Δ i p P :
envs_lookup i Δ = Some (p,P) → Δ ⊢ P ∗ envs_delete i p Δ.
-Proof. intros. rewrite envs_lookup_sound //. by rewrite always_if_elim. Qed.
+Proof. intros. rewrite envs_lookup_sound //. by rewrite persistently_if_elim. Qed.
Lemma envs_lookup_persistent_sound Δ i P :
envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
Proof.
- intros. apply (always_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
+ intros. apply (persistently_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
Qed.
Lemma envs_lookup_split Δ i p P :
@@ -164,7 +164,7 @@ Lemma envs_lookup_split Δ i p P :
Proof.
rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- - rewrite (env_lookup_perm Γp) //= always_sep.
+ - rewrite (env_lookup_perm Γp) //= persistently_sep.
rewrite pure_True // left_id.
cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
@@ -183,15 +183,15 @@ Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') → Δ ⊢ □?p [∗] Ps ∗ Δ'.
Proof.
revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
- { by rewrite always_pure left_id. }
+ { by rewrite persistently_pure left_id. }
destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
apply envs_lookup_delete_Some in Hj as [Hj ->].
destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
- rewrite always_if_sep -assoc. destruct q1; simpl.
+ rewrite persistently_if_sep -assoc. destruct q1; simpl.
- destruct rp.
- + rewrite envs_lookup_sound //; simpl. by rewrite IH // (always_elim_if q2).
- + rewrite envs_lookup_persistent_sound //. by rewrite IH // (always_elim_if q2).
- - rewrite envs_lookup_sound // IH //; simpl. by rewrite always_if_elim.
+ + rewrite envs_lookup_sound //; simpl. by rewrite IH // (persistently_elim_if q2).
+ + rewrite envs_lookup_persistent_sound //. by rewrite IH // (persistently_elim_if q2).
+ - rewrite envs_lookup_sound // IH //; simpl. by rewrite persistently_if_elim.
Qed.
Lemma envs_lookup_snoc Δ i p P :
@@ -216,7 +216,7 @@ Proof.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (strings.string_beq_reflect j i); naive_solver.
- + by rewrite always_sep assoc.
+ + by rewrite persistently_sep assoc.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (strings.string_beq_reflect j i); naive_solver.
@@ -234,7 +234,7 @@ Proof.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
naive_solver eauto using env_app_fresh.
+ rewrite (env_app_perm _ _ Γp') //.
- rewrite big_opL_app always_sep. solve_sep_entails.
+ rewrite big_opL_app persistently_sep. solve_sep_entails.
- destruct (env_app Γ Γp) eqn:Happ,
(env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
@@ -257,7 +257,7 @@ Proof.
intros j. apply (env_app_disjoint _ _ _ j) in Happ.
destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
+ rewrite (env_replace_perm _ _ Γp') //.
- rewrite big_opL_app always_sep. solve_sep_entails.
+ rewrite big_opL_app persistently_sep. solve_sep_entails.
- destruct (env_app Γ Γp) eqn:Happ,
(env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
apply wand_intro_l, sep_intro_True_l; [apply pure_intro|].
@@ -302,7 +302,7 @@ Proof.
Qed.
Lemma env_spatial_is_nil_persistent Δ :
- env_spatial_is_nil Δ = true → PersistentP Δ.
+ env_spatial_is_nil Δ = true → Persistent Δ.
Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
@@ -345,7 +345,7 @@ Lemma envs_split_sound Δ lr js Δ1 Δ2 :
envs_split lr js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ∗ Δ2.
Proof.
rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
- rewrite {2}envs_clear_spatial_sound sep_elim_l always_and_sep_r.
+ rewrite {2}envs_clear_spatial_sound sep_elim_l and_sep_r.
destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
apply envs_split_go_sound in HΔ as ->; last first.
{ intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
@@ -388,7 +388,7 @@ Proof. by constructor. Qed.
(** * Adequacy *)
Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
Proof.
- intros <-. rewrite /of_envs /= always_pure !right_id.
+ intros <-. rewrite /of_envs /= persistently_pure !right_id.
apply pure_intro; repeat constructor.
Qed.
@@ -450,8 +450,8 @@ Proof. by split. Qed.
Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n Δ2.
Proof.
- intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -always_laterN.
- repeat apply sep_mono; try apply always_mono.
+ intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
+ repeat apply sep_mono; try apply persistently_mono.
- rewrite -laterN_intro; apply pure_mono; destruct 1; constructor;
naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
- induction Hp; rewrite /= ?laterN_sep. apply laterN_intro. by apply sep_mono.
@@ -467,50 +467,50 @@ Lemma tac_löb Δ Δ' i Q :
envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
- intros ?? HQ. rewrite -(always_elim Q) -(löb (□ Q)) -always_later.
- apply impl_intro_l, (always_intro _ _).
+ intros ?? HQ. rewrite -(persistently_elim Q) -(löb (□ Q)) -persistently_later.
+ apply impl_intro_l, (persistently_intro _ _).
rewrite envs_app_sound //; simpl.
- by rewrite right_id always_and_sep_l' wand_elim_r HQ.
+ by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
Qed.
(** * Always *)
-Lemma tac_always_intro Δ Q :
+Lemma tac_persistently_intro Δ Q :
(envs_clear_spatial Δ ⊢ Q) → Δ ⊢ □ Q.
Proof.
intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
- by apply (always_intro _ _).
+ by apply (persistently_intro _ _).
Qed.
Lemma tac_persistent Δ Δ' i p P P' Q :
envs_lookup i Δ = Some (p, P) →
- IntoPersistentP p P P' →
+ IntoPersistent p P P' →
envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ? HP ? <-. rewrite envs_replace_sound //; simpl.
- by rewrite right_id (into_persistentP _ P) wand_elim_r.
+ by rewrite right_id (into_persistent _ P) wand_elim_r.
Qed.
(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
- (if env_spatial_is_nil Δ then TCTrue else PersistentP P) →
+ (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
envs_app false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ P → Q.
Proof.
intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
- - rewrite (persistentP Δ) envs_app_sound //; simpl.
- by rewrite right_id always_wand_impl always_elim.
+ - rewrite (persistent Δ) envs_app_sound //; simpl.
+ by rewrite right_id -persistently_impl_wand persistently_elim.
- apply impl_intro_l. rewrite envs_app_sound //; simpl.
- by rewrite always_and_sep_l right_id wand_elim_r.
+ by rewrite and_sep_l right_id wand_elim_r.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
- IntoPersistentP false P P' →
+ IntoPersistent false P P' →
envs_app true (Esnoc Enil i P') Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ P → Q.
Proof.
intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
- rewrite (_ : P = â–¡?false P) // (into_persistentP false P).
- by rewrite right_id always_and_sep_l wand_elim_r.
+ rewrite (_ : P = â–¡?false P) // (into_persistent false P).
+ by rewrite right_id persistently_and_sep_l wand_elim_r.
Qed.
Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
@@ -522,7 +522,7 @@ Proof.
intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
- IntoPersistentP false P P' →
+ IntoPersistent false P P' →
envs_app true (Esnoc Enil i P') Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
Proof.
@@ -552,11 +552,11 @@ Proof.
intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
- rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
- + by rewrite always_wand always_always !wand_elim_r.
+ + by rewrite persistently_wand persistent_persistently !wand_elim_r.
+ by rewrite !wand_elim_r.
- rewrite envs_lookup_sound //; simpl.
rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
- by rewrite right_id assoc (into_wand _ R) always_if_elim wand_elim_r wand_elim_r.
+ by rewrite right_id assoc (into_wand _ R) persistently_if_elim wand_elim_r wand_elim_r.
Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
@@ -574,7 +574,7 @@ Proof.
rewrite (envs_app_sound Δ2) //; simpl.
rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
- by rewrite always_if_elim assoc !wand_elim_r.
+ by rewrite persistently_if_elim assoc !wand_elim_r.
Qed.
Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
@@ -590,7 +590,7 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
Proof.
intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
- rewrite (into_wand _ R) assoc -(comm _ P1') -assoc always_if_elim.
+ rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite assoc !wand_elim_r.
Qed.
@@ -608,29 +608,29 @@ Qed.
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ') →
- IntoWand false R P1 P2 → PersistentP P1 →
+ IntoWand false R P1 P2 → Persistent P1 →
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
(Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
Proof.
intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
rewrite envs_lookup_sound //.
rewrite -(idemp uPred_and (envs_delete _ _ _)).
- rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
+ rewrite {1}HP1 (persistent P1) persistently_and_sep_l assoc.
rewrite envs_simple_replace_sound' //; simpl.
- rewrite right_id (into_wand _ R) (always_elim_if q) -always_if_sep wand_elim_l.
+ rewrite right_id (into_wand _ R) (persistently_elim_if q) -persistently_if_sep wand_elim_l.
by rewrite wand_elim_r.
Qed.
Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
envs_lookup j Δ = Some (q,P) →
- (Δ ⊢ R) → PersistentP R →
+ (Δ ⊢ R) → Persistent R →
envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ? HR ?? <-.
- rewrite -(idemp uPred_and Δ) {1}HR always_and_sep_l.
+ rewrite -(idemp uPred_and Δ) {1}HR and_sep_l.
rewrite envs_replace_sound //; simpl.
- by rewrite right_id assoc (sep_elim_l R) always_always wand_elim_r.
+ by rewrite right_id assoc (sep_elim_l R) persistent_persistently wand_elim_r.
Qed.
Lemma tac_revert Δ Δ' i p P Q :
@@ -638,7 +638,7 @@ Lemma tac_revert Δ Δ' i p P Q :
(Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q.
Proof.
intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
- by rewrite HQ /uPred_always_if wand_elim_r.
+ by rewrite HQ /uPred_persistently_if wand_elim_r.
Qed.
Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
@@ -659,7 +659,7 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
(of_envs Δ ⊢ Q).
Proof.
rewrite /IntoIH. intros HP ? HPQ.
- by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP // HPQ impl_elim_r.
+ by rewrite -(idemp uPred_and Δ) {1}(persistent Δ) {1}HP // HPQ impl_elim_r.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
@@ -676,11 +676,11 @@ Qed.
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P Q :
envs_split lr js Δ = Some (Δ1,Δ2) →
envs_app false (Esnoc Enil j P) Δ = Some Δ' →
- PersistentP P →
+ Persistent P →
(Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
- rewrite HP sep_elim_l (always_and_sep_l P) envs_app_sound //; simpl.
+ rewrite HP sep_elim_l (and_sep_l P) envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
Qed.
@@ -690,7 +690,7 @@ Lemma tac_assert_pure Δ Δ' j P φ Q :
φ → (Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ??? <-. rewrite envs_app_sound //; simpl.
- by rewrite right_id -(from_pure P) pure_True // -always_impl_wand True_impl.
+ by rewrite right_id -(from_pure P) pure_True // -impl_wand True_impl.
Qed.
Lemma tac_pose_proof Δ Δ' j P Q :
@@ -699,7 +699,7 @@ Lemma tac_pose_proof Δ Δ' j P Q :
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros HP ? <-. rewrite envs_app_sound //; simpl.
- by rewrite right_id -HP always_pure wand_True.
+ by rewrite right_id -HP persistently_pure wand_True.
Qed.
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -748,7 +748,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
Proof.
intros ?? A Δ' x y Φ HPxy HP ?? <-.
rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
- rewrite sep_elim_l HPxy always_and_sep_r.
+ rewrite sep_elim_l HPxy and_sep_r.
rewrite (envs_simple_replace_sound _ _ j) //; simpl.
rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr.
- apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I);
@@ -803,7 +803,7 @@ Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
- by destruct p; rewrite /= ?right_id (comm _ P1) ?always_and_sep wand_elim_r.
+ by destruct p; rewrite /= ?right_id (comm _ P1) ?persistently_and_sep wand_elim_r.
Qed.
(* Using this tactic, one can destruct a (non-separating) conjunction in the
@@ -824,7 +824,7 @@ Qed.
Lemma tac_frame_pure Δ (φ : Prop) P Q :
φ → Frame true ⌜φ⌠P Q → (Δ ⊢ Q) → Δ ⊢ P.
Proof.
- intros ?? ->. by rewrite -(frame ⌜φ⌠P) /= always_pure pure_True // left_id.
+ intros ?? ->. by rewrite -(frame ⌜φ⌠P) /= persistently_pure pure_True // left_id.
Qed.
Lemma tac_frame Δ Δ' i p R P Q :
@@ -849,7 +849,7 @@ Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
(Δ1 ⊢ Q) → (Δ2 ⊢ Q) → Δ ⊢ Q.
Proof.
intros ???? HP1 HP2. rewrite envs_lookup_sound //.
- rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
+ rewrite (into_or P) persistently_if_or sep_or_r; apply or_elim.
- rewrite (envs_simple_replace_sound' _ Δ1) //.
by rewrite /= right_id wand_elim_r.
- rewrite (envs_simple_replace_sound' _ Δ2) //.
@@ -890,7 +890,7 @@ Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
Δ ⊢ Q.
Proof.
intros ?? HΦ. rewrite envs_lookup_sound //.
- rewrite (into_exist P) always_if_exist sep_exist_r.
+ rewrite (into_exist P) persistently_if_exist sep_exist_r.
apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Qed.
@@ -906,6 +906,6 @@ Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
(Δ' ⊢ Q') → Δ ⊢ Q.
Proof.
intros ??? HΔ. rewrite envs_replace_sound //; simpl.
- rewrite right_id HΔ always_if_elim. by apply elim_modal.
+ rewrite right_id HΔ persistently_if_elim. by apply elim_modal.
Qed.
End tactics.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5295e6dba1d5c212bbf04e5c42e8d4658cf09a9d..cfc0658260fd598ed221f0fac755a92a0be74082 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -166,7 +166,7 @@ Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
[env_reflexivity || fail "iPersistent:" H "not found"
|apply _ ||
- let Q := match goal with |- IntoPersistentP _ ?Q _ => Q end in
+ let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
fail "iPersistent:" Q "not persistent"
|env_reflexivity|].
@@ -300,7 +300,7 @@ Local Tactic Notation "iIntro" constr(H) :=
[ (* (?Q → _) *)
eapply tac_impl_intro with _ H; (* (i:=H) *)
[env_cbv; apply _ ||
- let P := lazymatch goal with |- PersistentP ?P => P end in
+ let P := lazymatch goal with |- Persistent ?P => P end in
fail 1 "iIntro: introducing non-persistent" H ":" P
"into non-empty spatial context"
|env_reflexivity || fail "iIntro:" H "not fresh"
@@ -317,14 +317,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
[ (* (?P → _) *)
eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
[apply _ ||
- let P := match goal with |- IntoPersistentP _ ?P _ => P end in
+ let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail 1 "iIntro: " P " not persistent"
|env_reflexivity || fail 1 "iIntro:" H "not fresh"
|]
| (* (?P -∗ _) *)
eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
[apply _ ||
- let P := match goal with |- IntoPersistentP _ ?P _ => P end in
+ let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail 1 "iIntro: " P " not persistent"
|env_reflexivity || fail 1 "iIntro:" H "not fresh"
|]
@@ -426,7 +426,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|apply _ ||
- let Q := match goal with |- PersistentP ?Q => Q end in
+ let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
|env_reflexivity
|iFrame Hs_frame; done_if d (*goal*)
@@ -452,7 +452,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|apply _ ||
- let Q := match goal with |- PersistentP ?Q => Q end in
+ let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
|env_reflexivity
|solve [iFrame "∗ #"]
@@ -501,7 +501,7 @@ Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
[env_reflexivity || fail "iSpecialize:" H "not found"
|iSpecializeArgs H xs; iSpecializePat H pat; last (iExact H)
|apply _ ||
- let Q := match goal with |- PersistentP ?Q => Q end in
+ let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
|env_reflexivity|(* goal *)]
| false => iSpecializeArgs H xs; iSpecializePat H pat
@@ -802,8 +802,8 @@ Local Tactic Notation "iExistDestruct" constr(H)
(** * Always *)
Tactic Notation "iAlways":=
iStartProof;
- apply tac_always_intro; env_cbv
- || fail "iAlways: the goal is not an always modality".
+ apply tac_persistently_intro; env_cbv
+ || fail "iAlways: the goal is not an persistently modality".
(** * Later *)
Tactic Notation "iNext" open_constr(n) :=
@@ -1217,7 +1217,7 @@ Instance copy_destruct_impl {M} (P Q : uPred M) :
CopyDestruct Q → CopyDestruct (P → Q).
Instance copy_destruct_wand {M} (P Q : uPred M) :
CopyDestruct Q → CopyDestruct (P -∗ Q).
-Instance copy_destruct_always {M} (P : uPred M) :
+Instance copy_destruct_persistently {M} (P : uPred M) :
CopyDestruct P → CopyDestruct (□ P).
Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 5896d63912131dc0e63bc5e214243e58859f496c..5fedc7f4cd2cf9a618b7c9d938dcbdbcd2920b3f 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -152,17 +152,17 @@ 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).
+ Global Instance frag_core_id n : CoreId (Frag n).
Proof. by constructor. Qed.
Lemma auth_frag_valid j n : ✓ (Auth n ⋅ Frag j) → (j ≤ n)%nat.
Proof. simpl. case_decide. done. by intros []. Qed.
@@ -191,7 +191,7 @@ Section counter_proof.
(∃ N γ, inv N (I γ l) ∧ own γ (Frag n))%I.
(** The main proofs. *)
- Global Instance C_persistent l n : PersistentP (C l n).
+ Global Instance C_persistent l n : Persistent (C l n).
Proof. apply _. Qed.
Lemma newcounter_spec :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index ef633861b4fc3517ad8df26f5369faa4a70cd740..71505deab13254b7af0dbea0c04a4133b18e39a7 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -78,7 +78,7 @@ Proof.
done.
Qed.
-Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P → Q → P ∗ Q)%I.
+Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∗ Q)%I.
Proof. iIntros "H1 H2". by iFrame. Qed.
Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌠→ P → ⌜ φ ∧ ψ ⌠∧ P)%I.
@@ -142,11 +142,11 @@ Proof.
iSpecialize ("H" $! _ [#10]). done.
Qed.
-Lemma test_eauto_iFramE P Q R `{!PersistentP R} :
+Lemma test_eauto_iFramE P Q R `{!Persistent R} :
P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
Proof. eauto with iFrame. Qed.
-Lemma test_iCombine_persistent P Q R `{!PersistentP R} :
+Lemma test_iCombine_persistent P Q R `{!Persistent R} :
P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
@@ -177,7 +177,7 @@ Lemma test_iFrame_persistent (P Q : uPred M) :
□ P -∗ Q -∗ □ (P ∗ P) ∗ (P ∧ Q ∨ Q).
Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
-Lemma test_iSplit_always P Q : □ P -∗ □ (P ∗ P).
+Lemma test_iSplit_persistently P Q : □ P -∗ □ (P ∗ P).
Proof. iIntros "#?". by iSplit. Qed.
Lemma test_iSpecialize_persistent P Q :