Chapter 7  Proof handling

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 called the local context of the goal. Initially, the local context contains the local variables and hypotheses of the current section (see Section 1.3.1) and the local variables and hypotheses of the theorem statement. It is enriched by the use of certain tactics (see e.g. intro in Section 8.3.1).

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 [76, 6, 72, 79], Coq  stores proofs as terms of Cic. Those terms are called proof terms.


Error message: When one attempts to use a proof editing command out of the proof editing mode, Coq  raises the error message : No focused proof.

7.1  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:

Theorem ident [binders] : form.

The list of assertion commands is given in Section 1.3.5. The command Goal can also be used.

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

7.1.2  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 messages:

  1. Attempt to save an incomplete proof
  2. 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.


Variants:

  1. Defined.

    Defines the proved term as a transparent constant.

  2. Save.

    This is a deprecated equivalent to Qed.

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

  4. Save Theorem ident.
    Save Lemma ident.
    Save Remark ident.
    Save Fact ident. Save Corollary ident. Save Proposition ident.

    Are equivalent to Save ident.

7.1.3  Admitted.

This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom.

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


Variant: Proof.

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

7.1.5  Proof using ident1 …identn.

This command applies in proof editing mode. It declares the set of section variables (see 1.3.1) 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 ident1 …identn with tactic. in Section 8.9.6.

7.1.6  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 messages:

  1. No focused proof (No proof-editing in progress)


Variants:

  1. Abort ident.

    Aborts the editing of the proof named ident.

  2. Abort All.

    Aborts all current goals, switching back to the Coq toplevel.

7.1.7  Existential num := term.

This command allows to instantiate an existential variable. num is an index in the list of uninstantiated existential variables displayed by Show Existentials. (described in Section 7.3.1)

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.


See also: instantiate (num:= term). in Section 8.4.4.
See also: Grab Existential Variables. below.

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

7.2  Navigation in the proof tree

7.2.1  Undo.

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


Error messages:

  1. No focused proof (No proof-editing in progress)


Variants:

  1. Undo num.

    Repeats Undo num times.

7.2.2  Restart.

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


Error messages:

  1. No focused proof to restart

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


Variant:

  1. Focus num.
    This focuses the attention on the numth subgoal to prove.

7.2.4  Unfocus.

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

7.2.5  Unfocused.

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

7.2.6  { and }

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 example in next section.


Error messages:

  1. Error: This proof is focused, but cannot be unfocused this way You are trying to use a bullet that is already in use or a } but the current subproof has not been fully solved.

7.2.7  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. Available bullets are -, + and * (without a terminating period).

The following example script illustrates all these features:

Coq < Goal (((True/\True)/\True)/\True)/\True.

Coq < Proof.

Coq <   split.

Coq <   - split.

Coq <     + split.

Coq <       * { split.

Coq <           - trivial.

Coq <           - trivial.

Coq <         }
Coq <       * trivial.

Coq <     + trivial.

Coq <   - assert True.

Coq <     { trivial. }
Coq <     assumption.

Remark: In ProofGeneral (emacs interface to coq), you must use bullets with this priority ordering to have a correct indentation: -, +, *. That is - must be the outer bullet and * the inner one, like in the example above.


Error messages:

  1. Error: No such unproven subgoal there is no proof under focus (because it has just been solved), so the command you are trying to use cannot be applied. You need to first focus the next proof by using the bullet corresponding to the right level (using an incorrect bullet also generates this message).
  2. Error: This proof is focused, but cannot be unfocused this way You are trying to use a bullet that is already in use or a } but the current subproof has not been fully solved.

7.3  Requesting information

7.3.1  Show.

This command displays the current goals.


Variants:

  1. Show num.
    Displays only the num-th subgoal.

    Error messages:
    1. No such goal
    2. No focused proof
  2. Show Implicits.
    Displays the current goals, printing the implicit arguments of constants.
  3. Show Implicits num.
    Same as above, only displaying the num-th subgoal.
  4. 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>.
  5. Show Tree.
    This command is deactivated.
  6. 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.
  7. 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.
  8. 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.
  9. Show Intros.
    This command is similar to the previous one, it simulates the naming process of an Intros.
  10. 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.

7.3.2  Guarded.

Some tactics (e.g. refine 8.2.3) 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 to verify 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."

7.4  Controlling the effect of proof editing commands

7.4.1  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.4.2  Unset Hyps Limit.

This command goes back to the default mode which is to print all available hypotheses.

7.4.3  Set Automatic Introduction.

The option Automatic Introduction controls the way binders are handled in assertion commands such as Theorem ident [binders] : form. When the option is set, which is the default, binders are automatically put in the local context of the goal to prove.

The option can be unset by issuing Unset Automatic Introduction. When the option is unset, binders are discharged on the statement to be proved and a tactic such as intro (see Section 8.3.1) has to be used to move the assumptions to the local context.