aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-pro.tex
blob: 0760d716e32e5ededbea17212365dcda37999000 (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
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
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
\chapter[Proof handling]{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 called the {\em \index*{local context}} of the goal.
Initially, the local context contains the local variables and
hypotheses of the current section (see Section~\ref{Variable}) and the
local variables and hypotheses of the theorem statement.  It is
enriched by the use of certain tactics (see e.g. {\tt intro} in
Section~\ref{intro}).

When a proof is completed, the message {\tt Proof completed} is
displayed. One can then register 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}.

\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}

The proof editing mode is entered by asserting a statement, which
typically is the assertion of a theorem:

\begin{quote}
{\tt Theorem {\ident} \zeroone{\binders} : {\form}.\comindex{Theorem}
\label{Theorem}}
\end{quote}

The list of assertion commands is given in
Section~\ref{Assertions}. The command {\tt Goal} can also be used.

\subsection[Goal {\form}.]{\tt Goal {\form}.\comindex{Goal}\label{Goal}}

This is intended for quick assertion of statements, without knowing in
advance which name to give to the assertion, typically for quick
testing of the provability of a statement. If the proof of the
statement is eventually completed and validated, the statement is then
bound to the name {\tt Unnamed\_thm} (or a variant of this name not
already used for another statement).

\subsection[\tt Qed.]{\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 {\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.

\end{Variants}

\subsection[\tt Admitted.]{\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 Proof {\term}.]{\tt Proof {\term}.\comindex{Proof}
\label{BeginProof}}
This command applies in proof editing mode. It is equivalent to {\tt
  exact {\term}. Qed.} That is, you have to give the full proof in
one gulp, as a proof term (see Section~\ref{exact}).

\variant {\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.}

\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.

\subsection[{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}]
{{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}
\comindex{Proof using} \label{ProofUsing}}

This command applies in proof editing mode. 
It declares the set of section variables (see~\ref{Variable}) 
used by the proof. At {\tt Qed} time, the system will assert that 
the set of section variables actually used in the proof is a subset of
the declared one.

The set of declared variables is closed under type dependency.
For example if {\tt T} is variable and {\tt a} is a variable of
type {\tt T}, the commands {\tt Proof using a} and
{\tt Proof using T a} are actually equivalent.

\variant {\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$} {\tt with} {\tac}{\tt .} 
in Section~\ref{ProofWith}.

\variant {\tt Proof using All.} 

  Use all section variables.

\variant {\tt Proof using Type.} 
\variant {\tt Proof using.} 
  
  Use only section variables occurring in the statement.

\variant {\tt Proof using Type*.} 
  
  The {\tt *} operator computes the forward transitive closure.
  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
  {\tt Type* } is the forward transitive closure of the entire set of
  section variables occurring in the statement.

\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
  
  Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.

\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}

\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}

\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}

\variant {\tt Proof using \nterm{collection} * .}

  Use section variables being, respectively, in the set union, set difference,
  set complement, set forward transitive closure.
  See Section~\ref{Collection} to know how to form a named
  collection.
  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.

\subsubsection{{\tt Proof using} options}
\optindex{Default Proof Using}
\optindex{Suggest Proof Using}
% \optindex{Proof Using Clear Unused}

The following options modify the behavior of {\tt Proof using}.

\variant {\tt Set Default Proof Using "expression".} 

  Use {\tt expression} as the default {\tt Proof using} value.
  E.g. {\tt Set Default Proof Using "a b".} will complete all {\tt Proof }
  commands not followed by a {\tt using} part with {\tt using a b}.

\variant {\tt Set Suggest Proof Using.}

  When {\tt Qed} is performed, suggest a {\tt using} annotation if
  the user did not provide one.

% \variant{\tt Unset Proof Using Clear Unused.}
% 
%   When {\tt Proof using a} all section variables but for {\tt a} and
%   the variables used in the type of {\tt a} are cleared.
%   This option can be used to turn off this behavior.
% 
\subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
\comindex{Collection}\label{Collection}

The command {\tt Collection} can be used to name a set of section hypotheses,
with the purpose of making {\tt Proof using} annotations more compact.

\variant {\tt Collection Some := x y z.}

  Define the collection named "Some" containing {\tt x y} and {\tt z} 

