Proof handling¶
In Coq’s proof editing mode all toplevel commands documented in
Chapter 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
tactics. They are the very tools allowing the user to deal with
logical reasoning. They are documented in Chapter Tactics.
When switching in editing proof mode, the prompt Coq <
is changed into
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 local context
of the goal. Initially, the local context contains the local variables and
hypotheses of the current section (see Section Assumptions) and
the local variables and hypotheses of the theorem statement. It is enriched by
the use of certain tactics (see e.g. intro
).
When a proof is completed, the message 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 λcalculus, known as the CurryHoward isomorphism
[How80][Bar81][GLT89][Hue89], Coq stores proofs as terms of Cic. Those
terms are called proof terms.

Error
No focused proof
¶
Coq raises this error message when one attempts to use a proof editing command out of the proof editing mode.
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 using an assertion command like Theorem
. The
list of assertion commands is given in Section Assertions and proofs. The command
Goal
can also be used.
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 Unnamed_thm
(or a variant of this name not already
used for another statement).

Command
Qed
¶
This command is available in interactive editing proof mode when the
proof is completed. Then Qed
extracts a proof term from the proof
script, switches back to Coq toplevel and attaches the extracted
proof term to the declared name of the original goal. This name is
added to the environment as an opaque constant.

Error
Attempt to save an incomplete proof
¶
Note
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.

Variant
Defined.
¶
Defines the proved term as a transparent constant.

Variant
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 Goal
command.

Command
Admitted.
¶
This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom.
This command applies in proof editing mode. It is equivalent to
That is, you have to give the full proof in one gulp, as a proof term (see Section Applying theorems).

Variant
Proof.
¶
Is a noop which is useful to delimit the sequence of tactic commands
which start a proof, after a Theorem
command. It is a good practice to
use Proof
. as an opening parenthesis, closed in the script with a
closing Qed
.
See also: Proof with tactic.
in Section
Setting implicit automation tactics.

Command
Proof using ident1 … identn.
¶
This command applies in proof editing mode. It declares the set of
section variables (see Assumptions) used by the proof. At 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 T
is variable and a is a variable of type T
, the commands
Proof using a
and Proof using T a`
are actually equivalent.

Variant
Proof using ident1 … identn with tactic.
in Section Setting implicit automation tactics.

Variant
Proof using All.
Use all section variables.

Variant
Proof using Type.

Variant
Proof using.
Use only section variables occurring in the statement.

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

Variant
Proof using (ident1 … identn).
Use all section variables except ident1
… identn
.

Variant
Proof using collection1 + collection2 .

Variant
Proof using collection1  collection2 .

Variant
Proof using collection  ( ident1 … identn ).

Variant
Proof using collection * .
Use section variables being, respectively, in the set union, set
difference, set complement, set forward transitive closure. See
Section Name a set of section hypotheses for Proof using to know how to form a named collection. The *
operator
binds stronger than +
and 
.
Proof using options¶
The following options modify the behavior of Proof using
.

Option
Default Proof Using “expression”.
¶ Use
expression
as the defaultProof`
using value. E.g.Set Default Proof Using "a b"
. will complete allProof
commands not followed by a using part with usinga
b
.

Option
Suggest Proof Using.
¶ When
Qed
is performed, suggest a using annotation if the user did not provide one.
Name a set of section hypotheses for Proof using
¶
The command Collection
can be used to name a set of section
hypotheses, with the purpose of making Proof using
annotations more
compact.

Variant
Collection Some := x y z
Define the collection named “Some” containing x
, y
and z
.

Variant
Collection Fewer := Some  z
Define the collection named “Fewer” containing only x
and y
.

Variant
Collection Many := Fewer + Some

Variant
Collection Many := Fewer  Some
Define the collection named “Many” containing the set union or set difference of “Fewer” and “Some”.

Variant
Collection Many := Fewer  (x y)
Define the collection named “Many” containing the set difference of
“Fewer” and the unnamed collection x
y

Command
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.

Error
No focused proof (No proofediting in progress)
¶

Variant
Abort ident.
Aborts the editing of the proof named ident
.

Variant
Abort All.
Aborts all current goals, switching back to the Coq toplevel.
This command instantiates an existential variable. num
is an index in
the list of uninstantiated existential variables displayed by Show
Existentials
(described in Section Requesting information).
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 instantiate
.
See also: instantiate (num:= term).
in Section
Controlling the proof flow.
See also: Grab Existential Variables.
below.

Command
Grab Existential Variables.
¶
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.
Requesting information¶

Command
Show.
¶
This command displays the current goals.

Variant
Show num
Displays only the num
th subgoal.

Error
No such goal
¶

Error
No focused proof

Variant
Show ident.
Displays the named goal ident
. This is useful in
particular to display a shelved goal but only works if the
corresponding existential variable has been named by the user
(see Existential variables) as in the following example.
Example
 Goal exists n, n = 0.
 1 subgoal ============================ exists n : nat, n = 0
 eexists ?[n].
 1 focused subgoal (shelved: 1) ============================ ?n = 0
 Show n.
 subgoal n is: ============================ nat

Variant
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
<Your Tactic Text here>
.

Variant
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 subterms 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 holeplacer are also printed.

Variant
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.

Variant
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 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 intro
into a qualified one such as intro y13
. In the case of a nonproduct
goal, it prints nothing.

Variant
Show Intros.
This command is similar to the previous one, it simulates the naming process of an intros.

Variant
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.

Variant
Show Match ident.
This variant displays a template of the Gallina
match
construct with a branch for each constructor of the type
ident
Example
 Show Match nat.
 match # with  O =>  S x => end

Error
Unknown inductive type
¶

Variant
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.

Command
Guarded.
¶
Some tactics (e.g. refine
Applying theorems) allow to build proofs using
fixpoint or cofixpoint 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 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.
Controlling the effect of proof editing commands¶
This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable in the proof development. When unset, it goes back to the default mode which is to print all available hypotheses.

Option
Automatic Introduction
¶
This option controls the way binders are handled
in assertion commands such as Theorem ident [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 Unset Automatic Introduction
. When
the option is unset, binders are discharged on the statement to be
proved and a tactic such as intro (see Section Managing the local context) has to be
used to move the assumptions to the local context.
Controlling memory usage¶
When experiencing high memory usage the following commands can be used to force Coq to optimize some of its internal data structures.

Command
Optimize Proof.
¶
This command forces Coq to shrink the data structure used to represent the ongoing proof.

Command
Optimize Heap.
¶
This command forces the OCaml runtime to perform a heap compaction.
This is in general an expensive operation.
See: OCaml Gc
There is also an analogous tactic optimize_heap
.