Merge branch 'change-turnstile' into 'master'

Change ascii turnstile

See merge request iris/iris!435

CHANGELOG.md

@@ -143,7 +143,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * New ASCII versions of Iris notations. These are marked parsing 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 `⊣⊢`
+  - entailment: `|-` for `⊢` and `-|-` for `⊣⊢`
   - logic[†]: `->` for `→`, `/\\` for `∧`, `\\/` for `∨`, and `<->` for `↔`
   - quantifiers[†]: `forall` for `∀` and `exists` for `∃`
   - separation logic: `**` for `∗`, `-*` for `-∗`, and `*-*` for `∗-∗`

tests/bi_ascii_parsing.ref

+"test1"
+     : string
+True%I
+(⊢ True)
+"test2"
+     : string
+False%I True%I
+(False -∗ True)

tests/bi_ascii_parsing.v

+Require Import Coq.Strings.String.
+Require Import iris.bi.bi.
+Require Import iris.bi.ascii.
+
+Local Open Scope string_scope.
+
+(* this file demonstrates that the [|-] notation does not
+   conflict with the ltac notation.
+ *)
+Section with_bi.
+  Context {PROP : bi}.
+  Variables P Q R : PROP.
+
+  Local Open Scope stdpp_scope.
+
+  Ltac pg :=
+    match goal with
+    | |- ?X => idtac X
+    end.
+
+  Ltac foo g :=
+    lazymatch g with
+    | |- ?T => idtac T
+    | ?U |- ?T => idtac U T
+    end.
+
+  Ltac bar :=
+    match goal with
+    | |- ?G => foo G
+    end.
+
+  Check "test1".
+  Lemma test1 : |-@{PROP} True.
+  Proof. bar. pg. Abort.
+
+  Check "test2".
+  Lemma test2 : False |-@{PROP} True.
+  Proof. bar. pg. Abort.
+End with_bi.

tests/proofmode_ascii.v

@@ -12,7 +12,7 @@ Section base_logic_tests.
   Implicit Types P Q R : uPred M.
 
   Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
-    |-- forall (x y : nat) a b,
+    |- forall (x y : nat) a b,
       x ≡ y ->
       <#> (uPred_ownM (a ⋅ b) -*
       (exists y1 y2 c, P1 ((x + y1) + y2) /\ True /\ <#> uPred_ownM c) -*
@@ -37,7 +37,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.
@@ -119,7 +119,7 @@ Section iris_tests.
   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.
+         |- |={⊤}=> na_own t E1 ** na_own t E2  ** |> P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)". Show.
@@ -129,7 +129,7 @@ Section iris_tests.
   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.
+         |- |={⊤}=> na_own t E1 ** na_own t E2  ** |> P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)" "Hclose". Show.
@@ -242,7 +242,7 @@ Section monpred_tests.
   Check "test_iInv".
   Lemma test_iInv N E 𝓟 :
     ↑N ⊆ E ->
-    ⎡inv N 𝓟⎤ |--@{monPredI} |={E}=> emp.
+    ⎡inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
   Proof.
     iIntros (?) "Hinv".
     iInv N as "HP". Show.
@@ -252,7 +252,7 @@ Section monpred_tests.
   Check "test_iInv_with_close".
   Lemma test_iInv_with_close N E 𝓟 :
     ↑N ⊆ E ->
-    ⎡inv N 𝓟⎤ |--@{monPredI} |={E}=> emp.
+    ⎡inv N 𝓟⎤ |-@{monPredI} |={E}=> emp.
   Proof.
     iIntros (?) "Hinv".
     iInv N as "HP" "Hclose". Show.
@@ -266,89 +266,89 @@ Section parsing_tests.
 Context {PROP : bi}.
 Implicit Types P : PROP.
 
-Lemma test_bi_emp_valid : |--@{PROP} True.
+Lemma test_bi_emp_valid : |-@{PROP} True.
 Proof. naive_solver. Qed.
 
-Lemma test_bi_emp_valid_parens : (|--@{PROP} True) /\ ((|--@{PROP} True)).
+Lemma test_bi_emp_valid_parens : (|-@{PROP} True) /\ ((|-@{PROP} True)).
 Proof. naive_solver. Qed.
 
-Lemma test_bi_emp_valid_parens_space_open : ( |--@{PROP} True).
+Lemma test_bi_emp_valid_parens_space_open : ( |-@{PROP} True).
 Proof. naive_solver. Qed.
 
-Lemma test_bi_emp_valid_parens_space_close : (|--@{PROP} True ).
+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 /\
   (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 /\
   ((P -|-@{PROP} P)) /\ ((-|-@{PROP})) P P.
 Proof. naive_solver. Qed.
 
 Lemma test_entails_annot_sections_space_open P :
-  ( P |--@{PROP} 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 /\
   (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
 Proof. naive_solver. Qed.
 
 
 Check "p1".
-Lemma p1 : forall P, True -> P |-- P.
+Lemma p1 : forall P, True -> P |- P.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p2".
-Lemma p2 : forall P, True /\ (P |-- P).
+Lemma p2 : forall P, True /\ (P |- P).
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p3".
-Lemma p3 : exists P, P |-- P.
+Lemma p3 : exists P, P |- P.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p4".
-Lemma p4 : |--@{PROP} exists (x : nat), ⌜x = 0⌝.
+Lemma p4 : |-@{PROP} exists (x : nat), ⌜x = 0⌝.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p5".
-Lemma p5 : |--@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝.
+Lemma p5 : |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p6".
-Lemma p6 : exists! (z : nat), |--@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝.
+Lemma p6 : exists! (z : nat), |-@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p7".
-Lemma p7 : forall (a : nat), a = 0 -> forall y, True |--@{PROP} ⌜y >= 0⌝.
+Lemma p7 : forall (a : nat), a = 0 -> forall y, True |-@{PROP} ⌜y >= 0⌝.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p8".
-Lemma p8 : forall (a : nat), a = 0 -> forall y, |--@{PROP} ⌜y >= 0⌝.
+Lemma p8 : forall (a : nat), a = 0 -> forall y, |-@{PROP} ⌜y >= 0⌝.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.
 
 Check "p9".
-Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |--@{PROP} forall z : nat, ⌜z >= 0⌝.
+Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |-@{PROP} forall z : nat, ⌜z >= 0⌝.
 Proof.
   Unset Printing Notations. Show. Set Printing Notations.
 Abort.

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)
+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)
+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.
-Notation "'(|--@{' PROP } )" := (⊢@{PROP}) (only parsing) : stdpp_scope.
+Notation "(|-)" := (⊢) (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.
+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 "'(|-@{' 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)