\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Proof mode

Proof mode is used to prove theorems. Coq enters proof mode when you begin a proof, such as with the Theorem command. It exits proof mode when you complete a proof, such as with the Qed command. Tactics, which are available only in proof mode, incrementally transform incomplete proofs to eventually generate a complete proof.

When you run Coq interactively, such as through CoqIDE, Proof General or coqtop, Coq shows the current proof state (the incomplete proof) as you enter tactics. This information isn't shown when you run Coq in batch mode with coqc.

Proof State

The proof state consists of one or more unproven goals. Each goal has a conclusion (the statement that is to be proven) and a local context, which contains named hypotheses (which are propositions), variables and local definitions that can be used in proving the conclusion. The proof may also use constants from the global environment such as definitions and proven theorems.

The term "goal" may refer to an entire goal or to the conclusion of a goal, depending on the context.

The conclusion appears below a line and the local context appears above the line. The conclusion is a type. Each item in the local context begins with a name and ends, after a colon, with an associated type. Local definitions are shown in the form n := 0 : nat, for example, in which nat is the type of 0.

The local context of a goal contains items specific to the goal as well as section-local variables and hypotheses (see Assumptions) defined in the current section. The latter are included in the initial proof state. Items in the local context are ordered; an item can only refer to items that appear before it. (A more mathematical description of the local context is here.)

The global environment has definitions and proven theorems that are global in scope. (A more mathematical description of the global environment is here.)

When you begin proving a theorem, the proof state shows the statement of the theorem below the line and often nothing in the local context:

Parameter P: nat -> Prop.
P is declared
Goal forall n m: nat, n > m -> P 1 /\ P 2.
1 subgoal ============================ forall n m : nat, n > m -> P 1 /\ P 2

After applying the intros tactic, we see hypotheses above the line. The names of variables (n and m) and hypotheses (H) appear before a colon, followed by the type they represent.

intros.
1 subgoal n, m : nat H : n > m ============================ P 1 /\ P 2

Some tactics, such as split, create new goals, which may be referred to as subgoals for clarity. Goals are numbered from 1 to N at each step of the proof to permit applying a tactic to specific goals. The local context is only shown for the first goal.

split.
2 subgoals n, m : nat H : n > m ============================ P 1 subgoal 2 is: P 2

"Variables" may refer specifically to local context items for which the type of their type is Set or Type, and "hypotheses" refers to items that are propositions, for which the type of their type is Prop or SProp, but these terms are also used interchangeably.

let t_n := type of n in idtac "type of n :" t_n; let tt_n := type of t_n in idtac "type of" t_n ":" tt_n.
type of n : nat type of nat : Set
let t_H := type of H in idtac "type of H :" t_H; let tt_H := type of t_H in idtac "type of" t_H ":" tt_H.
type of H : (n > m) type of (n > m) : Prop

A proof script, consisting of the tactics that are applied to prove a theorem, is often informally referred to as a "proof". The real proof, whether complete or incomplete, is a term, the proof term, which users may occasionally want to examine. (This is based on the Curry-Howard isomorphism [How80][Bar81][GLT89][Hue89], which is a correspondence between between proofs and terms and between propositions and types of λ-calculus. The isomorphism is also sometimes called the "propositions-as-types correspondence".)

The Show Proof command displays the incomplete proof term before you've completed the proof. For example, here's the proof term after using the split tactic above:

Show Proof.
(fun (n m : nat) (H : n > m) => conj ?Goal ?Goal0)

The incomplete parts, the goals, are represented by existential variables with names that begin with ?Goal. The Show Existentials command shows each existential with the hypotheses and conclusion for the associated goal.

Show Existentials.
Existential 1 = ?Goal : [n : nat m : nat H : n > m |- P 1] Existential 2 = ?Goal0 : [n : nat m : nat H : n > m |- P 2]

Coq's kernel verifies the correctness of proof terms when it exits proof mode by checking that the proof term is well-typed and that its type is the same as the theorem statement.

After a proof is completed, Print <theorem_name> shows the proof term and its type. The type appears after the colon (forall ...), as for this theorem from Coq's standard library:

Print proj1.
Fetching opaque proofs from disk for Coq.Init.Logic proj1 = fun (A B : Prop) (H : A /\ B) => match H with | conj H0 _ => H0 end : forall A B : Prop, A /\ B -> A Arguments proj1 [A B]%type_scope _

Entering and exiting proof mode

Coq enters proof mode when you begin a proof through commands such as Theorem or Goal. Coq user interfaces usually have a way to indicate that you're in proof mode.

Tactics are available only in proof mode (currently they give syntax errors outside of proof mode). Most commands can be used both in and out of proof mode, but some commands only work in or outside of proof mode.

When the proof is completed, you can exit proof mode with commands such as Qed, Defined and Save.

Command Goal type

Asserts an unnamed proposition. This is intended for quick tests that a proposition is provable. If the proof is eventually completed and validated, you can assign a name with the Save or Defined commands. If no name is given, the name will be Unnamed_thm (or, if that name is already defined, a variant of that).

