From 4886e15fa52d87b560934bdebc43a03a93a8ecdf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 Oct 2017 13:39:08 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`Timeless`=20=E2=86=92=20`Discrete`=20?=
=?UTF-8?q?(discrete=20OFE=20elements).?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
theories/algebra/agree.v | 6 +--
theories/algebra/auth.v | 6 +--
theories/algebra/cmra.v | 24 ++++++------
theories/algebra/csum.v | 10 ++---
theories/algebra/excl.v | 8 ++--
theories/algebra/frac_auth.v | 8 ++--
theories/algebra/gmap.v | 22 +++++------
theories/algebra/iprod.v | 22 +++++------
theories/algebra/list.v | 8 ++--
theories/algebra/local_updates.v | 6 +--
theories/algebra/ofe.v | 56 ++++++++++++++--------------
theories/algebra/vector.v | 8 ++--
theories/base_logic/derived.v | 8 ++--
theories/base_logic/lib/own.v | 2 +-
theories/base_logic/primitive.v | 4 +-
theories/proofmode/class_instances.v | 4 +-
16 files changed, 100 insertions(+), 102 deletions(-)
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index f11577309..2356a14c5 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -149,12 +149,12 @@ Proof. rewrite /CMRATotal; eauto. Qed.
Global Instance agree_persistent (x : agree A) : Persistent x.
Proof. by constructor. Qed.
-Global Instance agree_ofe_discrete : OFEDiscrete A → CMRADiscrete agreeR.
+Global Instance agree_cmra_discrete : OFEDiscrete A → CMRADiscrete agreeR.
Proof.
intros HD. split.
- - intros x y [H H'] n; split=> a; setoid_rewrite <-(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 :=
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index cb65e14e8..f29794655 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -49,9 +49,9 @@ 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 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).
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index fb78065ee..7c1067fca 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -530,22 +530,22 @@ 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 *)
@@ -557,7 +557,7 @@ Qed.
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 *)
@@ -567,7 +567,7 @@ Lemma cancelable x `{!Cancelable x} y z : ✓(x ⋅ y) → x ⋅ y ≡ x ⋅ z
Proof. rewrite !equiv_dist cmra_valid_validN. intros. by apply (cancelableN x). Qed.
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.
@@ -598,7 +598,7 @@ Proof. rewrite comm. eauto using id_free_r. Qed.
Lemma discrete_id_free x `{CMRADiscrete A}:
(∀ y, ✓ x → x ⋅ y ≡ x → False) → IdFree x.
Proof.
- intros Hx y ??. apply (Hx y), (timeless _); eauto using cmra_discrete_valid.
+ 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.
@@ -845,7 +845,7 @@ 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).
Proof. by destruct H. Qed.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index a4185fee3..c1536c960 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -97,15 +97,15 @@ Next Obligation.
Qed.
Global Instance csum_ofe_discrete : OFEDiscrete A → OFEDiscrete B → OFEDiscrete csumC.
-Proof. by inversion_clear 3; constructor; apply (timeless _). Qed.
+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.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index e7f2385ed..b5f99ab6c 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -60,13 +60,13 @@ Proof.
Qed.
Global Instance excl_ofe_discrete : OFEDiscrete A → OFEDiscrete exclC.
-Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
+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 *)
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 3107f8331..09294255e 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.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 9ae5fba83..310f2598e 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -38,7 +38,7 @@ Next Obligation.
Qed.
Global Instance gmap_ofe_discrete : OFEDiscrete A → OFEDiscrete gmapC.
-Proof. intros ? m m' ? i. by apply (timeless _). Qed.
+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 _ {_ _} _.
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 60fb8fea4..9b116b172 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.
@@ -140,9 +140,9 @@ Section iprod_cmra.
Qed.
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_empty_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.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index c008b004c..6a647027f 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -78,12 +78,12 @@ Next Obligation.
Qed.
Global Instance list_ofe_discrete : OFEDiscrete A → OFEDiscrete listC.
-Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
+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.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 0884225f3..8667cbe67 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -56,8 +56,8 @@ Section updates.
(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' :
@@ -76,7 +76,7 @@ Section updates.
(✓ 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.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index afe5aa35a..e4defa69a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -99,15 +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.
-
-Class OFEDiscrete (A : ofeT) := ofe_discrete_timeless (x : A) :> Timeless x.
+(** 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 OFEDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
Hint Mode OFEDiscrete ! : typeclass_instances.
(** OFEs with a completion *)
@@ -165,8 +163,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 +186,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 +271,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.
@@ -683,9 +681,9 @@ 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 (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,10 +862,10 @@ 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 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.
@@ -993,7 +991,7 @@ Section option.
Qed.
Global Instance option_ofe_discrete : OFEDiscrete A → OFEDiscrete optionC.
- Proof. destruct 2; constructor; by apply (timeless _). Qed.
+ Proof. destruct 2; constructor; by apply (discrete _). Qed.
Global Instance Some_ne : NonExpansive (@Some A).
Proof. by constructor. Qed.
@@ -1005,10 +1003,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,8 +1222,8 @@ 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 (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/vector.v b/theories/algebra/vector.v
index d6a91347d..f8cfc7b0b 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -21,13 +21,13 @@ 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_ofe_discrete m : OFEDiscrete A → OFEDiscrete (vecC m).
Proof. intros ? v. induction v; apply _. Qed.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index aceaa62ea..521b45989 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -794,7 +794,7 @@ Proof.
by rewrite -bupd_intro -or_intro_l.
Qed.
-(* Timeless instances *)
+(* Discrete instances *)
Global Instance TimelessP_proper : Proper ((≡) ==> iff) (@TimelessP M).
Proof. solve_proper. Qed.
Global Instance pure_timeless φ : TimelessP (⌜φ⌠: uPred M)%I.
@@ -848,9 +848,9 @@ Proof. intros; rewrite /TimelessP except_0_always -always_later; auto. Qed.
Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?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 → TimelessP (a ≡ b : uPred M)%I.
+Proof. intros. rewrite /TimelessP !discrete_eq. apply (timelessP _). Qed.
+Global Instance ownM_timeless (a : M) : Discrete a → TimelessP (uPred_ownM a).
Proof.
intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b.
rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 4049d8dc2..0774fd641 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -106,7 +106,7 @@ Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
Proof. by rewrite comm -own_valid_r. Qed.
-Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
+Global Instance own_timeless γ a : Discrete a → TimelessP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 08ed253eb..3a180f3e1 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -563,9 +563,9 @@ Proof. by unseal. Qed.
(* Discrete *)
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/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index beb33f1e1..18f94ea69 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -42,8 +42,8 @@ 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.
+ 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.
--
GitLab