diff options
Diffstat (limited to 'doc/sphinx/proof-engine/proof-handling.rst')
-rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 633 |
1 files changed, 318 insertions, 315 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 52cde52c6..eba0db3ff 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -8,176 +8,190 @@ 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 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`). +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* [[How80]_, -[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq| -stores proofs as terms of |Cic|. Those terms -are called *proof terms*. +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. -.. 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: 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 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. -The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The -command ``Goal`` can also be used. +.. cmd:: Goal @form -.. 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 -.. 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. -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:: -.. 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. + 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. + .. 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 -.. cmd:: Admitted. + This command is available in interactive editing mode to give up + the current proof and declare the initial goal as an axiom. -This command is available in interactive editing proof 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. -.. cmd:: Proof @term. + .. exn:: No focused proof (No proof-editing in progress). -This command applies in proof editing mode. It is equivalent to + .. cmdv:: Abort @ident -.. cmd:: exact @term. Qed. + Aborts the editing of the proof named :token:`ident` (in case you have + nested proofs). -That is, you have to give the full proof in one gulp, as a -proof term (see Section :ref:`applyingtheorems`). + .. seealso:: :opt:`Nested Proofs Allowed` + .. cmdv:: Abort All -.. cmdv:: Proof. + Aborts all current goals. -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``. +.. 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`). -See also: ``Proof with tactic.`` in Section -:ref:`setimpautotactics`. +.. 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`. -.. cmd:: Proof using @ident1 ... @identn. + .. seealso:: :cmd:`Proof with` -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. +.. cmd:: Proof using {+ @ident } -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. + 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 @ident1 ... @identn with @tactic. + .. cmdv:: Proof using {+ @ident } with @tactic -in Section :ref:`setimpautotactics`. + Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`. -.. cmdv:: Proof using All. + .. seealso:: :ref:`tactics-implicit-automation` -Use all section variables. + .. cmdv:: Proof using All + Use all section variables. -.. cmdv:: Proof using Type. + .. cmdv:: Proof using {? Type } -.. cmdv:: Proof using. + Use only section variables occurring in the statement. -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 Type*. + .. cmdv:: Proof using -({+ @ident }) -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 the list of :token:`ident`. + .. cmdv:: Proof using @collection1 + @collection2 -.. cmdv:: Proof using -(@ident1 ... @identn). + Use section variables from the union of both collections. + See :ref:`nameaset` to know how to form a named collection. -Use all section variables except :n:`@ident1` ... :n:`@identn`. + .. cmdv:: Proof using @collection1 - @collection2 + Use section variables which are in the first collection but not in the + second one. -.. cmdv:: Proof using @collection1 + @collection2 . + .. 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 @collection1 - @collection2 . + .. cmdv:: Proof using @collection * - -.. 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 ``-``. + Use section variables in the forward transitive closure of the collection. + The ``*`` operator binds stronger than ``+`` and ``-``. Proof using options @@ -186,176 +200,151 @@ Proof using options The following options modify the behavior of ``Proof using``. -.. cmdv:: Set Default Proof Using "@expression". +.. 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``. -.. cmdv:: Set Suggest Proof Using. +.. opt:: Suggest Proof Using -When ``Qed`` is performed, suggest a using annotation if the user did not -provide one. + 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`` ```````````````````````````````````````````````````` -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). +.. cmd:: Collection @ident := @expression -Define the collection named "Many" containing the set difference of -"Fewer" and the unnamed collection ``x`` ``y``. + This can be used to name a set of section + hypotheses, with the purpose of making ``Proof using`` annotations more + compact. + .. example:: -.. cmd:: Abort. + Define the collection named ``Some`` containing ``x``, ``y`` and ``z``:: -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. + Collection Some := x y z. + Define the collection named ``Fewer`` containing only ``x`` and ``y``:: -.. exn:: No focused proof (No proof-editing in progress) + 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 -.. cmdv:: Abort @ident. + Define the collection named ``Many`` containing the set difference of + ``Fewer`` and the unnamed collection ``x y``:: -Aborts the editing of the proof named :n:`@ident`. + Collection Many := Fewer - (x y) -.. cmdv:: Abort All. -Aborts all current goals, switching back to the |Coq| -toplevel. +.. 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`. -.. cmd:: Existential @num := @term. + 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`. -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`). +.. cmd:: Grab Existential Variables -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. + 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 -.. cmd:: Undo. - -This command cancels the effect of the last command. Thus, it -backtracks one step. + This command cancels the effect of the last command. Thus, it + backtracks one step. +.. cmdv:: Undo @num -.. cmdv:: Undo @num. + Repeats Undo :token:`num` times. -Repeats Undo :n:`@num` times. +.. cmdv:: Restart + :name: Restart -.. cmdv:: Restart. + This command restores the proof editing process to the original goal. -This command restores the proof editing process to the original goal. + .. exn:: No focused proof to restart. +.. cmd:: Focus -.. exn:: No focused proof to restart + 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 -.. cmd:: Focus. + Prefer the use of bullets or focusing brackets (see below). -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 :token:`num` th subgoal to prove. -.. cmdv:: Focus @num. + .. deprecated:: 8.8 -This focuses the attention on the :n:`@num` th subgoal to -prove. + Prefer the use of focusing brackets with a goal selector (see below). -*This command is deprecated since 8.8*: prefer the use of bullets or -focusing brackets instead, including :n:`@num : %{` +.. cmd:: Unfocus -.. cmd:: Unfocus. + This command restores to focus the goal that were suspended by the + last :cmd:`Focus` command. -This command restores to focus the goal that were suspended by the -last ``Focus`` command. + .. deprecated:: 8.8 -*This command is deprecated since 8.8.* +.. cmd:: Unfocused -.. cmd:: Unfocused. - -Succeeds if the proof is fully unfocused, fails is there are some -goals out of focus. + Succeeds if the proof is fully unfocused, fails if there are some + goals out of focus. +.. _curly-braces: .. cmd:: %{ %| %} -The command ``{`` (without a terminating period) focuses on the first -goal, much like ``Focus.`` does, however, the subproof can only be -unfocused when it has been fully solved ( *i.e.* when there is no -focused goal left). Unfocusing is then handled by ``}`` (again, without a -terminating period). See also example in next section. + 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. + 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: %{ + .. cmdv:: @num: %{ -This focuses on the :n:`@num` th subgoal to prove. + This focuses on the :token:`num` th subgoal to prove. -Error messages: + Error messages: -.. exn:: This proof is focused, but cannot be unfocused this way + .. 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. + You are trying to use ``}`` but the current subproof has not been fully solved. -.. exn:: No such goal + .. exn:: No such goal. + :name: No such goal. (Focusing) -.. exn:: Brackets only support the single numbered goal selector + .. exn:: Brackets only support the single numbered goal selector. + See also error messages about bullets below. -See also error messages about bullets below. +.. _bullets: Bullets ``````` @@ -404,171 +393,185 @@ The following example script illustrates all these features: assumption. -.. exn:: Wrong bullet @bullet1 : Current bullet @bullet2 is not finished. +.. 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. +.. 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 ``````````````````` +.. opt:: Bullet Behavior %( "None" %| "Strict Subproofs" %) -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). + 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. +.. 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:`exvariables`) 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` + + .. example:: + .. coqtop:: all - Show Match nat. + Show Match nat. -.. exn:: Unknown inductive type + .. exn:: Unknown inductive type. -.. exn:: 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. +.. 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. + 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 ``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 ------------------------------------------------ -.. opt:: Hyps Limit @num. +.. 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 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 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:: 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. +.. opt:: Nested Proofs Allowed -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. + 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 @@ -578,15 +581,15 @@ 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. +.. 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. +.. 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`) + 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`. |