diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 46 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 622 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 249 |
5 files changed, 509 insertions, 469 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 247d5d899c..009758319b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -178,6 +178,7 @@ Sequence A sequence is an expression of the following form: .. tacn:: @expr ; @expr + :name: ; The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, @@ -193,6 +194,7 @@ Different tactics can be applied to the different goals using the following form: .. tacn:: [> {*| @expr }] + :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i=0,...,n and all have to be tactics. The :n:`v__i` is applied to the @@ -240,6 +242,7 @@ We can restrict the application of a tactic to a subset of the currently focused goals with: .. tacn:: @toplevel_selector : @expr + :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: @@ -290,6 +293,7 @@ For loop There is a for loop that repeats a tactic :token:`num` times: .. tacn:: do @num @expr + :name: do :n:`@expr` is evaluated to ``v`` which must be a tactic value. This tactic value ``v`` is applied :token:`num` times. Supposing :token:`num` > 1, after the @@ -303,6 +307,7 @@ Repeat loop We have a repeat loop with: .. tacn:: repeat @expr + :name: repeat :n:`@expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is applied to each focused goal independently. If the application succeeds, the @@ -316,6 +321,7 @@ Error catching We can catch the tactic errors with: .. tacn:: try @expr + :name: try :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused goal independently. If the application of @@ -329,6 +335,7 @@ Detecting progress We can check if a tactic made progress with: .. tacn:: progress expr + :name: progress :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` is applied to each focued subgoal independently. If the application of ``v`` @@ -343,6 +350,7 @@ Backtracking branching We can branch with the following structure: .. tacn:: @expr__1 + @expr__2 + :name: + (backtracking branching) :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied to @@ -365,6 +373,7 @@ restrict to a local, left biased, branching and consider the first tactic to work (i.e. which does not fail) among a panel of tactics: .. tacn:: first [{*| @expr}] + :name: first The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values, for i=1,...,n. Supposing n>1, it applies, in each focused @@ -396,6 +405,7 @@ Yet another way of branching without backtracking is the following structure: .. tacn:: @expr__1 || @expr__2 + :name: || (left-biased branching) :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is @@ -410,6 +420,7 @@ Generalized biased branching The tactic .. tacn:: tryif @expr__1 then @expr__2 else @expr__3 + :name: tryif is a generalization of the biased-branching tactics above. The expression :n:`@expr__1` is evaluated to :n:`v__1`, which is then @@ -430,6 +441,7 @@ Another way of restricting backtracking is to restrict a tactic to a single success *a posteriori*: .. tacn:: once @expr + :name: once :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, @@ -443,6 +455,7 @@ Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @expr + :name: exactly_once :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied if it has at most one success. If ``v`` fails, @@ -467,6 +480,7 @@ Checking the failure Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @expr + :name: assert_fails This behaves like :n:`tryif @expr then fail 0 tac "succeeds" else idtac`. @@ -477,6 +491,7 @@ Coq provides a derived tactic to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @expr + :name: assert_suceeds This behaves like :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. @@ -488,6 +503,7 @@ We may consider the first to solve (i.e. which generates no subgoal) among a panel of tactics: .. tacn:: solve [{*| @expr}] + :name: solve The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values, for i=1,...,n. Supposing n>1, it applies :n:`v__1` to @@ -508,6 +524,7 @@ The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but it appears in the proof script. .. tacn:: idtac {* message_token} + :name: idtac This prints the given tokens. Strings and integers are printed literally. If a (term) variable is given, its contents are printed. @@ -516,6 +533,7 @@ Failing ~~~~~~~ .. tacn:: fail + :name: fail This is the always-failing tactic: it does not solve any goal. It is useful for defining other tacticals since it can be caught by @@ -543,6 +561,7 @@ Failing This is a combination of the previous variants. .. tacv:: gfail + :name: gfail This variant fails even if there are no goals left. @@ -565,6 +584,7 @@ We can force a tactic to stop if it has not finished after a certain amount of time: .. tacn:: timeout @num @expr + :name: timeout :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds @@ -586,6 +606,7 @@ Timing a tactic A tactic execution can be timed: .. tacn:: time @string @expr + :name: time evaluates :n:`@expr` and displays the time the tactic expression ran, whether it fails or successes. In case of several successes, the time for each successive @@ -600,6 +621,7 @@ Tactic expressions that produce terms can be timed with the experimental tactic .. tacn:: time_constr expr + :name: time_constr which evaluates :n:`@expr ()` and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is @@ -610,10 +632,12 @@ tactic implemented using the tactics .. tacn:: restart_timer @string + :name: restart_timer and .. tacn:: finish_timing {? @string} @string + :name: finish_timing which (re)set and display an optionally named timer, respectively. The parenthesized string argument to :n:`finish_timing` is also optional, and @@ -951,6 +975,7 @@ Testing boolean expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: guard @test + :name: guard The :tacn:`guard` tactic tests a boolean expression, and fails if the expression evaluates to false. If the expression evaluates to true, it succeeds @@ -976,6 +1001,7 @@ Proving a subgoal as a separate lemma ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: abstract @expr + :name: abstract From the outside, :n:`abstract @expr` is the same as :n:`solve @expr`. Internally it saves an auxiliary lemma called ``ident_subproofn`` where @@ -1000,6 +1026,7 @@ Proving a subgoal as a separate lemma don’t play well with asynchronous proofs. .. tacv:: transparent_abstract @expr + :name: transparent_abstract Save the subproof in a transparent lemma rather than an opaque one. @@ -1220,28 +1247,33 @@ performance bug. Unset Ltac Profiling. .. tacn:: start ltac profiling + :name: start ltac profiling This tactic behaves like :tacn:`idtac` but enables the profiler. .. tacn:: stop ltac profiling + :name: stop ltac profiling Similarly to :tacn:`start ltac profiling`, this tactic behaves like :tacn:`idtac`. Together, they allow you to exclude parts of a proof script from profiling. .. tacn:: reset ltac profile + :name: reset ltac profile This tactic behaves like the corresponding vernacular command and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. .. tacn:: show ltac profile + :name: show ltac profile This tactic behaves like the corresponding vernacular command and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. .. tacn:: show ltac profile @string + :name: show ltac profile This tactic behaves like the corresponding vernacular command and allow displaying and resetting the profile from tactic scripts for @@ -1261,6 +1293,7 @@ Run-time optimization tactic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: optimize_heap + :name: optimize_heap This tactic behaves like :n:`idtac`, except that running it compacts the heap in the OCaml run-time system. It is analogous to the Vernacular diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index a77b127ebe..86c94bab36 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -58,13 +58,14 @@ 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 + :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. +added to the environment as an opaque constant. .. exn:: Attempt to save an incomplete proof @@ -81,6 +82,7 @@ a while when the proof is large. In some exceptional cases one may even incur a memory overflow. .. cmdv:: Defined. + :name: Defined (interactive proof) Defines the proved term as a transparent constant. @@ -91,6 +93,7 @@ command (and the following ones) can only be used if the original goal has been opened using the ``Goal`` command. .. cmd:: Admitted. + :name: Admitted (interactive proof) This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom. @@ -105,8 +108,8 @@ This command applies in proof editing mode. It is equivalent to That is, you have to give the full proof in one gulp, as a proof term (see Section :ref:`applyingtheorems`). - .. cmdv:: Proof. + :name: Proof (interactive 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 @@ -182,49 +185,51 @@ 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 ``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 := @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. +.. cmdv:: Collection Some := x y z Define the collection named "Some" containing ``x``, ``y`` and ``z``. -.. cmdv:: Collection Fewer := Some - 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. +.. 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). +.. cmdv:: Collection Many := Fewer - (x y) Define the collection named "Many" containing the set difference of -"Fewer" and the unnamed collection ``x`` ``y``. +"Fewer" and the unnamed collection ``x`` ``y`` .. cmd:: Abort. @@ -288,6 +293,7 @@ backtracks one step. Repeats Undo :n:`@num` times. .. cmdv:: Restart. + :name: Restart This command restores the proof editing process to the original goal. @@ -424,11 +430,11 @@ Set Bullet Behavior The bullet behavior can be controlled by the following commands. -.. opt:: Bullet Behavior "None". +.. opt:: Bullet Behavior "None" This makes bullets inactive. -.. opt:: Bullet Behavior "Strict Subproofs". +.. opt:: Bullet Behavior "Strict Subproofs" This makes bullets active (this is the default behavior). @@ -551,7 +557,7 @@ 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 @@ -560,7 +566,7 @@ When unset, it goes back to the default mode which is to print all available hypotheses. -.. opt:: Automatic Introduction. +.. opt:: Automatic Introduction This option controls the way binders are handled in assertion commands such as ``Theorem ident [binders] : form``. When the diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 074c6f1e28..977a5b8fad 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -493,7 +493,10 @@ inferred from the whole context of the goal (see for example section Definitions ~~~~~~~~~~~ -The pose tactic allows to add a defined constant to a proof context. +.. tacn:: pose + :name: pose (ssreflect) + +This tactic allows to add a defined constant to a proof context. |SSR| generalizes this tactic in several ways. In particular, the |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: @@ -1349,6 +1352,7 @@ Discharge The general syntax of the discharging tactical ``:`` is: .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch } + :name: ... : ... (ssreflect) .. prodn:: d_item ::= {? @occ_switch %| @clear_switch } @term @@ -1500,9 +1504,11 @@ side of an equation. The abstract tactic ``````````````````` -The ``abstract`` tactic assigns an ``abstract`` constant previously -introduced with the ``[: name ]`` intro pattern -(see section :ref:`introduction_ssr`). +.. tacn:: abstract: {+ d_item} + :name abstract (ssreflect) + +This tactic assigns an abstract constant previously introduced with the ``[: +name ]`` intro pattern (see section :ref:`introduction_ssr`). In a goal like the following:: @@ -1809,6 +1815,8 @@ of a :token:`d_item` immediately following this ``/`` switch, using the syntax: .. tacv:: case: {+ @d_item } / {+ @d_item } + :name: case (ssreflect) + .. tacv:: elim: {+ @d_item } / {+ @d_item } The :token:`d_item` on the right side of the ``/`` switch are discharged as @@ -2132,7 +2140,7 @@ tactic using the given second tactic, and fails if it does not succeed. Its analogue .. tacn:: @tactic ; first by @tactic - :name: first + :name: first (ssreflect) tries to solve the first subgoal generated by the first tactic using the second given tactic, and fails if it does not succeed. @@ -2212,7 +2220,7 @@ Iteration thanks to the do tactical, whose general syntax is: .. tacn:: do {? @mult } ( @tactic | [ {+| @tactic } ] ) - :name: do + :name: do (ssreflect) where :token:`mult` is a *multiplier*. @@ -2749,12 +2757,9 @@ type classes inference. No inference for ``t``. Unresolved instances are quantified in the (inferred) type of ``t`` and abstracted in ``t``. +.. opt:: SsrHave NoTCResolution -The behavior of |SSR| 1.4 and below (never resolve type classes) -can be restored with the option - -.. cmd:: Set SsrHave NoTCResolution. - + This option restores the behavior of |SSR| 1.4 and below (never resolve type classes). Variants: the suff and wlog tactics ``````````````````````````````````` @@ -3727,6 +3732,7 @@ We provide a special tactic unlock for unfolding such definitions while removing “locks”, e.g., the tactic: .. tacn:: unlock {? @occ_switch } @ident + :name: unlock replaces the occurrence(s) of :token:`ident` coded by the :token:`occ_switch` with the corresponding body. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 08aa7110d1..7a45272f25 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -51,20 +51,15 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. cmd:: Set Default Goal Selector @toplevel_selector. +.. opt:: Default Goal Selector @toplevel_selector -After using this command, the default selector – used when no selector -is specified when applying a tactic – is set to the chosen value. The -initial value is 1, hence the tactics are, by default, applied to the -first goal. Using Set Default Goal Selector ‘‘all’’ will make is so -that tactics are, by default, applied to every goal simultaneously. -Then, to apply a tactic tac to the first goal only, you can write -1:tac. Although more selectors are available, only ‘‘all’’ or a single -natural number are valid default goal selectors. - -.. cmd:: Test Default Goal Selector. - -This command displays the current default selector. + This option controls the default selector – used when no selector is + specified when applying a tactic – is set to the chosen value. The initial + value is 1, hence the tactics are, by default, applied to the first goal. + Using value ``all`` will make is so that tactics are, by default, applied to + every goal simultaneously. Then, to apply a tactic tac to the first goal + only, you can write ``1:tac``. Although more selectors are available, only + ``all`` or a single natural number are valid default goal selectors. .. _bindingslist: @@ -123,14 +118,12 @@ following syntax: The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that -occurrences have to be selected in the hypotheses named :n:`@ident`. If no numbers -are given for hypothesis :n:`@ident`, then all the occurrences of `term` in the -hypothesis are selected. If numbers are given, they refer to occurrences of -`term` when the term is printed using option ``Set Printing All`` (see -:ref:`printing_constructions_full`), counting from left to right. In -particular, occurrences of `term` in implicit arguments (see -:ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) -are counted. +occurrences have to be selected in the hypotheses named :n:`@ident`. If no +numbers are given for hypothesis :n:`@ident`, then all the occurrences of `term` +in the hypothesis are selected. If numbers are given, they refer to occurrences +of `term` when the term is printed using option :opt:`Printing All`, counting +from left to right. In particular, occurrences of `term` in implicit arguments +(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. If a minus sign is given between at and the list of occurrences, it negates the condition so that the clause denotes all the occurrences @@ -175,6 +168,7 @@ term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then .. exn:: Not an exact proof. .. tacv:: eexact @term. + :name: eexact This tactic behaves like exact but is able to handle terms and goals with meta-variables. @@ -188,6 +182,7 @@ the goal. If it is the case, the subgoal is proved. Otherwise, it fails. .. exn:: No such assumption. .. tacv:: eassumption + :name: eassumption This tactic behaves like assumption but is able to handle goals with meta-variables. @@ -240,6 +235,7 @@ useful to advanced users. cast around it. .. tacv:: simple refine @term + :name: simple refine This tactic behaves like refine, but it does not shelve any subgoal. It does not perform any beta-reduction either. @@ -250,6 +246,7 @@ useful to advanced users. resolution of typeclasses. .. tacv:: simple notypeclasses refine @term + :name: simple notypeclasses refine This tactic behaves like ``simple refine`` except it performs typechecking without resolution of typeclasses. @@ -320,6 +317,7 @@ instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. .. tacv:: simple apply @term. + :name: simple apply This behaves like ``apply`` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example @@ -342,11 +340,12 @@ does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} + :name: simple eapply This summarizes the different syntaxes for ``apply`` and ``eapply``. .. tacv:: lapply @term - :name: `lapply + :name: lapply This tactic applies to any goal, say :g:`G`. The argument term has to be well-formed in the current context, its type being reducible to a non-dependent @@ -437,7 +436,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: -.. opt:: Set Universal Lemma Under Conjunction. +.. opt:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). @@ -522,8 +521,8 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. constructor of :g:`I`, then ``constructor i`` is equivalent to ``intros; apply c``:sub:`i`. -.. exn:: Not an inductive product. -.. exn:: Not enough constructors. +.. exn:: Not an inductive product +.. exn:: Not enough constructors .. tacv:: constructor @@ -541,34 +540,39 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. The terms in the @bindings_list are checked in the context where constructor is executed and not in the context where @apply is executed (the introductions are not taken into account). .. tacv:: split + :name: split This applies only if :g:`I` has a single constructor. It is then equivalent to :n:`constructor 1.`. It is typically used in the case of a conjunction :g:`A` :math:`\wedge` :g:`B`. -.. exn:: Not an inductive goal with 1 constructor. +.. exn:: Not an inductive goal with 1 constructor .. tacv:: exists @val + :name: exists This applies only if :g:`I` has a single constructor. It is then equivalent to :n:`intros; constructor 1 with @bindings_list.` It is typically used in the case of an existential quantification :math:`\exists`:g:`x, P(x).` -.. exn:: Not an inductive goal with 1 constructor. +.. exn:: Not an inductive goal with 1 constructor .. tacv:: exists @bindings_list This iteratively applies :n:`exists @bindings_list`. .. tacv:: left + :name: left + .. tacv:: right + :name: right These tactics apply only if :g:`I` has two constructors, for instance in the case of a disjunction :g:`A` :math:`\vee` :g:`B`. Then, they are respectively equivalent to ``constructor 1`` and ``constructor 2``. -.. exn:: Not an inductive goal with 2 constructors. +.. exn:: Not an inductive goal with 2 constructors .. tacv:: left with @bindings_list .. tacv:: right with @bindings_list @@ -579,15 +583,25 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. for the appropriate ``i``. .. tacv:: econstructor + :name: econstructor + .. tacv:: eexists + :name: eexists + .. tacv:: esplit + :name: esplit + .. tacv:: eleft + :name: eleft + .. tacv:: eright + :name: eright - These tactics and their variants behave like ``constructor``, ``exists``, - ``split``, ``left``, ``right`` and their variants but they introduce - existential variables instead of failing when the instantiation of a - variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). + These tactics and their variants behave like :tacn:`constructor`, + :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their variants + but they introduce existential variables instead of failing when the + instantiation of a variable cannot be found (cf. :tacn:`eapply` and + :tacn:`apply`). .. _managingthelocalcontext: @@ -618,7 +632,7 @@ the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. .. exn:: No product even after head-reduction. -.. exn:: ident is already used. +.. exn:: @ident is already used. .. tacv:: intros @@ -829,15 +843,10 @@ quantification or an implication. so that all the arguments of the i-th constructors of the corresponding inductive type are introduced can be controlled with the following option: - .. cmd:: Set Bracketing Last Introduction Pattern. - - Force completion, if needed, when the last introduction pattern is a - disjunctive or conjunctive pattern (this is the default). - - .. cmd:: Unset Bracketing Last Introduction Pattern. + .. opt:: Bracketing Last Introduction Pattern - Deactivate completion when the last introduction pattern is a disjunctive or - conjunctive pattern. + Force completion, if needed, when the last introduction pattern is a + disjunctive or conjunctive pattern (on by default). .. tacn:: clear @ident :name: clear @@ -857,6 +866,7 @@ quantification or an implication. This is equivalent to :n:`clear @ident. ... clear @ident.` .. tacv:: clearbody @ident + :name: clearbody This tactic expects :n:`@ident` to be a local definition then clears its body. Otherwise said, this tactic turns a definition into an assumption. @@ -878,7 +888,7 @@ quantification or an implication. it. .. tacn:: revert {+ @ident} - :name: revert ... + :name: revert This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses (possibly defined) to the goal, if this respects dependencies. This tactic is @@ -994,6 +1004,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: eset (@ident {+ @binder} := @term ) in @goal_occurrences .. tacv:: eset @term in @goal_occurrences + :name: eset While the different variants of :tacn:`set` expect that no existential variables are generated by the tactic, :n:`eset` removes this constraint. In @@ -1001,6 +1012,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. :tacn:`epose`, i.e. when the :`@term` does not occur in the goal. .. tacv:: remember @term as @ident + :name: remember This behaves as :n:`set (@ident:= @term ) in *` and using a logical (Leibniz’s) equality instead of a local definition. @@ -1018,6 +1030,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: eremember @term as @ident .. tacv:: eremember @term as @ident in @goal_occurrences .. tacv:: eremember @term as @ident eqn:@ident + :name: eremember + While the different variants of :n:`remember` expect that no existential variables are generated by the tactic, :n:`eremember` removes this constraint. @@ -1124,6 +1138,7 @@ Controlling the proof flow .. exn:: Variable @ident is already declared .. tacv:: eassert form as intro_pattern by tactic + :name: eassert .. tacv:: assert (@ident := @term) @@ -1133,6 +1148,7 @@ Controlling the proof flow to prove it. .. tacv:: pose proof @term {? as intro_pattern} + :name: pose proof This tactic behaves like :n:`assert T {? as intro_pattern} by exact @term` where :g:`T` is the type of :g:`term`. In particular, @@ -1146,6 +1162,7 @@ Controlling the proof flow the tactic, :n:`epose proof` removes this constraint. .. tacv:: enough (@ident : form) + :name: enough This adds a new hypothesis of name :n:`@ident` asserting :n:`form` to the goal the tactic :n:`enough` is applied to. A new subgoal stating :n:`form` is @@ -1171,13 +1188,17 @@ Controlling the proof flow applied to all of them. .. tacv:: eenough (@ident : form) by tactic + :name: eenough + .. tacv:: eenough form by tactic + .. tacv:: eenough form as intro_pattern by tactic While the different variants of :n:`enough` expect that no existential variables are generated by the tactic, :n:`eenough` removes this constraint. -.. tacv:: cut form +.. tacv:: cut @form + :name: cut This tactic applies to any goal. It implements the non-dependent case of the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference @@ -1187,6 +1208,7 @@ Controlling the proof flow .. tacv:: specialize (ident {* @term}) {? as intro_pattern} .. tacv:: specialize ident with @bindings_list {? as intro_pattern} + :name: specialize The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or @@ -1239,7 +1261,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :g:`Set Printing All`). + expression printed using option :opt:`Printing All`). .. tacv:: generalize @term as @ident @@ -1428,6 +1450,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) dependent premises of the type of :n:`@term` (see :ref:`syntax of bindings <bindingslist>`). .. tacv:: edestruct @term + :name: edestruct This tactic behaves like :n:`destruct @term` except that it does not fail if the instance of a dependent premises of the type of :n:`@term` is not @@ -1454,6 +1477,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) the effects of the `with`, `as`, `eqn:`, `using`, and `in` clauses. .. tacv:: case term + :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without recursion. It behaves as :n:`elim @term` but using a case-analysis @@ -1463,14 +1487,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Analogous to :n:`elim @term with @bindings_list` above. -.. tacv:: ecase @term -.. tacv:: ecase @term with @bindings_list +.. tacv:: ecase @term {? with @bindings_list } + :name: ecase In case the type of :n:`@term` has dependent premises, or dependent premises whose values are not inferable from the :n:`with @bindings_list` clause, :n:`ecase` turns them into existential variables to be resolved later on. .. tacv:: simple destruct @ident + :name: simple destruct This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident` is a quantified variable of the goal. @@ -1561,6 +1586,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) premises of the type of :n:`term` (see :ref:`bindings list <bindingslist>`). .. tacv:: einduction @term + :name: einduction This tactic behaves like :tacn:`induction` except that it does not fail if some dependent premise of the type of :n:`@term` is not inferable. Instead, @@ -1633,6 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) (see :ref:`bindings list <bindingslist>`). .. tacv:: eelim @term + :name: eelim In case the type of :n:`@term` has dependent premises, this turns them into existential variables to be resolved later on. @@ -1651,7 +1678,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) These are the most general forms of ``elim`` and ``eelim``. It combines the effects of the ``using`` clause and of the two uses of the ``with`` clause. -.. tacv:: elimtype form +.. tacv:: elimtype @form + :name: elimtype The argument :n:`form` must be inductively defined. :n:`elimtype I` is equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the @@ -1661,6 +1689,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`elimtype I; 2:exact t.` .. tacv:: simple induction @ident + :name: simple induction This tactic behaves as :n:`intros until @ident; elim @ident` when :n:`@ident` is a quantified variable of the goal. @@ -1745,6 +1774,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) other ones need not be further generalized. .. tacv:: dependent destruction @ident + :name: dependent destruction This performs the generalization of the instance :n:`@ident` but uses ``destruct`` instead of induction on the generalized hypothesis. This gives @@ -1854,6 +1884,7 @@ See also: :ref:`advanced-recursive-functions` .. tacv:: ediscriminate @num .. tacv:: ediscriminate @term {? with @bindings_list} + :name: ediscriminate This works the same as ``discriminate`` but if the type of :n:`@term`, or the type of the hypothesis referred to by :n:`@num`, has uninstantiated @@ -1933,6 +1964,7 @@ the use of a sigma type is avoided. .. tacv:: einjection @num .. tacv:: einjection @term {? with @bindings_list} + :name: einjection This works the same as :n:`injection` but if the type of :n:`@term`, or the type of the hypothesis referred to by :n:`@num`, has uninstantiated @@ -1960,17 +1992,19 @@ the use of a sigma type is avoided. to the number of new equalities. The original equality is erased if it corresponds to an hypothesis. -It is possible to ensure that :n:`injection @term` erases the original -hypothesis and leaves the generated equalities in the context rather -than putting them as antecedents of the current goal, as if giving -:n:`injection @term as` (with an empty list of names). To obtain this -behavior, the option ``Set Structural Injection`` must be activated. This -option is off by default. +.. opt:: Structural Injection + + This option ensure that :n:`injection @term` erases the original hypothesis + and leaves the generated equalities in the context rather than putting them + as antecedents of the current goal, as if giving :n:`injection @term as` + (with an empty list of names). This option is off by default. + +.. opt:: Keep Proof Equalities -By default, ``injection`` only creates new equalities between :n:`@terms` whose -type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for -objects that are proofs of a statement in :g:`Prop`. This behavior can be -turned off by setting the option ``Set Keep Proof Equalities``. + By default, :tacn:`injection` only creates new equalities between :n:`@terms` + whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special + behavior for objects that are proofs of a statement in :g:`Prop`. This option + controls this behavior. .. tacn:: inversion @ident :name: inversion @@ -1996,8 +2030,8 @@ turned off by setting the option ``Set Keep Proof Equalities``. equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort - :g:`Prop`). This behavior can be turned off by using the option ``Set Keep - Proof Equalities``. + :g:`Prop`). This behavior can be turned off by using the option + :opt`Keep Proof Equalities`. .. tacv:: inversion @num @@ -2122,6 +2156,7 @@ turned off by setting the option ``Set Keep Proof Equalities``. :n:`dependent inversion_clear @ident with @term`. .. tacv:: simple inversion @ident + :name: simple inversion It is a very primitive inversion tactic that derives all the necessary equalities but it does not simplify the constraints as ``inversion`` does. @@ -2422,6 +2457,7 @@ subgoals. leading to failure if these n rewrites are not possible. .. tacv:: erewrite @term + :name: erewrite This tactic works as :n:`rewrite @term` but turning unresolved bindings into existential variables, if any, instead of @@ -2468,6 +2504,7 @@ subgoals. clause argument must not contain any type of nor value of. .. tacv:: cutrewrite <- (@term = @term) + :cutrewrite: This tactic is deprecated. It acts like :n:`replace @term with @term`, or, equivalently as :n:`enough (@term = @term) as <-`. @@ -2511,30 +2548,30 @@ unfolded and cleared. context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` or :n:`@ident := t` exists, with :n:`@ident` not occurring in `t`. - .. note:: - The behavior of subst can be controlled using option ``Set Regular Subst - Tactic.`` When this option is activated, subst also deals with the - following corner cases: + .. opt:: Regular Subst Tactic - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the option, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or - `t′` respectively. - + The presence of a recursive equation which without the option would - be a cause of failure of :tacn:`subst`. - + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` - and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the - option would be a cause of failure of :tacn:`subst`. + This option controls the behavior of :tacn:`subst`. When it is + activated, :tacn:`subst` also deals with the following corner cases: - Additionally, it prevents a local definition such as :n:`@ident := t` to be - unfolded which otherwise it would exceptionally unfold in configurations - containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` - with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. The option is on by - default. + + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` + and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` + or :n:`u = @ident`:sub:`2`; without the option, a second call to + subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + `t′` respectively. + + The presence of a recursive equation which without the option would + be a cause of failure of :tacn:`subst`. + + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` + and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + option would be a cause of failure of :tacn:`subst`. + + Additionally, it prevents a local definition such as :n:`@ident := t` to be + unfolded which otherwise it would exceptionally unfold in configurations + containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` + with `u′` not a variable. Finally, it preserves the initial order of + hypotheses, which without the option it may break. The option is on by + default. .. tacn:: stepl @term @@ -2548,30 +2585,37 @@ where `eq` is typically a setoid equality. The application of :n:`stepl @term` then replaces the goal by :n:`R @term @term` and adds a new goal stating :n:`eq @term @term`. -Lemmas are added to the database using the command ``Declare Left Step @term.`` +.. cmd:: Declare Left Step @term + + Adds :n:`@term` to the database used by :tacn:`stepl`. + The tactic is especially useful for parametric setoids which are not accepted as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see :ref:`Generalizedrewriting`). .. tacv:: stepl @term by tactic - This applies :n:`stepl @term` then applies tactic to the second goal. + This applies :n:`stepl @term` then applies tactic to the second goal. .. tacv:: stepr @term stepr @term by tactic + :name: stepr + + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq + y z -> R x z`. - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq - y z -> R x z` and are registered using the command ``Declare Right Step - @term.`` + .. cmd:: Declare Right Step @term + + Adds :n:`@term` to the database used by :tacn:`stepr`. .. tacn:: change @term :name: change - This tactic applies to any goal. It implements the rule ``Conv`` given in - :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` - with `U` providing that `U` is well-formed and that `T` and `U` are - convertible. + This tactic applies to any goal. It implements the rule ``Conv`` given in + :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` + with `U` providing that `U` is well-formed and that `T` and `U` are + convertible. .. exn:: Not convertible @@ -2709,6 +2753,7 @@ the conversion in hypotheses :n:`{+ @ident}`. and :n:`lazy beta delta -{+ @qualid} iota zeta`. .. tacv:: vm_compute + :name: vm_compute This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. @@ -2718,6 +2763,7 @@ the conversion in hypotheses :n:`{+ @ident}`. reflection-based tactics. .. tacv:: native_compute + :name: native_compute This tactic evaluates the goal by compilation to Objective Caml as described in :cite:`FullReduction`. If Coq is running in native code, it can be @@ -3108,7 +3154,7 @@ the :tacn:`auto` and :tacn:`trivial` tactics: .. opt:: Info Auto .. opt:: Debug Auto .. opt:: Info Trivial -.. opt:: Info Trivial +.. opt:: Debug Trivial See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` @@ -3263,188 +3309,203 @@ observationally different from the legacy one. The general command to add a hint to some databases :n:`{+ @ident}` is -.. cmd:: Hint hint_definition : {+ @ident} +.. cmd:: Hint @hint_definition : {+ @ident} -**Variants:** + .. cmdv:: Hint @hint_definition -.. cmd:: Hint hint_definition + No database name is given: the hint is registered in the core database. - No database name is given: the hint is registered in the core database. + .. cmdv:: Local Hint @hint_definition : {+ @ident} -.. cmd:: Local Hint hint_definition : {+ @ident} + This is used to declare hints that must not be exported to the other modules + that require and import the current module. Inside a section, the option + Local is useless since hints do not survive anyway to the closure of + sections. - This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the option - Local is useless since hints do not survive anyway to the closure of - sections. + .. cmdv:: Local Hint @hint_definition -.. cmd:: Local Hint hint_definition + Idem for the core database. - Idem for the core database. + .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} + :name: Hint Resolve -The ``hint_definition`` is one of the following expressions: + This command adds :n:`simple apply @term` to the hint list with the head + symbol of the type of :n:`@term`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + associated :n:`@pattern` is inferred from the conclusion of the type of + :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@term` does not start with a product the tactic added in the hint list + is :n:`exact @term`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @term` is also stored in + the hints list. If the inferred type of :n:`@term` contains a dependent + quantification on a variable which occurs only in the premisses of the type + and not in its conclusion, no instance could be inferred for the variable by + unification with the goal. In this case, the hint is added to the hint list + of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A + typical example of a hint that is used only by :tacn:`eauto` is a transitivity + lemma. -+ :n:`Resolve @term {? | {? @num} {? @pattern}}` - This command adds :n:`simple apply @term` to the hint list with the head symbol of the type of - :n:`@term`. The cost of that hint is the number of subgoals generated by - :n:`simple apply @term` or :n:`@num` if specified. The associated :n:`@pattern` - is inferred from the conclusion of the type of :n:`@term` or the given - :n:`@pattern` if specified. In case the inferred type of :n:`@term` does not - start with a product the tactic added in the hint list is :n:`exact @term`. - In case this type can however be reduced to a type starting with a product, - the tactic :n:`simple apply @term` is also stored in the hints list. If the - inferred type of :n:`@term` contains a dependent quantification on a variable - which occurs only in the premisses of the type and not in its conclusion, no - instance could be inferred for the variable by unification with the goal. In - this case, the hint is added to the hint list of :tacn:`eauto` instead of the - hint list of auto and a warning is printed. A typical example of a hint that - is used only by ``eauto`` is a transitivity lemma. + .. exn:: @term cannot be used as a hint - .. exn:: @term cannot be used as a hint + The head symbol of the type of :n:`@term` is a bound variable such that + this tactic cannot be associated to a constant. - The head symbol of the type of :n:`@term` is a bound variable such that - this tactic cannot be associated to a constant. + .. cmdv:: Hint Resolve {+ @term} - **Variants:** + Adds each :n:`Hint Resolve @term`. - + :n:`Resolve {+ @term}` - Adds each :n:`Resolve @term`. + .. cmdv:: Hint Resolve -> @term - + :n:`Resolve -> @term` - Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentionned - before, the tactic actually used is a restricted version of ``apply``). + Adds the left-to-right implication of an equivalence as a hint (informally + the hint will be used as :n:`apply <- @term`, although as mentionned + before, the tactic actually used is a restricted version of + :tacn:`apply`). - + :n:`Resolve <- @term` - Adds the right-to-left implication of an equivalence as a hint. + .. cmdv:: Resolve <- @term -+ :n:`Immediate @term` - This command adds :n:`simple apply @term; trivial` to the hint list associated - with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are - not solved immediately by the ``trivial`` tactic (which only tries tactics - with cost 0).This command is useful for theorems such as the symmetry of - equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited - use in order to avoid useless proof-search.The cost of this tactic (which - never generates subgoals) is always 1, so that it is not used by ``trivial`` - itself. + Adds the right-to-left implication of an equivalence as a hint. - .. exn:: @term cannot be used as a hint + .. cmdv:: Hint Immediate @term + :name: Hint Immediate - **Variants:** + This command adds :n:`simple apply @term; trivial` to the hint list associated + with the head symbol of the type of :n:`@ident` in the given database. This + tactic will fail if all the subgoals generated by :n:`simple apply @term` are + not solved immediately by the ``trivial`` tactic (which only tries tactics + with cost 0).This command is useful for theorems such as the symmetry of + equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited + use in order to avoid useless proof-search. The cost of this tactic (which + never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` + itself. - + :n:`Immediate {+ @term}` - Adds each :n:`Immediate @term`. + .. exn:: @term cannot be used as a hint -+ :n:`Constructors @ident` - If :n:`@ident` is an inductive type, this command adds all its constructors as - hints of type Resolve. Then, when the conclusion of current goal has the form - :n:`(@ident ...)`, ``auto`` will try to apply each constructor. + .. cmdv:: Immediate {+ @term} - .. exn:: @ident is not an inductive type + Adds each :n:`Hint Immediate @term`. - **Variants:** + .. cmdv:: Hint Constructors @ident + :name: Hint Constructors - + :n:`Constructors {+ @ident}` - Adds each :n:`Constructors @ident`. + If :n:`@ident` is an inductive type, this command adds all its constructors as + hints of type ``Resolve``. Then, when the conclusion of current goal has the form + :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. -+ :n:`Unfold @qualid` - This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :n:`@ident`. - Its cost is 4. + .. exn:: @ident is not an inductive type - **Variants:** + .. cmdv:: Hint Constructors {+ @ident} - + :n:`Unfold {+ @ident}` - Adds each :n:`Unfold @ident`. + Adds each :n:`Hint Constructors @ident`. -+ :n:`Transparent`, :n:`Opaque @qualid` - This adds a transparency hint to the database, making :n:`@qualid` a - transparent or opaque constant during resolution. This information is used - during unification of the goal with any lemma in the database and inside the - discrimination network to relax or constrain it in the case of discriminated - databases. + .. cmdv:: Hint Unfold @qualid + :name: Hint Unfold - **Variants:** + This adds the tactic :n:`unfold @qualid` to the hint list that will only be + used when the head constant of the goal is :n:`@ident`. + Its cost is 4. - + :n:`Transparent`, :n:`Opaque {+ @ident}` - Declares each :n:`@ident` as a transparent or opaque constant. + .. cmdv:: Hint Unfold {+ @ident} -+ :n:`Extern @num {? @pattern} => tactic` - This hint type is to extend ``auto`` with tactics other than ``apply`` and - ``unfold``. For that, we must specify a cost, an optional :n:`@pattern` and a - :n:`tactic` to execute. Here is an example:: - - Hint Extern 4 (~(_ = _)) => discriminate. - - Now, when the head of the goal is a disequality, ``auto`` will try - discriminate if it does not manage to solve the goal with hints with a - cost less than 4. One can even use some sub-patterns of the pattern in - the tactic script. A sub-pattern is a question mark followed by an - identifier, like ``?X1`` or ``?X2``. Here is an example: - - .. example:: - .. coqtop:: reset all - - Require Import List. - Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. - Goal forall a b:list (nat * nat), {a = b} + {a <> b}. - Info 1 auto with eqdec. - -+ :n:`Cut @regexp` - - .. warning:: these hints currently only apply to typeclass - proof search and the ``typeclasses eauto`` tactic (:ref:`typeclasses-eauto`). - - This command can be used to cut the proof-search tree according to a regular - expression matching paths to be cut. The grammar for regular expressions is - the following. Beware, there is no operator precedence during parsing, one can - check with ``Print HintDb`` to verify the current cut expression: - - .. productionlist:: `regexp` - e : ident hint or instance identifier - :|_ any hint - :| e\|e′ disjunction - :| e e′ sequence - :| e * Kleene star - :| emp empty - :| eps epsilon - :| ( e ) - - The `emp` regexp does not match any search path while `eps` - matches the empty path. During proof search, the path of - successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note Hint Extern’s do not have - an associated identifier). - Before applying any hint :n:`@ident` the current path `p` extended with - :n:`@ident` is matched against the current cut expression `c` associated to - the hint database. If matching succeeds, the hint is *not* applied. The - semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the - initial cut expression being `emp`. - -+ :n:`Mode @qualid {* (+ | ! | -)}` - This sets an optional mode of use of the identifier :n:`@qualid`. When - proof-search faces a goal that ends in an application of :n:`@qualid` to - arguments :n:`@term ... @term`, the mode tells if the hints associated to - :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, - ``!`` or ``-`` items that specify if an argument of the identifier is to be - treated as an input (``+``), if its head only is an input (``!``) or an output - (``-``) of the identifier. For a mode to match a list of arguments, input - terms and input heads *must not* contain existential variables or be - existential variables respectively, while outputs can be any term. Multiple - modes can be declared for a single identifier, in that case only one mode - needs to match the arguments for the hints to be applied.The head of a term - is understood here as the applicative head, or the match or projection - scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is - especially useful for typeclasses, when one does not want to support default - instances and avoid ambiguity in general. Setting a parameter of a class as an - input forces proof-search to be driven by that index of the class, with ``!`` - giving more flexibility by allowing existentials to still appear deeper in the - index but not at its head. + Adds each :n:`Hint Unfold @ident`. -.. note:: - One can use an ``Extern`` hint with no pattern to do pattern-matching on - hypotheses using ``match goal`` with inside the tactic. + .. cmdv:: Hint %( Transparent %| Opaque %) @qualid + :name: Hint ( Transparent | Opaque ) + + This adds a transparency hint to the database, making :n:`@qualid` a + transparent or opaque constant during resolution. This information is used + during unification of the goal with any lemma in the database and inside the + discrimination network to relax or constrain it in the case of discriminated + databases. + + .. cmdv:: Hint %(Transparent | Opaque) {+ @ident} + + Declares each :n:`@ident` as a transparent or opaque constant. + + .. cmdv:: Hint Extern @num {? @pattern} => tactic + + This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and + :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a + :n:`@tactic` to execute. + + .. example:: + + .. coqtop:: in + + Hint Extern 4 (~(_ = _)) => discriminate. + + Now, when the head of the goal is a disequality, ``auto`` will try + discriminate if it does not manage to solve the goal with hints with a + cost less than 4. One can even use some sub-patterns of the pattern in + the tactic script. A sub-pattern is a question mark followed by an + identifier, like ``?X1`` or ``?X2``. Here is an example: + + .. example:: + + .. coqtop:: reset all + + Require Import List. + Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. + Goal forall a b:list (nat * nat), {a = b} + {a <> b}. + Info 1 auto with eqdec. + + .. cmdv:: Hint Cut @regexp + + .. warning:: + + These hints currently only apply to typeclass proof search and the + :tacn:`typeclasses eauto` tactic. + + This command can be used to cut the proof-search tree according to a regular + expression matching paths to be cut. The grammar for regular expressions is + the following. Beware, there is no operator precedence during parsing, one can + check with :cmd:`Print HintDb` to verify the current cut expression: + + .. productionlist:: `regexp` + e : ident hint or instance identifier + :|_ any hint + :| e\|e′ disjunction + :| e e′ sequence + :| e * Kleene star + :| emp empty + :| eps epsilon + :| ( e ) + + The `emp` regexp does not match any search path while `eps` + matches the empty path. During proof search, the path of + successive successful hints on a search branch is recorded, as a + list of identifiers for the hints (note Hint Extern’s do not have + an associated identifier). + Before applying any hint :n:`@ident` the current path `p` extended with + :n:`@ident` is matched against the current cut expression `c` associated to + the hint database. If matching succeeds, the hint is *not* applied. The + semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the + initial cut expression being `emp`. + + .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + + This sets an optional mode of use of the identifier :n:`@qualid`. When + proof-search faces a goal that ends in an application of :n:`@qualid` to + arguments :n:`@term ... @term`, the mode tells if the hints associated to + :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, + ``!`` or ``-`` items that specify if an argument of the identifier is to be + treated as an input (``+``), if its head only is an input (``!``) or an output + (``-``) of the identifier. For a mode to match a list of arguments, input + terms and input heads *must not* contain existential variables or be + existential variables respectively, while outputs can be any term. Multiple + modes can be declared for a single identifier, in that case only one mode + needs to match the arguments for the hints to be applied.The head of a term + is understood here as the applicative head, or the match or projection + scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is + especially useful for typeclasses, when one does not want to support default + instances and avoid ambiguity in general. Setting a parameter of a class as an + input forces proof-search to be driven by that index of the class, with ``!`` + giving more flexibility by allowing existentials to still appear deeper in the + index but not at its head. + + .. note:: + + One can use an ``Extern`` hint with no pattern to do pattern-matching on + hypotheses using ``match goal`` with inside the tactic. Hint databases defined in the Coq standard library @@ -3578,31 +3639,28 @@ We propose a smooth transitional path by providing the ``Loose Hint Behavior`` option which accepts three flags allowing for a fine-grained handling of non-imported hints. -**Variants:** - -.. cmd:: Set Loose Hint Behavior "Lax" +.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) - This is the default, and corresponds to the historical behavior, that - is, hints defined outside of a section have a global scope. + This option accepts three values, which control the behavior of hints w.r.t. + :cmd:`Import`: -.. cmd:: Set Loose Hint Behavior "Warn" + - "Lax": this is the default, and corresponds to the historical behavior, + that is, hints defined outside of a section have a global scope. - When set, it outputs a warning when a non-imported hint is used. Note that - this is an over-approximation, because a hint may be triggered by a run that - will eventually fail and backtrack, resulting in the hint not being actually - useful for the proof. + - "Warn": outputs a warning when a non-imported hint is used. Note that this + is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being + actually useful for the proof. -.. cmd:: Set Loose Hint Behavior "Strict" - - When set, it changes the behavior of an unloaded hint to a immediate fail - tactic, allowing to emulate an import-scoped hint mechanism. + - "Strict": changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. .. _tactics-implicit-automation: Setting implicit automation tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Proof with tactic +.. cmd:: Proof with @tactic This command may be used to start a proof. It defines a default tactic to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``. @@ -3616,11 +3674,11 @@ Setting implicit automation tactics Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmdv:: Proof using {+ @ident} with tactic + .. cmdv:: Proof using {+ @ident} with @tactic Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmd:: Declare Implicit Tactic tactic + .. cmd:: Declare Implicit Tactic @tactic This command declares a tactic to be used to solve implicit arguments that Coq does not know how to solve by unification. It is used every @@ -3684,11 +3742,12 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. an instantiation of `x` is necessary. .. tacv:: dtauto + :name: dtauto - While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``, - :tacn:`dtauto` recognizes also all inductive types with one constructors and - no indices, i.e. record-style connectives. + While :tacn:`tauto` recognizes inductively defined connectives isomorphic to + the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``, + :tacn:`dtauto` recognizes also all inductive types with one constructors and + no indices, i.e. record-style connectives. .. tacn:: intuition @tactic :name: intuition @@ -3734,17 +3793,10 @@ some incompatibilities. Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive types with one constructors and no indices, i.e. record-style connectives. -Some aspects of the tactic :tacn:`intuition` can be controlled using options. -To avoid that inner negations which do not need to be unfolded are -unfolded, use: - -.. cmd:: Unset Intuition Negation Unfolding +.. opt:: Intuition Negation Unfolding - -To do that all negations of the goal are unfolded even inner ones -(this is the default), use: - -.. cmd:: Set Intuition Negation Unfolding + Controls whether :tacn:`intuition` unfolds inner negations which do not need + to be unfolded. This option is on by default. .. tacn:: rtauto :name: rtauto @@ -3768,14 +3820,15 @@ first- order reasoning, written by Pierre Corbineau. It is not restricted to usual logical connectives but instead may reason about any first-order class inductive definition. -The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto -with \*`, it can be reset locally or globally using the ``Set Firstorder -Solver`` tactic vernacular command and printed using ``Print Firstorder -Solver``. +.. opt:: Firstorder Solver + + The default tactic used by :tacn:`firstorder` when no rule applies is + :g:`auto with *`, it can be reset locally or globally using this option and + printed using :cmd:`Print Firstorder Solver`. .. tacv:: firstorder @tactic - Tries to solve the goal with :n:`@tactic` when no logical rule may apply. + Tries to solve the goal with :n:`@tactic` when no logical rule may apply. .. tacv:: firstorder using {+ @qualid} @@ -3792,8 +3845,9 @@ Solver``. This combines the effects of the different variants of :tacn:`firstorder`. -Proof-search is bounded by a depth parameter which can be set by -typing the ``Set Firstorder Depth n`` vernacular command. +.. opt:: Firstorder Depth @natural + + This option controls the proof-search depth bound. .. tacn:: congruence :name: congruence @@ -4013,6 +4067,7 @@ symbol :g:`=`. .. tacv:: esimplify_eq @num .. tacv:: esimplify_eq @term {? with @bindings_list} + :name: esimplify_eq This works the same as ``simplify_eq`` but if the type of :n:`@term`, or the type of the hypothesis referred to by :n:`@num`, has uninstantiated @@ -4024,7 +4079,7 @@ symbol :g:`=`. :n:`intro @ident; simplify_eq @ident`. .. tacn:: dependent rewrite -> @ident - :name: dependent rewrite -> + :name: dependent rewrite This tactic applies to any goal. If :n:`@ident` has type :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each @@ -4292,7 +4347,7 @@ This tactics reverses the list of the focused goals. This tactic moves all goals under focus to a shelf. While on the shelf, goals will not be focused on. They can be solved by unification, or they can be called back into focus with the command - :tacn:`Unshelve`. + :cmd:`Unshelve`. .. tacv:: shelve_unifiable @@ -4308,8 +4363,7 @@ This tactics reverses the list of the focused goals. all:shelve_unifiable. reflexivity. -.. tacn:: Unshelve - :name: Unshelve +.. cmd:: Unshelve This command moves all the goals on the shelf (see :tacn:`shelve`) from the shelf into focus, by appending them to the end of the current diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index da4034fb8a..692ff294a6 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -39,6 +39,7 @@ This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid` denotes a global constant. .. cmdv:: About @qualid. + :name: About This displays various information about the object denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive, @@ -61,6 +62,7 @@ Variants: .. cmdv:: Inspect @num. + :name: Inspect This command displays the :n:`@num` last objects of the current environment, including sections and modules. @@ -77,14 +79,11 @@ section. Flags, Options and Tables ----------------------------- -|Coq| configurability is based on flags (e.g. ``Set Printing All`` in -Section :ref:`printing_constructions_full`), options (e.g. ``Set Printing Widthinteger`` in Section -:ref:`controlling-display`), or tables (e.g. ``Add Printing Record ident``, in Section -:ref:`record-types`). -The names of flags, options and tables are made of non-empty sequences of identifiers -(conventionally with capital initial -letter). The general commands handling flags, options and tables are -given below. +|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options +(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The +names of flags, options and tables are made of non-empty sequences of +identifiers (conventionally with capital initial letter). The general commands +handling flags, options and tables are given below. .. TODO : flag is not a syntax entry @@ -93,7 +92,6 @@ given below. This command switches :n:`@flag` on. The original state of :n:`@flag` is restored when the current module ends. - Variants: .. cmdv:: Local Set @flag. @@ -107,6 +105,11 @@ This command switches :n:`@flag` on. The original state of :n:`@flag` is *not* restored at the end of the module. Additionally, if set in a file, :n:`@flag` is switched on when the file is `Require`-d. +.. cmdv:: Export Set @flag. + + This command switches :n:`@flag` on. The original state + of :n:`@flag` is restored at the end of the current module, but :n:`@flag` + is switched on when this module is imported. .. cmd:: Unset @flag. @@ -128,6 +131,11 @@ This command switches :n:`@flag` off. The original state of :n:`@flag` is *not* restored at the end of the module. Additionally, if set in a file, :n:`@flag` is switched off when the file is `Require`-d. +.. cmdv:: Export Unset @flag. + + This command switches :n:`@flag` off. The original state + of :n:`@flag` is restored at the end of the current module, but :n:`@flag` + is switched off when this module is imported. .. cmd:: Test @flag. @@ -157,11 +165,16 @@ original value of :n:`@option` is *not* restored at the end of the module. Additionally, if set in a file, :n:`@option` is set to value when the file is `Require`-d. +.. cmdv:: Export Set @option. + + This command set :n:`@option` to :n:`@value`. The original state + of :n:`@option` is restored at the end of the current module, but :n:`@option` + is set to :n:`@value` when this module is imported. .. cmd:: Unset @option. -This command resets option to its default value. + This command turns off :n:`@option`. Variants: @@ -169,17 +182,20 @@ Variants: .. cmdv:: Local Unset @option. -This command resets :n:`@option` to its default -value. The original state of :n:`@option` is restored when the current -*section* ends. + This command turns off :n:`@option`. The original state of :n:`@option` is restored when the current + *section* ends. .. cmdv:: Global Unset @option. -This command resets :n:`@option` to its default -value. The original state of :n:`@option` is *not* restored at the end of the -module. Additionally, if unset in a file, :n:`@option` is reset to its -default value when the file is `Require`-d. + This command turns off :n:`@option`. The original state of :n:`@option` is *not* restored at the end of the + module. Additionally, if unset in a file, :n:`@option` is reset to its + default value when the file is `Require`-d. +.. cmdv:: Export Unset @option. + + This command turns off :n:`@option`. The original state of :n:`@option` is restored at the end of the + current module, but :n:`@option` is set to its default value when this module + is imported. .. cmd:: Test @option. @@ -190,9 +206,17 @@ This command prints the current value of :n:`@option`. .. TODO : table is not a syntax entry .. cmd:: Add @table @value. + :name: Add `table` `value` + .. cmd:: Remove @table @value. + :name: Remove `table` `value` + .. cmd:: Test @table @value. + :name: Test `table` `value` + .. cmd:: Test @table for @value. + :name: Test `table` for `value` + .. cmd:: Print Table @table. These are general commands for tables. @@ -256,11 +280,10 @@ See also: Section :ref:`performingcomputations`. .. cmd::Extraction @term. This command displays the extracted term from :n:`@term`. The extraction is -processed according to the distinction between ``Set`` and ``Prop``; that is -to say, between logical and computational content (see Section -:ref:`sorts`). The extracted term is displayed in OCaml -syntax, -where global identifiers are still displayed as in |Coq| terms. +processed according to the distinction between :g:`Set` and :g:`Prop`; that is +to say, between logical and computational content (see Section :ref:`sorts`). +The extracted term is displayed in OCaml syntax, where global identifiers are +still displayed as in |Coq| terms. Variants: @@ -698,9 +721,9 @@ The command did not find the file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`). -.. exn:: Compiled library ident.vo makes inconsistent assumptions over library qualid +.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid -The command tried to load library file `ident.vo` that +The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the one already loaded in the current |Coq| session. Probably `ident.v` was not properly recompiled with the last version of the file containing @@ -766,7 +789,7 @@ Error messages: .. exn:: File not found on loadpath : @string -.. exn:: Loading of ML object file forbidden in a native |Coq| +.. exn:: Loading of ML object file forbidden in a native Coq @@ -1030,16 +1053,13 @@ to |Coq| with the command: go();; +.. warning:: - -Warnings: - - -#. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, - see Section `interactive-use`). -#. You must have compiled |Coq| from the source package and set the - environment variable COQTOP to the root of your copy of the sources - (see Section `customization-by-environment-variables`). + #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, + see Section `interactive-use`). + #. You must have compiled |Coq| from the source package and set the + environment variable COQTOP to the root of your copy of the sources + (see Section `customization-by-environment-variables`). @@ -1065,20 +1085,11 @@ expressed in seconds), then it is interrupted and an error message is displayed. -.. cmd:: Set Default Timeout @num. - -After using this command, all subsequent commands behave as if they -were passed to a Timeout command. Commands already starting by a -`Timeout` are unaffected. - - -.. cmd:: Unset Default Timeout. +.. opt:: Default Timeout @num -This command turns off the use of a default timeout. - -.. cmd:: Test Default Timeout. - -This command displays whether some default timeout has been set or not. + This option controls a default timeout for subsequent commands, as if they + were passed to a :cmd:`Timeout` command. Commands already starting by a + :cmd:`Timeout` are unaffected. .. cmd:: Fail @command. @@ -1099,128 +1110,58 @@ Error messages: Controlling display ----------------------- +.. opt:: Silent -.. cmd:: Set Silent. - -This command turns off the normal displaying. - - -.. cmd:: Unset Silent. - -This command turns the normal display on. - -.. todo:: check that spaces are handled well - -.. cmd:: Set Warnings ‘‘(@ident {* , @ident } )’’. - -This command configures the display of warnings. It is experimental, -and expects, between quotes, a comma-separated list of warning names -or categories. Adding - in front of a warning or category disables it, -adding + makes it an error. It is possible to use the special -categories all and default, the latter containing the warnings enabled -by default. The flags are interpreted from left to right, so in case -of an overlap, the flags on the right have higher priority, meaning -that `A,-A` is equivalent to `-A`. - - -.. cmd:: Set Search Output Name Only. - -This command restricts the output of search commands to identifier -names; turning it on causes invocations of ``Search``, ``SearchHead``, -``SearchPattern``, ``SearchRewrite`` etc. to omit types from their output, -printing only identifiers. - - -.. cmd:: Unset Search Output Name Only. - -This command turns type display in search results back on. - - -.. cmd:: Set Printing Width @integer. - -This command sets which left-aligned part of the width of the screen -is used for display. - - -.. cmd:: Unset Printing Width. - -This command resets the width of the screen used for display to its -default value (which is 78 at the time of writing this documentation). - - -.. cmd:: Test Printing Width. - -This command displays the current screen width used for display. - - -.. cmd:: Set Printing Depth @integer. - -This command sets the nesting depth of the formatter used for pretty- -printing. Beyond this depth, display of subterms is replaced by dots. - - -.. cmd:: Unset Printing Depth. - -This command resets the nesting depth of the formatter used for -pretty-printing to its default value (at the time of writing this -documentation, the default value is 50). - - -.. cmd:: Test Printing Depth. - -This command displays the current nesting depth used for display. - - -.. cmd:: Unset Printing Compact Contexts. - -This command resets the displaying of goals contexts to non compact -mode (default at the time of writing this documentation). Non compact -means that consecutive variables of different types are printed on -different lines. - - -.. cmd:: Set Printing Compact Contexts. - -This command sets the displaying of goals contexts to compact mode. -The printer tries to reduce the vertical size of goals contexts by -putting several variables (even if of different types) on the same -line provided it does not exceed the printing width (See Set Printing -Width above). - - -.. cmd:: Test Printing Compact Contexts. - -This command displays the current state of compaction of goal. + This option controls the normal displaying. +.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" -.. cmd:: Unset Printing Unfocused. + This option configures the display of warnings. It is experimental, and + expects, between quotes, a comma-separated list of warning names or + categories. Adding - in front of a warning or category disables it, adding + + makes it an error. It is possible to use the special categories all and + default, the latter containing the warnings enabled by default. The flags are + interpreted from left to right, so in case of an overlap, the flags on the + right have higher priority, meaning that `A,-A` is equivalent to `-A`. -This command resets the displaying of goals to focused goals only -(default). Unfocused goals are created by focusing other goals with -bullets (see :ref:`bullets`) or curly braces (see `here <curly-braces>`). +.. opt:: Search Output Name Only + This option restricts the output of search commands to identifier names; + turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, + :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their + output, printing only identifiers. -.. cmd:: Set Printing Unfocused. +.. opt:: Printing Width @integer -This command enables the displaying of unfocused goals. The goals are -displayed after the focused ones and are distinguished by a separator. + This command sets which left-aligned part of the width of the screen is used + for display. At the time of writing this documentation, the default value + is 78. +.. opt:: Printing Depth @integer -.. cmd:: Test Printing Unfocused. + This option controls the nesting depth of the formatter used for pretty- + printing. Beyond this depth, display of subterms is replaced by dots. At the + time of writing this documentation, the default value is 50. -This command displays the current state of unfocused goals display. +.. opt:: Printing Compact Contexts + This option controls the compact display mode for goals contexts. When on, + the printer tries to reduce the vertical size of goals contexts by putting + several variables (even if of different types) on the same line provided it + does not exceed the printing width (see :opt:`Printing Width`). At the time + of writing this documentation, it is off by default. -.. cmd:: Set Printing Dependent Evars Line. +.. opt:: Printing Unfocused -This command enables the printing of the “(dependent evars: …)” line -when -emacs is passed. + This option controls whether unfocused goals are displayed. Such goals are + created by focusing other goals with bullets (see :ref:`bullets` or + :ref:`curly braces <curly-braces>`). It is off by default. +.. opt:: Printing Dependent Evars Line -.. cmd:: Unset Printing Dependent Evars Line. + This option controls the printing of the “(dependent evars: …)” line when + ``-emacs`` is passed. -This command disables the printing of the “(dependent evars: …)” line -when -emacs is passed. .. _vernac-controlling-the-reduction-strategies: @@ -1234,7 +1175,7 @@ conversion algorithm lazily compares applicative terms while the other is a brute-force but efficient algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms similar to the bytecode -representation used in the ZINC virtual machine [`98`]. It is +representation used in the ZINC virtual machine :cite:`Leroy90`. It is especially useful for intensive computation of algebraic values, such as numbers, and for reflection-based tactics. The commands to fine- tune the reduction strategies and the lazy conversion algorithm are |