aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/v8-syntax/memo-v8.tex
blob: 8d116de26f449164dcf5135b74070d11b9d75b13 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286

\documentclass{article}

\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage{fullpage}

\author{B.~Barras}
\title{An introduction to syntax of Coq V8}

%% Le _ est un caractère normal
\catcode`\_=13
\let\subscr=_
\def_{\ifmmode\sb\else\subscr\fi}

\def\NT#1{\langle\textit{#1}\rangle}
\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}}
\def\TERM#1{\textsf{\bf #1}}

\newenvironment{transbox}
  {\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline}
  {\end{tabular}\end{center}}
\def\TRANS#1#2
  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} \\}
\def\TRANSCOM#1#2#3
  {\begin{tabular}[t]{@{}l@{}}#1\end{tabular} & 
   \begin{tabular}[t]{@{}l@{}}#2\end{tabular} & #3 \\}

\begin{document}

\maketitle

The goal of this document is to introduce by example to the new syntax of
Coq. It is strongly recommended to read first the definition of the new
syntax, but this document should also be useful for the eager user who wants
to start with the new syntax quickly.


\section{Changes in lexical conventions w.r.t. V7}

\subsection{Identifiers}

The lexical conventions changed: \TERM{_} is not a regular identifier
anymore. It is used in terms as a placeholder for subterms to be inferred
at type-checking, and in patterns as a non-binding variable.

Furthermore, only letters (unicode letters), digits, single quotes and
_ are allowed after the first character.

\subsection{Quoted string}

Quoted strings are used typically to give a filename (which may not
be a regular identifier). As before they are written between double
quotes ("). Unlike for V7, there is no escape character: characters
are written normaly but the double quote which is doubled.

\section{Main changes in terms w.r.t. V7}


\subsection{Precedence of application}

In the new syntax, parentheses are not really part of the syntax of
application. The precedence of application (10) is tighter than all
prefix and infix notations. It makes it possible to remove parentheses
in many contexts.

\begin{transbox}
\TRANS{(A x)->(f x)=(g y)}{A x -> f x = g y}
\TRANS{(f [x]x)}{f (fun x => x)}
\end{transbox}


\subsection{Arithmetics and scopes}

The specialized notation for \TERM{Z} and \TERM{R} (introduced by
symbols \TERM{`} and \TERM{``}) have disappeared. They have been
replaced by the general notion of scope.

\begin{center}
\begin{tabular}{l|l|l}
type & scope name & delimiter \\
\hline
types & type_scope & \TERM{T} \\
\TERM{bool} & bool_scope & \\
\TERM{nat} & nat_scope & \TERM{nat} \\
\TERM{Z} & Z_scope & \TERM{Z} \\
\TERM{R} & R_scope & \TERM{R} \\
\TERM{positive} & positive_scope & \TERM{P}
\end{tabular}
\end{center}

In order to use notations of arithmetics on \TERM{Z}, its scope must be opened with command \verb+Open Scope Z_scope.+ Another possibility is using the scope change notation (\TERM{\%}). The latter notation is to be used when notations of several scopes appear in the same expression.

In examples below, scope changes are not needed if the appropriate scope
has been opened. Scope nat_scope is opened in the initial state of Coq.
\begin{transbox}
\TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}}
\TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}}
\TRANSCOM{(0)}{0}{\textrm{nat_scope}}
\end{transbox}

Below is a table that tells which notation is available in which
scope. The relative precedences and associativity of operators is the
same as in usual mathematics. See the reference manual for more
details. However, it is important to remember that unlike V7, the type
operators for product and sum are left associative, in order not to
clash with arithmetic operators.

\begin{center}
\begin{tabular}{l|l}
scope & notations \\
\hline
nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\
Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\
R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq$ \\
type_scope & $* ~+$ \\
bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\
list_scope & $\TERM{::} ~\TERM{++}$
\end{tabular}
\end{center}
(Note: $\leq$ is written \TERM{$<=$})



\subsection{Notation for implicit arguments}

The explicitation of arguments is closer to the \emph{bindings} notation in
tactics. Argument positions follow the argument names of the head constant.

\begin{transbox}
\TRANS{f 1!t1 2!t2}{f (x:=t1) (y:=t2)}
\TRANS{!f t1 t2}{@f t1 t2}
\end{transbox}


\subsection{Universal quantification}

The universal quantification and dependent product types are now
materialized with the \TERM{forall} keyword before the binders and a
comma after the binders.

The syntax of binders also changed significantly. A binder can simply be
a name when its type can be inferred. In other cases, the name and the type
of the variable are put between parentheses. When several consecutive
variables have the same type, they can be grouped. Finally, if all variables
have the same type parentheses can be omitted.

