Merge branch 'robbert/iNext_nat_cancel' into 'master'

Stronger `iNext` that performs arithmetic cancelation

Closes #148

See merge request FP/iris-coq!109

theories/heap_lang/proofmode.v

@@ -27,7 +27,7 @@ Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
   envs_entails Δ (WP e1 @ s; E {{ Φ }}).
 Proof.
@@ -141,7 +141,7 @@ Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
   IntoVal e v →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
     envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) →
@@ -168,7 +168,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
@@ -191,7 +191,7 @@ Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
   IntoVal e v' →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) →
@@ -216,7 +216,7 @@ Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
@@ -238,7 +238,7 @@ Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
@@ -263,7 +263,7 @@ Qed.
 
 Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
   IntoVal e2 (LitV (LitInt i2)) →
-  IntoLaterNEnvs 1 Δ Δ' →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ LitV (LitInt i1))%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ' = Some Δ'' →
   envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }}) →

theories/proofmode/class_instances.v

 From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
-From stdpp Require Import gmultiset.
+From stdpp Require Import gmultiset nat_cancel.
 From iris.base_logic Require Import big_op tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -167,93 +167,112 @@ Global Instance from_always_plainly P : FromAlways true (■ P) P.
 Proof. by rewrite /FromAlways. Qed.
 
 (* IntoLater *)
-Global Instance into_laterN_later n P Q :
-  IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q | 0.
-Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
-Global Instance into_laterN_later_further n P Q :
-  IntoLaterN' n P Q → IntoLaterN' n (▷ P) (▷ Q) | 1000.
-Proof. rewrite /IntoLaterN' /IntoLaterN =>->. by rewrite -laterN_later. Qed.
-
-Global Instance into_laterN_laterN n P : IntoLaterN' n (▷^n P) P | 0.
+Class MakeLaterN (n : nat) (P lP : uPred M) := make_laterN : ▷^n P ⊣⊢ lP.
+Global Instance make_laterN_true n : MakeLaterN n True True | 0.
+Proof. by rewrite /MakeLaterN laterN_True. Qed.
+Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
 Proof. done. Qed.
