diff options
Diffstat (limited to 'doc/sphinx/proof-engine/proof-handling.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 595 |
1 files changed, 595 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 000000000..eba0db3ff --- /dev/null +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -0,0 +1,595 @@ +.. 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. 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 instance, in 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,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 :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. + + .. 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). + + .. cmdv:: Abort @ident + + Aborts the editing of the proof named :token:`ident` (in case you have + nested proofs). + + .. seealso:: :opt:`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 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 {+ @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 @collection1 + @collection2 + + Use section variables from the union of both collections. + See :ref:`nameaset` to know how to form a named collection. + + .. cmdv:: Proof using @collection1 - @collection2 + + 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 "@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 :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 := @expression + + 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. + +.. 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: + +.. 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 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 :token:`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 apply 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. + + .. exn:: No focused proof. + + .. cmdv:: Show @num + + Displays only the :token:`num` th subgoal. + + .. exn:: No such goal. + + + .. 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 + + 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>``. + + .. cmdv:: Show Proof + :name: 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 + :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 + + 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 + :token:`ident` + + .. example:: + .. coqtop:: all + + Show Match nat. + + .. exn:: Unknown inductive type. + + .. 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. + + +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 :n:`Theorem @ident {? @binders} : @term`. 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. + + +.. opt:: 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`. |