Merge branch 'ascii-notation' into 'master'

ASCII notation

Closes #270

See merge request iris/iris!396

CHANGELOG.md

@@ -11,7 +11,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   splitting and other forms of weakening.
 * Updated the strong variant of the opening lemma for cancellable invariants
   to match that of regular invariants, where you can pick the mask at a later time.
-  
+
 **Changes in program logic:**
 
 * In the axiomatization of ectx languages we replace the axiom of positivity of
@@ -148,6 +148,25 @@ s/\blist_singletonM_included\b/list_singleton_included/g
 ' $(find theories -name "*.v")
 ```
 
+* New ASCII versions of Iris notations. These are marked printing only and
+  can be made available using `Require Import iris.bi.ascii`. The new
+  notations are (notations marked [†] are disambiguated using notation scopes):
+  - entailment: `|--` for `⊢` and `-|-` for `⊣⊢`
+  - logic[†]: `->` for `→`, `/\\` for `∧`, `\\/` for `∨`, and `<->` for `↔`
+  - quantifiers[†]: `forall` for `∀` and `exists` for `∃`
+  - separation logic: `**` for `∗`, `-*` for `-∗`, and `*-*` for `∗-∗`
+  - step indexing: `|>` for `▷`
+  - modalities: `<#>` for `□` and `<except_0>` for `◇`
+  - most derived notations can be computed from previous notations using the
+    substitutions above, e.g. replace `∗` with `*` and `▷` with `|>`. Examples
+    include the following:
+    - `|={E1,E2}=* P` for `|={E1,E2}=∗`
+    - `P ={E}=* Q` for `P ={E}=∗ Q`
+    - `P ={E1,E2}=* Q` for `P ={E1,E2}=∗ Q`
+    - `|={E1,E2,E3}|>=> Q` for `|={E1,E2,E3}▷=> Q`
+    - `|={E1,E2}|>=>^n Q` for `|={E1,E2}▷=>^n Q`
+    The full list can be found in [theories/bi/ascii.v](theories/bi/ascii.v),
+    where the ASCII notations are defined in terms of the unicode notations.
 
 **Changes in heap_lang:**
 

_CoqProject

@@ -49,6 +49,7 @@ theories/bi/derived_laws_sbi.v
 theories/bi/plainly.v
 theories/bi/big_op.v
 theories/bi/updates.v
+theories/bi/ascii.v
 theories/bi/bi.v
 theories/bi/tactics.v
 theories/bi/monpred.v

tests/proofmode_ascii.ref

