products/Sources/formale Sprachen/Coq/doc/sphinx/proof-engine image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: gallina-extensions.rst   Sprache: Unknown

Spracherkennung für: .rst vermutete Sprache: Haskell {Haskell[356] Ada[569] Abap[790]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

.. _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. 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 :ref:`tactics`.

Coq user interfaces usually have a way of marking whether the user has
switched to proof editing mode. For instancein coqtop the prompt ``Coq <``   is changed into
:n:`@ident <`   where :token:`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,H89`, |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 :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

   This command is available in interactive editing proof mode when the
   proof is completed. Then :cmd:`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.
      :undocumented:

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

      Same as :cmd:`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 :ref:`performingcomputations`,
      :cmd:`Opaque`, :cmd:`Transparent`).

   .. cmdv:: Save @ident
      :name: Save

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

.. cmd:: Admitted

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

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

   .. cmdv::  Abort @ident

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

      .. seealso:: :flag:`Nested Proofs Allowed`

   .. cmdv:: Abort All

      Aborts all current goals.

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

   This command applies in proof editing mode. It is equivalent to
   :n:`exact @term. Qed.`
   That is, you have to give the full proof in one gulp, as a
   proof term (see Section :ref:`applyingtheorems`).

.. cmd:: Proof

   Is a no-op which is useful to delimit the sequence of tactic commands
   which start a proof, after a :cmd:`Theorem` command. It is a good practice to
   use :cmd:`Proof` as an opening parenthesis, closed in the script with a
   closing :cmd:`Qed`.

   .. seealso:: :cmd:`Proof with`

.. cmd:: Proof using {+ @ident }

   This command applies in proof editing mode. It declares the set of
   section variables (see :ref:`gallina-assumptions`) used by the proof.
   At :cmd:`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 a variable and ``a`` is a variable of type
   ``T``, then the commands ``Proof using a`` and ``Proof using T a``
   are equivalent.

   .. cmdv:: Proof using {+ @ident } with @tactic

      Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`.

      .. seealso:: :ref:`tactics-implicit-automation`

   .. cmdv:: Proof using All

      Use all section variables.

   .. cmdv:: Proof using {? Type }

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

      Use all section variables except the list of :token:`ident`.

   .. cmdv:: Proof using @collection__1 + @collection__2

      Use section variables from the union of both collections.
      See :ref:`nameaset` to know how to form a named collection.

   .. cmdv:: Proof using @collection__1 - @collection__2

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

   .. cmdv:: Proof using @collection - ({+ @ident })

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

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


.. opt:: Default Proof Using "@collection"
   :name: Default Proof Using

   Use :n:`@collection` 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 :cmd:`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 := @collection

   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)



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

   This command instantiates an existential variable. :token:`num` is an index in
   the list of uninstantiated existential variables displayed by :cmd:`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 :tacn:`instantiate`.

.. 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 :token:`num` times.

.. cmdv:: Restart
   :name: Restart

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

   .. exn:: No focused proof to restart.
      :undocumented:

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

   .. deprecated:: 8.8

      Prefer the use of bullets or focusing brackets (see below).

.. cmdv:: Focus @num

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

   .. deprecated:: 8.8

      Prefer the use of focusing brackets with a goal selector (see below).

