Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/auth.v

@@ -14,7 +14,8 @@ Notation "● a" := (Auth (Excl a) ∅) (at level 20).
 (* COFE *)
 Section cofe.
 Context {A : cofeT}.
-Implicit Types a b : A.
+Implicit Types a : excl A.
+Implicit Types b : A.
 Implicit Types x y : auth A.
 
 Instance auth_equiv : Equiv (auth A) := λ x y,
@@ -51,9 +52,12 @@ Proof.
     apply (conv_compl n (chain_map own c)).
 Qed.
 Canonical Structure authC := CofeT auth_cofe_mixin.
-Global Instance auth_timeless (x : auth A) :
-  Timeless (authoritative x) → Timeless (own x) → Timeless x.
-Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). 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.
+Proof. intros ? [??]; apply _. Qed.
 Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
 Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
 End cofe.
@@ -87,6 +91,7 @@ Instance auth_op : Op (auth A) := λ x y,
   Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y).
 Instance auth_minus : Minus (auth A) := λ x y,
   Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y).
+
 Lemma auth_included (x y : auth A) :
   x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
 Proof.
@@ -136,6 +141,12 @@ Proof.
     by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
 Qed.
 Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
+Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authRA.
+Proof.
+  split; first apply _.
+  intros [[] ?]; by rewrite /= /cmra_valid /cmra_validN /=
+    -?cmra_discrete_included_iff -?cmra_discrete_valid_iff.
+Qed.
 
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :

algebra/cmra.v

@@ -134,6 +134,12 @@ Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
 }.
 Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅.
 
+(** * Discrete CMRAs *)
+Class CMRADiscrete (A : cmraT) : Prop := {
+  cmra_discrete :> Discrete A;
+  cmra_discrete_valid (x : A) : ✓{0} x → ✓ x
+}.
+
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
@@ -319,6 +325,24 @@ Proof.
   by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
 Qed.
 
