diff options
Diffstat (limited to 'doc/sphinx/proof-engine/proof-handling.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 480 |
1 files changed, 235 insertions, 245 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index df8ef74f7..6d0b27728 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -8,12 +8,13 @@ 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 +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`. -When switching in editing proof mode, the prompt ``Coq <`` is changed into -``ident <`` where ``ident`` is the declared name of the theorem currently -edited. + +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 @@ -36,8 +37,8 @@ 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. + Coq raises this error message when one attempts to use a proof editing command + out of the proof editing mode. .. _proof-editing-mode: @@ -46,139 +47,149 @@ 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 +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). + 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. + 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. + .. exn:: Attempt to save an incomplete proof. -.. note:: + .. note:: - Sometimes an error occurs when building the proof term, because - tactics do not enforce completely the term construction - constraints. + 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. + 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) + .. cmdv:: Defined + :name: Defined -Defines the proved term as a transparent constant. + 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 + .. cmdv:: Save @ident + :name: Save -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. + 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 - :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 + This command is available in interactive editing mode to give up + the current proof and declare the initial goal as an axiom. - exact @term. Qed. +.. cmd:: Abort -That is, you have to give the full proof in one gulp, as a -proof term (see Section :ref:`applyingtheorems`). + 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. -.. cmdv:: Proof - :name: Proof (interactive proof) + .. exn:: No focused proof (No proof-editing in progress). -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``. + .. cmdv:: Abort @ident + Aborts the editing of the proof named :token:`ident` (in case you have + nested proofs). -See also: ``Proof with tactic.`` in Section -:ref:`tactics-implicit-automation`. + .. cmdv:: Abort All + Aborts all current goals. -.. cmd:: Proof using @ident1 ... @identn +.. cmd:: Proof @term + :name: Proof `term` -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. + 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`). -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. +.. 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`. -.. cmdv:: Proof using @ident1 ... @identn with @tactic + .. seealso:: :cmd:`Proof with` -in Section :ref:`tactics-implicit-automation`. +.. cmd:: Proof using {+ @ident } -.. cmdv:: Proof using All + 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. -Use all section variables. + 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 -.. cmdv:: Proof using Type + Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`. -.. cmdv:: Proof using + .. seealso:: :ref:`tactics-implicit-automation` -Use only section variables occurring in the statement. + .. cmdv:: Proof using All + Use all section variables. -.. cmdv:: Proof using Type* + .. 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. + Use only section variables occurring in the statement. + .. cmdv:: Proof using Type* -.. cmdv:: Proof using -(@ident1 ... @identn) + 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. -Use all section variables except :n:`@ident1` ... :n:`@identn`. + .. cmdv:: Proof using -({+ @ident }) + Use all section variables except the list of :token:`ident`. -.. cmdv:: Proof using @collection1 + @collection2 + .. 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 + .. cmdv:: Proof using @collection1 - @collection2 + Use section variables which are in the first collection but not in the + second one. -.. cmdv:: Proof using @collection - ( @ident1 ... @identn ) + .. 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 * + .. 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 ``-``. + Use section variables in the forward transitive closure of the collection. + The ``*`` operator binds stronger than ``+`` and ``-``. Proof using options @@ -189,14 +200,14 @@ 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``. + 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 + When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not provide one. .. _`nameaset`: @@ -204,80 +215,50 @@ The following options modify the behavior of ``Proof using``. 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``. +.. 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. -.. cmdv:: Collection Fewer := Some - z + .. example:: -Define the collection named "Fewer" containing only ``x`` and ``y``. + Define the collection named ``Some`` containing ``x``, ``y`` and ``z``:: + Collection Some := x y z. -.. cmdv:: Collection Many := Fewer + Some -.. cmdv:: Collection Many := Fewer - Some + Define the collection named ``Fewer`` containing only ``x`` and ``y``:: -Define the collection named "Many" containing the set union or set -difference of "Fewer" and "Some". + Collection Fewer := Some - z + 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 + Collection Many := Fewer + Some + Collection Many := Fewer - Some -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. + Define the collection named ``Many`` containing the set difference of + ``Fewer`` and the unnamed collection ``x y``:: - -.. 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. + Collection Many := Fewer - (x y) .. 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. + 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. + 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 @@ -290,7 +271,7 @@ Navigation in the proof tree .. cmdv:: Undo @num - Repeats Undo :n:`@num` times. + Repeats Undo :token:`num` times. .. cmdv:: Restart :name: Restart @@ -306,19 +287,22 @@ Navigation in the proof tree 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 :n:`@num` th subgoal to prove. + This focuses the attention on the :token:`num` th subgoal to prove. .. deprecated:: 8.8 - Prefer the use of bullets or - focusing brackets instead, including :n:`@num : %{` + 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 ``Focus`` command. + last :cmd:`Focus` command. .. deprecated:: 8.8 @@ -332,7 +316,7 @@ Navigation in the proof tree .. cmd:: %{ %| %} The command ``{`` (without a terminating period) focuses on the first - goal, much like ``Focus.`` does, however, the subproof can only be + 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. @@ -341,9 +325,9 @@ Navigation in the proof tree together with a suggestion about the right bullet or ``}`` to unfocus it or focus the next one. -.. cmdv:: @num: %{ + .. cmdv:: @num: %{ - This focuses on the :n:`@num` th subgoal to prove. + This focuses on the :token:`num` th subgoal to prove. Error messages: @@ -409,19 +393,19 @@ The following example script illustrates all these features: .. 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. + 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. + 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. + 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 ``}``. + You just finished a goal focused by ``{``, you must unfocus it with ``}``. Set Bullet Behavior ``````````````````` @@ -440,110 +424,116 @@ Requesting information .. cmd:: Show -This command displays the current goals. + This command displays the current goals. + .. exn:: No focused proof. -.. cmdv:: Show @num + .. cmdv:: Show @num -Displays only the :n:`@num`-th subgoal. + Displays only the :token:`num` th subgoal. -.. exn:: No such goal. -.. exn:: No focused proof. + .. exn:: No such goal. -.. 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. + .. cmdv:: Show @ident -.. example:: + 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. - .. coqtop:: all + .. example:: - Goal exists n, n = 0. - eexists ?[n]. - Show n. + .. coqtop:: all -.. cmdv:: Show Script + Goal exists n, n = 0. + eexists ?[n]. + Show n. -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 + .. cmdv:: Show Script + :name: Show Script -``<Your Tactic Text here>``. + 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 -.. cmdv:: Show Proof + ``<Your Tactic Text here>``. -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 Proof + :name: Show Proof -.. cmdv:: Show Conjectures + 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. -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 Conjectures + :name: Show Conjectures -.. cmdv:: Show Intro + 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. -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 Intro + :name: Show Intro -.. cmdv:: Show Intros + 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. -This command is similar to the previous one, it -simulates the naming process of an intros. + .. cmdv:: Show Intros + :name: Show Intros -.. cmdv:: Show Existentials + This command is similar to the previous one, it + simulates the naming process of an :tacn:`intros`. -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 Existentials + :name: Show Existentials -.. cmdv:: Show Match @ident + It displays the set of all uninstantiated + existential variables in the current proof tree, along with the type + and the context of each variable. -This variant displays a template of the Gallina -``match`` construct with a branch for each constructor of the type -:n:`@ident` + .. cmdv:: Show Match @ident -.. example:: - .. coqtop:: all + This variant displays a template of the Gallina + ``match`` construct with a branch for each constructor of the type + :token:`ident` - Show Match nat. + .. example:: + .. coqtop:: all -.. exn:: Unknown inductive type. + Show Match nat. -.. _ShowUniverses: + .. exn:: Unknown inductive type. -.. cmdv:: Show Universes + .. 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. + 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. + 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. + 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 @@ -552,23 +542,23 @@ 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. + 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. + 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. + 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 @@ -580,13 +570,13 @@ 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. + 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`. + 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`. |