\variant {\tt Collection Fewer := Some - x.} 
  
  Define the collection named "Fewer" containing only {\tt x y} 

\variant {\tt Collection Many := Fewer + Some.} 
\variant {\tt Collection Many := Fewer - Some.} 
  
  Define the collection named "Many" containing the set union or set difference
  of "Fewer" and "Some".

\variant {\tt Collection Many := Fewer - (x y).}

  Define the collection named "Many" containing the set difference
  of "Fewer" and the unnamed collection {\tt x y}.

\subsection[\tt Abort.]{\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 Existential {\num} := {\term}.]{\tt Existential  {\num} := {\term}.\comindex{Existential}
\label{Existential}}

This command instantiates an existential variable. {\tt \num}
is an index in the list of uninstantiated existential variables
displayed by {\tt Show Existentials} (described in Section~\ref{Show}).

This command is intended to be used to instantiate existential
variables when the proof is completed but some uninstantiated
existential variables remain. To instantiate existential variables
during proof edition, you should use the tactic {\tt instantiate}.

\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}.
\SeeAlso {\tt Grab Existential Variables.} below.

\subsection[\tt Grab Existential Variables.]{\tt Grab Existential Variables.\comindex{Grab Existential Variables}
\label{GrabEvars}}

This command can be run when a proof has no more goal to be solved but has remaining
uninstantiated existential variables. It takes every uninstantiated existential variable
and turns it into a goal.

%%%%%%%%
\section{Navigation in the proof tree}
%%%%%%%%

\subsection[\tt Undo.]{\tt Undo.\comindex{Undo}}

This command cancels the effect of the last command.  Thus, it
backtracks one step.

\begin{Variants}

\item {\tt Undo {\num}.}

  Repeats {\tt Undo} {\num} times.

\end{Variants}

\subsection[\tt Restart.]{\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.]{\tt Focus.\comindex{Focus}}
This focuses the attention on the first subgoal to prove and the printing
of the other subgoals is suspended until the focused subgoal is
solved or unfocused. This is useful when there are many current
subgoals which clutter your screen.

\begin{Variant}
\item {\tt Focus {\num}.}\\ 
This focuses the attention on the $\num^{th}$ subgoal to prove.

\end{Variant}

\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
This command restores to focus the goal that were suspended by the
last {\tt Focus} command.

\subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
Succeeds in the proof is fully unfocused, fails is there are some
goals out of focus.

\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}
The command {\tt \{} (without a terminating period) focuses on the
first goal, much like {\tt Focus.} does, however, the subproof can
only be unfocused when it has been fully solved (\emph{i.e.} when
there is no focused goal left). Unfocusing is then handled by {\tt \}}
(again, without a terminating period). See also example in next section.

Note that when a focused goal is proved a message is displayed
together with a suggestion about the right bullet or {\tt \}} to
unfocus it or focus the next one.

\begin{ErrMsgs}
\item \errindex{This proof is focused, but cannot be unfocused
    this way} You are trying to use {\tt \}} but the current subproof
  has not been fully solved.
\item see also error message about bullets below.
\end{ErrMsgs}

\subsection[Bullets]{Bullets\comindex{+ (command)}
  \comindex{- (command)}\comindex{* (command)}\index{Bullets}}
Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with
bullets. The use of a bullet $b$ for the first time focuses on the
first goal $g$, the same bullet cannot be used again until the proof
of $g$ is completed, then it is mandatory to focus the next goal with $b$. The
consequence is that $g$ and all goals present when $g$ was focused are
focused with the same bullet $b$. See the example below.

Different bullets can be used to nest levels. The scope of bullet does
not go beyond enclosing {\tt \{} and {\tt \}}, so bullets can be
reused as further nesting levels provided they are delimited by these.
Available bullets are {\tt -}, {\tt +}, {\tt *}, {\tt --}, {\tt ++}, {\tt **},
{\tt ---}, {\tt +++}, {\tt ***}, ... (without a
terminating period).

Note again that when a focused goal is proved a message is displayed
together with a suggestion about the right bullet or {\tt \}} to
unfocus it or focus the next one.

Remark: In {\ProofGeneral} (Emacs interface to {\Coq}), you must use
bullets with the priority ordering shown above to have a correct
indentation. For example {\tt -} must be the outer bullet and {\tt **}
the inner one in the example below.

