In Coq’s proof editing mode all top-level 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. They 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.
Coq user interfaces usually have a way of marking whether the user has
switched to proof editing mode. For instance, in coqtop 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.
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 Curry-Howard isomorphism
[How80][Bar81][GLT89][Hue89], Coq stores proofs as terms of Cic. Those
terms are called proof terms.
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
list of assertion commands is given in 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).
This command is available in interactive editing proof mode when the proof is completed. Then
Qedextracts 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 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.
Qedbut the proof is then declared transparent, which means that its content can be explicitly used for type checking and that it can be unfolded in conversion tactics (see Performing computations,
This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom.
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).¶
Aborts the editing of the proof named
ident(in case you have nested proofs).
Aborts all current goals.
This command applies in proof editing mode. It is equivalent to
exact term. Qed.That is, you have to give the full proof in one gulp, as a proof term (see Section Applying theorems).
Is a no-op which is useful to delimit the sequence of tactic commands which start a proof, after a
Theoremcommand. It is a good practice to use
Proofas an opening parenthesis, closed in the script with a closing
Proof using ident+¶
This command applies in proof editing mode. It declares the set of section variables (see Assumptions) used by the proof. At
Qedtime, 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
Tis a variable and
ais a variable of type
T, then the commands
Proof using aand
Proof using T aare equivalent.
Proof using ident+ with tactic
Combines in a single line
Proof using All
Use all section variables.
Proof using Type?
Use only section variables occurring in the statement.
Proof using Type*
*operator computes the forward transitive closure. E.g. if the variable
p < 5then
poccurs in the type of
Type*is the forward transitive closure of the entire set of section variables occurring in the statement.
Proof using collection1 + collection2
Use section variables from the union of both collections. See Name a set of section hypotheses for Proof using to know how to form a named collection.
Proof using collection1 - collection2
Use section variables which are in the first collection but not in the second one.
Proof using collection - (ident+)
Use section variables which are in the first collection but not in the list of
Proof using collection *
Use section variables in the forward transitive closure of the collection. The
*operator binds stronger than
Proof using options¶
The following options modify the behavior of
Default Proof Using "expression"¶
expressionas the default
Proof usingvalue. E.g.
Set Default Proof Using "a b"will complete all
Proofcommands not followed by a
using a b.
Name a set of section hypotheses for
Collection ident := expression¶
This can be used to name a set of section hypotheses, with the purpose of making
Proof usingannotations more compact.
Define the collection named
Collection Some := x y z.
Define the collection named
Collection Fewer := Some - z
Define the collection named
Manycontaining the set union or set difference of
Collection Many := Fewer + Some Collection Many := Fewer - Some
Define the collection named
Manycontaining the set difference of
Fewerand the unnamed collection
Collection Many := Fewer - (x y)
Existential num := term¶
This command instantiates an existential variable.
numis an index in the list of uninstantiated existential variables displayed by
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
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.
This command displays the current goals.
No focused proof.
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.
- 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
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>.
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 placeholder are also printed.
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.
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
introinto a qualified one such as
intro y13. In the case of a non-product goal, it prints nothing.
This command is similar to the previous one, it simulates the naming process of an
It displays the set of all uninstantiated existential variables in the current proof tree, along with the type and the context of each variable.
Show Match ident
This variant displays a template of the Gallina
matchconstruct with a branch for each constructor of the type
- Show Match nat.
- match # with | O => | S x => end
Unknown inductive type.¶
It displays the set of all universe constraints and its normalized form at the current stage of the proof, useful for debugging universe inconsistencies.
Some tactics (e.g.
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.
Guardedallows 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.
Showing differences between proof steps¶
Coq can automatically highlight the differences between successive proof steps.
For example, the following screenshots of CoqIDE and coqtop show the application
of the same
intros tactic. The tactic creates two new hypotheses, highlighted in green.
The conclusion is entirely in pale green because although it’s changed, no tokens were added
to it. The second screenshot uses the "removed" option, so it shows the conclusion a
second time with the old text, with deletions marked in red. Also, since the hypotheses are
new, no line of old text is shown for them.
How to enable diffs¶
Diffs "on" "off" "removed"¶
The “on” option highlights added tokens in green, while the “removed” option additionally reprints items with removed tokens in red. Unchanged tokens in modified items are shown with pale green or red. (Colors are user-configurable.)
For coqtop, showing diffs can be enabled when starting coqtop with the
-diffs on|off|removed command-line option or by setting the
within Coq. You will need to provide the
-color on|auto command-line option when
you start coqtop in either case.
Colors for coqtop can be configured by setting the
variable. See section By environment variables. Diffs
use the tags
In CoqIDE, diffs should be enabled from the
View menu. Don’t use the
command in CoqIDE. You can change the background colors shown for diffs from the
Edit | Preferences | Tags panel by changing the settings for the
diff.removed.bg tags. This panel also
lets you control other attributes of the highlights, such as the foreground
color, bold, italic, underline and strikeout.
Note: As of this writing (August 2018), Proof General will need minor changes to be able to show diffs correctly. We hope it will support this feature soon. See https://github.com/ProofGeneral/PG/issues/381 for the current status.
How diffs are calculated¶
Diffs are calculated as follows:
- Select the old proof state to compare to, which is the proof state before
the last tactic that changed the proof. Changes that only affect the view
of the proof, such as
all: swap 1 2, are ignored.
- For each goal in the new proof state, determine what old goal to compare it to—the one it is derived from or is the same as. Match the hypotheses by name (order is ignored), handling compacted items specially.
- For each hypothesis and conclusion (the “items”) in each goal, pass them as strings to the lexer to break them into tokens. Then apply the Myers diff algorithm [Mye86] on the tokens and add appropriate highlighting.
- Aside from the highlights, output for the "on" option should be identical to the undiffed output.
- Goals completed in the last proof step will not be shown even with the "removed" setting.
This screen shot shows the result of applying a
split tactic that replaces one goal
with 2 goals. Notice that the goal
P 1 is not highlighted at all after
the split because it has not changed.
This is how diffs may appear after applying a
intro tactic that results
in compacted hypotheses:
Controlling the effect of proof editing commands¶
Hyps Limit num¶
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.
This option controls the way binders are handled in assertion commands such as
Theorem ident binders? : term. When the option is on, which is the default, binders are automatically put in the local context of the goal to prove.
When the option is off, 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.
Nested Proofs Allowed¶
When turned on (it is off by default), this option enables support for nested proofs: a new assertion command can be inserted before the current proof is finished, in which case Coq will temporarily switch to the proof of this nested lemma. When the proof of the nested lemma is finished (with
Defined), its statement will be made available (as if it had been proved before starting the previous proof) and Coq will switch back to the proof of the previous assertion.
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.
This command forces Coq to shrink the data structure used to represent the ongoing proof.
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