Type class of uPreds that are stable under □.

iris/hoare.v

@@ -33,15 +33,15 @@ Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.
 Lemma ht_val E v :
   {{ True }} of_val v @ E {{ λ v', ■ (v = v') }}.
 Proof.
-  rewrite -{1}always_const; apply always_intro, impl_intro_l.
+  apply (always_intro' _ _), impl_intro_l.
   by rewrite -wp_value -pvs_intro; apply const_intro.
 Qed.
 Lemma ht_vs E P P' Q Q' e :
   (P >{E}> P' ∧ {{ P' }} e @ E {{ Q' }} ∧ ∀ v, Q' v >{E}> Q v)
   ⊑ {{ P }} e @ E {{ Q }}.
 Proof.
-  rewrite -always_forall -!always_and; apply always_intro, impl_intro_l.
-  rewrite !always_and (associative _ P) (always_elim (P → _)) impl_elim_r.
+  apply (always_intro' _ _), impl_intro_l.
+  rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
   rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
   rewrite wp_pvs; apply wp_mono=> v.
   by rewrite (forall_elim _ v) pvs_impl_r !pvs_trans'.
@@ -51,8 +51,8 @@ Lemma ht_atomic E1 E2 P P' Q Q' e :
   (P >{E1,E2}> P' ∧ {{ P' }} e @ E2 {{ Q' }} ∧ ∀ v, Q' v >{E2,E1}> Q v)
   ⊑ {{ P }} e @ E1 {{ Q }}.
 Proof.
-  intros; rewrite -always_forall -!always_and; apply always_intro, impl_intro_l.
-  rewrite !always_and (associative _ P) (always_elim (P → _)) impl_elim_r.
+  intros ??; apply (always_intro' _ _), impl_intro_l.
+  rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
   rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
   rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
   rewrite (forall_elim _ v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
@@ -61,8 +61,8 @@ Lemma ht_bind `(HK : is_ctx K) E P Q Q' e :
   ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} K (of_val v) @ E {{ Q' }})
   ⊑ {{ P }} K e @ E {{ Q' }}.
 Proof.
-  intros; rewrite -always_forall -!always_and; apply always_intro, impl_intro_l.
-  rewrite !always_and (associative _ P) (always_elim (P → _)) impl_elim_r.
+  intros; apply (always_intro' _ _), impl_intro_l.
+  rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
   rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
   rewrite (forall_elim _ v) pvs_impl_r wp_pvs; apply wp_mono=> v'.
   by rewrite pvs_trans'.

iris/pviewshifts.v

@@ -120,10 +120,12 @@ Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
 Proof. apply pvs_trans; solve_elem_of. Qed.
 Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
 Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed.
-Lemma pvs_always_l E1 E2 P Q : (□ P ∧ pvs E1 E2 Q) ⊑ pvs E1 E2 (□ P ∧ Q).
-Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
-Lemma pvs_always_r E1 E2 P Q : (pvs E1 E2 P ∧ □ Q) ⊑ pvs E1 E2 (P ∧ □ Q).
-Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
+Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
+  (P ∧ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ∧ Q).
+Proof. by rewrite !always_and_sep_l' pvs_frame_l. Qed.
+Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
+  (pvs E1 E2 P ∧ Q) ⊑ pvs E1 E2 (P ∧ Q).
+Proof. by rewrite !always_and_sep_r' pvs_frame_r. Qed.
 Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q.
 Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
 Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q.

iris/weakestpre.v

@@ -177,10 +177,12 @@ Proof.
   rewrite (commutative _ (▷ R)%I); setoid_rewrite (commutative _ R).
   apply wp_frame_later_r.
 Qed.
-Lemma wp_always_l E e Q R : (□ R ∧ wp E e Q) ⊑ wp E e (λ v, □ R ∧ Q v).
-Proof. by setoid_rewrite always_and_sep_l; rewrite wp_frame_l. Qed.
-Lemma wp_always_r E e Q R : (wp E e Q ∧ □ R) ⊑ wp E e (λ v, Q v ∧ □ R).
-Proof. by setoid_rewrite always_and_sep_r; rewrite wp_frame_r. Qed.
+Lemma wp_always_l E e Q R `{!AlwaysStable R} :
+  (R ∧ wp E e Q) ⊑ wp E e (λ v, R ∧ Q v).
+Proof. by setoid_rewrite (always_and_sep_l' _ _); rewrite wp_frame_l. Qed.
+Lemma wp_always_r E e Q R `{!AlwaysStable R} :
+  (wp E e Q ∧ R) ⊑ wp E e (λ v, Q v ∧ R).
+Proof. by setoid_rewrite (always_and_sep_r' _ _); rewrite wp_frame_r. Qed.
 Lemma wp_impl_l E e Q1 Q2 : ((□ ∀ v, Q1 v → Q2 v) ∧ wp E e Q1) ⊑ wp E e Q2.
 Proof.
   rewrite wp_always_l; apply wp_mono=> v.

modures/logic.v

@@ -223,6 +223,8 @@ Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
 
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
 Arguments timelessP {_} _ {_} _ _ _ _.
+Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
+Arguments always_stable {_} _ {_} _ _ _ _.
 
 Module uPred. Section uPred_logic.
 Context {M : cmraT}.
@@ -685,8 +687,6 @@ Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
 Proof. done. Qed.
 
 (* Always derived *)
-Lemma always_always P : (□ □ P)%I ≡ (□ P)%I.
-Proof. apply (anti_symmetric (⊑)); auto using always_elim, always_intro. Qed.
 Lemma always_mono P Q : P ⊑ Q → □ P ⊑ □ Q.
 Proof. intros. apply always_intro. by rewrite always_elim. Qed.
 Hint Resolve always_mono.
@@ -709,7 +709,7 @@ Proof. apply (anti_symmetric (⊑)); auto using always_and_sep_1. Qed.
 Lemma always_and_sep_l P Q : (□ P ∧ Q)%I ≡ (□ P ★ Q)%I.
 Proof. apply (anti_symmetric (⊑)); auto using always_and_sep_l_1. Qed.
 Lemma always_and_sep_r P Q : (P ∧ □ Q)%I ≡ (P ★ □ Q)%I.
-Proof. rewrite !(commutative _ P); apply always_and_sep_l. Qed.
+Proof. by rewrite !(commutative _ P) always_and_sep_l. Qed.
 Lemma always_sep P Q : (□ (P ★ Q))%I ≡ (□ P ★ □ Q)%I.
 Proof. by rewrite -always_and_sep -always_and_sep_l always_and. Qed.
 Lemma always_wand P Q : □ (P -★ Q) ⊑ (□ P -★ □ Q).
@@ -755,6 +755,8 @@ Qed.
 Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
   (∀ n, ✓{n} a → ✓{n} b) → (✓ a) ⊑ (✓ b).
 Proof. by intros ? x n ?; simpl; auto. Qed.
+Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
+Proof. done. Qed.
 Lemma own_invalid (a : M) : ¬ ✓{1} a → uPred_own a ⊑ False.
 Proof. by intros; rewrite own_valid valid_elim. Qed.
 
@@ -850,4 +852,45 @@ Proof.
   intro; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
     cmra_timeless_included_l; eauto using cmra_valid_le.
 Qed.
+
+(* Always stable *)
+Notation AS := AlwaysStable.
+Global Instance const_always_stable φ : AS (■ φ : uPred M)%I.
+Proof. by rewrite /AlwaysStable always_const. Qed.
+Global Instance always_always_stable P : AS (□ P).
+Proof. by intros; apply always_intro. Qed.
+Global Instance and_always_stable P Q: AS P → AS Q → AS (P ∧ Q).
+Proof. by intros; rewrite /AlwaysStable always_and; apply and_mono. Qed.
+Global Instance or_always_stable P Q : AS P → AS Q → AS (P ∨ Q).
+Proof. by intros; rewrite /AlwaysStable always_or; apply or_mono. Qed.
+Global Instance sep_always_stable P Q: AS P → AS Q → AS (P ★ Q).
+Proof. by intros; rewrite /AlwaysStable always_sep; apply sep_mono. Qed.
+Global Instance forall_always_stable {A} (P : A → uPred M) :
+  (∀ x, AS (P x)) → AS (∀ x, P x).
+Proof. by intros; rewrite /AlwaysStable always_forall; apply forall_mono. Qed.
+Global Instance exist_always_stable {A} (P : A → uPred M) :
+  (∀ x, AS (P x)) → AS (∃ x, P x).
+Proof. by intros; rewrite /AlwaysStable always_exist; apply exist_mono. Qed.
+Global Instance eq_always_stable {A : cofeT} (a b : A) : AS (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /AlwaysStable always_eq. Qed.
+Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I.
+Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
+Global Instance later_always_stable P : AS P → AS (▷ P).
+Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
+Global Instance own_unit_always_stable (a : M) : AS (uPred_own (unit a)).
+Proof. by rewrite /AlwaysStable always_own_unit. Qed.
+Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) :
+  AS P → (∀ x, AS (Q x)) → AS (default P mx Q).
+Proof. destruct mx; apply _. Qed.
+
+Lemma always_always P `{!AlwaysStable P} : (□ P)%I ≡ P.
+Proof. apply (anti_symmetric (⊑)); auto using always_elim. Qed.
+Lemma always_intro' P Q `{!AlwaysStable P} : P ⊑ Q → P ⊑ □ Q.
+Proof. rewrite -(always_always P); apply always_intro. Qed.
+Lemma always_and_sep_l' P Q `{!AlwaysStable P} : (P ∧ Q)%I ≡ (P ★ Q)%I.
+Proof. by rewrite -(always_always P) always_and_sep_l. Qed.
+Lemma always_and_sep_r' P Q `{!AlwaysStable Q} : (P ∧ Q)%I ≡ (P ★ Q)%I.
+Proof. by rewrite -(always_always Q) always_and_sep_r. Qed.
+Lemma always_sep_dup' P `{!AlwaysStable P} : P ≡ (P ★ P)%I.
+Proof. by rewrite -(always_always P) -always_sep_dup. Qed.
 End uPred_logic. End uPred.