diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 95a4cdd9dd8eeefddda995b272de201918d77c16..802ca57a5926943f680a82a4d51e593f03946e20 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -31,6 +31,7 @@ variables:
- /^ci/
except:
- triggers
+ - schedules
## Build jobs
diff --git a/opam b/opam
index 49542ad819c7559bb7b0431f18c4b57c7edc59d4..8619a00e79de7230c78fe9c7e04e4329a44a835c 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.7.1" & < "8.8~" | (= "dev") }
- "coq-stdpp" { (= "dev.2018-02-03.0") | (= "dev") }
+ "coq-stdpp" { (= "dev.2018-02-19.1") | (= "dev") }
]
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index d5f27a26100d2bf1f86d99aa9d1f1711bd4131e6..08470051f88b13fb08f0e93aeed2129d353a0ad1 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -47,8 +47,8 @@ Section proofs.
Proof.
iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
- iNext. iAlways. iSplit; (iIntros "[[? Ho]|?]";
- [iLeft; iFrame "Ho"; by iApply "HPQ"|by iRight]).
+ iNext; iAlways.
+ iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index b75704bb0439af170769225ce8d32eb03941a948..c108b3f36103123f7a063778b7eaf0ca7a600cf5 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -92,7 +92,7 @@ Section proof.
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
- { iNext. iExists o, n. iFrame. eauto. }
+ { iNext. iExists o, n. iFrame. }
iModIntro. wp_let. wp_op. case_bool_decide; [|done].
wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 593f812d7e2263c7faf21bd2ead38e58c560151c..991a9e695319160388a6395ee83527743cfec2f9 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -26,7 +26,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.
@@ -140,7 +140,7 @@ Implicit Types Δ : envs (uPredI (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 {{ Φ }})) →
@@ -167,7 +167,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 {{ Φ }}).
@@ -190,7 +190,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 {{ Φ }}).
@@ -239,7 +239,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 {{ Φ }}) →
@@ -265,7 +265,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 {{ Φ }}) →
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d5bc2467b4b3ea5269b938a0c97a235eba0606d3..c365846e507f8e121479529b95e9327181002184 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -1,5 +1,6 @@
-From iris.proofmode Require Export classes.
+From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
+From iris.proofmode Require Export classes.
Set Default Proof Using "Type".
Import bi.
@@ -322,7 +323,6 @@ Global Instance into_wand_wand p q P Q P' :
Proof.
rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
Qed.
-
Global Instance into_wand_impl_false_false P Q P' :
Absorbing P' → Absorbing (P' → Q) →
FromAssumption false P P' → IntoWand false false (P' → Q) P Q.
@@ -330,7 +330,6 @@ Proof.
rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
by rewrite sep_and impl_elim_l.
Qed.
-
Global Instance into_wand_impl_false_true P Q P' :
Absorbing P' → FromAssumption true P P' →
IntoWand false true (P' → Q) P Q.
@@ -339,7 +338,6 @@ Proof.
rewrite -(affinely_persistently_idemp P) HP.
by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
Qed.
-
Global Instance into_wand_impl_true_false P Q P' :
Affine P' → FromAssumption false P P' →
IntoWand true false (P' → Q) P Q.
@@ -348,7 +346,6 @@ Proof.
rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
by rewrite affinely_persistently_elim impl_elim_l.
Qed.
-
Global Instance into_wand_impl_true_true P Q P' :
FromAssumption true P P' → IntoWand true true (P' → Q) P Q.
Proof.
@@ -883,8 +880,8 @@ Proof. intros. by rewrite /MakeSep comm. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
Proof. by rewrite /MakeSep. Qed.
-Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
- Frame true R P1 Q1 → MaybeFrame true R P2 Q2 → MakeSep Q1 Q2 Q' →
+Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
+ Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
Frame true R (P1 ∗ P2) Q' | 9.
Proof.
rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
@@ -926,28 +923,15 @@ Proof. intros. by rewrite /MakeAnd comm. Qed.
Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. by rewrite /MakeAnd. Qed.
-Global Instance frame_and_l p R P1 P2 Q1 Q2 Q :
- Frame p R P1 Q1 → MaybeFrame p R P2 Q2 →
- MakeAnd Q1 Q2 Q → Frame p R (P1 ∧ P2) Q | 9.
+Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
+ MaybeFrame p R P1 Q1 progress1 →
+ MaybeFrame p R P2 Q2 progress2 →
+ TCEq (progress1 || progress2) true →
+ MakeAnd Q1 Q2 Q' →
+ Frame p R (P1 ∧ P2) Q' | 9.
Proof.
- rewrite /Frame /MakeAnd => <- <- <- /=.
- auto using and_intro, and_elim_l, and_elim_r, sep_mono.
-Qed.
-Global Instance frame_and_persistent_r R P1 P2 Q2 Q :
- Frame true R P2 Q2 →
- MakeAnd P1 Q2 Q → Frame true R (P1 ∧ P2) Q | 10.
-Proof.
- rewrite /Frame /MakeAnd => <- <- /=. rewrite -!persistently_and_affinely_sep_l.
- auto using and_intro, and_elim_l', and_elim_r'.
-Qed.
-Global Instance frame_and_r R P1 P2 Q2 Q :
- TCOr (Affine R) (Absorbing P1) →
- Frame false R P2 Q2 →
- MakeAnd P1 Q2 Q → Frame false R (P1 ∧ P2) Q | 10.
-Proof.
- rewrite /Frame /MakeAnd=> ? <- <- /=. apply and_intro.
- - by rewrite and_elim_l sep_elim_r.
- - by rewrite and_elim_r.
+ rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-. apply and_intro;
+ [rewrite and_elim_l|rewrite and_elim_r]; done.
Qed.
Class MakeOr (P Q PQ : PROP) := make_or : P ∨ Q ⊣⊢ PQ.
@@ -963,21 +947,33 @@ Proof. intros. by rewrite /MakeOr or_emp. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
Proof. by rewrite /MakeOr. Qed.
-Global Instance frame_or_persistent_l R P1 P2 Q1 Q2 Q :
- Frame true R P1 Q1 → MaybeFrame true R P2 Q2 → MakeOr Q1 Q2 Q →
- Frame true R (P1 ∨ P2) Q | 9.
-Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
-Global Instance frame_or_persistent_r R P1 P2 Q1 Q2 Q :
- MaybeFrame true R P2 Q2 → MakeOr P1 Q2 Q →
- Frame true R (P1 ∨ P2) Q | 10.
-Proof.
- rewrite /Frame /MaybeFrame /MakeOr => <- <- /=.
- by rewrite sep_or_l sep_elim_r.
-Qed.
-Global Instance frame_or R P1 P2 Q1 Q2 Q :
- Frame false R P1 Q1 → Frame false R P2 Q2 → MakeOr Q1 Q2 Q →
- Frame false R (P1 ∨ P2) Q.
-Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+(* We could in principle write the instance [frame_or_spatial] by a bunch of
+instances, i.e. (omitting the parameter [p = false]):
+
+ Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
+ Frame R P1 True → Frame R (P1 ∨ P2) P2
+ Frame R P2 True → Frame R (P1 ∨ P2) P1
+
+The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
+multiple times, whereas the current solution makes sure that said inference
+appears at most once.
+
+If Coq would memorize the results of type class resolution, the solution with
+multiple instances would be preferred (and more Prolog-like). *)
+Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
+ MaybeFrame false R P1 Q1 progress1 → MaybeFrame false R P2 Q2 progress2 →
+ TCOr (TCEq (progress1 && progress2) true) (TCOr
+ (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
+ (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
+ MakeOr Q1 Q2 Q →
+ Frame false R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+
+Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
+ MaybeFrame true R P1 Q1 progress1 → MaybeFrame true R P2 Q2 progress2 →
+ TCEq (progress1 || progress2) true →
+ MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
Global Instance frame_wand p R P1 P2 Q2 :
Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
@@ -1041,6 +1037,23 @@ Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
(∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+Global Instance frame_impl_persistent R P1 P2 Q2 :
+ Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
+Proof.
+ rewrite /Frame /= => ?. apply impl_intro_l.
+ by rewrite -persistently_and_affinely_sep_l assoc (comm _ P1) -assoc impl_elim_r
+ persistently_and_affinely_sep_l.
+Qed.
+Global Instance frame_impl R P1 P2 Q2 :
+ Persistent P1 → Absorbing P1 →
+ Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
+Proof.
+ rewrite /Frame /==> ???. apply impl_intro_l.
+ rewrite {1}(persistent P1) persistently_and_affinely_sep_l assoc.
+ rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_affinely_sep_l.
+ rewrite persistently_elim impl_elim_r //.
+Qed.
+
(* FromModal *)
Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
Proof. apply absorbingly_intro. Qed.
@@ -1123,7 +1136,6 @@ Proof.
rewrite /IntoWand /= => HR.
by rewrite !later_affinely_persistently_if_2 -later_wand HR.
Qed.
-
Global Instance into_wand_later_args p q R P Q :
IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
Proof.
@@ -1131,14 +1143,12 @@ Proof.
by rewrite !later_affinely_persistently_if_2
(later_intro (â–¡?p R)%I) -later_wand HR.
Qed.
-
Global Instance into_wand_laterN n p q R P Q :
IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
Proof.
rewrite /IntoWand /= => HR.
by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
Qed.
-
Global Instance into_wand_laterN_args n p q R P Q :
IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
Proof.
@@ -1497,20 +1507,31 @@ Global Instance frame_eq_embed `{SbiEmbedding PROP PROP'} p P Q (Q' : PROP')
Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
Proof. rewrite /Frame /MakeEmbed -sbi_embed_internal_eq. apply (frame_embed p P Q). Qed.
-Class MakeLater (P lP : PROP) := make_later : ▷ P ⊣⊢ lP.
-Arguments MakeLater _%I _%I.
-
-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. by rewrite /MakeLater. Qed.
+Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ▷^n P ⊣⊢ lP.
+Arguments MakeLaterN _%nat _%I _%I.
+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. by rewrite /MakeLaterN. Qed.
+Global Instance make_laterN_1 P : MakeLaterN 1 P (â–· P) | 2.
+Proof. by rewrite /MakeLaterN. Qed.
+Global Instance make_laterN_default P : MakeLaterN n P (â–·^n P) | 100.
+Proof. by rewrite /MakeLaterN. Qed.
Global Instance frame_later p R R' P Q Q' :
- 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 later_affinely_persistently_if_2 later_sep.
Qed.
+Global Instance frame_laterN p n R R' P Q Q' :
+ NoBackTrack (MaybeIntoLaterN n R' R) →
+ Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
+Proof.
+ rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
+ by rewrite laterN_affinely_persistently_if_2 laterN_sep.
+Qed.
Global Instance frame_bupd `{BUpdFacts PROP} p R P Q :
Frame p R P Q → Frame p R (|==> P) (|==> Q).
@@ -1519,21 +1540,6 @@ Global Instance frame_fupd `{FUpdFacts PROP} p E1 E2 R P Q :
Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
-Class MakeLaterN (n : nat) (P lP : PROP) := make_laterN : ▷^n P ⊣⊢ lP.
-Arguments MakeLaterN _%nat _%I _%I.
-
-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. by rewrite /MakeLaterN. Qed.
-
-Global Instance frame_laterN p n R R' P Q Q' :
- IntoLaterN n R' R → Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
-Proof.
- rewrite /Frame /MakeLaterN /IntoLaterN=>-> <- <-.
- by rewrite laterN_affinely_persistently_if_2 laterN_sep.
-Qed.
-
Class MakeExcept0 (P Q : PROP) := make_except_0 : ◇ P ⊣⊢ Q.
Arguments MakeExcept0 _%I _%I.
@@ -1550,109 +1556,118 @@ Proof.
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.
-Proof. by rewrite /IntoLaterN' /IntoLaterN. 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 into_laterN_0 P : IntoLaterN 0 P P.
+Proof. by rewrite /IntoLaterN /MaybeIntoLaterN. 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_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_forall {A} n (Φ Ψ : A → PROP) :
- (∀ 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_laterN_exist {A} n (Φ Ψ : A → PROP) :
- (∀ 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_later_affinely n P Q :
- IntoLaterN n P Q → IntoLaterN n (bi_affinely P) (bi_affinely Q).
-Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
+ MaybeIntoLaterN n P Q → MaybeIntoLaterN n (bi_affinely P) (bi_affinely Q).
+Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
Global Instance into_later_absorbingly n P Q :
- IntoLaterN n P Q → IntoLaterN n (bi_absorbingly P) (bi_absorbingly Q).
-Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
+ MaybeIntoLaterN n P Q → MaybeIntoLaterN n (bi_absorbingly P) (bi_absorbingly Q).
+Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
Global Instance into_later_plainly n P Q :
- IntoLaterN n P Q → IntoLaterN n (bi_plainly P) (bi_plainly Q).
-Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_plainly. Qed.
+ MaybeIntoLaterN n P Q → MaybeIntoLaterN n (bi_plainly P) (bi_plainly Q).
+Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
Global Instance into_later_persistently n P Q :
- IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
-Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+ MaybeIntoLaterN n P Q → MaybeIntoLaterN n (bi_persistently P) (bi_persistently Q).
+Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
- IntoLaterN n P Q → IntoLaterN n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
+ MaybeIntoLaterN n P Q → MaybeIntoLaterN n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. 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 → PROP) (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 → PROP) (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 → PROP) (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 → PROP) (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.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 0a2261f32902478c64e2f0c84609d193288db57a..c8f8629023eccc606a8d65d1f7fe91f50986c48a 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -367,20 +367,24 @@ Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.
-Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
+(* The boolean [progress] indicates whether actual framing has been performed.
+If it is [false], then the default instance [maybe_frame_default] below has been
+used. *)
+Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : □?p R ∗ Q ⊢ P.
-Arguments MaybeFrame {_} _ _%I _%I _%I.
-Arguments maybe_frame {_} _%I _%I _%I {_}.
-Hint Mode MaybeFrame + + ! ! - : typeclass_instances.
+Arguments MaybeFrame {_} _ _%I _%I _%I _.
+Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
+Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
- Frame p R P Q → MaybeFrame p R P Q.
+ Frame p R P Q → MaybeFrame p R P Q true.
Proof. done. Qed.
+
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
- MaybeFrame true R P P | 100.
+ MaybeFrame true R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
- TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P | 100.
+ TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
Class IntoExcept0 {PROP : sbi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
@@ -389,42 +393,50 @@ Arguments into_except_0 {_} _%I _%I {_}.
Hint Mode IntoExcept0 + ! - : typeclass_instances.
Hint Mode IntoExcept0 + - ! : 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 {PROP : sbi} (n : nat) (P Q : PROP) := into_laterN : P ⊢ ▷^n Q.
+Class MaybeIntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
+ maybe_into_laterN : P ⊢ ▷^n Q.
+Arguments MaybeIntoLaterN {_} _%nat_scope _%I _%I.
+Arguments maybe_into_laterN {_} _%nat_scope _%I _%I {_}.
+Hint Mode MaybeIntoLaterN + - - - : typeclass_instances.
+
+Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
+ into_laterN :> MaybeIntoLaterN n P Q.
Arguments IntoLaterN {_} _%nat_scope _%I _%I.
-Arguments into_laterN {_} _%nat_scope _%I _%I {_}.
-Hint Mode IntoLaterN + - - - : typeclass_instances.
-
-Class IntoLaterN' {PROP : sbi} (n : nat) (P Q : PROP) :=
- into_laterN' :> IntoLaterN n P Q.
-Arguments IntoLaterN' {_} _%nat_scope _%I _%I.
-Hint Mode IntoLaterN' + - ! - : typeclass_instances.
+Hint Mode IntoLaterN + - ! - : typeclass_instances.
-Instance into_laterN_default {PROP : sbi} n (P : PROP) : IntoLaterN n P P | 1000.
+Instance maybe_into_laterN_default {PROP : sbi} n (P : PROP) :
+ MaybeIntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
+(* In the case both parameters are evars and n=0, we have to stop the
+ search and unify both evars immediately instead of looping using
+ other instances. *)
+Instance maybe_into_laterN_default_0 {PROP : sbi} (P : PROP) :
+ MaybeIntoLaterN 0 P P | 0.
+Proof. apply _. Qed.
Class FromLaterN {PROP : sbi} (n : nat) (P Q : PROP) := from_laterN : ▷^n Q ⊢ P.
Arguments FromLaterN {_} _%nat_scope _%I _%I.
@@ -457,7 +469,7 @@ with the exception of:
- [FromAssumption] used by [iAssumption]
- [Frame] and [MaybeFrame] used by [iFrame]
-- [IntoLaterN] and [FromLaterN] used by [iNext]
+- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iPersistent]
*)
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index a0f432a175b3fd5cc7e41c1a6d82cd2177dca775..43731e08d16072c7b4f3bc762d108b7dc1448918 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1195,27 +1195,27 @@ Proof.
Qed.
(** * Later *)
-Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
- into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
-Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
- 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 PROP) :=
+ into_laterN_env : env_Forall2 (MaybeIntoLaterN n) Γ1 Γ2.
+Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
+ 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_and !laterN_sep.
rewrite -{1}laterN_intro -laterN_affinely_persistently_2.
@@ -1228,7 +1228,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_eq => ?? HQ.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 790f15a0ff45b0104bc2cc1394f5fbeb4510b421..0b4165240dea1a17d050f8ae9d6a885a3b85a3fa 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -432,10 +432,10 @@ Global Instance into_except_0_monPred_at_bwd i P ð“Ÿ Q :
IntoExcept0 P Q → MakeMonPredAt i P 𓟠→ IntoExcept0 𓟠(Q i).
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
-Global Instance into_later_monPred_at i n P Q ð“ :
- IntoLaterN n P Q → MakeMonPredAt i Q ð“ → IntoLaterN n (P i) ð“ .
+Global Instance maybe_into_later_monPred_at i n P Q ð“ :
+ MaybeIntoLaterN n P Q → MakeMonPredAt i Q ð“ → MaybeIntoLaterN n (P i) ð“ .
Proof.
- rewrite /IntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
+ rewrite /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
by rewrite monPred_at_later.
Qed.
Global Instance from_later_monPred_at i n P Q ð“ :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e915b21a8d60d50e496a1a72f3efcd95d0fb34ff..b2824988eb0cb91d43563dacd68b7458c16f5dba 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -987,7 +987,7 @@ Tactic Notation "iNext" open_constr(n) :=
notypeclasses refine (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*)].
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 55f7f55abae02197b572095738fe11e1c0d05a47..e431212004f2b5f52e44fab49dc66753de9cdc5e 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -116,6 +116,20 @@ Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
φ → bi_affinely ⌜y ≡ z⌠-∗ (⌜ φ ⌠∧ ⌜ φ ⌠∧ y ≡ z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
+Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
+ BiAffine PROP →
+ □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2).
+Proof. intros ?. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
+Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
+Proof. iIntros "HP". iFrame "HP". auto. Qed.
+
+Lemma test_iFrame_conjunction_1 P Q :
+ P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+Lemma test_iFrame_conjunction_2 P Q :
+ P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+
Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
Proof.
iIntros "HF".
@@ -294,12 +308,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_specialize_affine_pure (φ : Prop) P :
φ → (bi_affinely ⌜φ⌠-∗ P) ⊢ P.