path: root/doc/sphinx/proof-engine/proof-handling.rst

.. include:: ../replaces.rst
.. _proofhandling:

-------------------
 Proof handling
-------------------

In |Coq|’s proof editing mode all top-level commands documented in
Chapter :ref:`vernacularcommands` 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 :ref:`tactics`.
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 :ref:`gallina-assumptions`) and
the local variables and hypotheses of the theorem statement. It is enriched by
the use of certain tactics (see e.g. :tacn:`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*
:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those
terms are called *proof terms*.


.. exn:: No focused proof.

Coq raises this error message when one attempts to use a proof editing command
out of the proof editing mode.

.. _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 :cmd:`Theorem`. The
list of assertion commands is given in Section :ref:`Assertions`. The command
:cmd:`Goal` can also be used.

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

.. cmd:: Qed
   :name: Qed (interactive proof)

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.


.. exn:: Attempt to save an incomplete proof.

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

.. cmdv:: Defined
   :name: Defined (interactive proof)

Defines the proved term as a transparent constant.

.. cmdv:: Save @ident

Forces the name of the original goal to be :n:`@ident`. This
command (and the following ones) can only be used if the original goal
has been opened using the ``Goal`` command.

.. cmd:: Admitted
   :name: Admitted (interactive proof)

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

.. cmd:: Proof @term
   :name: Proof `term`

This command applies in proof editing mode. It is equivalent to

.. coqtop:: in

   exact @term. Qed.

That is, you have to give the full proof in one gulp, as a
proof term (see Section :ref:`applyingtheorems`).

.. cmdv:: Proof
   :name: Proof (interactive 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
:ref:`tactics-implicit-automation`.


.. cmd:: Proof using @ident1 ... @identn

This command applies in proof editing mode. It declares the set of
section variables (see :ref:`gallina-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.


.. cmdv:: Proof using @ident1 ... @identn with @tactic

in Section :ref:`tactics-implicit-automation`.

.. cmdv:: Proof using All

Use all section variables.


.. cmdv:: Proof using Type

.. cmdv:: Proof using

Use only section variables occurring in the statement.


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


.. cmdv:: Proof using -(@ident1 ... @identn)

Use all section variables except :n:`@ident1` ... :n:`@identn`.


.. cmdv:: Proof using @collection1 + @collection2


.. cmdv:: Proof using @collection1 - @collection2


.. cmdv:: Proof using @collection - ( @ident1 ... @identn )


.. cmdv:: Proof using @collection *

Use section variables being, respectively, in the set union, set
difference, set complement, set forward transitive closure. See
Section :ref:`nameaset` to know how to form a named collection. The ``*`` operator
binds stronger than ``+`` and ``-``.


Proof using options
```````````````````

The following options modify the behavior of ``Proof using``.


.. opt:: Default Proof Using "@expression"

   Use :n:`@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``.


.. opt:: Suggest Proof Using

   When ``Qed`` is performed, suggest a using annotation if the user did not
   provide one.

..  _`nameaset`:

Name a set of section hypotheses for ``Proof using``
````````````````````````````````````````````````````

.. cmd:: Collection @ident := @section_subset_expr

The command ``Collection`` can be used to name a set of section
hypotheses, with the purpose of making ``Proof using`` annotations more
compact.


.. cmdv:: Collection Some := x y z

Define the collection named "Some" containing ``x``, ``y`` and ``z``.


.. cmdv:: Collection Fewer := Some - z

Define the collection named "Fewer" containing only ``x`` and ``y``.


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

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


.. cmdv:: Collection Many := Fewer - (x y)

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


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


.. exn:: No focused proof (No proof-editing in progress).



.. cmdv::  Abort @ident

Aborts the editing of the proof named :n:`@ident`.

.. cmdv:: Abort All

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



.. cmd:: Existential @num := @term

This command instantiates an existential variable. :n:`@num` is an index in
the list of uninstantiated existential variables displayed by ``Show
Existentials`` (described in Section :ref:`requestinginformation`).

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 :tacn:`instantiate`.


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


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

.. cmd:: Undo

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

.. cmdv:: Undo @num

   Repeats Undo :n:`@num` times.

.. cmdv:: Restart
   :name: Restart

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

   .. exn:: No focused proof to restart.

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

.. cmdv:: Focus @num

   This focuses the attention on the :n:`@num` th subgoal to prove.

   .. deprecated:: 8.8

      Prefer the use of bullets or
      focusing brackets instead, including :n:`@num : %{`

.. cmd:: Unfocus

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

   .. deprecated:: 8.8

.. cmd:: Unfocused

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

.. _curly-braces:

.. cmd:: %{ %| %}

   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.

   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.

.. cmdv:: @num: %{

   This focuses on the :n:`@num` th subgoal to prove.

   Error messages:

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

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

   .. exn:: No such goal.
      :name: No such goal. (Focusing)

   .. exn:: Brackets only support the single numbered goal selector.

      See also error messages about bullets below.

.. _bullets:

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 ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period).

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.

.. note::

   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::
  .. coqtop:: all

    Goal (((True /\ True) /\ True) /\ True) /\ True.
    Proof.
    split.
    - split.
    + split.
    ** { split.
    - trivial.
    - trivial.
    }
    ** trivial.
    + trivial.
    - assert True.
    { trivial. }
    assumption.


.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished.

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

.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here.

You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here.

.. exn:: No such goal. Focus next goal with bullet @bullet.

You tried to applied a tactic but no goal where under focus. Using :n:`@bullet` is  mandatory here.

.. exn:: No such goal. Try unfocusing with %{.

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

Set Bullet Behavior
```````````````````
.. opt:: 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).

.. _requestinginformation:

Requesting information
----------------------


.. cmd:: Show

This command displays the current goals.


.. cmdv:: Show @num

Displays only the :n:`@num`-th subgoal.

.. exn:: No such goal.
.. exn:: No focused proof.

.. cmdv:: Show @ident

Displays the named goal :n:`@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 :ref:`existential-variables`) as in the following example.

.. example::

  .. coqtop:: all

    Goal exists n, n = 0.
    eexists ?[n].
    Show n.

.. cmdv:: 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>``.

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

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

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

.. cmdv:: Show Intros

This command is similar to the previous one, it
simulates the naming process of an intros.

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

.. cmdv:: Show Match @ident

This variant displays a template of the Gallina
``match`` construct with a branch for each constructor of the type
:n:`@ident`

.. example::
  .. coqtop:: all

     Show Match nat.

.. exn:: Unknown inductive type.

.. _ShowUniverses:

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


.. cmd:: Guarded

Some tactics (e.g. :tacn:`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 :cmd:`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
------------------------------------------------


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


.. opt:: Automatic Introduction

This option controls the way binders are handled
in assertion commands such as ``Theorem ident [binders] : form``. 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 :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
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.


.. cmd:: Optimize Proof

This command forces |Coq| to shrink the data structure used to represent
the ongoing proof.


.. cmd:: Optimize Heap

This command forces the |OCaml| runtime to perform a heap compaction.
This is in general an expensive operation.
See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
There is also an analogous tactic :tacn:`optimize_heap`.