6.1 Switching on/off the proof editing mode

6.1 Switching on/off the proof editing mode

6.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. Proof objects can only be abstracted
  2. A goal should be a type
  3. repeated goal not permitted in refining mode



See also: section 6.1.3

6.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. Clash with previous constant ...
    The implicit name is already defined. You have then to provide explicitly a new name (see variant 2 below).
  3. 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 fatal mistake.



Variants:
  1. Save. Is equivalent to Qed.
  2. Save ident.
    Forces the name of the original goal to be ident.
  3. Save Theorem ident.
    Is equivalent to Save ident.
  4. Save Remark ident.
    Defines the proved term as a local constant that will not exist anymore after the end of the current section.
  5. Defined.
    Defines the proved term as a transparent constant.

6.1.3 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 message: (see section 6.1.1)


Variants:
  1. Lemma ident : form.
    Is equivalent to Theorem ident : form.
  2. Remark ident : form.
    Analogous to Theorem except that ident will be unknown after closing the current section.
  3. Fact ident : form.
    Analogous to Theorem except that ident is known after closing the current section but will be unknown after closing the section which is above the current section.
  4. Definition ident : form.
    Analogous to Theorem, intended to be used in conjunction with Defined (see 5) in order to define a transparent constant.

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


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

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

6.1.6 Suspend.

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

6.1.7 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


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.1.0.html at 8/10/98