Use priority levels for `iFrame`. There's no syntax yet, so the fixes to the...

Use priority levels for `iFrame`. There's no syntax yet, so the fixes to the examples are temporarily.

iris/base_logic/lib/cancelable_invariants.v

 From iris.algebra Require Export frac.
 From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import proofmode.
+From iris.proofmode Require Import level proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
@@ -56,7 +56,8 @@ Section proofs.
   Lemma cinv_iff N γ P Q : cinv N γ P -∗ ▷ □ (P ↔ Q) -∗ cinv N γ Q.
   Proof.
     iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
-    iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
+    iSplit; at_level FrameLevel 2 (fun _ => (* frame ∨ *) iIntros "[?|$]");
+      iLeft; by iApply "HPQ".
   Qed.
 
   (*** Allocation rules. *)

iris/base_logic/lib/fancy_updates_from_vs.v

@@ -2,7 +2,7 @@
 view shift, and that the laws of the fancy update can be derived from the
 laws of the view shift. *)
 From stdpp Require Export coPset.
-From iris.proofmode Require Import proofmode.
+From iris.proofmode Require Import level proofmode.
 From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import options.
 
@@ -45,16 +45,18 @@ Proof. iIntros "HP". iExists P. iFrame "HP". iApply vs_impl; auto. Qed.
 Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
 Proof.
   iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
-  iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]").
+  iExists R; iFrame "HR".
+  at_level FrameLevel 2 (fun _ => (* frame ∧ *) iApply (vs_transitive with "[$Hvs]")).
   iApply vs_impl. iIntros "!> HP". by iApply HPQ.
 Qed.
 
 Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
 Proof.
   iDestruct 1 as (R) "[HR Hvs]". iExists R. iFrame "HR".
-  iApply (vs_transitive with "[$Hvs]"). clear R.
+  at_level FrameLevel 2 (fun _ => (* frame ∧ *) iApply (vs_transitive with "[$Hvs]")). clear R.
   iApply vs_exists; iIntros (R). iApply vs_persistent_intro_r; iIntros "Hvs".
-  iApply (vs_transitive with "[$Hvs]"). iApply vs_impl; auto.
+  at_level FrameLevel 2 (fun _ => (* frame ∧ *) iApply (vs_transitive with "[$Hvs]")).
+  iApply vs_impl; auto.
 Qed.
 
 Lemma fupd_mask_frame_r E1 E2 Ef P :

iris/base_logic/lib/na_invariants.v

 From iris.algebra Require Import gset coPset.
-From iris.proofmode Require Import proofmode.
+From iris.proofmode Require Import level proofmode.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
@@ -48,7 +48,8 @@ Section proofs.
     rewrite /na_inv. iIntros "(%i & % & HI) #HPQ".
     iExists i. iSplit; first done. iApply (inv_iff with "HI").
     iIntros "!> !>".
-    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
+    iSplit; at_level FrameLevel 2 (fun _ => (* frame ∨ *) iIntros "[[? Ho]|$]");
+      iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
 
   Lemma na_alloc : ⊢ |==> ∃ p, na_own p ⊤.

iris/bi/lib/fractional.v

 From iris.bi Require Export bi.
-From iris.proofmode Require Import classes class_instances.
+From iris.proofmode Require Import level classes class_instances.
 From iris.prelude Require Import options.
 
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
@@ -179,12 +179,13 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  Global Instance frame_fractional p R r Φ P q RES:
+  Global Instance frame_fractional p R r Φ P q RES :
+    AllowedLevel FrameLevel 3 →
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
     Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
   Proof.
