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 we call the local context of the goal. Initially, the local context is empty. It is enriched by the use of certain tactics (see mainly Section 8.3.5).

When a proof is achieved the message Proof completed is displayed. One can then store 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 [70, 6, 66, 73], Coq  stores proofs as terms of Cic. Those terms are called proof terms.

It is possible to edit several proofs at the same time: see section 7.1.8

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

7.1.1  Goal form.

This command switches Coq  to editing proof mode and sets form as the original goal. It associates the name Unnamed_thm to that goal.

Error messages:

1. the term form has type … which should be Set, Prop or Type

See also: Section 7.1.4

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.

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

   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  Theorem ident : form.

This command switches to interactive editing proof mode and declares ident as being the name of the original goal form. When declared as a Theorem, the name ident is known at all section levels: Theorem is a global lemma.

Error messages:

1. the term form has type … which should be Set, Prop or Type
2. identalready exists

   The name you provided already defined. You have then to choose another name.

Variants:

1. Lemma ident : form.

   It is equivalent to Theorem ident : form.

2. Remark ident : form.
   Fact ident : form.

   Used to have a different meaning, but are now equivalent to Theorem ident : form. They are kept for compatibility.

3. Definition ident : form.

   Analogous to Theorem, intended to be used in conjunction with Defined (see 1) in order to define a transparent constant.

4. Let ident : form.

   Analogous to Definition except that the definition is turned into a local definition on objects depending on it after closing the current section.

7.1.5  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.13.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  Suspend.

This command applies in proof editing mode. It switches back to the Coq toplevel, but without canceling the current proofs.

7.1.8  Resume.

This commands switches back to the editing of the last edited proof.

Error messages:

1. No proof-editing in progress

Variants:

1. Resume ident.

   Restarts the editing of the proof named ident. This can be used to navigate between currently edited proofs.

Error messages:

1. No such proof

7.1.9  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 intented 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.3.14.

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)
2. Undo stack would be exhausted

Variants:

1. Undo num.

   Repeats Undo num times.

7.2.2  Set Undo num.

This command changes the maximum number of Undo’s that will be possible when doing a proof. It only affects proofs started after this command, such that if you want to change the current undo limit inside a proof, you should first restart this proof.

7.2.3  Unset Undo.

This command resets the default number of possible Undo commands (which is currently 12).

7.2.4  Restart.

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

Error messages:

1. No focused proof to restart

7.2.5  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 num^th subgoal to prove.

7.2.6  Unfocus.

Turns off the focus mode.

7.3  Displaying 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 can be seen as a more structured way of displaying the state of the proof than that provided by Show Script. Instead of just giving the list of tactics that have been applied, it shows the derivation tree constructed by then. Each node of the tree contains the conclusion of the corresponding sub-derivation (i.e. a goal with its corresponding local context) and the tactic that has generated all the sub-derivations. The leaves of this tree are the goals which still remain to be proved.
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  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.3.3  Unset Hyps Limit.

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

7.4  DPL : A Declarative proof language for Coq (experimental)

An implementation of the DPL declarative proof language by Pierre Corbineau at the Radboud University Nijmegen (The Netherlands) is included in Coq.

Due to the experimental nature and hence the potentially unstable semantics of the language, its documentation is not included here. However, it can be found at :

http://www.cs.ru.nl/~corbineau/mmode.html