Proof handling¶
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. 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 Curry-Howard 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.
Entering and leaving 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 Assertions and proofs. The command
Goal
can also be used.
-
Command
Goal type
¶ 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 top-level and attaches the extracted proof term to the declared name of the original goal. The 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.
-
Error
-
Command
Save ident
¶ Saves a completed proof with the name
ident
, which overrides any name provided by theTheorem
command or its variants.
-
Command
Defined ident?
¶ Similar to
Qed
andSave
, except the proof is made 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,Opaque
,Transparent
). Ifident
is specified, the proof is defined with the given name, which overrides any name provided by theTheorem
command or its variants.
-
Command
Admitted
¶ This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom.
-
Command
Abort Allident?
¶ Cancels the current proof development, switching back to the previous proof development, or to the Coq toplevel if no other proof was being edited.
ident
Aborts editing the proof named
ident
for use when you have nested proofs. See alsoNested Proofs Allowed
.All
Aborts all current proofs.
-
Error
No focused proof (No proof-editing in progress).
¶
-
Command
Proof term
¶ 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).Warning
Use of this command is discouraged. In particular, it doesn't work in Proof General because it must immediately follow the command that opened proof mode, but Proof General inserts
Unset
Silent
before it (see Proof General issue #498).
-
Command
Proof
¶ Is a no-op which is useful to delimit the sequence of tactic commands which start a proof, after a
Theorem
command. It is a good practice to useProof
as an opening parenthesis, closed in the script with a closingQed
.See also
-
Command
Proof using section_var_expr with ltac_expr?
¶ - |Type *?|All
Opens proof editing mode, declaring the set of section variables (see Assumptions) used by the proof. At
Qed
time, the system verifies that the set of section variables 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 a variable anda
is a variable of typeT
, then the commandsProof using a
andProof using T a
are equivalent.The set of declared variables always includes the variables used by the statement. In other words
Proof using e
is equivalent toProof using Type + e
for any declaration expressione
.- section_var_expr50
Use all section variables except those specified by
section_var_expr50
section_var_expr0 + section_var_expr0
Use section variables from the union of both collections. See Name a set of section hypotheses for Proof using to see how to form a named collection.
section_var_expr0 - section_var_expr0
Use section variables which are in the first collection but not in the second one.
*?
Use the transitive closure of the specified collection.
Type
Use only section variables occurring in the statement. Specifying
*
uses the forward transitive closure of all the section variables occurring in the statement. For example, if the variableH
has typep < 5
thenH
is inp*
sincep
occurs in the type ofH
.All
Use all section variables.
See also
Proof using options¶
The following options modify the behavior of Proof using
.
-
Option
Default Proof Using "section_var_expr"
¶ Use
section_var_expr
as the defaultProof using
value. E.g.Set Default Proof Using "a b"
will complete allProof
commands not followed by ausing
part withusing a b
.
Name a set of section hypotheses for Proof using
¶
-
Command
Collection ident := section_var_expr
¶ This can be used to name a set of section hypotheses, with the purpose of making
Proof using
annotations more compact.Example
Define the collection named
Some
containingx
,y
andz
:Collection Some := x y z.
Define the collection named
Fewer
containing onlyx
andy
:Collection Fewer := Some - z
Define the collection named
Many
containing the set union or set difference ofFewer
andSome
:Collection Many := Fewer + Some Collection Many := Fewer - Some
Define the collection named
Many
containing the set difference ofFewer
and the unnamed collectionx y
:Collection Many := Fewer - (x y)
-
Command
Existential num : type? := term
¶ This command instantiates an existential variable.
num
is an index in the list of uninstantiated existential variables displayed byShow Existentials
.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
.
-
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.
Proof modes¶
When entering proof mode through commands such as Goal
and Proof
,
Coq picks by default the L
tac mode. Nonetheless, there exist other proof modes
shipped in the standard Coq installation, and furthermore some plugins define
their own proof modes. The default proof mode used when opening a proof can
be changed using the following option.
-
Option
Default Proof Mode string
¶ Select the proof mode to use when starting a proof. Depending on the proof mode, various syntactic constructs are allowed when writing an interactive proof. All proof modes support vernacular commands; the proof mode determines which tactic language and set of tactic definitions are available. The possible option values are:
"Classic"
Activates the
L
tac language and the tactics with the syntax documented in this manual. Some tactics are not available until the associated plugin is loaded, such asSSR
ormicromega
. This proof mode is set when the prelude is loaded."Noedit"
No tactic language is activated at all. This is the default when the prelude is not loaded, e.g. through the
-noinit
option forcoqc
."Ltac2"
Activates the Ltac2 language and the Ltac2-specific variants of the documented tactics. This value is only available after
Requiring
Ltac2.Importing
Ltac2 sets this mode.
Some external plugins also define their own proof mode, which can be activated with this command.
Requesting information¶
-
Command
Show identnum?
¶ Displays the current goals.
num
Display only the
num
-th subgoal.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
-
Error
No focused proof.
¶
-
Error
No such goal.
¶
-
Command
Show Proof Diffs removed??
¶ Displays the proof term generated by the tactics that have been applied so far. If the proof is incomplete, the term will contain holes, which correspond to subterms which are still to be constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier.
Experimental: Specifying “Diffs” highlights the difference between the current and previous proof step. By default, the command shows the output once with additions highlighted. Including “removed” shows the output twice: once showing removals and once showing additions. It does not examine the
Diffs
option. See Showing differences between proof steps.
-
Command
Show Conjectures
¶ Prints 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, there may be multiple names.
-
Command
Show Intro
¶ If the current goal begins by at least one product, 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 anonymousintro
into a qualified one such asintro y13
. In the case of a non-product goal, it prints nothing.
-
Command
Show Existentials
¶ Displays all open goals / existential variables in the current proof along with the type and the context of each variable.
-
Command
Show Match qualid
¶ Displays a template of the Gallina
match
construct with a branch for each constructor of the typequalid
. This is used internally by company-coq.Example
- Show Match nat.
- match # with | O => | S x => end
-
Error
Unknown inductive type.
¶
-
Command
Show Universes
¶ Displays the set of all universe constraints and its normalized form at the current stage of the proof, useful for debugging universe inconsistencies.
-
Command
Show Goal num at num
¶ Available in coqtop. Displays a goal at a proof state using the goal ID number and the proof state ID number. It is primarily for use by tools such as Prooftree that need to fetch goal history in this way. Prooftree is a tool for visualizing a proof as a tree that runs in Proof General.
-
Command
Guarded
¶ 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.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.
Showing differences between proof steps¶
Coq can automatically highlight the differences between successive proof steps
and between values in some error messages. Also, as an experimental feature,
Coq can also highlight differences between proof steps shown in the Show Proof
command, but only, for now, when using coqtop and Proof General.
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.
This image shows an error message with diff highlighting in CoqIDE:
How to enable diffs¶
-
Option
Diffs "on""off""removed"
¶ The “on” setting highlights added tokens in green, while the “removed” setting additionally reprints items with removed tokens in red. Unchanged tokens in modified items are shown with pale green or red. Diffs in error messages use red and green for the compared values; they appear regardless of the setting. (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 Diffs
option
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 COQ_COLORS
environment
variable. See section By environment variables. Diffs
use the tags diff.added
, diff.added.bg
, diff.removed
and diff.removed.bg
.
In CoqIDE, diffs should be enabled from the View
menu. Don’t use the Set Diffs
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.added
,
diff.added.bg
, diff.removed
and 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.
As of June 2019, Proof General can also display Coq-generated proof diffs automatically. Please see the PG documentation section "Showing Proof Diffs") for details.
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.
Notes:
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¶
-
Option
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.
-
Flag
Nested Proofs Allowed
¶ When turned on (it is off by default), this flag 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
Qed
orDefined
), 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¶
-
Command
Print Debug GC
¶ Prints heap usage statistics, which are values from the
stat
type of theGc
module described here in the OCaml documentation. Thelive_words
,heap_words
andtop_heap_words
values give the basic information. Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables.
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
¶ Shrink the data structure used to represent the current proof.
-
Command
Optimize Heap
¶ Perform a heap compaction. This is generally an expensive operation. See: OCaml Gc.compact There is also an analogous tactic
optimize_heap
.
Memory usage parameters can be set through the OCAMLRUNPARAM environment variable.