+(** ** Discrete *)
+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.
+Proof.
+  split; first by rewrite cmra_included_includedN.
+  intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
+Qed.
+Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A → Prop) :
+  (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
+Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
+Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
+  (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
+Proof. intros ? n. by setoid_rewrite <-cmra_discrete_valid_iff. Qed.
+
 (** ** RAs with an empty element *)
 Section identity.
   Context `{Empty A, !CMRAIdentity A}.
@@ -473,7 +497,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
 }.
 
 Section discrete.
-  Context {A : cofeT} `{∀ x : A, Timeless x}.
+  Context {A : cofeT} `{Discrete A}.
   Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
@@ -486,12 +510,8 @@ Section discrete.
       apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
-  Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
-    (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
-  Proof. intros Hvalid n z; apply Hvalid. Qed.
-  Lemma discrete_update (x y : discreteRA) :
-    (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y.
-  Proof. intros Hvalid n z; apply Hvalid. Qed.
+  Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
+  Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
 End discrete.
 
 (** ** CMRA for the unit type *)
@@ -506,7 +526,8 @@ Section unit.
   Canonical Structure unitRA : cmraT :=
     Eval cbv [unitC discreteRA cofe_car] in discreteRA unit_ra.
   Global Instance unit_cmra_identity : CMRAIdentity unitRA.
-  Proof. by split. Qed.
+  Global Instance unit_cmra_discrete : CMRADiscrete unitRA.
+  Proof. by apply discrete_cmra_discrete. Qed.
 End unit.
 
 (** ** Product *)
@@ -563,6 +584,10 @@ Section prod.
     - by split; rewrite /=left_id.
     - by intros ? [??]; split; apply (timeless _).
   Qed.
+  Global Instance prod_cmra_discrete :
+    CMRADiscrete A → CMRADiscrete B → CMRADiscrete prodRA.
+  Proof. split. apply _. by intros ? []; split; apply cmra_discrete_valid. Qed.
+
   Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
   Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
   Lemma prod_updateP P1 P2 (Q : A * B → Prop)  x :

algebra/cofe.v

@@ -90,6 +90,11 @@ Section cofe_mixin.
   Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
 End cofe_mixin.
 
+(** Discrete COFEs and Timeless elements *)
+Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
+Arguments timeless {_} _ {_} _ _.
+Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.
+
 (** General properties *)
 Section cofe.
   Context {A : cofeT}.
@@ -136,6 +141,12 @@ Section cofe.
   Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
   Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
     Proper ((≡) ==> (≡)) f | 100 := _.
+
+  Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
+  Proof.
+    split; intros; [by apply equiv_dist|].
+    apply (timeless _), dist_le with n; auto with lia.
+  Qed.
 End cofe.
 
 (** Mapping a chain *)
@@ -144,15 +155,6 @@ Program Definition chain_map `{Dist A, Dist B} (f : A → B)
   {| chain_car n := f (c n) |}.
 Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
 
-(** Timeless elements *)
-Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
-Arguments timeless {_} _ {_} _ _.
-Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
-Proof.
-  split; intros; [by apply equiv_dist|].
-  apply (timeless _), dist_le with n; auto with lia.
-Qed.
-
 (** Fixpoint *)
 Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
@@ -256,7 +258,7 @@ Section unit.
   Definition unit_cofe_mixin : CofeMixin unit.
   Proof. by repeat split; try exists 0. Qed.
   Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
-  Global Instance unit_timeless (x : ()) : Timeless x.
+  Global Instance unit_discrete_cofe : Discrete unitC.
   Proof. done. Qed.
 End unit.
 
@@ -285,6 +287,8 @@ Section product.
   Global Instance pair_timeless (x : A) (y : B) :
     Timeless x → Timeless y → Timeless (x,y).
   Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
+  Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC.
+  Proof. intros ?? [??]; apply _. Qed.
 End product.
 
 Arguments prodC : clear implicits.
@@ -315,8 +319,8 @@ Section discrete_cofe.
       symmetry; apply (chain_cauchy c 0 (S n)); omega.
   Qed.
   Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
-  Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
-  Proof. by intros y. Qed.
+  Global Instance discrete_discrete_cofe : Discrete discreteC.
+  Proof. by intros x y. Qed.
 End discrete_cofe.
 Arguments discreteC _ {_ _}.
 

algebra/dec_agree.v

 From algebra Require Export cmra.
-From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
 Local Arguments unit _ _ !_ /.
 
-(* This is isomorphic to optiob, but has a very different RA structure. *)
+(* This is isomorphic to option, but has a very different RA structure. *)
 Inductive dec_agree (A : Type) : Type := 
   | DecAgree : A → dec_agree A
   | DecAgreeBot : dec_agree A.
@@ -35,33 +34,23 @@ Proof.
   - apply _.
   - apply _.
   - apply _.
-  - intros [?|] [?|] [?|]; simpl; repeat (case_match; simpl); subst; congruence.
-  - intros [?|] [?|]; simpl; repeat (case_match; simpl); try subst; congruence.
-  - intros [?|]; simpl; repeat (case_match; simpl); try subst; congruence.
-  - intros [?|]; simpl; repeat (case_match; simpl); try subst; congruence.
-  - intros [?|] [?|] ?; simpl; done.
-  - intros [?|] [?|] ?; simpl; done.
-  - intros [?|] [?|] [[?|]]; simpl; repeat (case_match; simpl); subst;
-      try congruence; [].
-    case=>EQ. destruct EQ. done.
+  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
+  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
+  - intros [?|]; by repeat (simplify_eq/= || case_match).
+  - intros [?|]; by repeat (simplify_eq/= || case_match).
+  - by intros [?|] [?|] ?.
+  - by intros [?|] [?|] ?.
+  - intros [?|] [?|] [[?|]]; fold_leibniz;
+      intros; by repeat (simplify_eq/= || case_match).
 Qed.
 
 Canonical Structure dec_agreeRA : cmraT := discreteRA dec_agree_ra.
 
 (* Some properties of this CMRA *)
 Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x ≡ x.
-Proof.
-  destruct x as [x|]; simpl; repeat (case_match; simpl); try subst; congruence.
-Qed.
+Proof. destruct x; by repeat (simplify_eq/= || case_match). Qed.
 
 Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 ≡ x2.
-Proof.
-  destruct x1 as [x1|], x2 as [x2|]; simpl;repeat (case_match; simpl); by subst.
-Qed.
-
-Lemma dec_agree_equivI {M} a b : (DecAgree a ≡ DecAgree b)%I ≡ (a = b : uPred M)%I.
-Proof. do 2 split. by case. by destruct 1. Qed.
-Lemma dec_agree_validI {M} (x y : dec_agreeRA) : ✓ (x ⋅ y) ⊑ (x = y : uPred M).
-Proof. split=> r n _ ?. by apply: dec_agree_op_inv. Qed.
+Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
 
 End dec_agree.

algebra/dra.v

@@ -131,26 +131,20 @@ Proof.
       intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
 Qed.
 Definition validityRA : cmraT := discreteRA validity_ra.
+Instance validity_cmra_discrete :
+  CMRADiscrete validityRA := discrete_cmra_discrete _.
+
 Lemma validity_update (x y : validityRA) :
   (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
 Proof.
-  intros Hxy. apply discrete_update.
-  intros z (?&?&?); split_and!; try eapply Hxy; eauto.
+  intros Hxy; apply cmra_discrete_update=> z [?[??]].
+  split_and!; try eapply Hxy; eauto.
 Qed.
 
-Lemma to_validity_valid (x : A) :
-  ✓ to_validity x → ✓ x.
-Proof. intros. done. Qed.
-
 Lemma to_validity_op (x y : A) :
   (✓ (x ⋅ y) → ✓ x ∧ ✓ y ∧ x ⊥ y) →
   to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
-Proof.
-  intros Hvd. split; [split | done].
-  - simpl. auto.
-  - clear Hvd. simpl. intros (? & ? & ?).
-    auto using dra_op_valid, to_validity_valid.
-Qed.
+Proof. split; naive_solver auto using dra_op_valid. Qed.
 
 Lemma to_validity_included x y:
   (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
@@ -158,7 +152,7 @@ Proof.
   split.
   - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
     destruct Hvl' as [? [? ?]].
-    split; first by apply to_validity_valid.
+    split; first done.
     exists (validity_car z). split_and!; last done.
     + apply EQ. assumption.
     + by apply validity_valid_car_valid.
@@ -169,5 +163,4 @@ Proof.
     + intros _. setoid_subst. by apply dra_op_valid. 
     + intros _. rewrite /= EQ //.
 Qed.
-
 End dra.

algebra/excl.v

@@ -69,6 +69,10 @@ Proof.
        constructor; destruct (c 1); simplify_eq/=.
 Qed.
 Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
+Global Instance excl_discrete : Discrete A → Discrete exclC.
+Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
+Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
+Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
@@ -76,11 +80,6 @@ Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
 Proof. by inversion_clear 1; constructor. Qed.
 Global Instance ExclBot_timeless : Timeless (@ExclBot A).
 Proof. by inversion_clear 1; constructor. Qed.
-Global Instance excl_timeless :
-  (∀ x : A, Timeless x) → ∀ x : excl A, Timeless x.
-Proof. intros ? []; apply _. Qed.
-Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
-Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 (* CMRA *)
 Instance excl_valid : Valid (excl A) := λ x,
@@ -127,6 +126,9 @@ Qed.
 Canonical Structure exclRA : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin.
 Global Instance excl_cmra_identity : CMRAIdentity exclRA.
 Proof. split. done. by intros []. apply _. Qed.
+Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclRA.
+Proof. split. apply _. by intros []. Qed.
+
 Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅.
 Proof. by destruct y. Qed.
 Lemma excl_validN_inv_r n x y : ✓{n} (x ⋅ Excl y) → x = ∅.

algebra/fin_maps.v

@@ -29,7 +29,8 @@ Proof.
     by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
 Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
-
+Global Instance map_discrete : Discrete A → Discrete mapC.
+Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 (* why doesn't this go automatic? *)
 Global Instance mapC_leibniz: LeibnizEquiv A → LeibnizEquiv mapC.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
@@ -61,9 +62,6 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 
-Global Instance map_timeless `{∀ a : A, Timeless a} m : Timeless m.
-Proof. by intros m' ? i; apply: timeless. Qed.
-
 Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
@@ -168,8 +166,8 @@ Proof.
   - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   - apply map_empty_timeless.
 Qed.
-Global Instance mapRA_leibniz : LeibnizEquiv A → LeibnizEquiv mapRA.
-Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
+Global Instance map_cmra_discrete : CMRADiscrete A → CMRADiscrete mapRA.
+Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
 
 (** Internalized properties *)
 Lemma map_equivI {M} m1 m2 : (m1 ≡ m2)%I ≡ (∀ i, m1 !! i ≡ m2 !! i : uPred M)%I.

algebra/option.v

@@ -41,6 +41,9 @@ Proof.
     constructor.
 Qed.
 Canonical Structure optionC := CofeT option_cofe_mixin.
+Global Instance option_discrete : Discrete A → Discrete optionC.
+Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
+
 Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
 Proof. by constructor. Qed.
 Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
@@ -51,8 +54,6 @@ Global Instance None_timeless : Timeless (@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 option_timeless `{!∀ a : A, Timeless a} (mx : option A) : Timeless mx.
-Proof. destruct mx; auto with typeclass_instances. Qed.
 End cofe.
 
 Arguments optionC : clear implicits.
@@ -121,6 +122,8 @@ Qed.
 Canonical Structure optionRA := CMRAT option_cofe_mixin option_cmra_mixin.
 Global Instance option_cmra_identity : CMRAIdentity optionRA.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
+Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionRA.
+Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
 
 (** Misc *)
 Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.

algebra/sts.v

@@ -318,6 +318,9 @@ Implicit Types s : state sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
 
+Global Instance sts_cmra_discrete : CMRADiscrete (stsRA sts).
+Proof. apply validity_cmra_discrete. Qed.
+
 (** Setoids *)
 Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
 Proof. (* this proof is horrible *)

algebra/upred.v

@@ -896,7 +896,7 @@ Proof. split=> n x _; apply cmra_validN_op_l. Qed.
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
 Proof. by intros; rewrite ownM_valid valid_elim. Qed.
 Global Instance ownM_mono : Proper (flip (≼) ==> (⊑)) (@uPred_ownM M).
-Proof. intros x y [z ->]. rewrite ownM_op. eauto. Qed.
+Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 
 (* Products *)
 Lemma prod_equivI {A B : cofeT} (x y : A * B) :
@@ -912,11 +912,16 @@ Lemma later_equivI {A : cofeT} (x y : later A) :
 Proof. done. Qed.
 
 (* Discrete *)
-(* For equality, there already is timeless_eq *)
-Lemma discrete_validI {A : cofeT} `{∀ x : A, Timeless x}
-  `{Op A, Valid A, Unit A, Minus A} (ra : RA A) (x : discreteRA ra) :
-  (✓ x)%I ≡ (■ ✓ x : uPred M)%I.
-Proof. done. Qed.
+Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) :
+  (✓ a)%I ≡ (■ ✓ a : uPred M)%I.
+Proof. split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
+Lemma timeless_eq {A : cofeT} (a b : A) :
+  Timeless a → (a ≡ b)%I ≡ (■ (a ≡ b) : uPred M)%I.
+Proof.
+  intros ?. apply (anti_symm (⊑)).
+  - split=> n x ? ? /=. by apply (timeless_iff n a).
+  - eapply const_elim; first done. move=>->. apply eq_refl.
+Qed.
 
 (* Timeless *)
 Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
@@ -927,13 +932,17 @@ Proof.
   - move=> HP; split=> -[|n] x /=; auto; left.
     apply HP, uPred_weaken with n x; eauto using cmra_validN_le.
 Qed.
+
 Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof. by apply timelessP_spec=> -[|n] x. Qed.
+Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
+   TimelessP (✓ a : uPred M)%I.
+Proof. apply timelessP_spec=> n x /=. by rewrite -!cmra_discrete_valid_iff. Qed.
 Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
 Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
 Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
 Proof.
-  intros; rewrite /TimelessP later_or (timelessP P) (timelessP Q); eauto 10.
+  intros; rewrite /TimelessP later_or (timelessP _) (timelessP Q); eauto 10.
 Qed.
 Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
 Proof.
@@ -975,13 +984,6 @@ Proof.
   intros ?; apply timelessP_spec=> n x ??; apply cmra_included_includedN,
     cmra_timeless_included_l; eauto using cmra_validN_le.
 Qed.
-Lemma timeless_eq {A : cofeT} (a b : A) :
-  Timeless a → (a ≡ b)%I ≡ (■(a ≡ b) : uPred M)%I.
-Proof.
-  intros ?. apply (anti_symm (⊑)).
-  - split=> n x ? ? /=. by apply (timeless_iff n a).
-  - eapply const_elim; first done. move=>->. apply eq_refl.
-Qed.
 
 (* Always stable *)
 Local Notation AS := AlwaysStable.

heap_lang/heap.v

@@ -120,7 +120,7 @@ Section heap.
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.
     rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc left_id; apply const_elim_sep_l=> ?.
+    rewrite -assoc left_id discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_alloc_pst _ (of_heap h)) //.
     apply sep_mono_r; rewrite HP; apply later_mono.
     apply forall_mono=> l; apply wand_intro_l.
@@ -144,7 +144,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
       with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
+    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
     rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
@@ -162,7 +162,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
       with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
+    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite /heap_inv alter_singleton insert_insert.
     rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
@@ -182,7 +182,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
       with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
+    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
     rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
@@ -201,7 +201,7 @@ Section heap.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
       with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
+    rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) ?lookup_insert //.
     rewrite /heap_inv alter_singleton insert_insert.
     rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.

program_logic/auth.v

@@ -5,13 +5,12 @@ Import uPred.
 Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_inG :> inG Λ Σ (authRA A);
   auth_identity :> CMRAIdentity A;
-  (* TODO: Once we switched to RAs, this can be removed. *)
-  auth_timeless (a : A) :> Timeless a;
+  auth_timeless :> CMRADiscrete A;
 }.
 
 Definition authGF (A : cmraT) : iFunctor := constF (authRA A).
 Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
-  `{CMRAIdentity A, ∀ a : A, Timeless a} : authG Λ Σ A.
+  `{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
 Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
@@ -23,11 +22,11 @@ Definition auth_own := projT1 auth_own_aux.
 Definition auth_own_eq : @auth_own = @auth_own_def := projT2 auth_own_aux.
 Arguments auth_own {_ _ _ _ _} _ _.
 
-(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
-     is constantly valid. *)
-Definition auth_inv`{authG Λ Σ A} (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
-  (∃ a, (■ ✓ a ∧ own γ (● a)) ★ φ a)%I.
-Definition auth_ctx`{authG Λ Σ A} (γ : gname) (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+Definition auth_inv `{authG Λ Σ A}
+    (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
+  (∃ a, (✓ a ∧ own γ (● a)) ★ φ a)%I.
+Definition auth_ctx`{authG Λ Σ A}
+    (γ : gname) (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
   inv N (auth_inv γ φ).
 
 Instance: Params (@auth_inv) 6.
@@ -65,7 +64,7 @@ Section auth.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.
-      rewrite const_equiv // left_id. ecancel [▷ φ _]%I.
+      rewrite -valid_intro // left_id. ecancel [▷ φ _]%I.
       by rewrite -later_intro auth_own_eq -own_op auth_both_op. }
     rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
@@ -76,20 +75,19 @@ Section auth.
 
   Lemma auth_opened E γ a :
     (▷ auth_inv γ φ ★ auth_own γ a)
-    ⊑ (|={E}=> ∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
+    ⊑ (|={E}=> ∃ a', ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
     rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
     rewrite later_sep [(▷(_ ∧ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
-    rewrite always_and_sep_l -!assoc. apply const_elim_sep_l=>Hv.
+    rewrite always_and_sep_l -!assoc discrete_valid. apply const_elim_sep_l=>Hv.
     rewrite auth_own_eq [(▷φ _ ★ _)%I]comm assoc -own_op.
     rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
     apply exist_elim=>a'.
     rewrite left_id -(exist_intro a').
-    apply (eq_rewrite b (a ⋅ a') (λ x, ■ ✓ x ★ ▷ φ x ★ own γ (● x ⋅ ◯ a))%I).
-    { by move=>n ? ? /timeless_iff ->. }
+    apply (eq_rewrite b (a ⋅ a') (λ x, ✓ x ★ ▷ φ x ★ own γ (● x ⋅ ◯ a))%I).
+    { by move=>n x y /timeless_iff ->. }
     { by eauto with I. }
-    rewrite const_equiv // left_id comm.
-    apply sep_mono_r. by rewrite sep_elim_l.
+    rewrite -valid_intro // left_id comm. auto with I.
   Qed.
 
   Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
@@ -100,8 +98,8 @@ Section auth.
     intros HL Hv. rewrite /auth_inv auth_own_eq -(exist_intro (L a ⋅ a')).
     (* TODO it would be really nice to use cancel here *)
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
-    rewrite -pvs_frame_l. apply sep_mono; first done.
-    rewrite const_equiv // left_id -later_intro -own_op.
+    rewrite -pvs_frame_l. apply sep_mono_r.
+    rewrite -valid_intro // left_id -later_intro -own_op.
     by apply own_update, (auth_local_update_l L).
   Qed.
 
@@ -115,7 +113,7 @@ Section auth.
     nclose N ⊆ E →
     P ⊑ auth_ctx γ N φ →
     P ⊑ (▷ auth_own γ a ★ ∀ a',
-          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
             (auth_own γ (L a) -★ Ψ x))) →
@@ -147,7 +145,7 @@ Section auth.
     nclose N ⊆ E →
     P ⊑ auth_ctx γ N φ →
     P ⊑ (▷ auth_own γ a ★ (∀ a',
-          ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
+          ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
           fsa (E ∖ nclose N) (λ x,
             ■ (Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
             (auth_own γ (L a) -★ Ψ x)))) →

program_logic/sts.v

@@ -121,7 +121,7 @@ Section sts.
     rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
     rewrite -(exist_intro s).
     rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm.
-    rewrite own_valid_l discrete_validI.
+    rewrite own_valid_l discrete_valid.
     rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
     assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
     rewrite const_equiv // left_id comm sts_op_auth_frag //.
@@ -136,7 +136,7 @@ Section sts.