Merge branch 'fix-notation-3' into 'master'

Fix notation issues in #302 and add some missing "operator sections" for (bi)entailment

Closes #302

See merge request iris/iris!409

tests/proofmode.v

@@ -5,10 +5,6 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
-Lemma type_sbi_internal_eq_annot P :
-  P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P.
-Proof. done. Qed.
-
 Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
 
@@ -825,7 +821,54 @@ Proof.
 Qed.
 End tests.
 
-(** Test specifically if certain things print correctly. *)
+Section parsing_tests.
+Context {PROP : sbi}.
+Implicit Types P : PROP.
+
+(** Test notations for (bi)entailment and internal equality. These tests are
+especially extensive because of past problems such as
+https://gitlab.mpi-sws.org/iris/iris/-/issues/302. *)
+Lemma test_bi_emp_valid : ⊢@{PROP} True.
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens : (⊢@{PROP} True) ∧ ((⊢@{PROP} True)).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_open : ( ⊢@{PROP} True).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_close : (⊢@{PROP} True ).
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections P :
+  (P ⊢@{PROP} P) ∧ (⊢@{PROP}) P P ∧ (P ⊢.) P ∧ (.⊢ P) P ∧
+  (P ⊣⊢@{PROP} P) ∧ (⊣⊢@{PROP}) P P ∧ (P ⊣⊢.) P ∧ (.⊣⊢ P) P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_parens P :
+  ((P ⊢@{PROP} P)) ∧ ((⊢@{PROP})) P P ∧ ((P ⊢.)) P ∧ ((.⊢ P)) P ∧
+  ((P ⊣⊢@{PROP} P)) ∧ ((⊣⊢@{PROP})) P P ∧ ((P ⊣⊢.)) P ∧ ((.⊣⊢ P)) P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_open P :
+  ( P ⊢@{PROP} P) ∧ ( P ⊢.) P ∧
+  ( P ⊣⊢@{PROP} P) ∧ ( P ⊣⊢.) P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_close P :
+  (P ⊢@{PROP} P ) ∧ (⊢@{PROP} ) P P ∧ (.⊢ P ) P ∧
+  (P ⊣⊢@{PROP} P ) ∧ (⊣⊢@{PROP} ) P P ∧ (.⊣⊢ P ) P.
+Proof. naive_solver. Qed.
+
+Lemma test_sbi_internal_eq_annot_sections P :
+  ⊢@{PROP}
+    P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P ∧
+    ((P ≡@{PROP} P)) ∧ ((≡@{PROP})) P P ∧ ((P ≡.)) P ∧ ((.≡ P)) P ∧
+    ( P ≡@{PROP} P) ∧ ( P ≡.) P ∧
+    (P ≡@{PROP} P ) ∧ (≡@{PROP} ) P P ∧ (.≡ P ) P.
+Proof. naive_solver. Qed.
+End parsing_tests.
+
 Section printing_tests.
 Context {PROP : sbi} `{!BiFUpd PROP}.
 Implicit Types P Q R : PROP.

tests/proofmode_ascii.v

@@ -12,9 +12,9 @@ Section base_logic_tests.
     |-- forall (x y : nat) a b,
       x ≡ y ->
       <#> (uPred_ownM (a ⋅ b) -*
-      (exists y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ <#> uPred_ownM c) -*
+      (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))) -*
+      |> (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.
@@ -34,7 +34,7 @@ Section base_logic_tests.
   Qed.
 
   Lemma test_iFrame_pure (x y z : M) :
-    ✓ x -> ⌜y ≡ z⌝ |--@{uPredI M} ✓ x ∧ ✓ x ∧ y ≡ z.
+    ✓ 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.
@@ -159,8 +159,8 @@ Section iris_tests.
   (* 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.
+    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)".
@@ -168,7 +168,7 @@ Section iris_tests.
   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.
+  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.
@@ -177,8 +177,8 @@ Section iris_tests.
   (* 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.
+    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)".
@@ -188,8 +188,8 @@ Section iris_tests.
   (* 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.
+    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)".
@@ -258,3 +258,41 @@ Section monpred_tests.
   Qed.
 
 End monpred_tests.
+
+(** Test specifically if certain things parse correctly. *)
+Section parsing_tests.
+Context {PROP : sbi}.
+Implicit Types P : PROP.
+
+Lemma test_bi_emp_valid : |--@{PROP} True.
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens : (|--@{PROP} True) /\ ((|--@{PROP} True)).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_open : ( |--@{PROP} True).
+Proof. naive_solver. Qed.
+
+Lemma test_bi_emp_valid_parens_space_close : (|--@{PROP} True ).
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections P :
+  (P |--@{PROP} P) /\ (|--@{PROP}) P P /\
+  (P -|-@{PROP} P) /\ (-|-@{PROP}) P P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_parens P :
+  ((P |--@{PROP} P)) /\ ((|--@{PROP})) P P /\
+  ((P -|-@{PROP} P)) /\ ((-|-@{PROP})) P P.
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_open P :
+  ( P |--@{PROP} P) /\
+  ( P -|-@{PROP} P).
+Proof. naive_solver. Qed.
+
+Lemma test_entails_annot_sections_space_close P :
+  (P |--@{PROP} P ) /\ (|--@{PROP} ) P P /\
+  (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
+Proof. naive_solver. Qed.
+End parsing_tests.

theories/bi/ascii.v

@@ -8,17 +8,17 @@ 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 "'(|--@{' 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.
+(** Work around parsing issues: see [notation.v] for details. *)
+Notation "'(|--@{' PROP } Q )" := (⊢@{PROP} Q) (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 "'(-|-@{' PROP } )" := (⊣⊢@{PROP}) (only parsing) : stdpp_scope.
 
 Notation "P -* Q" := (P ⊢ Q)%stdpp (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
 

theories/bi/interface.v

@@ -262,12 +262,14 @@ Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
 Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
 Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
-Notation "('⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
+Notation "'(⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
 
 Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
 Notation "P '⊣⊢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
 Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
-Notation "('⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
+Notation "'(⊣⊢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
+Notation "( P ⊣⊢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
+Notation "(.⊣⊢ Q )" := (λ P, P ≡@{bi_car _} Q) (only parsing) : stdpp_scope.
 
 Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope.
 
@@ -305,6 +307,10 @@ Typeclasses Opaque bi_emp_valid.
 
 Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
 Notation "'⊢@{' PROP } Q" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
+(** Work around parsing issues: see [notation.v] for details. *)
+Notation "'(⊢@{' PROP } Q )" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
+Notation "(.⊢ Q )" := (λ P, P ⊢ Q) (only parsing) : stdpp_scope.
+Notation "( P ⊢.)" := (bi_entails P) (only parsing) : stdpp_scope.
 
 Module bi.
 Section bi_laws.
@@ -371,7 +377,7 @@ Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed.
 Lemma forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
 Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed.
 Lemma forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. eapply (bi_mixin_forall_elim  bi_entails), bi_bi_mixin. Qed.
+Proof. eapply (bi_mixin_forall_elim bi_entails), bi_bi_mixin. Qed.
 
 Lemma exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a.
 Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed.

theories/bi/notation.v

 (** Just reserve the notation. *)
 
-(** Turnstiles *)
+(** * Turnstiles *)
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "(⊢)".
-Reserved Notation "('⊢@{' PROP } )".
+Reserved Notation "'(⊢@{' PROP } )".
+Reserved Notation "( P ⊣⊢.)".
+Reserved Notation "(.⊣⊢ Q )".
 
 Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
 Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
 Reserved Notation "(⊣⊢)".
-Reserved Notation "('⊣⊢@{' PROP } )".
+Reserved Notation "'(⊣⊢@{' PROP } )".
+Reserved Notation "(.⊢ Q )".
+Reserved Notation "( P ⊢.)".
 
 Reserved Notation "⊢ Q" (at level 20, Q at level 200).
 Reserved Notation "'⊢@{' PROP } Q" (at level 20, Q at level 200).
+(** The definition must coincide with "'⊢@{' PROP } Q". *)
+Reserved Notation "'(⊢@{' PROP } Q )".
+(**
+Rationale:
+Notation [( '⊢@{' PROP } )] prevents parsing [(⊢@{PROP} Q)] using the
+[⊢@{PROP} Q] notation; since the latter parse arises from composing two
+notations, it is missed by the automatic left-factorization.
 
-(** BI connectives *)
+To fix that, we force left-factorization by explicitly composing parentheses with
+['⊢@{' PROP } Q] into the new notation [( '⊢@{' PROP } Q )],
+which successfully undergoes automatic left-factoring. *)
+
+
+(** * BI connectives *)
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
@@ -58,7 +74,7 @@ Reserved Notation "■? p P" (at level 20, p at level 9, P at level 20,
 Reserved Notation "'<obj>' P" (at level 20, right associativity).
 Reserved Notation "'<subj>' P" (at level 20, right associativity).
 
-(** Update modalities *)
+(** * Update modalities *)
 Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
 Reserved Notation "P ==∗ Q"
   (at level 99, Q at level 200, format "'[' P  '/' ==∗  Q ']'").
@@ -102,7 +118,7 @@ Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
    format "P  ={ E1 , E2 }▷=∗^ n  Q").
 
-(** Big Ops *)
+(** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
   (at level 200, l at level 10, k, x at level 1, right associativity,
    format "[∗  list]  k ↦ x  ∈  l ,  P").