Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
ce9313df
Commit
ce9313df
authored
Jun 06, 2018
by
Ralf Jung
Browse files
make updates and magic wand linebreaks consistent with coq builtin notation
parent
3660c994
Changes
3
Show whitespace changes
Inline
Sidebyside
tests/proofmode.ref
View file @
ce9313df
...
@@ 75,6 +75,48 @@
...
@@ 75,6 +75,48 @@
∗
∗
True
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
1 subgoal
PROP : sbi
PROP : sbi
...
@@ 83,8 +125,8 @@
...
@@ 83,8 +125,8 @@
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
============================
∗
∗
PPPPPPPPPPPPPPPPP
={E}=∗
PPPPPPPPPPPPPPPPP
QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E}=∗
QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
1 subgoal
1 subgoal
...
@@ 94,6 +136,7 @@
...
@@ 94,6 +136,7 @@
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
============================
============================
∗
∗
PPPPPPPPPPPPPPPPP ={E1,E2}=∗
PPPPPPPPPPPPPPPPP
QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
tests/proofmode.v
View file @
ce9313df
...
@@ 518,13 +518,34 @@ Proof.
...
@@ 518,13 +518,34 @@ Proof.
iIntros
"?"
.
Show
.
iIntros
"?"
.
Show
.
Abort
.
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
)
:
Lemma
long_fupd
E
(
PPPPPPPPPPPPPPPPP
QQQQQQQQQQQQQQQQQQ
:
PROP
)
:
PPPPPPPPPPPPPPPPP
={
E
}=
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
.
PPPPPPPPPPPPPPPPP
={
E
}=
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
.
Proof
.
Proof
.
iStartProof
.
Show
.
iStartProof
.
Show
.
Abort
.
Abort
.
Lemma
long_fupd_maskchanging
E1
E2
(
PPPPPPPPPPPPPPPPP
QQQQQQQQQQQQQQQQQQ
:
PROP
)
:
Lemma
long_fupd_nested
E1
E2
(
PPPPPPPPPPPPPPPPP
QQQQQQQQQQQQQQQQQQ
:
PROP
)
:
PPPPPPPPPPPPPPPPP
={
E1
,
E2
}=
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
.
PPPPPPPPPPPPPPPPP
={
E1
,
E2
}=
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
={
E1
,
E2
}=
∗
QQQQQQQQQQQQQQQQQQ
∗
QQQQQQQQQQQQQQQQQQ
.
Proof
.
Proof
.
iStartProof
.
Show
.
iStartProof
.
Show
.
Abort
.
Abort
.
...
...
theories/bi/notation.v
View file @
ce9313df
...
@@ 12,7 +12,9 @@ Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
...
@@ 12,7 +12,9 @@ Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
Reserved
Notation
"'emp'"
.
Reserved
Notation
"'emp'"
.
Reserved
Notation
"'⌜' φ '⌝'"
(
at
level
1
,
φ
at
level
200
,
format
"⌜ φ ⌝"
).
Reserved
Notation
"'⌜' φ '⌝'"
(
at
level
1
,
φ
at
level
200
,
format
"⌜ φ ⌝"
).
Reserved
Notation
"P ∗ Q"
(
at
level
80
,
right
associativity
).
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 ⎤"
.
Reserved
Notation
"⎡ P ⎤"
.
...
@@ 51,34 +53,34 @@ Reserved Notation "'<subj>' P" (at level 20, right associativity).
...
@@ 51,34 +53,34 @@ 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
"==> Q"
(
at
level
99
,
Q
at
level
200
,
format
"==> Q"
).
Reserved
Notation
"P ==∗ 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"
Reserved
Notation
"={ E1 , E2 }=> Q"
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
format
"={ E1 , E2 }=> Q"
).
format
"={ E1 , E2 }=> Q"
).
Reserved
Notation
"P ={ E1 , E2 }=∗ Q"
Reserved
Notation
"P ={ E1 , E2 }=∗ Q"
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
(
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"
Reserved
Notation
"={ E }=> Q"
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
format
"={ E }=> Q"
).
format
"={ E }=> Q"
).
Reserved
Notation
"P ={ E }=∗ Q"
Reserved
Notation
"P ={ E }=∗ Q"
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
format
"'[
' P ={ E }=∗
'/'
Q ']'"
).
format
"'[' P
'/'
={ E }=∗ Q ']'"
).
Reserved
Notation
"={ E1 , E2 }▷=> Q"
Reserved
Notation
"={ E1 , E2 }▷=> Q"
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
format
"={ E1 , E2 }▷=> Q"
).
format
"={ E1 , E2 }▷=> Q"
).
Reserved
Notation
"P ={ E1 , E2 }▷=∗ Q"
Reserved
Notation
"P ={ E1 , E2 }▷=∗ Q"
(
at
level
99
,
E1
,
E2
at
level
50
,
Q
at
level
200
,
(
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"
Reserved
Notation
"={ E }▷=> Q"
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
format
"={ E }▷=> Q"
).
format
"={ E }▷=> Q"
).
Reserved
Notation
"P ={ E }▷=∗ Q"
Reserved
Notation
"P ={ E }▷=∗ Q"
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
(
at
level
99
,
E
at
level
50
,
Q
at
level
200
,
format
"'[
' P ={ E }▷=∗
'/'
Q ']'"
).
format
"'[' P
'/'
={ E }▷=∗ Q ']'"
).
(** Big Ops *)
(** Big Ops *)
Reserved
Notation
"'[∗' 'list]' k ↦ x ∈ l , P"
Reserved
Notation
"'[∗' 'list]' k ↦ x ∈ l , P"
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment