notation.v 7.49 KB
Newer Older
1
(** Just reserve the notation. *)
Ralf Jung's avatar
Ralf Jung committed
2

3
(** * Turnstiles *)
4
5
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).
6
Reserved Notation "(⊢)".
7
8
9
Reserved Notation "'(⊢@{' PROP } )".
Reserved Notation "( P ⊣⊢.)".
Reserved Notation "(.⊣⊢ Q )".
10

11
12
Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
13
Reserved Notation "(⊣⊢)".
14
15
16
Reserved Notation "'(⊣⊢@{' PROP } )".
Reserved Notation "(.⊢ Q )".
Reserved Notation "( P ⊢.)".
Ralf Jung's avatar
Ralf Jung committed
17

Gregory Malecha's avatar
Gregory Malecha committed
18
19
Reserved Notation "⊢ Q" (at level 20, Q at level 200).
Reserved Notation "'⊢@{' PROP } Q" (at level 20, Q at level 200).
20
21
22
23
24
25
26
27
28
29
30
31
(** 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. *)

Gregory Malecha's avatar
Gregory Malecha committed
32

33
(** * BI connectives *)
34
35
36
Reserved Notation "'emp'".
Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
37
38
39
Reserved Notation "P -∗ Q"
  (at level 99, Q at level 200, right associativity,
   format "'[' P  '/' -∗  Q ']'").
40

Ralf Jung's avatar
Ralf Jung committed
41
42
Reserved Notation "⎡ P ⎤".

Ralf Jung's avatar
Ralf Jung committed
43
(** Modalities *)
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
Reserved Notation "'<pers>' P" (at level 20, right associativity).
Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<pers>?' p  P").

Reserved Notation "▷ P" (at level 20, right associativity).
Reserved Notation "▷? p P" (at level 20, p at level 9, P at level 20,
   format "▷? p  P").
Reserved Notation "▷^ n P" (at level 20, n at level 9, P at level 20,
   format "▷^ n  P").

Reserved Infix "∗-∗" (at level 95, no associativity).

Reserved Notation "'<affine>' P" (at level 20, right associativity).
Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<affine>?' p  P").

Reserved Notation "'<absorb>' P" (at level 20, right associativity).
61
62
Reserved Notation "'<absorb>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<absorb>?' p  P").
63
64
65
66
67
68
69
70
71
72
73

Reserved Notation "□ P" (at level 20, right associativity).
Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'□?' p  P").

Reserved Notation "◇ P" (at level 20, right associativity).

Reserved Notation "■ P" (at level 20, right associativity).
Reserved Notation "■? p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "■? p  P").

Ralf Jung's avatar
Ralf Jung committed
74
75
76
Reserved Notation "'<obj>' P" (at level 20, right associativity).
Reserved Notation "'<subj>' P" (at level 20, right associativity).

77
(** * Update modalities *)
78
Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
79
Reserved Notation "P ==∗ Q"
80
  (at level 99, Q at level 200, format "'[' P  '/' ==∗  Q ']'").
81

Ralf Jung's avatar
Ralf Jung committed
82
83
84
85
86
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,
87
   format "'[' P  '/' ={ E1 , E2 }=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
88
89
90
91
92
93

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,
94
   format "'[' P  '/' ={ E }=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
95

Ralf Jung's avatar
Ralf Jung committed
96
(** Step-taking fancy updates *)
97
Reserved Notation "|={ E1 } [ E2 ]▷=> Q"
Ralf Jung's avatar
Ralf Jung committed
98
  (at level 99, E1, E2 at level 50, Q at level 200,
99
100
   format "|={ E1 } [ E2 ]▷=>  Q").
Reserved Notation "P ={ E1 } [ E2 ]▷=∗ Q"
Ralf Jung's avatar
Ralf Jung committed
101
  (at level 99, E1, E2 at level 50, Q at level 200,
102
   format "'[' P  '/' ={ E1 } [ E2 ]▷=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
103
104
105
106
107
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,
108
   format "'[' P  '/' ={ E }▷=∗  Q ']'").
109

Ralf Jung's avatar
Ralf Jung committed
110
(** Multi-step-taking fancy updates *)
111
Reserved Notation "|={ E1 } [ E2 ]▷=>^ n Q"
112
  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
113
114
   format "|={ E1 } [ E2 ]▷=>^ n  Q").
Reserved Notation "P ={ E1 } [ E2 ]▷=∗^ n Q"
115
  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
116
117
118
119
120
121
122
   format "P  ={ E1 } [ E2 ]▷=∗^ n  Q").
Reserved Notation "|={ E }▷=>^ n Q"
  (at level 99, E at level 50, n at level 9, Q at level 200,
   format "|={ E }▷=>^ n  Q").
Reserved Notation "P ={ E }▷=∗^ n Q"
  (at level 99, E at level 50, n at level 9, Q at level 200,
   format "P  ={ E }▷=∗^ n  Q").
Ralf Jung's avatar
Ralf Jung committed
123

124
(** * Big Ops *)
Ralf Jung's avatar
Ralf Jung committed
125
126
127
128
129
130
131
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").
Reserved Notation "'[∗' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[∗  list]  x  ∈  l ,  P").

132
133
134
135
136
137
138
Reserved Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P"
  (at level 200, l1, l2 at level 10, k, x1, x2 at level 1, right associativity,
   format "[∗  list]  k ↦ x1 ; x2  ∈  l1 ; l2 ,  P").
Reserved Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P"
  (at level 200, l1, l2 at level 10, x1, x2 at level 1, right associativity,
   format "[∗  list]  x1 ; x2  ∈  l1 ; l2 ,  P").

Ralf Jung's avatar
Ralf Jung committed
139
140
141
142
143
144
145
146
147
148
149
Reserved Notation "'[∗]' Ps" (at level 20).

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").
Reserved Notation "'[∧' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[∧  list]  x  ∈  l ,  P").

Reserved Notation "'[∧]' Ps" (at level 20).

150
151
152
153
154
155
156
157
158
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").
Reserved Notation "'[∨' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[∨  list]  x  ∈  l ,  P").

Reserved Notation "'[∨]' Ps" (at level 20).

Ralf Jung's avatar
Ralf Jung committed
159
160
161
162
163
164
165
Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
  (at level 200, m at level 10, k, x at level 1, right associativity,
   format "[∗  map]  k ↦ x  ∈  m ,  P").
Reserved Notation "'[∗' 'map]' x ∈ m , P"
  (at level 200, m at level 10, x at level 1, right associativity,
   format "[∗  map]  x  ∈  m ,  P").

Dan Frumin's avatar
Dan Frumin committed
166
167
168
169
170
171
172
Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
  (at level 200, m1, m2 at level 10, k, x1, x2 at level 1, right associativity,
   format "[∗  map]  k ↦ x1 ; x2  ∈  m1 ; m2 ,  P").
Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
  (at level 200, m1, m2 at level 10, x1, x2 at level 1, right associativity,
   format "[∗  map]  x1 ; x2  ∈  m1 ; m2 ,  P").

Ralf Jung's avatar
Ralf Jung committed
173
174
175
176
177
178
179
180
Reserved Notation "'[∗' 'set]' x ∈ X , P"
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  set]  x  ∈  X ,  P").

Reserved Notation "'[∗' 'mset]' x ∈ X , P"
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  mset]  x  ∈  X ,  P").

181
(** Define the scope *)
Ralf Jung's avatar
Ralf Jung committed
182
Declare Scope bi_scope.
183
Delimit Scope bi_scope with I.