-    rewrite /Frame=>-[HR _][->?]H.
+    rewrite /Frame=> _ -[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
     - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
     - rewrite fractional /Frame /MakeSep=><-<-=>_.

iris/proofmode/classes.v

 From stdpp Require Import namespaces.
 From iris.bi Require Export bi.
-From iris.proofmode Require Import base.
+From iris.proofmode Require Import base level.
 From iris.proofmode Require Export ident_name modalities.
 From iris.prelude Require Import options.
 Import bi.
@@ -297,6 +297,8 @@ Proof. done. Qed.
 Global Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
 Proof. done. Qed.
 
+Record FrameLevel := {}.
+
 Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
 Global Arguments Frame {_} _ _%I _%I _%I.
 Global Arguments frame {_} _ _%I _%I _%I {_}.

iris/proofmode/frame_instances.v

 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi telescopes.
-From iris.proofmode Require Import classes.
+From iris.proofmode Require Import classes level.
 From iris.prelude Require Import options.
 Import bi.
 
@@ -150,13 +150,14 @@ Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
 Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
+  AllowedLevel FrameLevel 2 →
   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 /MaybeFrame /Frame /MakeAnd => <- <- _ <-.
+  rewrite /MaybeFrame /Frame /MakeAnd=> _ <- <- _ <-.
   apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; done.
 Qed.
 
@@ -185,19 +186,21 @@ 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 :
+  AllowedLevel FrameLevel 2 →
   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.
+Proof. rewrite /Frame /MakeOr=> _ <- <- _ <-. by rewrite -sep_or_l. Qed.
 
 Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
+  AllowedLevel FrameLevel 2 →
   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.
+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) | 2.

iris_deprecated/base_logic/sts.v

@@ -3,7 +3,7 @@ to use than just directly using the RA, hence it is deprecated and will be
 removed entirely after some grace period. *)
 
 From iris.algebra Require Export sts.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import level tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
@@ -125,7 +125,8 @@ Section sts.
     iIntros "Hφ". rewrite /sts_ctx /sts_own.
     iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
     { apply sts_auth_valid; set_solver. }
-    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
+    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op.
+    at_level FrameLevel 2 (fun _ => (* frame ∧ *) iIntros "[Hγ $]").
     iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
     rewrite /sts_inv. iNext. iExists s. by iFrame.
   Qed.

iris_heap_lang/lib/ticket_lock.v

 From iris.algebra Require Import excl auth gset.
-From iris.proofmode Require Import proofmode.
+From iris.proofmode Require Import proofmode level.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
@@ -101,7 +101,7 @@ Section proof.
     wp_load. destruct (decide (x = o)) as [->|Hneq].
     - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
       + iModIntro. iSplitL "Hlo Hln Hainv Ht".
-        { iNext. iExists o, n. iFrame. }
+        { iNext. iExists o, n. at_level FrameLevel 2 (fun _ => (* frame ∨ *) iFrame). }
         wp_pures. case_bool_decide; [|done]. wp_if.
         iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
       + iDestruct (own_valid_2 with "Ht Haown")

tests/mosel_paper.v

@@ -6,7 +6,7 @@ Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
 Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
 ICFP 2018 *)
 From iris.bi Require Import monpred.
-From iris.proofmode Require Import tactics monpred.
+From iris.proofmode Require Import level tactics monpred.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -23,7 +23,7 @@ Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
 P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
 Proof.
   iIntros "[HP H]". Show.
-  iFrame "HP". Show.
+  at_level FrameLevel 2 (fun _ => (* frame ∨ *) iFrame "HP"). Show.
   iAssumption.
 Qed.
 

tests/proofmode.v

 From iris.bi Require Import laterable.
-From iris.proofmode Require Import tactics intro_patterns.
+From iris.proofmode Require Import level tactics intro_patterns level.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
@@ -42,7 +42,7 @@ Proof.
   (* To test destruct: can also be part of the intro-pattern *)
   iDestruct "foo" as "[_ meh]".
   repeat iSplit; [|by iLeft|iIntros "#[]"].
-  iFrame "H2".
+  at_level FrameLevel 2 (fun _ => (* frame ∨ *) iFrame "H2").
   (* split takes a list of hypotheses just for the LHS *)
   iSplitL "H3".
   - iFrame "H3". iRight. auto.
@@ -51,7 +51,7 @@ Qed.
 
 Lemma demo_3 P1 P2 P3 :
   P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
-Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
+Proof. at_level FrameLevel 2 (fun _ => (* frame ∨ *) iIntros "($ & $ & $)"). iNext. by iExists 0. Qed.
 
 Lemma test_pure_space_separated P1 :
   <affine> ⌜True⌝ ∗ P1 -∗ P1.
@@ -86,7 +86,7 @@ Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
 Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
 
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : ⊢ (P → Q → P ∧ Q).
-Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
+Proof. iIntros "H1 #H2". at_level FrameLevel 2 (fun _ => (* frame ∧ *) iFrame "∗#"). Qed.
 
 Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
   Q ∗ □ (Q -∗ P) -∗ P ∗ Q.
@@ -530,21 +530,21 @@ Qed.
 
 Lemma test_iFrame_pure `{!BiInternalEq PROP} {A : ofe} (φ : Prop) (y z : A) :
   φ → <affine> ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
-Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
+Proof. iIntros (Hv) "#Hxy". at_level FrameLevel 2 (fun _ => (* frame ∧ *) 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.
+Proof. intros ?. iIntros "#HP1 HQ2 HP2". at_level FrameLevel 2 (fun _ => (* frame ∨ *) 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.
+Proof. iIntros "HP HQ". at_level FrameLevel 2 (fun _ => (* frame ∧ *) 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.
+Proof. iIntros "HP HQ". at_level FrameLevel 2 (fun _ => (* frame ∧ *) iFrame "HP HQ"). Qed.
 
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
@@ -633,7 +633,7 @@ Proof. iIntros "H". iNext. by iRewrite "H". Qed.
 
 Lemma test_iFrame_persistent (P Q : PROP) :
   □ P -∗ Q -∗ <pers> (P ∗ P) ∗ (P ∗ Q ∨ Q).
-Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
+Proof. iIntros "#HP". at_level FrameLevel 2 (fun _ => (* frame ∨ *) iFrame "HP"). at_level FrameLevel 2 (fun _ => (* frame ∨ *) iIntros "$"). Qed.
 
 Lemma test_iSplit_persistently P Q : □ P -∗ <pers> (P ∗ P).
 Proof. iIntros "#?". by iSplit. Qed.

tests/proofmode_ascii.v

-From iris.proofmode Require Import tactics monpred.
+From iris.proofmode Require Import level tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 From iris.prelude Require Import options.
@@ -42,7 +42,7 @@ Section base_logic_tests.
 
   Lemma test_iFrame_pure (x y z : M) :
     ✓ x -> ⌜y ≡ z⌝ |-@{uPredI M} ✓ x /\ ✓ x /\ y ≡ z.
-  Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.
+  Proof. iIntros (Hv) "Hxy". at_level FrameLevel 2 (fun _ => (* frame ∧ *) by iFrame (Hv) "Hxy"). Qed.
 
   Lemma test_iAssert_modality P : (|==> False) -* |==> P.
   Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.

tests/proofmode_iris.v

 From iris.algebra Require Import frac.
-From iris.proofmode Require Import tactics monpred.
+From iris.proofmode Require Import level tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 From iris.prelude Require Import options.
@@ -37,7 +37,7 @@ Section base_logic_tests.
 
   Lemma test_iFrame_pure (x y z : M) :
     ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
-  Proof. iIntros (Hv) "Hxy". by iFrame (Hv) "Hxy". Qed.
+  Proof. iIntros (Hv) "Hxy". at_level FrameLevel 2 (fun _ => (* frame ∧ *) by iFrame (Hv) "Hxy"). Qed.
 
   Lemma test_iAssert_modality P : (|==> False) -∗ |==> P.
   Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.

tests/proofmode_monpred.v

-From iris.proofmode Require Import tactics monpred.
+From iris.proofmode Require Import level tactics monpred.
 From iris.base_logic.lib Require Import invariants.
 From iris.prelude Require Import options.
 
@@ -107,7 +107,7 @@ Section tests.
   Lemma test_monPred_at_and_pure P i j :
     (monPred_in j ∧ P) i ⊢ ⌜ j ⊑ i ⌝ ∧ P i.
   Proof.
-    iDestruct 1 as "[% $]". done.
+    at_level FrameLevel 2 (fun _ => (* frame ∧ *) iDestruct 1 as "[% $]"). done.
   Qed.
   Lemma test_monPred_at_sep_pure P i j :
     (monPred_in j ∗ <absorb> P) i ⊢ ⌜ j ⊑ i ⌝ ∧ <absorb> P i.