Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

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/hoare_lifting.v

+Require Export iris.hoare iris.lifting.
+
+Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
+  (default True%I ef (λ e, ht E P e Q))
+  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : uPred_scope.
+Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
+  (True ⊑ default True ef (λ e, ht E P e Q))
+  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.
+
+Section lifting.
+Context {Σ : iParam}.
+Implicit Types e : iexpr Σ.
+Import uPred.
+
+Lemma ht_lift_step E1 E2
+    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P P' Q1 Q2 R e1 σ1 :
+  E1 ⊆ E2 → to_val e1 = None →
+  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  (P >{E2,E1}> (ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef,
+    (■ φ e2 σ2 ef ★ ownP σ2 ★ P') >{E1,E2}> (Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧
+    {{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }} ∧
+    {{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }})
+  ⊑ {{ P }} e1 @ E2 {{ R }}.
+Proof.
+  intros ?? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l.
+  rewrite (associative _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
+  rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
+  rewrite always_and_sep_r' -associative; apply sep_mono; first done.
+  rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
+  rewrite (forall_elim _ e2) (forall_elim _ σ2) (forall_elim _ ef).
+  apply wand_intro_l; rewrite !always_and_sep_l'.
+  rewrite (associative _ _ P') -(associative _ _ _ P') associative.
+  rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
+  rewrite pvs_frame_r; apply pvs_mono.
+  rewrite (commutative _ (Q1 _ _ _)) -associative (associative _ (Q1 _ _ _)).
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
+  rewrite associative (commutative _ _ (wp _ _ _)) -associative.
+  apply sep_mono; first done.
+  destruct ef as [e'|]; simpl; [|by apply const_intro].
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
+  by apply const_intro.
+Qed.
+Lemma ht_lift_atomic E
+    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P e1 σ1 :
+  atomic e1 →
+  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ coPset_all {{ λ _, True }}) ⊑
+  {{ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
+Proof.
+  intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
+  rewrite -(ht_lift_step E E φ'  _ P
+    (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I
+    (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
+    try by (rewrite /φ'; eauto using atomic_not_value, atomic_step).
+  apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
+  rewrite (forall_elim _ e2) (forall_elim _ σ2) (forall_elim _ ef).
+  apply and_intro; [|apply and_intro; [|done]].
+  * rewrite -vs_impl; apply (always_intro' _ _),impl_intro_l;rewrite and_elim_l.
+    rewrite !associative; apply sep_mono; last done.
+    rewrite -!always_and_sep_l' -!always_and_sep_r'; apply const_elim_l=>-[??].
+    by repeat apply and_intro; try apply const_intro.
+  * apply (always_intro' _ _), impl_intro_l; rewrite and_elim_l.
+    rewrite -always_and_sep_r'; apply const_elim_r=>-[[v Hv] ?].
+    rewrite -(of_to_val e2 v) // -wp_value -pvs_intro.
+    rewrite -(exist_intro _ σ2) -(exist_intro _ ef) (of_to_val e2) //.
+    by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
+Qed.
+Lemma ht_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 :
+  to_val e1 = None →
+  (∀ σ1, ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
+  (∀ e2 ef,
+    {{ ■ φ e2 ef ★ P }} e2 @ E {{ Q }} ∧
+    {{ ■ φ e2 ef ★ P' }} ef ?@ coPset_all {{ λ _, True }})
+  ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
+Proof.
+  intros ? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l.
+  rewrite -(wp_lift_pure_step E φ _ e1) //.
+  rewrite (later_intro (∀ _, _)) -later_and; apply later_mono.
+  apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
+  rewrite (forall_elim _ e2) (forall_elim _ ef).
+  rewrite always_and_sep_l' !always_and_sep_r' {1}(always_sep_dup' (■ _)).
+  rewrite {1}(associative _ (_ ★ _)%I) -(associative _ (■ _)%I).
+  rewrite (associative _ (■ _)%I P) -{1}(commutative _ P) -(associative _ P).
+  rewrite (associative _ (■ _)%I) associative -(associative _ (■ _ ★ P))%I.
+  rewrite (commutative _ (■ _ ★ P'))%I associative.
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
+  rewrite -associative; apply sep_mono; first done.
+  destruct ef as [e'|]; simpl; [|by apply const_intro].
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
+  by apply const_intro.
+Qed.
+Lemma ht_lift_pure_determistic_step E
+    (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 e2 ef :
+  to_val e1 = None →
+  (∀ σ1, prim_step e1 σ1 e2 σ1 ef) →
+  (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
+  ({{ P }} e2 @ E {{ Q }} ∧ {{ P' }} ef ?@ coPset_all {{ λ _, True }})
+  ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
+Proof.
+  intros ? Hsafe Hdet.
+  rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
+  apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
+  * apply (always_intro' _ _), impl_intro_l.
+    rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
+    by rewrite /ht always_elim impl_elim_r.
+  * destruct ef' as [e'|]; simpl; [|by apply const_intro].
+    apply (always_intro' _ _), impl_intro_l.
+    rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
+    by rewrite /= /ht always_elim impl_elim_r.
+Qed.
+End lifting.

iris/lifting.v

+Require Export iris.weakestpre.
+Require Import iris.wsat.
+Local Hint Extern 10 (_ ≤ _) => omega.
+Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
+Local Hint Extern 10 (✓{_} _) =>
+  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
+  solve_validN.
+
+Section lifting.
+Context {Σ : iParam}.
+Implicit Types v : ival Σ.
+Implicit Types e : iexpr Σ.
+Implicit Types σ : istate Σ.
+Transparent uPred_holds.
+
+Lemma wp_lift_step E1 E2
+    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
+  E1 ⊆ E2 → to_val e1 = None →
+  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★
+    pvs E1 E2 (wp E2 e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True))))
+  ⊑ wp E2 e1 Q.
+Proof.
+  intros ? He Hsafe Hstep r n ? Hvs; constructor; auto.
+  intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
+    as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
+  destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
+  { by apply ownP_spec; auto. }
+  { by rewrite (associative _). }
+  constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
+  destruct (λ H1 H2 H3, Hwp e2 σ2 ef (update_pst σ2 r1) k H1 H2 H3 rf k Ef σ2)
+    as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
+  { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
+  { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. }
+  by exists r1', r2'; split_ands; [| |by intros ? ->].
+Qed.
+Lemma wp_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) Q e1 :
+  to_val e1 = None →
+  (∀ σ1, ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
+  (▷ ∀ e2 ef, ■ φ e2 ef →
+    wp E e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True)))
+  ⊑ wp E e1 Q.
+Proof.
+  intros He Hsafe Hstep r [|n] ?; [done|]; intros Hwp; constructor; auto.
+  intros rf k Ef σ1 ???; split; [done|].
+  intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
+  destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto; [by destruct k|].
+  exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
+Qed.
+End lifting.

iris/ownership.v

@@ -9,9 +9,12 @@ Instance: Params (@inv) 2.
 Instance: Params (@ownP) 1.
 Instance: Params (@ownG) 1.
 
+Typeclasses Opaque inv ownG ownP.
+
 Section ownership.
 Context {Σ : iParam}.
 Implicit Types r : res' Σ.
+Implicit Types σ : istate Σ.
 Implicit Types P : iProp Σ.
 Implicit Types m : icmra' Σ.
 
@@ -22,15 +25,14 @@ Proof.
   apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
   by unfold inv; rewrite HPQ.
 Qed.
-Lemma inv_duplicate i P : inv i P ≡ (inv i P ★ inv i P)%I.
-Proof.
-  by rewrite /inv -uPred.own_op Res_op
-    map_op_singleton agree_idempotent !(left_id _ _).
-Qed.
 Lemma always_inv i P : (□ inv i P)%I ≡ inv i P.
 Proof.
   by apply uPred.always_own; rewrite Res_unit !ra_unit_empty map_unit_singleton.
 Qed.
+Global Instance inv_always_stable i P : AlwaysStable (inv i P).
+Proof. by rewrite /AlwaysStable always_inv. Qed.
+Lemma inv_sep_dup i P : inv i P ≡ (inv i P ★ inv i P)%I.
+Proof. apply (uPred.always_sep_dup' _). Qed.
 
 (* physical state *)
 Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Σ) ⊑ False.
@@ -38,6 +40,8 @@ Proof.
   rewrite /ownP -uPred.own_op Res_op.
   by apply uPred.own_invalid; intros (_&?&_).
 Qed.
+Global Instance ownP_timeless σ : TimelessP (ownP σ).
+Proof. rewrite /ownP; apply _. Qed.
 
 (* ghost state *)
 Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Σ).
@@ -51,6 +55,8 @@ Proof.
 Qed.
 Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
 Proof. by rewrite /ownG uPred.own_valid; apply uPred.valid_mono=> n [? []]. Qed.
+Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
+Proof. rewrite /ownG; apply _. Qed.
 
 (* inversion lemmas *)
 Lemma inv_spec r n i P :
@@ -63,6 +69,11 @@ Proof.
       (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
   * intros ?; split_ands; try apply cmra_empty_least; eauto.
 Qed.
+Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ={n}= Excl σ.
+Proof.
+  intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
+  naive_solver (apply cmra_empty_least).
+Qed.
 Lemma ownG_spec r n m : (ownG m) n r ↔ m ≼{n} gst r.
 Proof.
   rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_least).

iris/parameter.v

@@ -10,6 +10,7 @@ Record iParam := IParam {
   icmra : cofeT → cmraT;
   icmra_empty A : Empty (icmra A);
   icmra_empty_spec A : RAIdentity (icmra A);
+  icmra_empty_timeless A : Timeless (∅ : icmra A);
   icmra_map {A B} (f : A -n> B) : icmra A -n> icmra B;
   icmra_map_ne {A B} n : Proper (dist n ==> dist n) (@icmra_map A B);
   icmra_map_id {A : cofeT} (x : icmra A) : icmra_map cid x ≡ x;
@@ -19,7 +20,8 @@ Record iParam := IParam {
 }.
 Arguments IParam {_ _ _} _ _ {_ _} _ {_ _ _ _}.
 Existing Instances ilanguage.
-Existing Instances icmra_empty icmra_empty_spec icmra_map_ne icmra_map_mono.
+Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
+Existing Instances icmra_map_ne icmra_map_mono.
 
 Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
   (∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.

iris/pviewshifts.v

@@ -30,6 +30,7 @@ Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
 Implicit Types m : icmra' Σ.
+Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
 Proof.
@@ -120,10 +121,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/resources.v

@@ -161,6 +161,8 @@ Lemma lookup_wld_op_r n r1 r2 i P :
 Proof.
   rewrite (commutative _ r1) (commutative _ (wld r1)); apply lookup_wld_op_l.
 Qed.
+Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
+Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
 End res.
 Arguments resRA : clear implicits.
 

iris/weakestpre.v

@@ -58,6 +58,7 @@ Implicit Types P : iProp Σ.
 Implicit Types Q : ival Σ → iProp Σ.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
+Transparent uPred_holds.
 
 Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
   E1 ⊆ E2 → (∀ v r n', n' ≤ n → ✓{n'} r → Q1 v n' r → Q2 v n' r) →
@@ -177,10 +178,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.

iris/wsat.v

 Require Export iris.model prelude.co_pset.
+Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
 Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
 Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
@@ -21,6 +22,7 @@ Arguments wsat_pre_wld {_ _ _ _ _ _} _ _ _ _ _.
 Definition wsat {Σ} (n : nat) (E : coPset) (σ : istate Σ) (r : res' Σ) : Prop :=
   match n with 0 => True | S n => ∃ rs, wsat_pre n E σ rs (r ⋅ big_opM rs) end.
 Instance: Params (@wsat) 4.
+Arguments wsat : simpl never.
 
 Section wsat.
 Context {Σ : iParam}.
@@ -38,7 +40,25 @@ Global Instance wsat_ne n : Proper (dist n ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
 Global Instance wsat_proper n : Proper ((≡) ==> iff) (wsat (Σ:=Σ) n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
-Lemma wsat_valid n E σ (r : res' Σ) : wsat n E σ r → ✓{n} r.
+Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
+Proof.
+  destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
+  intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto.
+  intros i P ? HiP; destruct (wld (r ⋅ big_opM rs) !! i) as [P'|] eqn:HP';
+    [apply (injective Some) in HiP|inversion_clear HiP].
+  assert (P' ={S n}= to_agree $ Later $ iProp_unfold $
+                       iProp_fold $ later_car $ P' (S n)) as HPiso.
+  { rewrite iProp_unfold_fold later_eta to_agree_car //.
+    apply (map_lookup_validN _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. }
+  assert (P ={n'}= iProp_fold (later_car (P' (S n)))) as HPP'.
+  { apply (injective iProp_unfold), (injective Later), (injective to_agree).
+    by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
+  destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto.
+  { by rewrite HP' -HPiso. }
+  assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
+  exists r'; split; [done|apply HPP', uPred_weaken with r' n; auto].
+Qed.
+Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r.
 Proof.
   destruct n; [intros; apply cmra_valid_0|intros [rs ?]].
   eapply cmra_valid_op_l, wsat_pre_valid; eauto.
@@ -78,13 +98,19 @@ Proof.
     + intros. destruct (Hwld j P') as (r'&?&?); auto.
       exists r'; rewrite lookup_insert_ne; naive_solver.
 Qed.
-Lemma wsat_update_pst n E σ1 σ2 r :
-  pst r ={S n}= Excl σ1 → wsat (S n) E σ1 r → wsat (S n) E σ2 (update_pst σ2 r).
+Lemma wsat_update_pst n E σ1 σ1' r rf :
+  pst r ={S n}= Excl σ1 → wsat (S n) E σ1' (r ⋅ rf) →
+  σ1' = σ1 ∧ ∀ σ2, wsat (S n) E σ2 (update_pst σ2 r ⋅ rf).
 Proof.
-  intros Hr [rs [(?&Hpst&?) Hσ HE Hwld]]; simpl in *.
-  assert (pst (big_opM rs) = ∅) as Hpst_rs.
-  { by apply: (excl_validN_inv_l n σ1); rewrite -Hr. }
-  by exists rs; constructor; split_ands'; rewrite /= ?Hpst_rs.
+  intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
+  assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
+  { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r (associative _). }
+  assert (σ1' = σ1) as ->.
+  { apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
+    apply (injective Excl).
+    by rewrite -Hpst_r -Hpst -(associative _) Hpst' (right_id _). }
+  split; [done|exists rs].
+  by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
 Qed.
 Lemma wsat_update_gst n E σ r rf m1 (P : icmra' Σ → Prop) :
   m1 ≼{S n} gst r → m1 ⇝: P →

modures/agree.v

@@ -133,6 +133,8 @@ Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
 Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
+Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ={n}= x.
+Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
 End agree.
 
 Arguments agreeC : clear implicits.

modures/auth.v

@@ -3,6 +3,7 @@ Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
+Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
 Arguments own {_} _.
@@ -151,6 +152,12 @@ Arguments authRA : clear implicits.
 (* Functor *)
 Instance auth_fmap : FMap auth := λ A B f x,
   Auth (f <$> authoritative x) (f (own x)).
+Arguments auth_fmap _ _ _ !_ /.
+Lemma auth_fmap_id {A} (x : auth A) : id <$> x = x.
+Proof. by destruct x; rewrite /= excl_fmap_id. Qed.
+Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
+  g ∘ f <$> x = g <$> f <$> x.
+Proof. by destruct x; rewrite /= excl_fmap_compose. Qed.
 Instance auth_fmap_cmra_ne {A B : cmraT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
 Proof.

modures/cmra.v

@@ -220,6 +220,17 @@ Qed.
 Lemma cmra_empty_least `{Empty A, !RAIdentity A} n x : ∅ ≼{n} x.
 Proof. by exists x; rewrite (left_id _ _). Qed.
 
+(** ** big ops *)
+Section bigop.
+  Context `{Empty A, !RAIdentity A, FinMap K M}.
+  Lemma big_opM_lookup_valid n m i x :
+    ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
+  Proof.
+    intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
+    apply cmra_valid_op_l.
+  Qed.
+End bigop.
+
 (** ** Properties of [(⇝)] relation *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.

modures/cofe.v

@@ -311,6 +311,8 @@ Inductive later (A : Type) : Type := Later { later_car : A }.
 Add Printing Constructor later.
 Arguments Later {_} _.
 Arguments later_car {_} _.
+Lemma later_eta {A} (x : later A) : Later (later_car x) = x.
+Proof. by destruct x. Qed.
 
 Section later.
   Context {A : cofeT}.

modures/excl.v

@@ -66,6 +66,10 @@ Proof.
 Qed.
 Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
 
+Global Instance Excl_inj : Injective (≡) (≡) (@Excl A).
+Proof. by inversion_clear 1. Qed.
+Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A).
+Proof. by inversion_clear 1. Qed.
 Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
 Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
 Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
@@ -133,6 +137,11 @@ Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
 Proof. by destruct y. Qed.
 Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
 Proof. by destruct x. Qed.
+Lemma Excl_includedN n x y : ✓{n} y → Excl x ≼{n} y ↔ y ={n}= Excl x.
+Proof.
+  intros Hvalid; split; [destruct n as [|n]; [done|]|by intros ->].
+  by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
+Qed.
 
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.
@@ -147,6 +156,11 @@ Instance excl_fmap : FMap excl := λ A B f x,
   match x with
   | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
   end.
+Lemma excl_fmap_id {A} (x : excl A) : id <$> x = x.
+Proof. by destruct x. Qed.
+Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
+  g ∘ f <$> x = g <$> f <$> x.
+Proof. by destruct x. Qed.
 Instance excl_fmap_cmra_ne {A B : cofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap excl _ A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.

modures/logic.v

@@ -11,6 +11,8 @@ Record uPred (M : cmraT) : Type := IProp {
     uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
+Global Opaque uPred_holds.
+Local Transparent uPred_holds.
 Hint Resolve uPred_0.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
@@ -82,8 +84,8 @@ Hint Extern 0 (uPred_entails ?P ?P) => reflexivity.
 Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
 
 (** logical connectives *)
-Program Definition uPred_const {M} (P : Prop) : uPred M :=
-  {| uPred_holds n x := match n return _ with 0 => True | _ => P end |}.
+Program Definition uPred_const {M} (φ : Prop) : uPred M :=
+  {| uPred_holds n x := match n return _ with 0 => True | _ => φ end |}.
 Solve Obligations with done.
 Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
 Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
@@ -134,9 +136,9 @@ Next Obligation.
   assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
   { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using @ra_included_l.
     apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
-  exists x1, x2'; split_ands; [done| |].
-  * cofe_subst y; apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
-  * cofe_subst y; apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
+  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
+  * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
+  * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
 Qed.
 
 Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
@@ -188,7 +190,7 @@ Arguments uPred_holds {_} _%I _ _.
 Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ P" := (uPred_const P) (at level 20) : uPred_scope.
+Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.
@@ -223,9 +225,12 @@ 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}.
+Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
@@ -251,7 +256,7 @@ Qed.
 
 (** Non-expansiveness and setoid morphisms *)
 Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
-Proof. by intros P Q HPQ ? [|n] ?; try apply HPQ. Qed.
+Proof. by intros φ1 φ2 Hφ ? [|n] ?; try apply Hφ. Qed.
 Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
 Proof.
   intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
@@ -337,9 +342,9 @@ Global Instance iff_proper :
   Proper ((≡) ==> (≡) ==> (≡)) (@uPred_iff M) := ne_proper_2 _.
 
 (** Introduction and elimination rules *)
-Lemma const_intro P (Q : Prop) : Q → P ⊑ ■ Q.
+Lemma const_intro φ P : φ → P ⊑ ■ φ.
 Proof. by intros ?? [|?]. Qed.
-Lemma const_elim (P : Prop) Q R : Q ⊑ ■ P → (P → Q ⊑ R) → Q ⊑ R.
+Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
 Proof.
   intros HQP HQR x [|n] ??; first done.
   apply HQR; first eapply (HQP _ (S n)); eauto.
@@ -418,10 +423,10 @@ Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : Q ⊑ (P → R) → (P ∧ Q) ⊑ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
 
-Lemma const_elim_l (P : Prop) Q R : (P → Q ⊑ R) → (■ P ∧ Q) ⊑ R.
-Proof. intros; apply const_elim with P; eauto. Qed.
-Lemma const_elim_r (P : Prop) Q R : (P → Q ⊑ R) → (Q ∧ ■ P) ⊑ R.
-Proof. intros; apply const_elim with P; eauto. Qed.
+Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
+Proof. intros; apply const_elim with φ; eauto. Qed.
+Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.
+Proof. intros; apply const_elim with φ; eauto. Qed.
 Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
 Proof. intros ->; apply eq_refl. Qed.
 Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
@@ -430,8 +435,8 @@ Proof.
   intros n; solve_proper.
 Qed.
 
-Lemma const_mono (P Q: Prop) : (P → Q) → ■ P ⊑ ■ Q.
-Proof. intros; apply const_elim with P; eauto using const_intro. Qed.
+Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊑ ■ φ2.
+Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
 Lemma and_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∧ P') ⊑ (Q ∧ Q').
 Proof. auto. Qed.
 Lemma or_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∨ P') ⊑ (Q ∨ Q').
@@ -450,7 +455,7 @@ Lemma exist_mono {A} (P Q : A → uPred M) :
   (∀ a, P a ⊑ Q a) → (∃ a, P a) ⊑ (∃ a, Q a).
 Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
 Global Instance const_mono' : Proper (impl ==> (⊑)) (@uPred_const M).
-Proof. intros P Q; apply const_mono. Qed.
+Proof. intros φ1 φ2; apply const_mono. Qed.
 Global Instance and_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_and M).
 Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
 Global Instance or_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_or M).
@@ -535,7 +540,7 @@ Proof.
     + by rewrite (associative op) -Hy -Hx.
     + by exists y2, x2.
 Qed.
-Lemma wand_intro P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
+Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
 Proof.
   intros HPQR x n ?? x' n' ???; apply HPQR; auto.
   exists x, x'; split_ands; auto.
@@ -553,7 +558,7 @@ Hint Resolve sep_mono.
 Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
 Lemma wand_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P -★ P') ⊑ (Q -★ Q').
-Proof. intros HP HQ; apply wand_intro; rewrite HP -HQ; apply wand_elim_l. Qed.
+Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
 Global Instance wand_mono' : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_wand M).
 Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
 
@@ -568,6 +573,8 @@ Proof. intros ->; apply sep_elim_l. Qed.
 Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
+Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
+Proof. rewrite (commutative _); apply wand_intro_r. Qed.
 Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.
 Proof. rewrite (commutative _ P); apply wand_elim_l. Qed.
 Lemma wand_elim_l' P Q R : P ⊑ (Q -★ R) → (P ★ Q) ⊑ R.
@@ -577,7 +584,7 @@ Proof. intros ->; apply wand_elim_r. Qed.
 Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
-Proof. apply wand_intro, impl_elim with P; auto. Qed.
+Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
 
 Global Instance sep_False : LeftAbsorb (≡) False%I (@uPred_sep M).
 Proof. intros P; apply (anti_symmetric _); auto. Qed.
@@ -648,10 +655,10 @@ Proof.
   apply later_mono, impl_elim with P; auto.
 Qed.
 Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q).
-Proof. apply wand_intro; rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
+Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
 
 (* Always *)
-Lemma always_const (P : Prop) : (□ ■ P : uPred M)%I ≡ (■ P)%I.
+Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
 Proof. done. Qed.
 Lemma always_elim P : □ P ⊑ P.
 Proof.
@@ -684,8 +691,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.
@@ -708,11 +713,11 @@ 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).
-Proof. by apply wand_intro; rewrite -always_sep wand_elim_l. Qed.
+Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
 Lemma always_sep_dup P : (□ P)%I ≡ (□ P ★ □ P)%I.
 Proof. by rewrite -always_sep -always_and_sep (idempotent _). Qed.
 Lemma always_wand_impl P Q : (□ (P -★ Q))%I ≡ (□ (P → Q))%I.
@@ -754,6 +759,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.
 
@@ -802,7 +809,7 @@ Proof.
   * move=> HP x [|[|n]] /=; auto; left.
     apply HP, uPred_weaken with x (S n); eauto using cmra_valid_le.
 Qed.
-Global Instance const_timeless (P : Prop) : TimelessP (■ P : uPred M)%I.
+Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof. by apply timelessP_spec=> x [|n]. 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.
@@ -818,8 +825,9 @@ Qed.
 Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
 Proof.
   intros; rewrite /TimelessP later_sep (timelessP P) (timelessP Q).
-  apply wand_elim_l',or_elim;apply wand_intro; auto.
-  apply wand_elim_r',or_elim;apply wand_intro; rewrite ?(commutative _ Q); auto.
+  apply wand_elim_l', or_elim; apply wand_intro_r; auto.
+  apply wand_elim_r', or_elim; apply wand_intro_r; auto.
+  rewrite ?(commutative _ Q); auto.
 Qed.
 Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
 Proof.
@@ -849,4 +857,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.

prelude/tactics.v

@@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x :=
         try match H' with H => fail 2 end;
         setoid_rewrite H in H'
      end;
-     clear H
+     clear x H
   end.
 Ltac setoid_subst :=
   repeat match goal with