.. cmd:: Unfocus

   This command restores to focus the goal that were suspended by the
   last :cmd:`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:

.. index:: {
           }

.. cmd:: {| %{ | %} }

   The command ``{`` (without a terminating period) focuses on the first
   goal, much like :cmd:`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.

   .. cmdv:: @num: %{

      This focuses on the :token:`num`\-th subgoal to prove.

   .. cmdv:: [@ident]: %{

      This focuses on the named goal :token:`ident`.

      .. note::

         Goals are just existential variables and existential variables do not
         get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
         You may also wrap this in an Ltac-definition like:

         .. coqtop:: in

            Ltac name_goal name := refine ?[name].

      .. seealso:: :ref:`existential-variables`

      .. example::

         This first example uses the Ltac definition above, and the named goals
         only serve for documentation.

         .. coqtop:: all

            Goal forall n, n + 0 = n.
            Proof.
            induction n; [ name_goal base | name_goal step ].
            [base]: {

         .. coqtop:: all

            reflexivity.

         .. coqtop:: in

            }

         .. coqtop:: all

            [step]: {

         .. coqtop:: all

            simpl.
            f_equal.
            assumption.
            }
            Qed.

         This can also be a way of focusing on a shelved goal, for instance:

         .. coqtop:: all

            Goal exists n : nat, n = n.
            eexists ?[x].
            reflexivity.
            [x]: exact 0.
            Qed.

   .. 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 (@num).
      :undocumented:

   .. exn:: No such goal (@ident).
      :undocumented:

   .. exn:: Brackets do not support multi-goal selectors.

      Brackets are used to focus on a single goal given either by its position
      or by its name if it has one.

  .. seealso:: The 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. Bullets are made of
repeated ``-``, ``+`` or ``*`` symbols:

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

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

.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished.

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

.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here.

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

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

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

.. FIXME: the :noindex: below works around a Sphinx issue.
   (https://github.com/sphinx-doc/sphinx/issues/4979)
   It should be removed once that issue is fixed.

.. exn:: No such goal. Try unfocusing with %}.
   :noindex:

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

Set Bullet Behavior
```````````````````
.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
   :name: Bullet Behavior

   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.

   .. exn:: No focused proof.
      :undocumented:

   .. cmdv:: Show @num

      Displays only the :token:`num`\-th subgoal.

      .. exn:: No such goal.
         :undocumented:

   .. cmdv:: Show @ident

      Displays the named goal :token:`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 abort

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

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

      .. deprecated:: 8.10

         Please use a text editor.

   .. cmdv:: Show Proof
      :name: Show Proof

      Displays the proof term generated by the tactics
      that have been applied so far. If the proof is incomplete, the term
      will contain holes, which correspond to subterms which are still to be
      constructed. Each hole is an existential variable, which appears as a
      question mark followed by an identifier.

   .. cmdv:: Show Conjectures
      :name: 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
      :name: 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 :tacn:`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 :tacn:`intro`
      into a qualified one such as ``intro y13``. In the case of a non-product
      goal, it prints nothing.

   .. cmdv:: Show Intros
      :name: Show Intros

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

   .. cmdv:: Show Existentials
      :name: Show Existentials

      Displays all open goals / existential variables in the current proof
      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
      :token:`ident`

      .. example::

         .. coqtop:: all

            Show Match nat.

      .. exn:: Unknown inductive type.
         :undocumented:

   .. cmdv:: Show Universes
      :name: 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.

.. _showing_diffs:

Showing differences between proof steps
---------------------------------------


Coq can automatically highlight the differences between successive proof steps and between
values in some error messages.
For example, the following screenshots of CoqIDE and coqtop show the application
of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
The conclusion is entirely in pale green because although it’s changed, no tokens were added
to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
second time with the old text, with deletions marked in red.  Also, since the hypotheses are
new, no line of old text is shown for them.

.. comment screenshot produced with:
   Inductive ev : nat -> Prop :=
   | ev_0 : ev 0
   | ev_SS : forall n : nat, ev n -> ev (S (S n)).

   Fixpoint double (n:nat) :=
     match n with
     | O => O
     | S n' => S (S (double n'))
     end.

   Goal forall n, ev n -> exists k, n = double k.
   intros n E.

..

  .. image:: ../_static/diffs-coqide-on.png
     :alt: |CoqIDE| with Set Diffs on

..

  .. image:: ../_static/diffs-coqide-removed.png
     :alt: |CoqIDE| with Set Diffs removed

..

  .. image:: ../_static/diffs-coqtop-on3.png
     :alt: coqtop with Set Diffs on

This image shows an error message with diff highlighting in CoqIDE:

..

  .. image:: ../_static/diffs-error-message.png
     :alt: |CoqIDE| error message with diffs

How to enable diffs
```````````````````

.. opt:: Diffs {| "on" | "off" | "removed" }
   :name: Diffs

   The “on” setting highlights added tokens in green, while the “removed” setting
   additionally reprints items with removed tokens in red.  Unchanged tokens in
   modified items are shown with pale green or red.  Diffs in error messages
   use red and green for the compared values; they appear regardless of the setting.
   (Colors are user-configurable.)

For coqtop, showing diffs can be enabled when starting coqtop with the
``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
within Coq.  You will need to provide the ``-color on|auto`` command-line option when
you start coqtop in either case.

Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
variable.  See section :ref:`customization-by-environment-variables`.  Diffs
use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.

In CoqIDE, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
command in CoqIDE.  You can change the background colors shown for diffs from the
``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
lets you control other attributes of the highlights, such as the foreground
color, bold, italic, underline and strikeout.

As of June 2019, Proof General can also display Coq-generated proof diffs automatically.
Please see the PG documentation section
"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
for details.

How diffs are calculated
````````````````````````

Diffs are calculated as follows:

1. Select the old proof state to compare to, which is the proof state before
   the last tactic that changed the proof.  Changes that only affect the view
   of the proof, such as ``all: swap 1 2``, are ignored.

2. For each goal in the new proof state, determine what old goal to compare
   it to—the one it is derived from or is the same as.  Match the hypotheses by
   name (order is ignored), handling compacted items specially.

3. For each hypothesis and conclusion (the “items”) in each goal, pass
   them as strings to the lexer to break them into tokens.  Then apply the
   Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting.

Notes:

* Aside from the highlights, output for the "on" option should be identical
  to the undiffed output.
* Goals completed in the last proof step will not be shown even with the
  "removed" setting.

.. comment The following screenshots show diffs working with multiple goals and with compacted
   hypotheses.  In the first one, notice that the goal ``P 1`` is not highlighted at
   all after the split because it has not changed.

    .. todo: Use this script and remove the screenshots when COQ_COLORS
      works for coqtop in sphinx
    .. coqtop:: none

      Set Diffs "on".
      Parameter P : nat -> Prop.
      Goal P 1 /\ P 2 /\ P 3.

    .. coqtop:: out

      split.

    .. coqtop:: all abort

      2: split.

  ..

    .. coqtop:: none

      Set Diffs "on".
      Goal forall n m : nat, n + m = m + n.
      Set Diffs "on".

    .. coqtop:: out

       intros n.

    .. coqtop:: all abort

      intros m.

This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal
with 2 goals.  Notice that the goal ``P 1`` is not highlighted at all after
the split because it has not changed.

..

  .. image:: ../_static/diffs-coqide-multigoal.png
     :alt: coqide with Set Diffs on with multiple goals

This is how diffs may appear after applying a :tacn:`intro` tactic that results
in compacted hypotheses:

..

  .. image:: ../_static/diffs-coqide-compacted.png
     :alt: coqide with Set Diffs on with compacted hyptotheses

Controlling the effect of proof editing commands
------------------------------------------------


.. opt:: Hyps Limit @num
   :name: Hyps Limit

   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:: Nested Proofs Allowed

   When turned on (it is off by default), this option enables support for nested
   proofs: a new assertion command can be inserted before the current proof is
   finished, in which case Coq will temporarily switch to the proof of this
   *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
   or :cmd:`Defined`), its statement will be made available (as if it had been
   proved before starting the previous proof) and Coq will switch back to the
   proof of the previous assertion.


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

[ Dauer der Verarbeitung: 0.153 Sekunden  ]