-Global Instance into_laterN_laterN_plus n m P Q :
-  IntoLaterN m P Q → IntoLaterN' (n + m) (▷^n P) Q | 1.
-Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
-Global Instance into_laterN_laterN_further n m P Q :
-  IntoLaterN' m P Q → IntoLaterN' m (▷^n P) (▷^n Q) | 1000.
-Proof.
-  rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
+Global Instance make_laterN_1 P : MakeLaterN 1 P (▷ P) | 2.
+Proof. done. Qed.
+Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
+Proof. done. Qed.
+
+Global Instance into_laterN_0 P : IntoLaterN 0 P P.
+Proof. done. Qed.
+Global Instance into_laterN_later n n' m' P Q lQ :
+  NatCancel n 1 n' m' →
+  (** If canceling has failed (i.e. [1 = m']), we should make progress deeper
+  into [P], as such, we continue with the [IntoLaterN] class, which is required
+  to make progress. If canceling has succeeded, we do not need to make further
+  progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
+  into [P], as such, we continue with [MaybeIntoLaterN]. *)
+  TCIf (TCEq 1 m') (IntoLaterN n' P Q) (MaybeIntoLaterN n' P Q) →
+  MakeLaterN m' Q lQ →
+  IntoLaterN n (▷ P) lQ | 2.
+Proof.
+  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
+  move=> Hn [_ ->|->] <-;
+    by rewrite -later_laterN -laterN_plus -Hn Nat.add_comm.
+Qed.
+Global Instance into_laterN_laterN n m n' m' P Q lQ :
+  NatCancel n m n' m' →
+  TCIf (TCEq m m') (IntoLaterN n' P Q) (MaybeIntoLaterN n' P Q) →
+  MakeLaterN m' Q lQ →
+  IntoLaterN n (▷^m P) lQ | 1.
+Proof.
+  rewrite /MakeLaterN /IntoLaterN /MaybeIntoLaterN /NatCancel.
+  move=> Hn [_ ->|->] <-; by rewrite -!laterN_plus -Hn Nat.add_comm.
 Qed.
 
 Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
-  IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
-  IntoLaterN' n (P1 ∧ P2) (Q1 ∧ Q2) | 10.
-Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
+  IntoLaterN n P1 Q1 → MaybeIntoLaterN n P2 Q2 →
+  IntoLaterN n (P1 ∧ P2) (Q1 ∧ Q2) | 10.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_and. Qed.
 Global Instance into_laterN_and_r n P P2 Q2 :
-  IntoLaterN' n P2 Q2 → IntoLaterN' n (P ∧ P2) (P ∧ Q2) | 11.
+  IntoLaterN n P2 Q2 → IntoLaterN n (P ∧ P2) (P ∧ Q2) | 11.
 Proof.
-  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
 Qed.
 
 Global Instance into_later_forall {A} n (Φ Ψ : A → uPred M) :
-  (∀ x, IntoLaterN' n (Φ x) (Ψ x)) → IntoLaterN' n (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /IntoLaterN' /IntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) → IntoLaterN n (∀ x, Φ x) (∀ x, Ψ x).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
 Global Instance into_later_exist {A} n (Φ Ψ : A → uPred M) :
-  (∀ x, IntoLaterN' n (Φ x) (Ψ x)) →
-  IntoLaterN' n (∃ x, Φ x) (∃ x, Ψ x).
-Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) →
+  IntoLaterN n (∃ x, Φ x) (∃ x, Ψ x).
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
 
 Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
-  IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
-  IntoLaterN' n (P1 ∨ P2) (Q1 ∨ Q2) | 10.
-Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_or. Qed.
+  IntoLaterN n P1 Q1 → MaybeIntoLaterN n P2 Q2 →
+  IntoLaterN n (P1 ∨ P2) (Q1 ∨ Q2) | 10.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_or. Qed.
 Global Instance into_laterN_or_r n P P2 Q2 :
-  IntoLaterN' n P2 Q2 →
-  IntoLaterN' n (P ∨ P2) (P ∨ Q2) | 11.
+  IntoLaterN n P2 Q2 →
+  IntoLaterN n (P ∨ P2) (P ∨ Q2) | 11.
 Proof.
-  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
 Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
-  IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
-  IntoLaterN' n (P1 ∗ P2) (Q1 ∗ Q2) | 10.
-Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
+  IntoLaterN n P1 Q1 → MaybeIntoLaterN n P2 Q2 →
+  IntoLaterN n (P1 ∗ P2) (Q1 ∗ Q2) | 10.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
 Global Instance into_laterN_sep_r n P P2 Q2 :
-  IntoLaterN' n P2 Q2 →
-  IntoLaterN' n (P ∗ P2) (P ∗ Q2) | 11.
+  IntoLaterN n P2 Q2 →
+  IntoLaterN n (P ∗ P2) (P ∗ Q2) | 11.
 Proof.
-  rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
 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).
+  (∀ 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' /IntoLaterN=> ?.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opL_commute. 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, IntoLaterN' n (Φ k x) (Ψ k x)) →
-  IntoLaterN' n ([∗ 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 /IntoLaterN' /IntoLaterN=> ?.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opM_commute; by apply big_sepM_mono.
 Qed.
 Global Instance into_laterN_big_sepS n `{Countable A}
     (Φ Ψ : A → uPred M) (X : gset A) :
-  (∀ x, IntoLaterN' n (Φ x) (Ψ x)) →
-  IntoLaterN' n ([∗ 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' /IntoLaterN=> ?.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opS_commute; 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).
+  (∀ x, IntoLaterN n (Φ x) (Ψ x)) →
+  IntoLaterN n ([∗ mset] x ∈ X, Φ x) ([∗ mset] x ∈ X, Ψ x).
 Proof.
-  rewrite /IntoLaterN' /IntoLaterN=> ?.
+  rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
   rewrite big_opMS_commute; by apply big_sepMS_mono.
 Qed.
 
@@ -631,31 +650,19 @@ Proof.
   by rewrite and_sep_l assoc (comm _ P1) -assoc -(and_sep_l P1) impl_elim_r.
 Qed.
 
-Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
-Global Instance make_later_true : MakeLater True True.
-Proof. by rewrite /MakeLater later_True. Qed.
-Global Instance make_later_default P : MakeLater P (▷ P) | 100.
-Proof. done. Qed.
-
 Global Instance frame_later p R R' P Q Q' :
-  NoBackTrack (IntoLaterN 1 R' R) →
-  Frame p R P Q → MakeLater Q Q' → Frame p R' (▷ P) Q'.
+  NoBackTrack (MaybeIntoLaterN 1 R' R) →
+  Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
+  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite persistently_if_later 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 p n R R' P Q Q' :
-  NoBackTrack (IntoLaterN n R' R) →
+  NoBackTrack (MaybeIntoLaterN n R' R) →
   Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
 Proof.
-  rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
+  rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite persistently_if_laterN laterN_sep.
 Qed.
 

theories/proofmode/classes.v

@@ -76,40 +76,42 @@ Class FromAlways {M} (p : bool) (P Q : uPred M) :=
 Arguments from_always {_} _ _ _ {_}.
 Hint Mode FromAlways + - ! - : typeclass_instances.
 
-(* The class [IntoLaterN] has only two instances:
+(* The class [MaybeIntoLaterN] has only two instances:
 
-- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
-- The instance [IntoLaterN' n P Q → IntoLaterN n P Q], where [IntoLaterN']
-  is identical to [IntoLaterN], but computationally is supposed to make
-  progress, i.e. its instances should actually strip a later.
+- The default instance [MaybeIntoLaterN n P P], i.e. [▷^n P -∗ P]
+- The instance [IntoLaterN n P Q → MaybeIntoLaterN n P Q], where [IntoLaterN]
+  is identical to [MaybeIntoLaterN], but is supposed to make progress, i.e. it
+  should actually strip a later.
 
-The point of using the auxilary class [IntoLaterN'] is to ensure that the
-default instance is not applied deeply in the term, which may result in too many
-definitions being unfolded (see issue #55).
+The point of using the auxilary class [IntoLaterN] is to ensure that the
+default instance is not applied deeply inside a term, which may result in too
+many definitions being unfolded (see issue #55).
 
 For binary connectives we have the following instances:
 
 <<
-IntoLaterN' n P P'       IntoLaterN n Q Q'
+IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
 ------------------------------------------
-     IntoLaterN' n (P /\ Q) (P' /\ Q')
+     IntoLaterN n (P /\ Q) (P' /\ Q')
 
 
-      IntoLaterN' n Q Q'
+      IntoLaterN n Q Q'
 -------------------------------
-IntoLaterN' n (P /\ Q) (P /\ Q')
+IntoLaterN n (P /\ Q) (P /\ Q')
 >>
 *)
-Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P ⊢ ▷^n Q.
-Arguments into_laterN {_} _ _ _ {_}.
-Hint Mode IntoLaterN + - - - : typeclass_instances.
+Class MaybeIntoLaterN {M} (n : nat) (P Q : uPred M) :=
+  maybe_into_laterN : P ⊢ ▷^n Q.
+Arguments maybe_into_laterN {_} _ _ _ {_}.
+Hint Mode MaybeIntoLaterN + - - - : typeclass_instances.
 
-Class IntoLaterN' {M} (n : nat) (P Q : uPred M) :=
-  into_laterN' :> IntoLaterN n P Q.
-Arguments into_laterN' {_} _ _ _ {_}.
-Hint Mode IntoLaterN' + - ! - : typeclass_instances.
+Class IntoLaterN {M} (n : nat) (P Q : uPred M) :=
+  into_laterN :> MaybeIntoLaterN n P Q.
+Arguments into_laterN {_} _ _ _ {_}.
+Hint Mode IntoLaterN + - ! - : typeclass_instances.
 
-Instance into_laterN_default {M} n (P : uPred M) : IntoLaterN n P P | 1000.
+Instance maybe_into_laterN_default {M} n (P : uPred M) :
+  MaybeIntoLaterN n P P | 1000.
 Proof. apply laterN_intro. Qed.
 
 Class FromLaterN {M} (n : nat) (P Q : uPred M) := from_laterN : ▷^n Q ⊢ P.
@@ -279,7 +281,7 @@ with the exception of:
 
 - [FromAssumption] used by [iAssumption]
 - [Frame] used by [iFrame]
-- [IntoLaterN] and [FromLaterN] used by [iNext]
+- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
 - [IntoPersistent] used by [iPersistent]
 *)
 Instance into_pure_tc_opaque {M} (P : uPred M) φ :

theories/proofmode/coq_tactics.v

@@ -472,27 +472,27 @@ Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → env
 Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Later *)
-Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
-  into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
-Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
-  into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
-  into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
+Class MaybeIntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
+  into_laterN_env : env_Forall2 (MaybeIntoLaterN n) Γ1 Γ2.
+Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
+  into_later_persistent: MaybeIntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
+  into_later_spatial: MaybeIntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
+Global Instance into_laterN_env_nil n : MaybeIntoLaterNEnv n Enil Enil.
 Proof. constructor. Qed.
 Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
-  IntoLaterNEnv n Γ1 Γ2 → IntoLaterN n P Q →
-  IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
+  MaybeIntoLaterNEnv n Γ1 Γ2 → MaybeIntoLaterN n P Q →
+  MaybeIntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
 Proof. by constructor. Qed.
 
 Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
-  IntoLaterNEnv n Γp1 Γp2 → IntoLaterNEnv n Γs1 Γs2 →
-  IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
+  MaybeIntoLaterNEnv n Γp1 Γp2 → MaybeIntoLaterNEnv n Γs1 Γs2 →
+  MaybeIntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
 Proof. by split. Qed.
 
 Lemma into_laterN_env_sound n Δ1 Δ2 :
-  IntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
+  MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
   repeat apply sep_mono; try apply persistently_mono.
@@ -503,7 +503,7 @@ Proof.
 Qed.
 
 Lemma tac_next Δ Δ' n Q Q' :
-  FromLaterN n Q Q' → IntoLaterNEnvs n Δ Δ' →
+  FromLaterN n Q Q' → MaybeIntoLaterNEnvs n Δ Δ' →
   envs_entails Δ' Q' → envs_entails Δ Q.
 Proof.
   rewrite /envs_entails=> ?? HQ.

theories/proofmode/tactics.v

@@ -860,7 +860,7 @@ Tactic Notation "iNext" open_constr(n) :=
   eapply (tac_next _ _ n);
     [apply _ || fail "iNext:" P "does not contain" n "laters"
     |lazymatch goal with
-     | |- IntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
+     | |- MaybeIntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
      | _ => apply _
      end
     |lazy beta (* remove beta redexes caused by removing laters under binders*)].

theories/tests/proofmode.v

@@ -291,12 +291,29 @@ Proof.
   iSpecialize ("Hφ" with "[% //] HP"). done.
 Qed.
 
-Lemma test_iNext_laterN_later P n : ▷ ▷^n P ⊢ ▷^n ▷ P.
+Lemma test_iNext_laterN_later P n : ▷ ▷^n P -∗ ▷^n ▷ P.
 Proof. iIntros "H". iNext. by iNext. Qed.
-Lemma test_iNext_later_laterN P n : ▷^n ▷ P ⊢ ▷ ▷^n P.
+Lemma test_iNext_later_laterN P n : ▷^n ▷ P -∗ ▷ ▷^n P.
 Proof. iIntros "H". iNext. by iNext. Qed.
-Lemma test_iNext_laterN_laterN P n1 n2 : ▷ ▷^n1 ▷^n2 P ⊢ ▷^n1 ▷^n2 ▷ P.
+Lemma test_iNext_plus_1 P n1 n2 : ▷ ▷^n1 ▷^n2 P -∗ ▷^n1 ▷^n2 ▷ P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
+Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
+Proof. iIntros "H". iNext. done. Qed.
+Lemma test_iNext_plus_3 P Q n m k :
+  ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
+Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
+
+Lemma test_iNext_unfold P Q n m (R := (▷^n P)%I) :
+  R ⊢ ▷^m True.
+Proof.
+  iIntros "HR". iNext.
+  match goal with |-  context [ R ] => idtac | |- _ => fail end.
+  done.
+Qed.
+
+Lemma test_iNext_fail P Q a b c d e f g h i j:
+  ▷^(a + b) ▷^(c + d + e) P -∗ ▷^(f + g + h + i + j) True.
+Proof. iIntros "H". iNext. done. Qed.
 
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
 Proof.