From ce9313df4eb18735dc1c15215ede259b5be41ae0 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Wed, 6 Jun 2018 19:35:44 +0200
Subject: [PATCH] make updates and magic wand linebreaks consistent with coq
built-in notation
---
tests/proofmode.ref | 51 ++++++++++++++++++++++++++++++++++++++----
tests/proofmode.v | 25 +++++++++++++++++++--
theories/bi/notation.v | 14 +++++++-----
3 files changed, 78 insertions(+), 12 deletions(-)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 7f236c6de..4dcf318a5 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -75,6 +75,48 @@
--------------------------------------∗
True
+1 subgoal
+
+ PROP : sbi
+ BiFUpd0 : BiFUpd PROP
+ PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
+ ============================
+ --------------------------------------∗
+ PPPPPPPPPPPPPPPPP
+ → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+
+1 subgoal
+
+ PROP : sbi
+ BiFUpd0 : BiFUpd PROP
+ PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
+ ============================
+ --------------------------------------∗
+ PPPPPPPPPPPPPPPPP
+ → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+ → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+
+1 subgoal
+
+ PROP : sbi
+ BiFUpd0 : BiFUpd PROP
+ PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
+ ============================
+ --------------------------------------∗
+ PPPPPPPPPPPPPPPPP
+ -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+
+1 subgoal
+
+ PROP : sbi
+ BiFUpd0 : BiFUpd PROP
+ PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
+ ============================
+ --------------------------------------∗
+ PPPPPPPPPPPPPPPPP
+ -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+ -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+
1 subgoal
PROP : sbi
@@ -83,8 +125,8 @@
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
- PPPPPPPPPPPPPPPPP ={E}=∗
- QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+ PPPPPPPPPPPPPPPPP
+ ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
@@ -94,6 +136,7 @@
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
--------------------------------------∗
- PPPPPPPPPPPPPPPPP ={E1,E2}=∗
- QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+ PPPPPPPPPPPPPPPPP
+ ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+ ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e2178b33f..b0168e1f8 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -518,13 +518,34 @@ Proof.
iIntros "?". Show.
Abort.
+Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+ (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+Proof.
+ iStartProof. Show.
+Abort.
+Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+ (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+Proof.
+ iStartProof. Show.
+Abort.
+Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+ (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+Proof.
+ iStartProof. Show.
+Abort.
+Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+ (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+Proof.
+ iStartProof. Show.
+Abort.
Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
Proof.
iStartProof. Show.
Abort.
-Lemma long_fupd_maskchanging E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
- PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
+Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+ PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+ ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
Proof.
iStartProof. Show.
Abort.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 31d7168c9..426076425 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -12,7 +12,9 @@ Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
Reserved Notation "'emp'".
Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
-Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P -∗ Q"
+ (at level 99, Q at level 200, right associativity,
+ format "'[' P '/' -∗ Q ']'").
Reserved Notation "⎡ P ⎤".
@@ -51,34 +53,34 @@ Reserved Notation "'' P" (at level 20, right associativity).
(** 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 ']'").
+ (at level 99, Q at level 200, format "'[' P '/' ==∗ Q ']'").
Reserved Notation "|={ E1 , E2 }=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q").
Reserved Notation "P ={ E1 , E2 }=∗ Q"
(at level 99, E1,E2 at level 50, Q at level 200,
- format "'[ ' P ={ E1 , E2 }=∗ '/' Q ']'").
+ format "'[' P '/' ={ E1 , E2 }=∗ Q ']'").
Reserved Notation "|={ E }=> Q"
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q").
Reserved Notation "P ={ E }=∗ Q"
(at level 99, E at level 50, Q at level 200,
- format "'[ ' P ={ E }=∗ '/' Q ']'").
+ format "'[' P '/' ={ E }=∗ Q ']'").
Reserved Notation "|={ E1 , E2 }▷=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }▷=> Q").
Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
(at level 99, E1, E2 at level 50, Q at level 200,
- format "'[ ' P ={ E1 , E2 }▷=∗ '/' Q ']'").
+ format "'[' P '/' ={ E1 , E2 }▷=∗ Q ']'").
Reserved Notation "|={ E }▷=> Q"
(at level 99, E at level 50, Q at level 200,
format "|={ E }▷=> Q").
Reserved Notation "P ={ E }▷=∗ Q"
(at level 99, E at level 50, Q at level 200,
- format "'[ ' P ={ E }▷=∗ '/' Q ']'").
+ format "'[' P '/' ={ E }▷=∗ Q ']'").
(** Big Ops *)
Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
--
GitLab