Command Qed

Passes a completed proof term to Coq's kernel to check that the proof term is well-typed and to verify that its type matches the theorem statement. If it's verified, the proof term is added to the global environment as an opaque constant using the declared name from the original goal.

It's very rare for a proof term to fail verification. Generally this indicates a bug in a tactic you used or that you misused some unsafe tactics.

Error Attempt to save an incomplete proof.
Error No focused proof (No proof-editing in progress).

You tried to use a proof mode command such as Qed outside of proof mode.

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.

Command Save ident

Similar to Qed, except that the proof term is added to the global context with the name ident, which overrides any name provided by the Theorem command or its variants.

Command Defined ident?

Similar to Qed and Save, 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). If ident is specified, the proof is defined with the given name, which overrides any name provided by the Theorem command or its variants.

Command Admitted

This command is available in proof 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 also Nested Proofs Allowed.

All

Aborts all current proofs.

Error No focused proof (No proof-editing in progress).
Command Proof term

This command applies in proof 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 use Proof as an opening parenthesis, closed in the script with a closing Qed.

See also

Proof with

Command Proof using section_var_expr with ltac_expr?
section_var_expr::=starred_ident_ref*|-? section_var_expr50section_var_expr50::=section_var_expr0 - section_var_expr0|section_var_expr0 + section_var_expr0|section_var_expr0section_var_expr0::=starred_ident_ref|( section_var_expr ) *?starred_ident_ref::=ident *?|Type *?|All

Opens proof 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 and a is a variable of type T, then the commands Proof using a and Proof 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 to Proof using Type + e for any declaration expression e.

- 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 variable H has type p < 5 then H is in p* since p occurs in the type of H.

All

Use all section variables.

Attribute using

This attribute can be applied to the Definition, Example, Fixpoint and CoFixpoint commands as well as to Lemma and its variants. It takes a section_var_expr, in quotes, as its value. This is equivalent to specifying the same section_var_expr in Proof using.

Example

Section Test.
Variable n : nat.
n is declared
Hypothesis Hn : n <> 0.
Hn is declared
#[using="Hn"] Lemma example : 0 < n.
1 subgoal n : nat Hn : n <> 0 ============================ 0 < n
Abort.
End Test.

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 default Proof using value. E.g. Set Default Proof Using "a b" will complete all Proof commands not followed by a using part with using a b.

Flag 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

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 containing x, y and z:

Collection Some := x y z.

Define the collection named Fewer containing only x and y:

Collection Fewer := Some - z

Define the collection named Many containing the set union or set difference of Fewer and Some:

Collection Many := Fewer + Some
Collection Many := Fewer - Some

Define the collection named Many containing the set difference of Fewer and the unnamed collection x y:

Collection Many := Fewer - (x y)
Command Existential natural : type? := term

This command instantiates an existential variable. natural is an index in the list of uninstantiated existential variables displayed by Show 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.

Deprecated since version 8.13.

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.

Deprecated since version 8.13: Use Unshelve instead.

Proof modes

When entering proof mode through commands such as Goal and Proof, Coq picks by default the Ltac 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 a proof. All proof modes support commands; the proof mode determines which tactic language and set of tactic definitions are available. The possible option values are:

"Classic"

Activates the Ltac language and the tactics with the syntax documented in this manual. Some tactics are not available until the associated plugin is loaded, such as SSR or micromega. 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 for coqc.

"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 identnatural?

Displays the current goals.

natural

Display only the natural-th goal.

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.

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 "Show Proof" differences.

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

Command Show Intros

Similar to the previous command. Simulates the naming process of intros.

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 type qualid. 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 natural at natural

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 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. Coq can also highlight differences in the proof term. 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.

CoqIDE with Set Diffs on
CoqIDE with Set Diffs removed
coqtop with Set Diffs on

This image shows an error message with diff highlighting in CoqIDE:

CoqIDE error message with diffs

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.

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:

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

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

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

coqide with Set Diffs on with multiple goals

Diffs may appear like this after applying a intro tactic that results in a compacted hypotheses:

coqide with Set Diffs on with compacted hypotheses

"Show Proof" differences

To show differences in the proof term:

  • In coqtop and Proof General, use the Show Proof Diffs command.

  • In CoqIDE, position the cursor on or just after a tactic to compare the proof term after the tactic with the proof term before the tactic, then select View / Show Proof from the menu or enter the associated key binding. Differences will be shown applying the current Show Diffs setting from the View menu. If the current setting is Don't show diffs, diffs will not be shown.

    Output with the "added and removed" option looks like this:

    coqide with Set Diffs on with compacted hypotheses

Controlling proof mode

Option Hyps Limit natural

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

Flag Printing Goal Names

When turned on, the name of the goal is printed in proof mode, which can be useful in cases of cross references between goals.

Controlling memory usage

Command Print Debug GC

Prints heap usage statistics, which are values from the stat type of the Gc module described here in the OCaml documentation. The live_words, heap_words and top_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.