The following example script illustrates all these features:
\begin{coq_example*}
Goal (((True/\True)/\True)/\True)/\True.
Proof.
  split.
  - split.
    + split.
      ** { split.
          - trivial.
          - trivial.
        }
      ** trivial.
    + trivial.
  - assert True.
    { trivial. }
    assumption.
\end{coq_example*}


\begin{ErrMsgs}
\item \errindex{Wrong bullet {\abullet}1 : Current bullet
    {\abullet}2 is not finished.}

  Before using bullet {\abullet}1 again, you should first finish
  proving the current focused goal. Note that {\abullet}1 and
  {\abullet}2 may be the same.

\item \errindex{Wrong bullet {\abullet}1 : Bullet {\abullet}2
    is mandatory here.} You must put {\abullet}2 to focus next goal.
  No other bullet is allowed here.


\item \errindex{No such goal. Focus next goal with bullet
    {\abullet}.}

  You tried to applied a tactic but no goal where under focus. Using
  {\abullet} is mandatory here.

\item \errindex{No such goal. Try unfocusing with {"{\tt \}}"}.} You
  just finished a goal focused by {\tt \{}, you must unfocus it with "{\tt \}}".

\end{ErrMsgs}

The bullet behavior can be controlled by the following commands.

\begin{quote}
Set Bullet Behavior "None".
\end{quote}

This makes bullets inactive.

\begin{quote}
Set Bullet Behavior "Strict Subproofs".
\end{quote}

This makes bullets active (this is the default behavior).

\section{Requesting information}

\subsection[\tt Show.]{\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 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 
{\ProofGeneral} 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}.

\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
\\ It displays
the set of all uninstantiated existential variables in the current proof tree, 
along with the type and the context of each variable.

\item{\tt Show Match {\ident}.\label{ShowMatch}}\comindex{Show Match}\\
This variant displays a template of the Gallina {\tt match} construct 
with a branch for each constructor of the type {\ident}.

Example:

\begin{coq_example}
Show Match nat.  
\end{coq_example}
\begin{ErrMsgs}
\item \errindex{Unknown inductive type}
\end{ErrMsgs}

\item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes}
\\ It displays the set of all universe constraints and its
normalized form at the current stage of the proof, useful for
debugging universe inconsistencies.

\end{Variants}


\subsection[\tt Guarded.]{\tt Guarded.\comindex{Guarded}\label{Guarded}}

Some tactics (e.g. refine \ref{refine}) allow to build proofs using
fixpoint or co-fixpoint constructions. Due to the incremental nature
of interactive proof construction, the check of the termination (or
guardedness) of the recursive calls in the fixpoint or cofixpoint
constructions is postponed to the time of the completion of the proof.

The command \verb!Guarded! allows checking if the guard condition for
fixpoint and cofixpoint is violated at some time of the construction
of the proof without having to wait the completion of the proof."


\section{Controlling the effect of proof editing commands}

\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\optindex{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.]{\tt Unset Hyps Limit.\optindex{Hyps Limit}}
This command goes back to the default mode which is to print all
available hypotheses.


\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\optindex{Automatic Introduction}\label{Set Automatic Introduction}}

The option {\tt Automatic Introduction} controls the way binders are
handled in assertion commands such as {\tt Theorem {\ident}
  \zeroone{\binders} : {\form}}. When the option is set, which is the
default, {\binders} are automatically put in the local context of the
goal to prove.

The option can be unset by issuing {\tt Unset Automatic Introduction}.
When the option is unset, {\binders} are discharged on the statement
to be proved and a tactic such as {\tt intro} (see
Section~\ref{intro}) has to be used to move the assumptions to the
local context.

\section{Controlling memory usage\comindex{Optimize Proof}\comindex{Optimize Heap}}

When experiencing high memory usage the following commands can be
used to force Coq to optimize some of its internal data structures.

\subsection[\tt Optimize Proof.]{\tt Optimize Proof.}

This command forces Coq to shrink the data structure used to represent
the ongoing proof.

\subsection[\tt Optimize Heap.]{\tt Optimize Heap.}

This command forces the OCaml runtime to perform a heap compaction.
This is in general an expensive operation.  See:
  \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: