1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
2
"http://www.w3.org/TR/REC-html40/loose.dtd">
6
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
7
<META name="GENERATOR" content="hevea 1.07">
13
<A HREF="Reference-Manual008.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
14
<A HREF="toc.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
15
<A HREF="Reference-Manual010.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
18
<H1><A NAME="htoc153">Chapter 7</A> Proof handling</H1>
19
<A NAME="@default382"></A>
20
<A NAME="Proof-handling"></A>
21
In <FONT COLOR=navy>Coq</FONT>'s proof editing mode all top-level commands documented in
22
chapter <A HREF="Reference-Manual008.html#Vernacular-commands">6</A> remain available
23
and the user has access to specialized commands dealing with proof
24
development pragmas documented in this section. He can also use some
25
other specialized commands called <EM>tactics</EM>. They are the very
26
tools allowing the user to deal with logical reasoning. They are
27
documented in chapter <A HREF="Reference-Manual010.html#Tactics">8</A>.<BR>
28
When switching in editing proof mode, the prompt
29
<A NAME="@default383"></A>
30
<TT>Coq <</TT> is changed into <TT></TT><I><FONT COLOR=maroon>ident</FONT></I><TT> <</TT> where <I><FONT COLOR=maroon>ident</FONT></I> is the
31
declared name of the theorem currently edited.<BR>
33
At each stage of a proof development, one has a list of goals to
34
prove. Initially, the list consists only in the theorem itself. After
35
having applied some tactics, the list of goals contains the subgoals
36
generated by the tactics.<BR>
38
To each subgoal is associated a number of
39
hypotheses we call the <A NAME="@default384"><EM>local context</EM></A> of the goal.
40
Initially, the local context is empty. It is enriched by the use of
41
certain tactics (see mainly section <A HREF="Reference-Manual010.html#intro">8.3.5</A>).<BR>
43
When a proof is achieved the message <TT>Proof completed</TT> is
44
displayed. One can then store this proof as a defined constant in the
45
environment. Because there exists a correspondence between proofs and
46
terms of lambda-calculus, known as the <EM>Curry-Howard
47
isomorphism</EM> [<A HREF="biblio.html#How80"><CITE>68</CITE></A><CITE>, </CITE><A HREF="biblio.html#Bar91"><CITE>6</CITE></A><CITE>, </CITE><A HREF="biblio.html#Gir89"><CITE>64</CITE></A><CITE>, </CITE><A HREF="biblio.html#Hue89"><CITE>71</CITE></A>], <FONT COLOR=navy>Coq</FONT> stores proofs as
48
terms of <FONT COLOR=navy>Cic</FONT>. Those terms are called <EM>proof
49
terms</EM><A NAME="@default385"></A>.<BR>
51
It is possible to edit several proofs at the same time: see section
52
<A HREF="#Resume">7.1.8</A><BR>
55
<B>Error message: </B>When one attempts to use a proof editing command out of the
56
proof editing mode, <FONT COLOR=navy>Coq</FONT> raises the error message : <TT>No focused
57
proof</TT><A NAME="@error31"></A>.<BR>
60
<H2><A NAME="htoc154">7.1</A> Switching on/off the proof editing mode</H2>
62
<H3><A NAME="htoc155">7.1.1</A> <TT>Goal </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT></H3>
63
<A NAME="@default386"></A><A NAME="@command117"></A><A NAME="Goal"></A>
64
This command switches <FONT COLOR=navy>Coq</FONT> to editing proof mode and sets <I><FONT COLOR=maroon>form</FONT></I> as
65
the original goal. It associates the name <TT>Unnamed_thm</TT> to
69
<B>Error messages: </B><OL type=1><LI>
70
<TT>the term </TT><I><FONT COLOR=maroon>form</FONT></I><TT> has type ... which should be Set,
71
Prop or Type</TT><A NAME="@error32"></A>
74
<B>See also: </B>section <A HREF="#Theorem">7.1.4</A><BR>
77
<H3><A NAME="htoc156">7.1.2</A> <TT>Qed.</TT></H3><A NAME="@default387"></A><A NAME="@command118"></A><A NAME="Qed"></A>
78
This command is available in interactive editing proof mode when the
79
proof is completed. Then <TT>Qed</TT> extracts a proof term from the
80
proof script, switches back to <FONT COLOR=navy>Coq</FONT> top-level and attaches the
81
extracted proof term to the declared name of the original goal. This
82
name is added to the environment as an <TT>Opaque</TT> constant.<BR>
85
<B>Error messages: </B><OL type=1><LI>
86
<TT>Attempt to save an incomplete proof</TT><A NAME="@error33"></A>
87
<LI>Sometimes an error occurs when building the proof term,
88
because tactics do not enforce completely the term construction
91
The user should also be aware of the fact that since the proof term is
92
completely rechecked at this point, one may have to wait a while when
93
the proof is large. In some exceptional cases one may even incur a
97
<B>Variants: </B><OL type=1><LI><TT>Defined.</TT>
98
<A NAME="@default388"></A><A NAME="@command119"></A>
99
<A NAME="Defined"></A> <BR>
101
Defines the proved term as a transparent constant.<BR>
104
<A NAME="@default389"></A><A NAME="@command120"></A><BR>
106
Is equivalent to <TT>Qed</TT>.<BR>
108
<LI><TT>Save </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
110
Forces the name of the original goal to be <I><FONT COLOR=maroon>ident</FONT></I>. This command
111
(and the following ones) can only be used if the original goal has
112
been opened using the <TT>Goal</TT> command.<BR>
114
<LI><TT>Save Theorem </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
115
<TT>Save Lemma </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
116
<TT>Save Remark </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
117
<TT>Save Fact </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
119
Are equivalent to <TT>Save </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT>
122
<H3><A NAME="htoc157">7.1.3</A> <TT>Admitted.</TT></H3><A NAME="@default390"></A><A NAME="@command121"></A><A NAME="Admitted"></A>
123
This command is available in interactive editing proof mode to give up
124
the current proof and declare the initial goal as an axiom.<BR>
127
<H3><A NAME="htoc158">7.1.4</A> <TT>Theorem </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT></H3>
128
<A NAME="@default391"></A><A NAME="@command122"></A>
129
<A NAME="Theorem"></A>
130
This command switches to interactive editing proof mode and declares
131
<I><FONT COLOR=maroon>ident</FONT></I> as being the name of the original goal <I><FONT COLOR=maroon>form</FONT></I>. When declared
132
as a <TT>Theorem</TT>, the name <I><FONT COLOR=maroon>ident</FONT></I> is known at all section levels:
133
<TT>Theorem</TT> is a <I><FONT COLOR=maroon>global</FONT></I> lemma.<BR>
136
<B>Error messages: </B><OL type=1><LI><TT>the term </TT><I><FONT COLOR=maroon>form</FONT></I><TT> has type ... which should be Set,
137
Prop or Type</TT><A NAME="@error34"></A><BR>
139
<LI><TT></TT><I><FONT COLOR=maroon>ident</FONT></I><TT>already exists</TT><A NAME="@error35"></A><BR>
141
The name you provided already defined. You have then to choose
144
<B>Variants: </B><OL type=1><LI><TT>Lemma </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT>
145
<A NAME="@default392"></A><A NAME="@command123"></A><BR>
147
It is equivalent to <TT>Theorem </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT><BR>
149
<LI><TT>Remark </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT><A NAME="@default393"></A><A NAME="@command124"></A><BR>
150
<TT>Fact </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT><A NAME="@default394"></A><A NAME="@command125"></A><BR>
152
Used to have a different meaning, but are now equivalent to <TT>Theorem </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT> They are kept for compatibility.<BR>
154
<LI><TT>Definition </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT>
155
<A NAME="@default395"></A><A NAME="@command126"></A><BR>
157
Analogous to <TT>Theorem</TT>, intended to be used in conjunction with
158
<TT>Defined</TT> (see <A HREF="#Defined">1</A>) in order to define a
159
transparent constant.<BR>
161
<LI><TT>Local </TT><I><FONT COLOR=maroon>ident</FONT></I><TT> : </TT><I><FONT COLOR=maroon>form</FONT></I><TT>.</TT>
162
<A NAME="@default396"></A><A NAME="@command127"></A><BR>
164
Analogous to <TT>Definition</TT> except that the definition is turned
165
into a local definition on objects depending on it after closing the
169
<H3><A NAME="htoc159">7.1.5</A> <TT>Proof </TT><I><FONT COLOR=maroon>term</FONT></I><TT>.</TT></H3><A NAME="@default397"></A><A NAME="@command128"></A>
170
This command applies in proof editing mode. It is equivalent to <TT>exact </TT><I><FONT COLOR=maroon>term</FONT></I><TT>; Save.</TT> That is, you have to give the full proof in
171
one gulp, as a proof term (see section <A HREF="Reference-Manual010.html#exact">8.2.1</A>).<BR>
174
<B>Variants: </B><OL type=1><LI><TT>Proof.</TT><BR>
176
Is a noop which is useful to delimit the sequence of tactic commands
177
which start a proof, after a <TT>Theorem</TT> command. It is a good
178
practice to use <TT>Proof.</TT> as an opening parenthesis, closed in
179
the script with a closing <TT>Qed.</TT><BR>
181
<LI><TT>Proof with </TT><I><FONT COLOR=maroon>tactic</FONT></I><TT>.</TT><BR>
183
This command may be used to start a proof. It defines a default
184
tactic to be used each time a tactic command is ended by
185
``<CODE>...</CODE>''. In this case the tactic command typed by the user is
186
equivalent to <EM>command</EM>;<I><FONT COLOR=maroon>tactic</FONT></I>.</OL>
188
<H3><A NAME="htoc160">7.1.6</A> <TT>Abort.</TT></H3>
189
<A NAME="@default398"></A><A NAME="@command129"></A>
190
This command cancels the current proof development, switching back to
191
the previous proof development, or to the <FONT COLOR=navy>Coq</FONT> toplevel if no other
192
proof was edited.<BR>
195
<B>Error messages: </B><OL type=1><LI>
196
<TT>No focused proof (No proof-editing in progress)</TT><A NAME="@error36"></A>
199
<B>Variants: </B><OL type=1><LI><TT>Abort </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
201
Aborts the editing of the proof named <I><FONT COLOR=maroon>ident</FONT></I>.<BR>
203
<LI><TT>Abort All.</TT><BR>
205
Aborts all current goals, switching back to the <FONT COLOR=navy>Coq</FONT> toplevel.</OL>
207
<H3><A NAME="htoc161">7.1.7</A> <TT>Suspend.</TT></H3>
208
<A NAME="@default399"></A><A NAME="@command130"></A>
209
This command applies in proof editing mode. It switches back to the
210
<FONT COLOR=navy>Coq</FONT> toplevel, but without canceling the current proofs.<BR>
213
<H3><A NAME="htoc162">7.1.8</A> <TT>Resume.</TT></H3>
214
<A NAME="@default400"></A><A NAME="@command131"></A><A NAME="Resume"></A>
215
This commands switches back to the editing of the last edited proof.<BR>
218
<B>Error messages: </B><OL type=1><LI>
219
<TT>No proof-editing in progress</TT><A NAME="@error37"></A>
222
<B>Variants: </B><OL type=1><LI><TT>Resume </TT><I><FONT COLOR=maroon>ident</FONT></I><TT>.</TT><BR>
224
Restarts the editing of the proof named <I><FONT COLOR=maroon>ident</FONT></I>. This can be used
225
to navigate between currently edited proofs.</OL>
227
<B>Error messages: </B><OL type=1><LI>
228
<TT>No such proof</TT><A NAME="@error38"></A>
231
<H2><A NAME="htoc163">7.2</A> Navigation in the proof tree</H2>
233
<H3><A NAME="htoc164">7.2.1</A> <TT>Undo.</TT></H3>
234
<A NAME="@default401"></A><A NAME="@command132"></A>
235
This command cancels the effect of the last tactic command. Thus, it
236
backtracks one step.<BR>
239
<B>Error messages: </B><OL type=1><LI>
240
<TT>No focused proof (No proof-editing in progress)</TT><A NAME="@error39"></A>
241
<LI><TT>Undo stack would be exhausted</TT><A NAME="@error40"></A>
244
<B>Variants: </B><OL type=1><LI><TT>Undo </TT><I><FONT COLOR=maroon>num</FONT></I><TT>.</TT><BR>
246
Repeats <TT>Undo</TT> <I><FONT COLOR=maroon>num</FONT></I> times.</OL>
248
<H3><A NAME="htoc165">7.2.2</A> <TT>Set Undo </TT><I><FONT COLOR=maroon>num</FONT></I><TT>.</TT></H3>
249
<A NAME="@default402"></A><A NAME="@command133"></A>
250
This command changes the maximum number of <TT>Undo</TT>'s that will be
251
possible when doing a proof. It only affects proofs started after
252
this command, such that if you want to change the current undo limit
253
inside a proof, you should first restart this proof.<BR>
256
<H3><A NAME="htoc166">7.2.3</A> <TT>Unset Undo.</TT></H3>
257
<A NAME="@default403"></A><A NAME="@command134"></A>
258
This command resets the default number of possible <TT>Undo</TT> commands
259
(which is currently 12).<BR>
262
<H3><A NAME="htoc167">7.2.4</A> <TT>Restart.</TT></H3><A NAME="@default404"></A><A NAME="@command135"></A>
263
This command restores the proof editing process to the original goal.<BR>
266
<B>Error messages: </B><OL type=1><LI>
267
<TT>No focused proof to restart</TT><A NAME="@error41"></A>
270
<H3><A NAME="htoc168">7.2.5</A> <TT>Focus.</TT></H3><A NAME="@default405"></A><A NAME="@command136"></A>
271
Will focus the attention on the first subgoal to prove, the remaining
272
subgoals will no more be printed after the application of a tactic.
273
This is useful when there are many current subgoals which clutter your
277
<H3><A NAME="htoc169">7.2.6</A> <TT>Unfocus.</TT></H3><A NAME="@default406"></A><A NAME="@command137"></A>
278
Turns off the focus mode.<BR>
281
<H2><A NAME="htoc170">7.3</A> Displaying information</H2>
283
<H3><A NAME="htoc171">7.3.1</A> <TT>Show.</TT></H3><A NAME="@default407"></A><A NAME="@command138"></A><A NAME="Show"></A>
284
This command displays the current goals.<BR>
287
<B>Variants: </B><OL type=1><LI>
288
<TT>Show </TT><I><FONT COLOR=maroon>num</FONT></I><TT>.</TT><BR>
289
Displays only the <I><FONT COLOR=maroon>num</FONT></I>-th subgoal.<BR>
291
<B>Error messages: </B><OL type=a><LI>
292
<TT>No such goal</TT><A NAME="@error42"></A>
293
<LI><TT>No focused proof</TT><A NAME="@error43"></A>
296
<LI><TT>Show Implicits.</TT><A NAME="@default408"></A><A NAME="@command139"></A><BR>
297
Displays the current goals, printing the implicit arguments of
300
<LI><TT>Show Implicits </TT><I><FONT COLOR=maroon>num</FONT></I><TT>.</TT><BR>
301
Same as above, only displaying the <I><FONT COLOR=maroon>num</FONT></I>-th subgoal.<BR>
303
<LI><TT>Show Script.</TT><A NAME="@default409"></A><A NAME="@command140"></A><BR>
304
Displays the whole list of tactics applied from the beginning
305
of the current proof.
306
This tactics script may contain some holes (subgoals not yet proved).
307
They are printed under the form <CODE><Your Tactic Text here></CODE>.<BR>
309
<LI><TT>Show Tree.</TT><A NAME="@default410"></A><A NAME="@command141"></A><BR>
310
This command can be seen as a more structured way of
311
displaying the state of the proof than that
312
provided by <TT>Show Script</TT>. Instead of just giving
313
the list of tactics that have been applied, it
314
shows the derivation tree constructed by then.
315
Each node of the tree contains the conclusion
316
of the corresponding sub-derivation (i.e. a
317
goal with its corresponding local context) and
318
the tactic that has generated all the
319
sub-derivations. The leaves of this tree are
320
the goals which still remain to be proved.<BR>
322
<LI><TT>Show Proof.</TT><A NAME="@default411"></A><A NAME="@command142"></A><BR>
323
It displays the proof term generated by the
324
tactics that have been applied.
325
If the proof is not completed, this term contain holes,
326
which correspond to the sub-terms which are still to be
327
constructed. These holes appear as a question mark indexed
328
by an integer, and applied to the list of variables in
329
the context, since it may depend on them.
330
The types obtained by abstracting away the context from the
331
type of each hole-placer are also printed.<BR>
333
<LI><TT>Show Conjectures.</TT><A NAME="@default412"></A><A NAME="@command143"></A><BR>
334
It prints the list of the names of all the theorems that
335
are currently being proved.
336
As it is possible to start proving a previous lemma during
337
the proof of a theorem, this list may contain several
340
<LI><TT>Show Intro.</TT><A NAME="@default413"></A><A NAME="@command144"></A><BR>
341
If the current goal begins by at least one product, this command
342
prints the name of the first product, as it would be generated by
343
an anonymous <TT>Intro</TT>. The aim of this command is to ease the
344
writing of more robust scripts. For example, with an appropriate
345
Proof General macro, it is possible to transform any anonymous <TT>Intro</TT> into a qualified one such as <TT>Intro y13</TT>.
346
In the case of a non-product goal, it prints nothing. <BR>
348
<LI><TT>Show Intros.</TT><A NAME="@default414"></A><A NAME="@command145"></A><BR>
349
This command is similar to the previous one, it simulates the naming
350
process of an <TT>Intros</TT>.</OL>
352
<H3><A NAME="htoc172">7.3.2</A> <TT>Set Hyps Limit </TT><I><FONT COLOR=maroon>num</FONT></I><TT>.</TT></H3>
353
<A NAME="@default415"></A><A NAME="@command146"></A>
354
This command sets the maximum number of hypotheses displayed in
355
goals after the application of a tactic.
356
All the hypotheses remains usable in the proof development.<BR>
359
<H3><A NAME="htoc173">7.3.3</A> <TT>Unset Hyps Limit.</TT></H3>
360
<A NAME="@default416"></A><A NAME="@command147"></A>
361
This command goes back to the default mode which is to print all
362
available hypotheses.<BR>
365
<A HREF="Reference-Manual008.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
366
<A HREF="toc.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
367
<A HREF="Reference-Manual010.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
added
removed
manual/Reference-Manual009.html