\begin{transbox}
\TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B}
\TRANS{(x,y:nat)P}{forall (x y :~nat), P ~~\textrm{or}~~ forall x y :~nat, P}
\TRANS{(x,y:nat;z:A)P}{forall (x y :~nat) (z:A), P}
\TRANS{(x,y,z,t:?)P}{forall x y z t, P}
\TRANS{(x,y:nat;z:?)P}{forall (x y :~nat) z, P}
\end{transbox}

\subsection{Abstraction}

The notation for $\lambda$-abstraction follows that of universal
quantification. The binders are surrounded by keyword \TERM{fun}
and $\Rightarrow$ (\verb+=>+ in ascii).

\begin{transbox}
\TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c}
\end{transbox}


\subsection{Pattern-matching}

Beside the usage of the keyword pair \TERM{match}/\TERM{with} instead of
\TERM{Cases}/\TERM{of}, the main change is the notation for the type of
branches and return type. It is no longer written between \TERM{$<$ $>$} before
the \TERM{Cases} keyword, but interleaved with the destructured objects.

The idea is that for each destructured object, one may specify a variable
name to tell how the branches types depend on this destructured objects (case
of a dependent elimination), and also how they depend on the value of the
arguments of the inductive type of the destructured objects. The type of
branches is then given after the keyword \TERM{return}, unless it can be
inferred.

Moreover, when the destructured object is a variable, one may use this
variable in the return type.

\begin{transbox}
\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| (S k) => 1 end}
\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| .. end}
\TRANS{<[n:nat](P n)>Cases T of ... end}{match T as n return P n with ... end}
\TRANS{<[n:nat][p:(even n)]\~{}(odd n)>Cases p of\\~~ ... \\end}{match p in even n return \~{} odd n with\\~~ ...\\end}
\end{transbox}


\subsection{Fixpoints and cofixpoints}

An easier syntax for non-mutual fixpoints is provided, making it very close
to the usual notation for non-recursive functions. The decreasing argument
is now indicated by an annotation between curly braces, regardless of the
binders grouping. The annotation can be omitted if the binders introduce only
one variable. The type of the result can be omitted if inferable.

\begin{transbox}
\TRANS{Fix plus\{plus [n:nat] : nat -> nat :=\\~~ [m]...\}}{fix plus (n m:nat) \{struct n\}: nat := ...}
\TRANS{Fix fact\{fact [n:nat]: nat :=\\
~~Cases n of\\~~~~ O => (1) \\~~| (S k) => (mult n (fact k)) end\}}{fix fact
  (n:nat) :=\\
~~match n with \\~~~~0 => 1 \\~~| (S k) => n * fact k end}
\end{transbox}

There is a syntactic sugar for mutual fixpoints associated to a local
definition:

\begin{transbox}
\TRANS{let f := Fix f \{f [x:A] : T := M\} in\\(g (f y))}{let fix f (x:A) : T := M in\\g (f x)}
\end{transbox}

The same applies to cofixpoints, annotations are not allowed in that case.

\subsection{Notation for type cast}

\begin{transbox}
\TRANS{O :: nat}{0 : nat}
\end{transbox}

\section{Main changes in tactics w.r.t. V7}

The main change is that all tactic names are lowercase. This also holds for
Ltac keywords.

\subsection{Ltac}

Definitions of macros are introduced by \TERM{Ltac} instead of
\TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive
Definition}.

Rules of a match command are not between square brackets anymore.

Context (understand a term with a placeholder) instantiation \TERM{inst}
became \TERM{context}. Syntax is unified with subterm matching.

\begin{transbox}
\TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]}
\end{transbox}

\subsection{Named arguments of theorems}

\begin{transbox}
\TRANS{Apply thm with x:=t 1:=u}{apply thm with (x:=t) (1:=u)}
\end{transbox}


\subsection{Occurrences}

To avoid ambiguity between a numeric literal and the optionnal
occurence numbers of this term, the occurence numbers are put after
the term itself. This applies to tactic \TERM{pattern} and also
\TERM{unfold}
\begin{transbox}
\TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern (f x at 1 2) (d at 3 4) y z}
\end{transbox}

\section{Main changes in vernacular commands w.r.t. V7}


\subsection{Binders}

The binders of vernacular commands changed in the same way as those of
fixpoints. This also holds for parameters of inductive definitions.


\begin{transbox}
\TRANS{Definition x [a:A] : T := M}{Definition x (a:A) : T := M}
\TRANS{Inductive and [A,B:Prop]: Prop := \\~~conj : A->B->(and A B)}%
      {Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
\end{transbox}

\subsection{Hints}

The syntax of \emph{extern} hints changed: the pattern and the tactic
to be applied are separated by a \TERM{$\Rightarrow$}.
\begin{transbox}
\TRANS{Hint Extern 4 (toto ?) Apply lemma}{Hint Extern 4 (toto _) => apply lemma}
\end{transbox}

\end{document}