\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \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{\lb}{\lambda} \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}{\mathbb{N}} \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{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\cal S} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} \newcommand{\WFTWOLINES}[2]{{\cal 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}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

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.

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 Assertions and proofs. The command Goal can also be used.

Command Goal form

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. This name is added to the environment as an opaque constant.

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

Variant Defined

Same as Qed but 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, Opaque, Transparent).

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 mode to give up the current proof and declare the initial goal as an axiom.

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 proof-editing in progress).

Variant Abort ident

Aborts the editing of the proof named ident (in case you have nested proofs).

Variant Abort All

Aborts all current goals.

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

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.

参考

Proof with

Command Proof using ident+

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 ident+ with tactic

Combines in a single line Proof with and Proof using.

参考

Setting implicit automation tactics

Variant Proof using All

Use all section variables.

Variant Proof using Type?

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 -(ident+)

Use all section variables except the list of ident.

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

Variant Proof using collection1 - collection2

Use section variables which are in the first collection but not in the second one.

Variant Proof using collection - (ident+)

Use section variables which are in the first collection but not in the list of ident.

Variant Proof using collection *

Use section variables in the forward transitive closure of the 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 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 := expression

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 num := term

This command instantiates an existential variable. num 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.

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.

Navigation in the proof tree

Command Undo

This command cancels the effect of the last command. Thus, it backtracks one step.

Variant Undo num

Repeats Undo num times.

Variant Restart

This command restores the proof editing process to the original goal.

Error No focused proof to restart.

Command Focus

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.

バージョン 8.8 で非推奨: Prefer the use of bullets or focusing brackets (see below).

Variant Focus num

This focuses the attention on the num th subgoal to prove.

バージョン 8.8 で非推奨: Prefer the use of focusing brackets with a goal selector (see below).

Command Unfocus

This command restores to focus the goal that were suspended by the last Focus command.

バージョン 8.8 で非推奨.

Command Unfocused

Succeeds if the proof is fully unfocused, fails if there are some goals out of focus.

Command { | }

The command { (without a terminating period) focuses on the first goal, much like Focus does, however, the subproof can only be unfocused when it has been fully solved ( i.e. when there is no focused goal left). Unfocusing is then handled by } (again, without a terminating period). See also an example in the next section.

Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or } to unfocus it or focus the next one.

Variant num: {

This focuses on the num th subgoal to prove.

Error messages:

Error This proof is focused, but cannot be unfocused this way.

You are trying to use } but the current subproof has not been fully solved.

Error No such goal.

Error Brackets only support the single numbered goal selector.

参考

The error messages about bullets below.

Bullets

Alternatively to { and }, proofs can be structured with bullets. The use of a bullet b for the first time focuses on the first goal g, the same bullet cannot be used again until the proof of g is completed, then it is mandatory to focus the next goal with b. The consequence is that g and all goals present when g was focused are focused with the same bullet b. See the example below.

Different bullets can be used to nest levels. The scope of bullet does not go beyond enclosing { and }, so bullets can be reused as further nesting levels provided they are delimited by these. Bullets are made of repeated -, + or * symbols:

bullet ::= -+ | ++ | *+

Note again that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or } to unfocus it or focus the next one.

注釈

In Proof General (Emacs interface to Coq), you must use bullets with the priority ordering shown above to have a correct indentation. For example - must be the outer bullet and ** the inner one in the example below.

The following example script illustrates all these features:

Example

Goal (((True /\ True) /\ True) /\ True) /\ True.

1 subgoal ============================ (((True /\ True) /\ True) /\ True) /\ True

Proof.

split.

2 subgoals ============================ ((True /\ True) /\ True) /\ True subgoal 2 is: True

- split.

1 subgoal ============================ ((True /\ True) /\ True) /\ True 2 subgoals ============================ (True /\ True) /\ True subgoal 2 is: True

+ split.

1 subgoal ============================ (True /\ True) /\ True 2 subgoals ============================ True /\ True subgoal 2 is: True

** { split.

1 subgoal ============================ True /\ True 1 subgoal ============================ True /\ True 2 subgoals ============================ True subgoal 2 is: True

- trivial.

1 subgoal ============================ True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. 4 subgoals subgoal 1 is: True subgoal 2 is: True subgoal 3 is: True subgoal 4 is: True

- trivial.

1 subgoal ============================ True This subproof is complete, but there are some unfocused goals. Try unfocusing with "}". 3 subgoals subgoal 1 is: True subgoal 2 is: True subgoal 3 is: True

} ** trivial.

This subproof is complete, but there are some unfocused goals. Focus next goal with bullet **. 3 subgoals subgoal 1 is: True subgoal 2 is: True subgoal 3 is: True 1 subgoal ============================ True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet +. 2 subgoals subgoal 1 is: True subgoal 2 is: True

+ trivial.

1 subgoal ============================ True This subproof is complete, but there are some unfocused goals. Focus next goal with bullet -. 1 subgoal subgoal 1 is: True

- assert True.

1 subgoal ============================ True 2 subgoals ============================ True subgoal 2 is: True

{ trivial.

1 subgoal ============================ True This subproof is complete, but there are some unfocused goals. Try unfocusing with "}". 1 subgoal subgoal 1 is: True

} assumption.

1 subgoal H : True ============================ True No more subgoals.

Qed.

Unnamed_thm is defined

Error Wrong bullet bullet1: Current bullet bullet2 is not finished.

Before using bullet bullet1 again, you should first finish proving the current focused goal. Note that bullet1 and bullet2 may be the same.

Error Wrong bullet bullet1: Bullet bullet2 is mandatory here.

You must put bullet2 to focus on the next goal. No other bullet is allowed here.

Error No such goal. Focus next goal with bullet bullet.

You tried to apply a tactic but no goals were under focus. Using bullet is mandatory here.

Error No such goal. Try unfocusing with }.

You just finished a goal focused by {, you must unfocus it with }.

Set Bullet Behavior

Option Bullet Behavior ( "None" | "Strict Subproofs" )

This option controls the bullet behavior and can take two possible values:

• "None": this makes bullets inactive.

• "Strict Subproofs": this makes bullets active (this is the default behavior).

Requesting information

Command Show

This command displays the current goals.

Error No focused proof.

Variant Show num

Displays only the num-th subgoal.

Error No such goal.

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

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 non-product 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) 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.

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 Automatic Introduction

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.

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.