1
\chapter[Proof handling]{Proof handling\index{Proof editing}
2
\label{Proof-handling}}
4
In \Coq's proof editing mode all top-level commands documented in
5
Chapter~\ref{Vernacular-commands} remain available
6
and the user has access to specialized commands dealing with proof
7
development pragmas documented in this section. He can also use some
8
other specialized commands called {\em tactics}. They are the very
9
tools allowing the user to deal with logical reasoning. They are
10
documented in Chapter~\ref{Tactics}.\\
11
When switching in editing proof mode, the prompt
13
{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
14
declared name of the theorem currently edited.
16
At each stage of a proof development, one has a list of goals to
17
prove. Initially, the list consists only in the theorem itself. After
18
having applied some tactics, the list of goals contains the subgoals
19
generated by the tactics.
21
To each subgoal is associated a number of
22
hypotheses we call the {\em \index*{local context}} of the goal.
23
Initially, the local context is empty. It is enriched by the use of
24
certain tactics (see mainly Section~\ref{intro}).
26
When a proof is achieved the message {\tt Proof completed} is
27
displayed. One can then store this proof as a defined constant in the
28
environment. Because there exists a correspondence between proofs and
29
terms of $\lambda$-calculus, known as the {\em Curry-Howard
30
isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
31
terms of {\sc Cic}. Those terms are called {\em proof
32
terms}\index{Proof term}.
34
It is possible to edit several proofs at the same time: see section
37
\ErrMsg When one attempts to use a proof editing command out of the
38
proof editing mode, \Coq~ raises the error message : \errindex{No focused
41
\section{Switching on/off the proof editing mode}
43
\subsection[\tt Goal {\form}.]{\tt Goal {\form}.\comindex{Goal}\label{Goal}}
44
This command switches \Coq~ to editing proof mode and sets {\form} as
45
the original goal. It associates the name {\tt Unnamed\_thm} to
49
\item \errindex{the term \form\ has type \ldots{} which should be Set,
51
%\item \errindex{Proof objects can only be abstracted}
52
%\item \errindex{A goal should be a type}
53
%\item \errindex{repeated goal not permitted in refining mode}
54
%the command {\tt Goal} cannot be used while a proof is already being edited.
57
\SeeAlso Section~\ref{Theorem}
59
\subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}}
60
This command is available in interactive editing proof mode when the
61
proof is completed. Then {\tt Qed} extracts a proof term from the
62
proof script, switches back to {\Coq} top-level and attaches the
63
extracted proof term to the declared name of the original goal. This
64
name is added to the environment as an {\tt Opaque} constant.
67
\item \errindex{Attempt to save an incomplete proof}
68
%\item \ident\ \errindex{already exists}\\
69
% The implicit name is already defined. You have then to provide
70
% explicitly a new name (see variant 3 below).
71
\item Sometimes an error occurs when building the proof term,
72
because tactics do not enforce completely the term construction
75
The user should also be aware of the fact that since the proof term is
76
completely rechecked at this point, one may have to wait a while when
77
the proof is large. In some exceptional cases one may even incur a
87
Defines the proved term as a transparent constant.
92
Is equivalent to {\tt Qed}.
94
\item {\tt Save {\ident}.}
96
Forces the name of the original goal to be {\ident}. This command
97
(and the following ones) can only be used if the original goal has
98
been opened using the {\tt Goal} command.
100
\item {\tt Save Theorem {\ident}.} \\
101
{\tt Save Lemma {\ident}.} \\
102
{\tt Save Remark {\ident}.}\\
103
{\tt Save Fact {\ident}.}
105
Are equivalent to {\tt Save {\ident}.}
108
\subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}}
109
This command is available in interactive editing proof mode to give up
110
the current proof and declare the initial goal as an axiom.
112
\subsection[\tt Theorem {\ident} : {\form}.]{\tt Theorem {\ident} : {\form}.\comindex{Theorem}
115
This command switches to interactive editing proof mode and declares
116
{\ident} as being the name of the original goal {\form}. When declared
117
as a {\tt Theorem}, the name {\ident} is known at all section levels:
118
{\tt Theorem} is a {\sl global} lemma.
120
%\ErrMsg (see Section~\ref{Goal})
124
\item \errindex{the term \form\ has type \ldots{} which should be Set,
127
\item \errindexbis{\ident already exists}{already exists}
129
The name you provided already defined. You have then to choose
137
\item {\tt Lemma {\ident} : {\form}.}
140
It is equivalent to {\tt Theorem {\ident} : {\form}.}
142
\item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\
143
{\tt Fact {\ident} : {\form}.}\comindex{Fact}
145
Used to have a different meaning, but are now equivalent to {\tt
146
Theorem {\ident} : {\form}.} They are kept for compatibility.
148
\item {\tt Definition {\ident} : {\form}.}
149
\comindex{Definition}
151
Analogous to {\tt Theorem}, intended to be used in conjunction with
152
{\tt Defined} (see \ref{Defined}) in order to define a
153
transparent constant.
155
\item {\tt Let {\ident} : {\form}.}
158
Analogous to {\tt Definition} except that the definition is turned
159
into a local definition on objects depending on it after closing the
163
\subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof}
165
This command applies in proof editing mode. It is equivalent to {\tt
166
exact {\term}; Save.} That is, you have to give the full proof in
167
one gulp, as a proof term (see Section~\ref{exact}).
169
\variant {\tt Proof.}
171
Is a noop which is useful to delimit the sequence of tactic commands
172
which start a proof, after a {\tt Theorem} command. It is a good
173
practice to use {\tt Proof.} as an opening parenthesis, closed in
174
the script with a closing {\tt Qed.}
176
\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
178
\subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
180
This command cancels the current proof development, switching back to
181
the previous proof development, or to the \Coq\ toplevel if no other
185
\item \errindex{No focused proof (No proof-editing in progress)}
190
\item {\tt Abort {\ident}.}
192
Aborts the editing of the proof named {\ident}.
194
\item {\tt Abort All.}
196
Aborts all current goals, switching back to the \Coq\ toplevel.
201
\subsection[\tt Suspend.]{\tt Suspend.\comindex{Suspend}}
203
This command applies in proof editing mode. It switches back to the
204
\Coq\ toplevel, but without canceling the current proofs.
207
\subsection[\tt Resume.]{\tt Resume.\comindex{Resume}\label{Resume}}
209
This commands switches back to the editing of the last edited proof.
212
\item \errindex{No proof-editing in progress}
217
\item {\tt Resume {\ident}.}
219
Restarts the editing of the proof named {\ident}. This can be used
220
to navigate between currently edited proofs.
225
\item \errindex{No such proof}
230
\subsection[\tt Existential {\num} := {\term}.]{\tt Existential {\num} := {\term}.\comindex{Existential}
233
This command allows to instantiate an existential variable. {\tt \num}
234
is an index in the list of uninstantiated existential variables
235
displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
237
This command is intented to be used to instantiate existential
238
variables when the proof is completed but some uninstantiated
239
existential variables remain. To instantiate existential variables
240
during proof edition, you should use the tactic {\tt instantiate}.
242
\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}.
246
\section{Navigation in the proof tree}
249
\subsection[\tt Undo.]{\tt Undo.\comindex{Undo}}
251
This command cancels the effect of the last tactic command. Thus, it
255
\item \errindex{No focused proof (No proof-editing in progress)}
256
\item \errindex{Undo stack would be exhausted}
261
\item {\tt Undo {\num}.}
263
Repeats {\tt Undo} {\num} times.
267
\subsection[\tt Set Undo {\num}.]{\tt Set Undo {\num}.\comindex{Set Undo}}
269
This command changes the maximum number of {\tt Undo}'s that will be
270
possible when doing a proof. It only affects proofs started after
271
this command, such that if you want to change the current undo limit
272
inside a proof, you should first restart this proof.
274
\subsection[\tt Unset Undo.]{\tt Unset Undo.\comindex{Unset Undo}}
276
This command resets the default number of possible {\tt Undo} commands
277
(which is currently 12).
279
\subsection[\tt Restart.]{\tt Restart.\comindex{Restart}}
280
This command restores the proof editing process to the original goal.
283
\item \errindex{No focused proof to restart}
286
\subsection[\tt Focus.]{\tt Focus.\comindex{Focus}}
287
This focuses the attention on the first subgoal to prove and the printing
288
of the other subgoals is suspended until the focused subgoal is
289
solved or unfocused. This is useful when there are many current
290
subgoals which clutter your screen.
293
\item {\tt Focus {\num}.}\\
294
This focuses the attention on the $\num^{th}$ subgoal to prove.
298
\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
299
Turns off the focus mode.
302
\section{Requesting information}
304
\subsection[\tt Show.]{\tt Show.\comindex{Show}\label{Show}}
305
This command displays the current goals.
308
\item {\tt Show {\num}.}\\
309
Displays only the {\num}-th subgoal.\\
311
\item \errindex{No such goal}
312
\item \errindex{No focused proof}
315
\item {\tt Show Implicits.}\comindex{Show Implicits}\\
316
Displays the current goals, printing the implicit arguments of
319
\item {\tt Show Implicits {\num}.}\\
320
Same as above, only displaying the {\num}-th subgoal.
322
\item {\tt Show Script.}\comindex{Show Script}\\
323
Displays the whole list of tactics applied from the beginning
324
of the current proof.
325
This tactics script may contain some holes (subgoals not yet proved).
326
They are printed under the form \verb!<Your Tactic Text here>!.
328
\item {\tt Show Tree.}\comindex{Show Tree}\\
329
This command can be seen as a more structured way of
330
displaying the state of the proof than that
331
provided by {\tt Show Script}. Instead of just giving
332
the list of tactics that have been applied, it
333
shows the derivation tree constructed by then.
334
Each node of the tree contains the conclusion
335
of the corresponding sub-derivation (i.e. a
336
goal with its corresponding local context) and
337
the tactic that has generated all the
338
sub-derivations. The leaves of this tree are
339
the goals which still remain to be proved.
341
%\item {\tt Show Node}\comindex{Show Node}\\
344
\item {\tt Show Proof.}\comindex{Show Proof}\\
345
It displays the proof term generated by the
346
tactics that have been applied.
347
If the proof is not completed, this term contain holes,
348
which correspond to the sub-terms which are still to be
349
constructed. These holes appear as a question mark indexed
350
by an integer, and applied to the list of variables in
351
the context, since it may depend on them.
352
The types obtained by abstracting away the context from the
353
type of each hole-placer are also printed.
355
\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\
356
It prints the list of the names of all the theorems that
357
are currently being proved.
358
As it is possible to start proving a previous lemma during
359
the proof of a theorem, this list may contain several
362
\item{\tt Show Intro.}\comindex{Show Intro}\\
363
If the current goal begins by at least one product, this command
364
prints the name of the first product, as it would be generated by
365
an anonymous {\tt Intro}. The aim of this command is to ease the
366
writing of more robust scripts. For example, with an appropriate
367
Proof General macro, it is possible to transform any anonymous {\tt
368
Intro} into a qualified one such as {\tt Intro y13}.
369
In the case of a non-product goal, it prints nothing.
371
\item{\tt Show Intros.}\comindex{Show Intros}\\
372
This command is similar to the previous one, it simulates the naming
373
process of an {\tt Intros}.
375
\item{\tt Show Existentials}\comindex{Show Existentials}\\ It displays
376
the set of all uninstantiated existential variables in the current proof tree,
377
along with the type and the context of each variable.
382
\subsection[\tt Guarded.]{\tt Guarded.\comindex{Guarded}\label{Guarded}}
384
Some tactics (e.g. refine \ref{refine}) allow to build proofs using
385
fixpoint or co-fixpoint constructions. Due to the incremental nature
386
of interactive proof construction, the check of the termination (or
387
guardedness) of the recursive calls in the fixpoint or cofixpoint
388
constructions is postponed to the time of the completion of the proof.
390
The command \verb!Guarded! allows to verify if the guard condition for
391
fixpoint and cofixpoint is violated at some time of the construction
392
of the proof without having to wait the completion of the proof."
395
\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\comindex{Set Hyps Limit}}
396
This command sets the maximum number of hypotheses displayed in
397
goals after the application of a tactic.
398
All the hypotheses remains usable in the proof development.
401
\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\comindex{Unset Hyps Limit}}
402
This command goes back to the default mode which is to print all
403
available hypotheses.
405
% $Id: RefMan-pro.tex 10479 2008-01-29 16:51:14Z corbinea $
409
%%% TeX-master: "Reference-Manual"
added
removed
doc/refman/RefMan-pro.tex
