1
\chapter{Proof handling}
5
In \Coq's proof editing mode all top-level commands documented in
6
chapter \ref{Vernacular-commands} remain available
7
and the user has access to specialized commands dealing with proof
8
development pragmas documented in this section. He can also use some
9
other specialized commands called {\em tactics}. They are the very
10
tools allowing the user to deal with logical reasoning. They are
11
documented in chapter \ref{Tactics}.\\
12
When switching in editing proof mode, the prompt
14
{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
15
declared name of the theorem currently edited.
17
At each stage of a proof development, one has a list of goals to
18
prove. Initially, the list consists only in the theorem itself. After
19
having applied some tactics, the list of goals contains the subgoals
20
generated by the tactics.
22
To each subgoal is associated a number of
23
hypotheses we call the {\em \index*{local context}} of the goal.
24
Initially, the local context is empty. It is enriched by the use of
25
certain tactics (see mainly section~\ref{intro}).
27
When a proof is achieved the message {\tt Proof completed} is
28
displayed. One can then store this proof as a defined constant in the
29
environment. Because there exists a correspondence between proofs and
30
terms of $\lambda$-calculus, known as the {\em Curry-Howard
31
isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
32
terms of {\sc Cic}. Those terms are called {\em proof
33
terms}\index{Proof term}.
35
It is possible to edit several proofs at the same time: see section
38
\ErrMsg When one attempts to use a proof editing command out of the
39
proof editing mode, \Coq~ raises the error message : \errindex{No focused
42
\section{Switching on/off the proof editing mode}
44
\subsection{\tt Goal {\form}.}
45
\comindex{Goal}\label{Goal}
46
This command switches \Coq~ to editing proof mode and sets {\form} as
47
the original goal. It associates the name {\tt Unnamed\_thm} to
51
\item \errindex{the term \form\ has type \ldots{} which should be Set,
53
%\item \errindex{Proof objects can only be abstracted}
54
%\item \errindex{A goal should be a type}
55
%\item \errindex{repeated goal not permitted in refining mode}
56
%the command {\tt Goal} cannot be used while a proof is already being edited.
59
\SeeAlso section \ref{Theorem}
61
\subsection{\tt Qed.}\comindex{Qed}\label{Qed}
62
This command is available in interactive editing proof mode when the
63
proof is completed. Then {\tt Qed} extracts a proof term from the
64
proof script, switches back to {\Coq} top-level and attaches the
65
extracted proof term to the declared name of the original goal. This
66
name is added to the environment as an {\tt Opaque} constant.
69
\item \errindex{Attempt to save an incomplete proof}
70
%\item \ident\ \errindex{already exists}\\
71
% The implicit name is already defined. You have then to provide
72
% explicitly a new name (see variant 3 below).
73
\item Sometimes an error occurs when building the proof term,
74
because tactics do not enforce completely the term construction
77
The user should also be aware of the fact that since the proof term is
78
completely rechecked at this point, one may have to wait a while when
79
the proof is large. In some exceptional cases one may even incur a
89
Defines the proved term as a transparent constant.
94
Is equivalent to {\tt Qed}.
96
\item {\tt Save {\ident}.}
98
Forces the name of the original goal to be {\ident}. This command
99
(and the following ones) can only be used if the original goal has
100
been opened using the {\tt Goal} command.
102
\item {\tt Save Theorem {\ident}.} \\
103
{\tt Save Lemma {\ident}.} \\
104
{\tt Save Remark {\ident}.}\\
105
{\tt Save Fact {\ident}.}
107
Are equivalent to {\tt Save {\ident}.}
110
\subsection{\tt Admitted.}\comindex{Admitted}\label{Admitted}
111
This command is available in interactive editing proof mode to give up
112
the current proof and declare the initial goal as an axiom.
114
\subsection{\tt Theorem {\ident} : {\form}.}
118
This command switches to interactive editing proof mode and declares
119
{\ident} as being the name of the original goal {\form}. When declared
120
as a {\tt Theorem}, the name {\ident} is known at all section levels:
121
{\tt Theorem} is a {\sl global} lemma.
123
%\ErrMsg (see section \ref{Goal})
127
\item \errindex{the term \form\ has type \ldots{} which should be Set,
130
\item \errindexbis{\ident already exists}{already exists}
132
The name you provided already defined. You have then to choose
140
\item {\tt Lemma {\ident} : {\form}.}
143
It is equivalent to {\tt Theorem {\ident} : {\form}.}
145
\item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
146
{\tt Fact {\ident} : {\form}.}\comindex{Fact}
148
Used to have a different meaning, but are now equivalent to {\tt
149
Theorem {\ident} : {\form}.} They are kept for compatibility.
151
\item {\tt Definition {\ident} : {\form}.}
152
\comindex{Definition}
154
Analogous to {\tt Theorem}, intended to be used in conjunction with
155
{\tt Defined} (see \ref{Defined}) in order to define a
156
transparent constant.
158
\item {\tt Let {\ident} : {\form}.}
161
Analogous to {\tt Definition} except that the definition is turned
162
into a local definition on objects depending on it after closing the
166
\subsection{\tt Proof {\term}.}
169
This command applies in proof editing mode. It is equivalent to {\tt
170
exact {\term}; Save.} That is, you have to give the full proof in
171
one gulp, as a proof term (see section \ref{exact}).
173
\variant {\tt Proof.}
175
Is a noop which is useful to delimit the sequence of tactic commands
176
which start a proof, after a {\tt Theorem} command. It is a good
177
practice to use {\tt Proof.} as an opening parenthesis, closed in
178
the script with a closing {\tt Qed.}
180
\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
182
\subsection{\tt Abort.}
185
This command cancels the current proof development, switching back to
186
the previous proof development, or to the \Coq\ toplevel if no other
190
\item \errindex{No focused proof (No proof-editing in progress)}
195
\item {\tt Abort {\ident}.}
197
Aborts the editing of the proof named {\ident}.
199
\item {\tt Abort All.}
201
Aborts all current goals, switching back to the \Coq\ toplevel.
205
\subsection{\tt Suspend.}
208
This command applies in proof editing mode. It switches back to the
209
\Coq\ toplevel, but without canceling the current proofs.
211
\subsection{\tt Resume.}
212
\comindex{Resume}\label{Resume}
214
This commands switches back to the editing of the last edited proof.
217
\item \errindex{No proof-editing in progress}
222
\item {\tt Resume {\ident}.}
224
Restarts the editing of the proof named {\ident}. This can be used
225
to navigate between currently edited proofs.
230
\item \errindex{No such proof}
233
\section{Navigation in the proof tree}
235
\subsection{\tt Undo.}
238
This command cancels the effect of the last tactic command. Thus, it
242
\item \errindex{No focused proof (No proof-editing in progress)}
243
\item \errindex{Undo stack would be exhausted}
248
\item {\tt Undo {\num}.}
250
Repeats {\tt Undo} {\num} times.
254
\subsection{\tt Set Undo {\num}.}
257
This command changes the maximum number of {\tt Undo}'s that will be
258
possible when doing a proof. It only affects proofs started after
259
this command, such that if you want to change the current undo limit
260
inside a proof, you should first restart this proof.
262
\subsection{\tt Unset Undo.}
263
\comindex{Unset Undo}
265
This command resets the default number of possible {\tt Undo} commands
266
(which is currently 12).
268
\subsection{\tt Restart.}\comindex{Restart}
269
This command restores the proof editing process to the original goal.
272
\item \errindex{No focused proof to restart}
275
\subsection{\tt Focus.}\comindex{Focus}
276
This focuses the attention on the first subgoal to prove and the printing
277
of the other subgoals is suspended until the focused subgoal is
278
solved or unfocused. This is useful when there are many current
279
subgoals which clutter your screen.
282
\item {\tt Focus {\num}.}\\
283
This focuses the attention on the $\num^{\scriptsize th}$ subgoal to prove.
287
\subsection{\tt Unfocus.}\comindex{Unfocus}
288
Turns off the focus mode.
291
\section{Displaying information}
293
\subsection{\tt Show.}\comindex{Show}\label{Show}
294
This command displays the current goals.
297
\item {\tt Show {\num}.}\\
298
Displays only the {\num}-th subgoal.\\
300
\item \errindex{No such goal}
301
\item \errindex{No focused proof}
304
\item {\tt Show Implicits.}\comindex{Show Implicits}\\
305
Displays the current goals, printing the implicit arguments of
308
\item {\tt Show Implicits {\num}.}\\
309
Same as above, only displaying the {\num}-th subgoal.
311
\item {\tt Show Script.}\comindex{Show Script}\\
312
Displays the whole list of tactics applied from the beginning
313
of the current proof.
314
This tactics script may contain some holes (subgoals not yet proved).
315
They are printed under the form \verb!<Your Tactic Text here>!.
317
\item {\tt Show Tree.}\comindex{Show Tree}\\
318
This command can be seen as a more structured way of
319
displaying the state of the proof than that
320
provided by {\tt Show Script}. Instead of just giving
321
the list of tactics that have been applied, it
322
shows the derivation tree constructed by then.
323
Each node of the tree contains the conclusion
324
of the corresponding sub-derivation (i.e. a
325
goal with its corresponding local context) and
326
the tactic that has generated all the
327
sub-derivations. The leaves of this tree are
328
the goals which still remain to be proved.
330
%\item {\tt Show Node}\comindex{Show Node}\\
333
\item {\tt Show Proof.}\comindex{Show Proof}\\
334
It displays the proof term generated by the
335
tactics that have been applied.
336
If the proof is not completed, this term contain holes,
337
which correspond to the sub-terms which are still to be
338
constructed. These holes appear as a question mark indexed
339
by an integer, and applied to the list of variables in
340
the context, since it may depend on them.
341
The types obtained by abstracting away the context from the
342
type of each hole-placer are also printed.
344
\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\
345
It prints the list of the names of all the theorems that
346
are currently being proved.
347
As it is possible to start proving a previous lemma during
348
the proof of a theorem, this list may contain several
351
\item{\tt Show Intro.}\comindex{Show Intro}\\
352
If the current goal begins by at least one product, this command
353
prints the name of the first product, as it would be generated by
354
an anonymous {\tt Intro}. The aim of this command is to ease the
355
writing of more robust scripts. For example, with an appropriate
356
Proof General macro, it is possible to transform any anonymous {\tt
357
Intro} into a qualified one such as {\tt Intro y13}.
358
In the case of a non-product goal, it prints nothing.
360
\item{\tt Show Intros.}\comindex{Show Intros}\\
361
This command is similar to the previous one, it simulates the naming
362
process of an {\tt Intros}.
366
\subsection{\tt Set Hyps Limit {\num}.}
367
\comindex{Set Hyps Limit}
368
This command sets the maximum number of hypotheses displayed in
369
goals after the application of a tactic.
370
All the hypotheses remains usable in the proof development.
372
\subsection{\tt Unset Hyps Limit.}
373
\comindex{Unset Hyps Limit}
374
This command goes back to the default mode which is to print all
375
available hypotheses.
377
\section{$DPL$ : A Declarative proof language for Coq \emph{(experimental)} }
379
An implementation of the $DPL$ declarative proof language by Pierre Corbineau at the Radboud University Nijmegen (The Netherlands) is included in Coq.
381
Due to the experimental nature and hence the potentially unstable semantics of the language, its documentation is not included here. However, it can be found at :
383
\url{http://www.cs.ru.nl/~corbineau/mmode.html}
388
% $Id: RefMan-pro.tex 9286 2006-10-26 17:43:00Z corbinea $
392
%%% TeX-master: "Reference-Manual"
added
removed
refman/RefMan-pro.tex