+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : inv N (<pers> P)
+  "H2" : ▷ <pers> P
+  --------------------------------------□
+  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  N : namespace
+  P : iProp Σ
+  ============================
+  "H" : inv N (<pers> P)
+  "H2" : ▷ <pers> P
+  --------------------------------------□
+  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> ▷ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : iProp Σ
+  ============================
+  _ : cinv N γ (<pers> P)
+  "HP" : ▷ <pers> P
+  --------------------------------------□
+  "Hown" : cinv_own γ p
+  --------------------------------------∗
+  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  γ : gname
+  p : Qp
+  N : namespace
+  P : iProp Σ
+  ============================
+  _ : cinv N γ (<pers> P)
+  "HP" : ▷ <pers> P
+  --------------------------------------□
+  "Hown" : cinv_own γ p
+  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E2
+  ============================
+  _ : na_inv t N (<pers> P)
+  "HP" : ▷ <pers> P
+  --------------------------------------□
+  "Hown1" : na_own t E1
+  "Hown2" : na_own t (E2 ∖ ↑N)
+  --------------------------------------∗
+  |={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
+          ∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
+  
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  t : na_inv_pool_name
+  N : namespace
+  E1, E2 : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E2
+  ============================
+  _ : na_inv t N (<pers> P)
+  "HP" : ▷ <pers> P
+  --------------------------------------□
+  "Hown1" : na_own t E1
+  "Hown2" : na_own t (E2 ∖ ↑N)
+  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
+  --------------------------------------∗
+  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
+  
+"test_iInv_12"
+     : string
+The command has indeed failed with message:
+Tactic failure: iInv: selector 34 is not of the right type .
+The command has indeed failed with message:
+Tactic failure: iInv: invariant nroot not found.
+The command has indeed failed with message:
+Tactic failure: iInv: invariant "H2" not found.
+"test_iInv"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  I : biIndex
+  N : namespace
+  E : coPset
+  𝓟 : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  "HP" : ⎡ ▷ 𝓟 ⎤
+  --------------------------------------∗
+  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
+  
+"test_iInv_with_close"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  invG0 : invG Σ
+  I : biIndex
+  N : namespace
+  E : coPset
+  𝓟 : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  "HP" : ⎡ ▷ 𝓟 ⎤
+  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
+  --------------------------------------∗
+  |={E ∖ ↑N,E}=> emp
+  

tests/proofmode_ascii.v

+From iris.proofmode Require Import tactics monpred.
+From iris.base_logic Require Import base_logic.
+From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+
+From iris.bi Require Import ascii.
+
+Section base_logic_tests.
+  Context {M : ucmraT}.
+  Implicit Types P Q R : uPred M.
+
+  Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
+    |-- forall (x y : nat) a b,
+      x ≡ y ->
+      <#> (uPred_ownM (a ⋅ b) -*
+      (exists y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ <#> uPred_ownM c) -*
+      <#> |> (forall z, P2 z ∨ True -> P2 z) -*
+      |> (forall n m : nat, P1 n -> <#> (True ∧ P2 n -> <#> (⌜n = n⌝ ↔ P3 n))) -*
+      |> ⌜x = 0⌝ \/ exists x z, |> P3 (x + z) ** uPred_ownM b ** uPred_ownM (core b)).
+  Proof.
+    iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
+    { iLeft. by iNext. }
+    iRight.
+    iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
+    iPoseProof "Hc" as "foo".
+    iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
+    iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]".
+    { by rewrite cmra_core_r. }
+    iIntros "{$Hac $Ha}".
+    iExists (S j + z1), z2.
+    iNext.
+    iApply ("H3" $! _ 0 with "[$]").
+    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - done.
+  Qed.
+
+  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.
+
+  Lemma test_iAssert_modality P : (|==> False) -* |==> P.
+  Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
+
+  Lemma test_iStartProof_1 P : P -* P.
+  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Lemma test_iStartProof_2 P : P -* P.
+  Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
+  Lemma test_iStartProof_3 P : P -* P.
+  Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
+  Lemma test_iStartProof_4 P : P -* P.
+  Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
+End base_logic_tests.
+
+Section iris_tests.
+  Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
+  Implicit Types P Q R : iProp Σ.
+
+  Lemma test_masks  N E P Q R :
+    ↑N ⊆ E ->
+    (True -* P -* inv N Q -* True -* R) -* P -* |> Q ={E}=* R.
+  Proof.
+    iIntros (?) "H HP HQ".
+    iApply ("H" with "[% //] [$] [> HQ] [> //]").
+    by iApply inv_alloc.
+  Qed.
+
+  Lemma test_iInv_0 N P: inv N (<pers> P) ={⊤}=* |> P.
+  Proof.
+    iIntros "#H".
+    iInv N as "#H2". Show.
+    iModIntro. iSplit; auto.
+  Qed.
+
+  Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={⊤}=* |> P.
+  Proof.
+    iIntros "#H".
+    iInv N as "#H2" "Hclose". Show.
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
+  Lemma test_iInv_1 N E P:
+    ↑N ⊆ E ->
+    inv N (<pers> P) ={E}=* |> P.
+  Proof.
+    iIntros (?) "#H".
+    iInv N as "#H2".
+    iModIntro. iSplit; auto.
+  Qed.
+
+  Lemma test_iInv_2 γ p N P:
+    cinv N γ (<pers> P) ** cinv_own γ p ={⊤}=* cinv_own γ p ** |> P.
+  Proof.
+    iIntros "(#?&?)".
+    iInv N as "(#HP&Hown)". Show.
+    iModIntro. iSplit; auto with iFrame.
+  Qed.
+
+  Lemma test_iInv_2_with_close γ p N P:
+    cinv N γ (<pers> P) ** cinv_own γ p ={⊤}=* cinv_own γ p ** |> P.
+  Proof.
+    iIntros "(#?&?)".
+    iInv N as "(#HP&Hown)" "Hclose". Show.
+    iMod ("Hclose" with "HP").
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  Lemma test_iInv_3 γ p1 p2 N P:
+    cinv N γ (<pers> P) ** cinv_own γ p1 ** cinv_own γ p2
+      ={⊤}=* cinv_own γ p1 ** cinv_own γ p2  ** |> P.
+  Proof.
+    iIntros "(#?&Hown1&Hown2)".
+    iInv N with "[Hown2 //]" as "(#HP&Hown2)".
+    iModIntro. iSplit; auto with iFrame.
+  Qed.
+
+  Lemma test_iInv_4 t N E1 E2 P:
+    ↑N ⊆ E2 ->
+    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
+         |-- |={⊤}=> na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N as "(#HP&Hown2)". Show.
+    iModIntro. iSplitL "Hown2"; auto with iFrame.
+  Qed.
+
+  Lemma test_iInv_4_with_close t N E1 E2 P:
+    ↑N ⊆ E2 ->
+    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
+         |-- |={⊤}=> na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N as "(#HP&Hown2)" "Hclose". Show.
+    iMod ("Hclose" with "[HP Hown2]").
+    { iFrame. done. }
+    iModIntro. iFrame. by iNext.
+  Qed.
+
+  (* test named selection of which na_own to use *)
+  Lemma test_iInv_5 t N E1 E2 P:
+    ↑N ⊆ E2 ->
+    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
+      ={⊤}=* na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N with "Hown2" as "(#HP&Hown2)".
+    iModIntro. iSplitL "Hown2"; auto with iFrame.
+  Qed.
+
+  Lemma test_iInv_6 t N E1 E2 P:
+    ↑N ⊆ E1 ->
+    na_inv t N (<pers> P) ** na_own t E1 ** na_own t E2
+      ={⊤}=* na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&Hown1&Hown2)".
+    iInv N with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
+  Qed.
+
+  (* test robustness in presence of other invariants *)
+  Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 ->
+    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P  ** na_own t E1 ** na_own t E2
+      ={⊤}=* na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
+    iInv N3 with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
+  Qed.
+
+  (* iInv should work even where we have "inv N P" in which P contains an evar *)
+  Lemma test_iInv_8 N : ∃ P, inv N P ={⊤}=* P ≡ True ∧ inv N P.
+  Proof.
+    eexists. iIntros "#H".
+    iInv N as "HP". iFrame "HP". auto.
+  Qed.
+
+  (* test selection by hypothesis name instead of namespace *)
+  Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 ->
+    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P  ** na_own t E1 ** na_own t E2
+      ={⊤}=* na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
+    iInv "HInv" with "Hown1" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
+  Qed.
+
+  (* test selection by hypothesis name instead of namespace *)
+  Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
+    ↑N3 ⊆ E1 ->
+    inv N1 P ** na_inv t N3 (<pers> P) ** inv N2 P  ** na_own t E1 ** na_own t E2
+      ={⊤}=* na_own t E1 ** na_own t E2  ** |> P.
+  Proof.
+    iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
+    iInv "HInv" as "(#HP&Hown1)".
+    iModIntro. iSplitL "Hown1"; auto with iFrame.
+  Qed.
+
+  (* test selection by ident name *)
+  Lemma test_iInv_11 N P: inv N (<pers> P) ={⊤}=* |> P.
+  Proof.
+    let H := iFresh in
+    (iIntros H; iInv H as "#H2"). auto.
+  Qed.
+
+  (* error messages *)
+  Check "test_iInv_12".
+  Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=* True.
+  Proof.
+    iIntros "H".
+    Fail iInv 34 as "#H2".
+    Fail iInv nroot as "#H2".
+    Fail iInv "H2" as "#H2".
+    done.
+  Qed.
+
+  (* test destruction of existentials when opening an invariant *)
+  Lemma test_iInv_13 N:
+    inv N (∃ (v1 v2 v3 : nat), emp ** emp ** emp) ={⊤}=* |> emp.
+  Proof.
+    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)".
+    eauto.
+  Qed.
+
+  Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
+    x' ≼ x ->
+    own γ x -* own γ x'.
+  Proof. intros. by iApply own_mono. Qed.
+End iris_tests.
+
+Section monpred_tests.
+  Context `{!invG Σ}.
+  Context {I : biIndex}.
+  Local Notation monPred := (monPred I (iPropI Σ)).
+  Local Notation monPredI := (monPredI I (iPropI Σ)).
+  Local Notation monPredSI := (monPredSI I (iPropSI Σ)).
+  Implicit Types P Q R : monPred.
+  Implicit Types 𝓟 𝓠 𝓡 : iProp Σ.
+
+  Check "test_iInv".
+  Lemma test_iInv N E 𝓟 :
+    ↑N ⊆ E ->
+    ⎡inv N 𝓟⎤ |--@{monPredI} |={E}=> emp.
+  Proof.
+    iIntros (?) "Hinv".
+    iInv N as "HP". Show.
+    iFrame "HP". auto.
+  Qed.
+
+  Check "test_iInv_with_close".
+  Lemma test_iInv_with_close N E 𝓟 :
+    ↑N ⊆ E ->
+    ⎡inv N 𝓟⎤ |--@{monPredI} |={E}=> emp.
+  Proof.
+    iIntros (?) "Hinv".
+    iInv N as "HP" "Hclose". Show.
+    iMod ("Hclose" with "HP"). auto.
+  Qed.
+
+End monpred_tests.

theories/bi/ascii.v

+From iris.bi Require Import interface derived_connectives updates.
+From iris.algebra Require Export ofe.
+
+(** note: we use [|--] instead of [|-] because the latter is used by
+    Ltac's [match goal] construct.
+ *)
+Notation "P |-- Q" := (P ⊢ Q)
+  (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
+Notation "P '|--@{' PROP } Q" := (P ⊢@{PROP} Q) (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
+Notation "(|--)" := (⊢) (only parsing) : stdpp_scope.
+(* FIXME: fix notation *)
+Notation "('|--@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
+
+Notation "|-- Q" := (⊢ Q%I) (at level 20, Q at level 200, only parsing) : stdpp_scope.
+Notation "'|--@{' PROP } Q" := (⊢@{PROP} Q) (at level 20, Q at level 200, only parsing) : stdpp_scope.
+
+Notation "P -|- Q" := (P ⊣⊢ Q) (at level 95, no associativity, only parsing) : stdpp_scope.
+Notation "P '-|-@{' PROP } Q" := (P ⊣⊢@{PROP} Q) (at level 95, no associativity, only parsing) : stdpp_scope.
+Notation "(-|-)" := (⊣⊢) (only parsing) : stdpp_scope.
+(* FIXME: fix notation *)
+Notation "('-|-@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
+
+Notation "P -* Q" := (P ⊢ Q)%stdpp (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
+
+(* FIXME: Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope. *)
+Notation "P /\ Q" := (P ∧ Q)%I (only parsing) : bi_scope.
+Notation "(/\)" := bi_and (only parsing) : bi_scope.
+Notation "P \/ Q" := (P ∨ Q)%I (only parsing) : bi_scope.
+Notation "(\/)" := bi_or (only parsing) : bi_scope.
+Notation "P -> Q" := (P → Q)%I (only parsing) : bi_scope.
+Notation "P ** Q" := (P ∗ Q)%I (at level 80, right associativity, only parsing) : bi_scope.
+Notation "(**)" := bi_sep (only parsing) : bi_scope.
+Notation "P -* Q" := (P -∗ Q)%I
+  (at level 99, Q at level 200, right associativity, only parsing) : bi_scope.
+
+(* ∀ x .. y , P *)
+Notation "'forall' x .. y , P" :=
+  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) (at level 200, x binder, right associativity, only parsing) : bi_scope.
+(* ∃ x .. y , P *)
+Notation "'exists' x .. y , P" :=
+  (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) (at level 200, x binder, right associativity, only parsing) : bi_scope.
+
+Notation "|> P" := (▷ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+Notation "|>? p P" := (▷?p P)%I (at level 20, p at level 9, P at level 20,
+   only parsing) : bi_scope.
+Notation "|>^ n P" := (▷^n P)%I (at level 20, n at level 9, P at level 20,
+   only parsing) : bi_scope.
+
+Notation "P <-> Q" := (P ↔ Q)%I (at level 95, no associativity, only parsing) : bi_scope.
+
+Notation "P *-* Q" := (P ∗-∗ Q)%I (at level 95, no associativity, only parsing) : bi_scope.
+
+Notation "'<#>' P" := (□ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+Notation "'<#>?' p P" := (□?p P)%I (at level 20, p at level 9, P at level 20,
+   right associativity, only parsing) : bi_scope.
+
+Notation "'<except_0>' P" := (◇ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+
+Notation "mP -*? Q" := (mP -∗? Q)%I
+  (at level 99, Q at level 200, right associativity, only parsing) : bi_scope.
+
+Notation "P ==* Q" := (P ==∗ Q)%stdpp (at level 99, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ==* Q" := (P ==∗ Q)%I (at level 99, Q at level 200, only parsing) : bi_scope.
+
+Notation "P ={ E1 , E2 }=* Q" := (P ={E1,E2}=∗ Q)%I (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E1 , E2 }=* Q" := (P ={E1,E2}=∗ Q) (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+
+Notation "P ={ E }=* Q" := (P ={E}=∗ Q)%I (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E }=* Q" := (P ={E}=∗ Q) (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope
+.
+
+Notation "|={ E1 , E2 , E3 }|>=> Q" := (|={E1,E2,E3}▷=> Q)%I (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E1 , E2 , E3 }|>=* Q" := (P ={E1,E2,E3}▷=∗ Q)%I (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "|={ E1 , E2 }|>=> Q" := (|={E1,E2}▷=> Q)%I (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
+
+Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q) (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)%I (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
+
+Notation "|={ E }|>=> Q" := (|={E}▷=> Q)%I (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E }|>=* Q" := (P ={E}▷=∗ Q)%I (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "|={ E1 , E2 }|>=>^ n Q" := (|={E1,E2}▷=>^n Q)%I (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing) : bi_scope.