Fix entailment notations `(⊢@{PROP})` and `(⊣⊢@{PROP} )` etc.

Fix #302, including their ASCII variants.
- Don't use quotes `'` that are not surrounded by spaces.
- However, notation `'(⊢@{' PROP } )` prevents parsing `(⊢@{PROP} Q)` using the
`⊢@{PROP} Q` notation.

To fix that, we force left-factorization: we add a notation for `'(⊢@{' PROP }
Q )`, defined to coincide with '⊢@{' PROP } Q but which can be left-factored
with `( '⊢@{' PROP } )`.

- Add left and right operator sections for (bi)entailment
- Add tests.

Also do all of the above also for ASCII notations, except for operator sections,
which seem to require more discussion.

tests/proofmode.v

@@ -5,10 +5,6 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
-Lemma test_sbi_internal_eq_annot_sections P :
-  ⊢@{PROP} P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P.
-Proof. by iSplit. 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

@@ -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.

theories/bi/notation.v

@@ -4,15 +4,31 @@
 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.
+
+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'".