In Coq's proof editing mode all top-level commands documented in
chapter 6 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 8.
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 we call the local context of the goal.
Initially, the local context is empty. It is enriched by the use of
certain tactics (see mainly section 8.3.5).
When a proof is achieved the message Proof completed is
displayed. One can then store this proof as a defined constant in the
environment. Because there exists a correspondence between proofs and
terms of λ-calculus, known as the Curry-Howard
isomorphism [68, 6, 64, 71], Coq stores proofs as
terms of Cic. Those terms are called proof
It is possible to edit several proofs at the same time: see section
Error message: When one attempts to use a proof editing command out of the
proof editing mode, Coq raises the error message : No focused
7.1 Switching on/off the proof editing mode
7.1.1 Goal form.
This command switches Coq to editing proof mode and sets form as
the original goal. It associates the name Unnamed_thm to
the term form has type ... which should be Set,
Prop or Type
See also: section 7.1.4
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 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 Opaque constant.
Attempt to save an incomplete proof
- Sometimes an error occurs when building the proof term,
because tactics do not enforce completely the term construction
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
This command is available in interactive editing proof mode to give up
the current proof and declare the initial goal as an axiom.
Defines the proved term as a transparent constant.
Is equivalent to Qed.
- 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.
- Save Theorem ident.
Save Lemma ident.
Save Remark ident.
Save Fact ident.
Are equivalent to Save ident.
7.1.4 Theorem ident : form.
This command switches to interactive editing proof mode and declares
ident as being the name of the original goal form. When declared
as a Theorem, the name ident is known at all section levels:
Theorem is a global lemma.
- the term form has type ... which should be Set,
Prop or Type
- identalready exists
The name you provided already defined. You have then to choose
- Lemma ident : form.
It is equivalent to Theorem ident : form.
- Remark ident : form.
Fact ident : form.
Used to have a different meaning, but are now equivalent to Theorem ident : form. They are kept for compatibility.
- Definition ident : form.
Analogous to Theorem, intended to be used in conjunction with
Defined (see 1) in order to define a
- Let ident : form.
Analogous to Definition except that the definition is turned
into a local definition on objects depending on it after closing the
7.1.5 Proof term.
This command applies in proof editing mode. It is equivalent to exact term; Save. That is, you have to give the full proof in
one gulp, as a proof term (see section 8.2.1).
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 8.13.6.
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.
No focused proof (No proof-editing in progress)
This command applies in proof editing mode. It switches back to the
Coq toplevel, but without canceling the current proofs.
- Abort ident.
Aborts the editing of the proof named ident.
- Abort All.
Aborts all current goals, switching back to the Coq toplevel.
This commands switches back to the editing of the last edited proof.
No proof-editing in progress
- Resume ident.
Restarts the editing of the proof named ident. This can be used
to navigate between currently edited proofs.
No such proof
7.2 Navigation in the proof tree
This command cancels the effect of the last tactic command. Thus, it
backtracks one step.
No focused proof (No proof-editing in progress)
- Undo stack would be exhausted
- Undo num.
Repeats Undo num times.
7.2.2 Set Undo num.
This command changes the maximum number of Undo's that will be
possible when doing a proof. It only affects proofs started after
this command, such that if you want to change the current undo limit
inside a proof, you should first restart this proof.
7.2.3 Unset Undo.
This command resets the default number of possible Undo commands
(which is currently 12).
This command restores the proof editing process to the original goal.
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.
No focused proof to restart
Turns off the focus mode.
This focuses the attention on the numth subgoal to prove.
7.3 Displaying information
This command displays the current goals.
Displays only the num-th subgoal.
No such goal
- No focused proof
- Show Implicits.
Displays the current goals, printing the implicit arguments of
- Show Implicits num.
Same as above, only displaying the num-th subgoal.
- 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>.
- Show Tree.
This command can be seen as a more structured way of
displaying the state of the proof than that
provided by 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.
- 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.
- 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
- 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 non-product goal, it prints nothing.
- Show Intros.
This command is similar to the previous one, it simulates the naming
process of an Intros.
7.3.2 Set Hyps Limit num.
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.
7.3.3 Unset Hyps Limit.
This command goes back to the default mode which is to print all