Generalize iNext to support multiple and iterated laters.

heap_lang/lib/barrier/proof.v

@@ -127,7 +127,7 @@ Proof.
   iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
   iMod ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
   iSplit; [iPureIntro; by eauto using signal_step|].
-  iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
+  rewrite {2}/barrier_inv /ress /=. iNext. iFrame "Hl".
   iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
   iNext. iIntros "_"; by iApply "Hr".
 Qed.
@@ -142,7 +142,7 @@ Proof.
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   wp_load. destruct p.
   - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
-    { iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
+    { iSplit; first done. rewrite {2}/barrier_inv /=. by iFrame. }
     iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     iModIntro. wp_if.
@@ -155,7 +155,7 @@ Proof.
     { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
     iMod ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
     { iSplit; [iPureIntro; by eauto using wait_step|].
-      iNext. rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame. auto. }
+      rewrite {2}/barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
     iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by auto.
     iModIntro. wp_if.
     iApply "HΦ". iApply "HQR". by iRewrite "Heq".
@@ -175,7 +175,7 @@ Proof.
   iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
   { iSplit; first by eauto using split_step.
-    iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
+    rewrite {2}/barrier_inv /=. iNext. iFrame "Hl".
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
     ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".

heap_lang/proofmode.v

@@ -15,7 +15,7 @@ Implicit Types Δ : envs (iResUR Σ).
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
     (Δ'' ⊢ Φ (LitV (LitLoc l)))) →
@@ -23,28 +23,28 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
 Proof.
   intros ???? HΔ. eapply wand_apply; first exact:wp_alloc. rewrite -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
 
 Lemma tac_wp_load Δ Δ' E i l q v Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ Φ v) →
   Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. eapply wand_apply; first exact:wp_load. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   to_val e = Some v' →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   (Δ'' ⊢ Φ (LitV LitUnit)) →
@@ -52,28 +52,28 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
 Proof.
   intros. eapply wand_apply; first by eapply wp_store. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   (Δ' ⊢ Φ (LitV (LitBool false))) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. eapply wand_apply; first exact:wp_cas_fail. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   (Δ'' ⊢ Φ (LitV (LitBool true))) →
@@ -81,7 +81,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
 Proof.
   intros; subst. eapply wand_apply; first exact:wp_cas_suc. rewrite -assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 End heap.

proofmode/class_instances.v

 From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
+From iris.prelude Require Import gmultiset.
 From iris.base_logic Require Import big_op.
 Import uPred.
 
@@ -58,47 +59,81 @@ Global Instance into_persistentP_persistent P :
 Proof. done. Qed.
 
 (* IntoLater *)
-Global Instance into_later_default P : IntoLater P P | 1000.
-Proof. apply later_intro. Qed.
-Global Instance into_later_later P : IntoLater (▷ P) P.
+Global Instance into_laterN_default n P : IntoLaterN n P P | 1000.
+Proof. apply laterN_intro. Qed.
+Global Instance into_laterN_later n P Q :
+  IntoLaterN n P Q → IntoLaterN (S n) (▷ P) Q.
+Proof. by rewrite /IntoLaterN=>->. Qed.
+Global Instance into_laterN_laterN n P : IntoLaterN n (▷^n P) P.
 Proof. done. Qed.
-Global Instance into_later_and P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance into_later_or P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance into_later_sep P1 P2 Q1 Q2 :
-  IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
-
-Global Instance into_later_big_sepM `{Countable K} {A}
+Global Instance into_laterN_laterN_plus n m P Q :
+  IntoLaterN m P Q → IntoLaterN (n + m) (▷^n P) Q.
+Proof. rewrite /IntoLaterN=>->. by rewrite laterN_plus. Qed.
+
+Global Instance into_laterN_and n P1 P2 Q1 Q2 :
+  IntoLaterN n P1 Q1 → IntoLaterN n P2 Q2 → IntoLaterN n (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite laterN_and; apply and_mono. Qed.
+Global Instance into_laterN_or n P1 P2 Q1 Q2 :
+  IntoLaterN n P1 Q1 → IntoLaterN n P2 Q2 → IntoLaterN n (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite laterN_or; apply or_mono. Qed.
+Global Instance into_laterN_sep n P1 P2 Q1 Q2 :
+  IntoLaterN n P1 Q1 → IntoLaterN n P2 Q2 → IntoLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
+Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
+
+Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat → A → uPred M) (l: list A) :
+  (∀ x k, IntoLaterN n (Φ k x) (Ψ k x)) →
+  IntoLaterN n ([∗ list] k ↦ x ∈ l, Φ k x) ([∗ list] k ↦ x ∈ l, Ψ k x).
+Proof.
+  rewrite /IntoLaterN=> ?. rewrite big_sepL_laterN. by apply big_sepL_mono.
+Qed.
+Global Instance into_laterN_big_sepM n `{Countable K} {A}
     (Φ Ψ : K → A → uPred M) (m : gmap K A) :
-  (∀ x k, IntoLater (Φ k x) (Ψ k x)) →
-  IntoLater ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
+  (∀ x k, IntoLaterN n (Φ k x) (Ψ k x)) →
+  IntoLaterN n ([∗ map] k ↦ x ∈ m, Φ k x) ([∗ map] k ↦ x ∈ m, Ψ k x).
 Proof.
-  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
+  rewrite /IntoLaterN=> ?. rewrite big_sepM_laterN; by apply big_sepM_mono.
 Qed.
-Global Instance into_later_big_sepS `{Countable A}
+Global Instance into_laterN_big_sepS n `{Countable A}
     (Φ Ψ : A → uPred M) (X : gset A) :
-  (∀ x, IntoLater (Φ x) (Ψ x)) →
-  IntoLater ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) →
+  IntoLaterN n ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ x).
+Proof.
+  rewrite /IntoLaterN=> ?. rewrite big_sepS_laterN; by apply big_sepS_mono.
+Qed.
+Global Instance into_laterN_big_sepMS n `{Countable A}
+    (Φ Ψ : A → uPred M) (X : gmultiset A) :
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) →
+  IntoLaterN n ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ x).
 Proof.
-  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
+  rewrite /IntoLaterN=> ?. rewrite big_sepMS_laterN; by apply big_sepMS_mono.
 Qed.
 
 (* FromLater *)
-Global Instance from_later_later P : FromLater (▷ P) P.
+Global Instance from_laterN_later P :FromLaterN 1 (▷ P) P | 0.
 Proof. done. Qed.
-Global Instance from_later_and P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance from_later_or P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance from_later_sep P1 P2 Q1 Q2 :
-  FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∗ P2) (Q1 ∗ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
+Global Instance from_laterN_laterN n P : FromLaterN n (▷^n P) P | 0.
+Proof. done. Qed.
+
+(* The instances below are used when stripping a specific number of laters, or
+to balance laters in different branches of ∧, ∨ and ∗. *)
+Global Instance from_laterN_0 P : FromLaterN 0 P P | 100. (* fallthrough *)
+Proof. done. Qed.
+Global Instance from_laterN_later_S n P Q :
+  FromLaterN n P Q → FromLaterN (S n) (▷ P) Q.
+Proof. by rewrite /FromLaterN=><-. Qed.
+Global Instance from_laterN_later_plus n m P Q :
+  FromLaterN m P Q → FromLaterN (n + m) (▷^n P) Q.
+Proof. rewrite /FromLaterN=><-. by rewrite laterN_plus. Qed.
+
+Global Instance from_later_and n P1 P2 Q1 Q2 :
+  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite laterN_and; apply and_mono. Qed.
+Global Instance from_later_or n P1 P2 Q1 Q2 :
+  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite laterN_or; apply or_mono. Qed.
+Global Instance from_later_sep n P1 P2 Q1 Q2 :
+  FromLaterN n P1 Q1 → FromLaterN n P2 Q2 → FromLaterN n (P1 ∗ P2) (Q1 ∗ Q2).
+Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand P Q Q' :
@@ -113,9 +148,12 @@ Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
 Proof. apply and_elim_r', impl_wand. Qed.
 Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
-Global Instance into_wand_later {M} (R P Q : uPred M) :
+Global Instance into_wand_later (R P Q : uPred M) :
   IntoWand R P Q → IntoWand R (▷ P) (▷ Q) | 100.
 Proof. rewrite /IntoWand=>->. by rewrite -later_wand -later_intro. Qed.
+Global Instance into_wand_laterN n (R P Q : uPred M) :
+  IntoWand R P Q → IntoWand R (▷^n P) (▷^n Q) | 100.
+Proof. rewrite /IntoWand=>->. by rewrite -laterN_wand -laterN_intro. Qed.
 Global Instance into_wand_bupd R P Q :
   IntoWand R P Q → IntoWand R (|==> P) (|==> Q) | 100.
 Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed.
@@ -137,6 +175,9 @@ Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
 Global Instance from_and_later P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
+Global Instance from_and_laterN n P Q1 Q2 :
+  FromAnd P Q1 Q2 → FromAnd (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite laterN_and. Qed.
 
 (* FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
@@ -153,23 +194,33 @@ Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
 Global Instance from_sep_later P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
+Global Instance from_sep_laterN n P Q1 Q2 :
+  FromSep P Q1 Q2 → FromSep (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /FromSep=> <-. by rewrite laterN_sep. Qed.
 Global Instance from_sep_bupd P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
 
+Global Instance from_sep_big_sepL {A} (Φ Ψ1 Ψ2 : nat → A → uPred M) l :
+  (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  FromSep ([∗ list] k ↦ x ∈ l, Φ k x)
+    ([∗ list] k ↦ x ∈ l, Ψ1 k x) ([∗ list] k ↦ x ∈ l, Ψ2 k x).
+Proof. rewrite /FromSep=>?. rewrite -big_sepL_sepL. by apply big_sepL_mono. Qed.
 Global Instance from_sep_big_sepM
     `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
   (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
   FromSep ([∗ map] k ↦ x ∈ m, Φ k x)
     ([∗ map] k ↦ x ∈ m, Ψ1 k x) ([∗ map] k ↦ x ∈ m, Ψ2 k x).
-Proof.
-  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
-Qed.
+Proof. rewrite /FromSep=>?. rewrite -big_sepM_sepM. by apply big_sepM_mono. Qed.
 Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
   (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
   FromSep ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ1 x) ([∗ set] x ∈ X, Ψ2 x).
+Proof. rewrite /FromSep=>?. rewrite -big_sepS_sepS. by apply big_sepS_mono. Qed.
+Global Instance from_sep_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
+  (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
+  FromSep ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ1 x) ([∗ mset] x ∈ X, Ψ2 x).
 Proof.
-  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+  rewrite /FromSep=> ?. rewrite -big_sepMS_sepMS. by apply big_sepMS_mono.
 Qed.
 
 (* FromOp *)
@@ -227,7 +278,19 @@ Qed.
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?later_and ?later_sep. Qed.
+Global Instance into_and_laterN n p P Q1 Q2 :
+  IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
+Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
 
+Global Instance into_and_big_sepL {A} (Φ Ψ1 Ψ2 : nat → A → uPred M) p l :
+  (∀ k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+  IntoAnd p ([∗ list] k ↦ x ∈ l, Φ k x)
+    ([∗ list] k ↦ x ∈ l, Ψ1 k x) ([∗ list] k ↦ x ∈ l, Ψ2 k x).
+Proof.
+  rewrite /IntoAnd=> HΦ. destruct p.
+  - rewrite -big_sepL_and. apply big_sepL_mono; auto.
+  - rewrite -big_sepL_sepL. apply big_sepL_mono; auto.
+Qed.
 Global Instance into_and_big_sepM
     `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
   (∀ k x, IntoAnd p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
@@ -235,9 +298,7 @@ Global Instance into_and_big_sepM
     ([∗ map] k ↦ x ∈ m, Ψ1 k x) ([∗ map] k ↦ x ∈ m, Ψ2 k x).
 Proof.
   rewrite /IntoAnd=> HΦ. destruct p.
-  - apply and_intro; apply big_sepM_mono; auto.
-    + intros k x ?. by rewrite HΦ and_elim_l.
-    + intros k x ?. by rewrite HΦ and_elim_r.
+  - rewrite -big_sepM_and. apply big_sepM_mono; auto.
   - rewrite -big_sepM_sepM. apply big_sepM_mono; auto.
 Qed.
 Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
@@ -245,11 +306,17 @@ Global Instance into_and_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p
   IntoAnd p ([∗ set] x ∈ X, Φ x) ([∗ set] x ∈ X, Ψ1 x) ([∗ set] x ∈ X, Ψ2 x).
 Proof.
   rewrite /IntoAnd=> HΦ. destruct p.
-  - apply and_intro; apply big_sepS_mono; auto.
-    + intros x ?. by rewrite HΦ and_elim_l.
-    + intros x ?. by rewrite HΦ and_elim_r.
+  - rewrite -big_sepS_and. apply big_sepS_mono; auto.
   - rewrite -big_sepS_sepS. apply big_sepS_mono; auto.
 Qed.
+Global Instance into_and_big_sepMS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
+  (∀ x, IntoAnd p (Φ x) (Ψ1 x) (Ψ2 x)) →
+  IntoAnd p ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ1 x) ([∗ mset] x ∈ X, Ψ2 x).
+Proof.
+  rewrite /IntoAnd=> HΦ. destruct p.
+  - rewrite -big_sepMS_and. apply big_sepMS_mono; auto.
+  - rewrite -big_sepMS_sepMS. apply big_sepMS_mono; auto.
+Qed.
 
 (* Frame *)
 Global Instance frame_here R : Frame R R True.
@@ -310,9 +377,21 @@ Global Instance make_later_default P : MakeLater P (▷ P) | 100.
 Proof. done. Qed.
 
 Global Instance frame_later R R' P Q Q' :
-  IntoLater R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
+  IntoLaterN 1 R' R → Frame R P Q → MakeLater Q Q' → Frame R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLater=>-> <- <-. by rewrite later_sep.
+  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite later_sep.
+Qed.
+
+Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ▷^n P ⊣⊢ lP.
+Global Instance make_laterN_true n : MakeLaterN n True True.
+Proof. by rewrite /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_laterN n R R' P Q Q' :
+  IntoLaterN n R' R → Frame R P Q → MakeLaterN n Q Q' → Frame R' (▷^n P) Q'.
+Proof.
+  rewrite /Frame /MakeLater /IntoLaterN=>-> <- <-. by rewrite laterN_sep.
 Qed.
 
 Class MakeExcept0 (P Q : uPred M) := make_except_0 : ◇ P ⊣⊢ Q.
@@ -352,6 +431,9 @@ Proof. rewrite /FromOr=> <-. by rewrite always_or. Qed.
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromOr=><-. by rewrite later_or. Qed.