Remove useless notion ValidTimeless.

modures/auth.v

@@ -134,14 +134,6 @@ Proof.
   split; simpl; [apply ra_empty_valid|].
   by intros x; constructor; simpl; rewrite (left_id _ _).
 Qed.
-Global Instance auth_frag_valid_timeless (x : A) :
-  ValidTimeless x → ValidTimeless (◯ x).
-Proof. by intros ??; apply (valid_timeless x). Qed.
-Global Instance auth_valid_timeless `{Empty A, !RAIdentity A} (x : A) :
-  ValidTimeless x → ValidTimeless (● x).
-Proof.
-  by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
-Qed.
 Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
 Lemma auth_includedN' n (x y : authC A) :

modures/cmra.v

@@ -116,13 +116,6 @@ Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
 Infix "⇝" := cmra_update (at level 70).
 Instance: Params (@cmra_update) 3.
 
-(** Timeless validity *)
-(* Not sure whether this is useful, see the rule [uPred_valid_elim_timeless]
-in logic.v *)
-Class ValidTimeless {A : cmraT} (x : A) :=
-  valid_timeless : validN 1 x → valid x.
-Arguments valid_timeless {_} _ {_} _.
-
 (** Properties **)
 Section cmra.
 Context {A : cmraT}.
@@ -275,8 +268,6 @@ Section discrete.
   Qed.
   Definition discreteRA : cmraT :=
     CMRAT discrete_cofe_mixin discrete_cmra_mixin discrete_extend_mixin.
-  Global Instance discrete_timeless (x : A) : ValidTimeless (x : discreteRA).
-  Proof. by intros ?. Qed.
   Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} :
     (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → (x : discreteRA) ⇝: P.
   Proof.
@@ -344,9 +335,6 @@ Section prod.
   Qed.
   Canonical Structure prodRA : cmraT :=
     CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin.
-  Instance pair_timeless (x : A) (y : B) :
-    ValidTimeless x → ValidTimeless y → ValidTimeless (x,y).
-  Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
 End prod.
 Arguments prodRA : clear implicits.
 

modures/excl.v

@@ -127,8 +127,6 @@ Proof.
 Qed.
 Canonical Structure exclRA : cmraT :=
   CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
-Global Instance excl_valid_timeless (x : excl A) : ValidTimeless x.
-Proof. by destruct x; intros ?. Qed.
 
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.

modures/fin_maps.v

@@ -151,25 +151,6 @@ Proof.
 Qed.
 Canonical Structure mapRA : cmraT :=
   CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
-
-Global Instance map_empty_valid_timeless : ValidTimeless (∅ : gmap K A).
-Proof. by intros ??; rewrite lookup_empty. Qed.
-Global Instance map_ra_insert_valid_timeless (m : gmap K A) i x:
-  ValidTimeless x → ValidTimeless m → m !! i = None →
-  ValidTimeless (<[i:=x]>m).
-Proof.
-  intros ?? Hi Hm j; destruct (decide (i = j)); simplify_map_equality.
-  { specialize (Hm j); simplify_map_equality. by apply (valid_timeless _). }
-  generalize j; clear dependent j; rapply (valid_timeless m).
-  intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|].
-  by specialize (Hm j); simplify_map_equality.
-Qed.
-Global Instance map_ra_singleton_valid_timeless (i : K) x :
-  ValidTimeless x → ValidTimeless {[ i ↦ x ]}.
-Proof.
-  intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _).
-  by rewrite lookup_empty.
-Qed.
 End cmra.
 Arguments mapRA _ {_ _} _.
 

modures/logic.v

@@ -706,12 +706,15 @@ Lemma own_valid (a : M) : uPred_own a ⊆ (✓ a)%I.
 Proof. move => x n Hv [a' ?]; cofe_subst; eauto using cmra_valid_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True%I ⊆ (✓ a : uPred M)%I.
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
-Lemma valid_elim_timeless {A : cmraT} (a : A) :
-  ValidTimeless a → ¬ ✓ a → (✓ a : uPred M)%I ⊆ False%I.
+Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{1} a → (✓ a : uPred M)%I ⊆ False%I.
 Proof.
-  intros ? Hvalid x [|n] ??; [done|apply Hvalid].
-  apply (valid_timeless _), cmra_valid_le with (S n); auto with lia.
+  intros Ha x [|n] ??; [|apply Ha, cmra_valid_le with (S n)]; auto with lia.
 Qed.
+Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
+  (∀ n, ✓{n} a → ✓{n} b) → (✓ a)%I ⊆ (✓ b : uPred M)%I.
+Proof. by intros ? x n ?; simpl; auto. Qed.
+Lemma own_invalid (a : M) : ¬ ✓{1} a → uPred_own a ⊆ False%I.
+Proof. by intros; rewrite ->own_valid, ->valid_elim. Qed.
 
 (* Big ops *)
 Global Instance uPred_big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M).

modures/option.v

@@ -142,12 +142,6 @@ Lemma option_op_positive_dist_l n x y : x ⋅ y ={n}= None → x ={n}= None.
 Proof. by destruct x, y; inversion_clear 1. Qed.
 Lemma option_op_positive_dist_r n x y : x ⋅ y ={n}= None → y ={n}= None.
 Proof. by destruct x, y; inversion_clear 1. Qed.
-
-Global Instance None_valid_timeless : ValidTimeless (@None A).
-Proof. done. Qed.
-Global Instance Some_valid_timeless x :
-  ValidTimeless x → ValidTimeless (Some x).
-Proof. by intros ? y; apply (valid_timeless x). Qed.
 End cmra.
 
 Arguments optionRA : clear implicits.