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
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
|
\chapter{Proof handling}
\index{Proof editing}
\label{Proof-handling}
In \Coq's proof editing mode all top-level commands documented in
chapter \ref{Vernacular-commands} remain available
and the user has access to specialized commands dealing with proof
development pragmas documented in this section. He can also use some
other specialized commands called {\em tactics}. They are the very
tools allowing the user to deal with logical reasoning. They are
documented in chapter \ref{Tactics}.\\
When switching in editing proof mode, the prompt
\index{Prompt}
{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
declared name of the theorem currently edited.
At each stage of a proof development, one has a list of goals to
prove. Initially, the list consists only in the theorem itself. After
having applied some tactics, the list of goals contains the subgoals
generated by the tactics.
To each subgoal is associated a number of
hypotheses we call the {\em \index*{local context}} of the goal.
Initially, the local context is empty. It is enriched by the use of
certain tactics (see mainly section~\ref{intro}).
When a proof is achieved the message {\tt Proof completed} is
displayed. One can then store this proof as a defined constant in the
environment. Because there exists a correspondence between proofs and
terms of $\lambda$-calculus, known as the {\em Curry-Howard
isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
terms of {\sc Cic}. Those terms are called {\em proof
terms}\index{Proof term}.
It is possible to edit several proofs at the same time: see section
\ref{Resume}
\ErrMsg When one attempts to use a proof editing command out of the
proof editing mode, \Coq~ raises the error message : \errindex{No focused
proof}.
\section{Switching on/off the proof editing mode}
\subsection{\tt Goal {\form}.}
\comindex{Goal}\label{Goal}
This command switches \Coq~ to editing proof mode and sets {\form} as
the original goal. It associates the name {\tt Unnamed\_thm} to
that goal.
\begin{ErrMsgs}
\item \errindex{the term \form\ has type \ldots{} which should be Set,
Prop or Type}
%\item \errindex{Proof objects can only be abstracted}
%\item \errindex{A goal should be a type}
%\item \errindex{repeated goal not permitted in refining mode}
%the command {\tt Goal} cannot be used while a proof is already being edited.
\end{ErrMsgs}
\SeeAlso section \ref{Theorem}
\subsection{\tt Qed.}\comindex{Qed}\label{Qed}
This command is available in interactive editing proof mode when the
proof is completed. Then {\tt Qed} extracts a proof term from the
proof script, switches back to {\Coq} top-level and attaches the
extracted proof term to the declared name of the original goal. This
name is added to the environment as an {\tt Opaque} constant.
\begin{ErrMsgs}
\item \errindex{Attempt to save an incomplete proof}
%\item \ident\ \errindex{already exists}\\
% The implicit name is already defined. You have then to provide
% explicitly a new name (see variant 3 below).
\item Sometimes an error occurs when building the proof term,
because tactics do not enforce completely the term construction
constraints.
The user should also be aware of the fact that since the proof term is
completely rechecked at this point, one may have to wait a while when
the proof is large. In some exceptional cases one may even incur a
memory overflow.
\end{ErrMsgs}
\begin{Variants}
\item {\tt Defined.}
\comindex{Defined}
\label{Defined}
Defines the proved term as a transparent constant.
\item {\tt Save.}
\comindex{Save}
Is equivalent to {\tt Qed}.
\item {\tt Save {\ident}.}
Forces the name of the original goal to be {\ident}. This command
(and the following ones) can only be used if the original goal has
been opened using the {\tt Goal} command.
\item {\tt Save Theorem {\ident}.} \\
{\tt Save Lemma {\ident}.} \\
{\tt Save Remark {\ident}.}\\
{\tt Save Fact {\ident}.}
Are equivalent to {\tt Save {\ident}.}
\end{Variants}
\subsection{\tt Admitted.}\comindex{Admitted}\label{Admitted}
This command is available in interactive editing proof mode to give up
the current proof and declare the initial goal as an axiom.
\subsection{\tt Theorem {\ident} : {\form}.}
\comindex{Theorem}
\label{Theorem}
This command switches to interactive editing proof mode and declares
{\ident} as being the name of the original goal {\form}. When declared
as a {\tt Theorem}, the name {\ident} is known at all section levels:
{\tt Theorem} is a {\sl global} lemma.
%\ErrMsg (see section \ref{Goal})
\begin{ErrMsgs}
\item \errindex{the term \form\ has type \ldots{} which should be Set,
Prop or Type}
\item \errindexbis{\ident already exists}{already exists}
The name you provided already defined. You have then to choose
another name.
\end{ErrMsgs}
\begin{Variants}
\item {\tt Lemma {\ident} : {\form}.}
\comindex{Lemma}
It is equivalent to {\tt Theorem {\ident} : {\form}.}
\item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
{\tt Fact {\ident} : {\form}.}\comindex{Fact}
Used to have a different meaning, but are now equivalent to {\tt
Theorem {\ident} : {\form}.} They are kept for compatibility.
\item {\tt Definition {\ident} : {\form}.}
\comindex{Definition}
Analogous to {\tt Theorem}, intended to be used in conjunction with
{\tt Defined} (see \ref{Defined}) in order to define a
transparent constant.
\item {\tt Local {\ident} : {\form}.}
\comindex{Local}
Analogous to {\tt Definition} except that the definition is turned
into a local definition on objects depending on it after closing the
current section.
\end{Variants}
\subsection{\tt Proof {\term}.}\comindex{Proof}
This command applies in proof editing mode. It is equivalent to {\tt
exact {\term}; Save.} That is, you have to give the full proof in
one gulp, as a proof term (see section \ref{exact}).
\begin{Variants}
\item{\tt Proof.}
Is a noop which is useful to delimit the sequence of tactic commands
which start a proof, after a {\tt Theorem} command. It is a good
practice to use {\tt Proof.} as an opening parenthesis, closed in
the script with a closing {\tt Qed.}
\item{\tt Proof with {\tac}.}
This command may be used to start a proof. It defines a default
tactic to be used each time a tactic command is ended by
``\verb#...#''. In this case the tactic command typed by the user is
equivalent to \emph{command};{\tac}.
\end{Variants}
\subsection{\tt Abort.}
\comindex{Abort}
This command cancels the current proof development, switching back to
the previous proof development, or to the \Coq\ toplevel if no other
proof was edited.
\begin{ErrMsgs}
\item \errindex{No focused proof (No proof-editing in progress)}
\end{ErrMsgs}
\begin{Variants}
\item {\tt Abort {\ident}.}
Aborts the editing of the proof named {\ident}.
\item {\tt Abort All.}
Aborts all current goals, switching back to the \Coq\ toplevel.
\end{Variants}
\subsection{\tt Suspend.}
\comindex{Suspend}
This command applies in proof editing mode. It switches back to the
\Coq\ toplevel, but without canceling the current proofs.
\subsection{\tt Resume.}
\comindex{Resume}\label{Resume}
This commands switches back to the editing of the last edited proof.
\begin{ErrMsgs}
\item \errindex{No proof-editing in progress}
\end{ErrMsgs}
\begin{Variants}
\item {\tt Resume {\ident}.}
Restarts the editing of the proof named {\ident}. This can be used
to navigate between currently edited proofs.
\end{Variants}
\begin{ErrMsgs}
\item \errindex{No such proof}
\end{ErrMsgs}
\section{Navigation in the proof tree}
\subsection{\tt Undo.}
\comindex{Undo}
This command cancels the effect of the last tactic command. Thus, it
backtracks one step.
\begin{ErrMsgs}
\item \errindex{No focused proof (No proof-editing in progress)}
\item \errindex{Undo stack would be exhausted}
\end{ErrMsgs}
\begin{Variants}
\item {\tt Undo {\num}.}
Repeats {\tt Undo} {\num} times.
\end{Variants}
\subsection{\tt Set Undo {\num}.}
\comindex{Set Undo}
This command changes the maximum number of {\tt Undo}'s that will be
possible when doing a proof. It only affects proofs started after
this command, such that if you want to change the current undo limit
inside a proof, you should first restart this proof.
\subsection{\tt Unset Undo.}
\comindex{Unset Undo}
This command resets the default number of possible {\tt Undo} commands
(which is currently 12).
\subsection{\tt Restart.}\comindex{Restart}
This command restores the proof editing process to the original goal.
\begin{ErrMsgs}
\item \errindex{No focused proof to restart}
\end{ErrMsgs}
\subsection{\tt Focus.}\comindex{Focus}
Will focus the attention on the first subgoal to prove, the remaining
subgoals will no more be printed after the application of a tactic.
This is useful when there are many current subgoals which clutter your
screen.
\subsection{\tt Unfocus.}\comindex{Unfocus}
Turns off the focus mode.
\section{Displaying information}
\subsection{\tt Show.}\comindex{Show}\label{Show}
This command displays the current goals.
\begin{Variants}
\item {\tt Show {\num}.}\\
Displays only the {\num}-th subgoal.\\
\begin{ErrMsgs}
\item \errindex{No such goal}
\item \errindex{No focused proof}
\end{ErrMsgs}
\item {\tt Show Implicits.}\comindex{Show Implicits}\\
Displays the current goals, printing the implicit arguments of
constants.
\item {\tt Show Implicits {\num}.}\\
Same as above, only displaying the {\num}-th subgoal.
\item {\tt Show Script.}\comindex{Show Script}\\
Displays the whole list of tactics applied from the beginning
of the current proof.
This tactics script may contain some holes (subgoals not yet proved).
They are printed under the form \verb!<Your Tactic Text here>!.
\item {\tt Show Tree.}\comindex{Show Tree}\\
This command can be seen as a more structured way of
displaying the state of the proof than that
provided by {\tt Show Script}. Instead of just giving
the list of tactics that have been applied, it
shows the derivation tree constructed by then.
Each node of the tree contains the conclusion
of the corresponding sub-derivation (i.e. a
goal with its corresponding local context) and
the tactic that has generated all the
sub-derivations. The leaves of this tree are
the goals which still remain to be proved.
%\item {\tt Show Node}\comindex{Show Node}\\
% Not yet documented
\item {\tt Show Proof.}\comindex{Show Proof}\\
It displays the proof term generated by the
tactics that have been applied.
If the proof is not completed, this term contain holes,
which correspond to the sub-terms which are still to be
constructed. These holes appear as a question mark indexed
by an integer, and applied to the list of variables in
the context, since it may depend on them.
The types obtained by abstracting away the context from the
type of each hole-placer are also printed.
\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\
It prints the list of the names of all the theorems that
are currently being proved.
As it is possible to start proving a previous lemma during
the proof of a theorem, this list may contain several
names.
\item{\tt Show Intro.}\comindex{Show Intro}\\
If the current goal begins by at least one product, this command
prints the name of the first product, as it would be generated by
an anonymous {\tt Intro}. The aim of this command is to ease the
writing of more robust scripts. For example, with an appropriate
Proof General macro, it is possible to transform any anonymous {\tt
Intro} into a qualified one such as {\tt Intro y13}.
In the case of a non-product goal, it prints nothing.
\item{\tt Show Intros.}\comindex{Show Intros}\\
This command is similar to the previous one, it simulates the naming
process of an {\tt Intros}.
\end{Variants}
\subsection{\tt Set Hyps Limit {\num}.}
\comindex{Set Hyps Limit}
This command sets the maximum number of hypotheses displayed in
goals after the application of a tactic.
All the hypotheses remains usable in the proof development.
\subsection{\tt Unset Hyps Limit.}
\comindex{Unset Hyps Limit}
This command goes back to the default mode which is to print all
available hypotheses.
% $Id$
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|