Merge PR #7162: Sphinx doc chapter 7

1 files changed, 592 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
new file mode 100644
index 0000000000..52cde52c69
--- /dev/null
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -0,0 +1,592 @@
+.. 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:`TODO_gallina_assumptions`)
+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
+:ref:`managingthelocalcontext`).
+
+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* [[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.
+
+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:
+
+.. cmd:: Theorem @ident [@binders] : @form.
+
+The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The
+command ``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 ``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.
+
+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.
+
+This command is available in interactive editing proof mode to give up
+the current proof and declare the initial goal as an axiom.
+
+
+.. cmd:: Proof @term.
+
+This command applies in proof editing mode. It is equivalent to
+
+.. cmd:: 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.
+
+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:`setimpautotactics`.
+
+
+.. cmd:: Proof using @ident1 ... @identn.
+
+This command applies in proof editing mode. It declares the set of
+section variables (see :ref:`TODO-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:`setimpautotactics`.
+
+.. 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``.
+
+
+.. cmdv:: Set 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``.
+
+
+.. cmdv:: Set 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``
+````````````````````````````````````````````````````
+
+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 instantiate.
+
+
+See also: ``instantiate (num:= term).`` in Section
+:ref:`TODO-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.
+
+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.
+
+*This command is deprecated since 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.
+
+*This command is deprecated since 8.8.*
+
+.. cmd:: Unfocused.
+
+Succeeds if the proof is fully unfocused, fails is there are some
+goals out of focus.
+
+
+.. 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
+
+.. exn:: Brackets only support the single numbered goal selector
+
+
+See also error messages about bullets below.
+
+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
+```````````````````
+
+The bullet behavior can be controlled by the following commands.
+
+.. opt:: Bullet Behavior "None".
+
+This makes bullets inactive.
+
+.. opt:: Bullet Behavior "Strict Subproofs".
+
+This makes bullets active (this is the default behavior).
+
+
+
+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:`exvariables`) 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
+
+.. exn:: 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. refine :ref:`applyingtheorems`) 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 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 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 :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 ``optimize_heap`` (see~:ref:`tactic-optimizeheap`)