From a3ee82e80083fff971e382f52d9295fda2210e2d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 16 Apr 2018 21:26:55 +0200 Subject: [Sphinx] Clean-up indices --- doc/sphinx/proof-engine/ltac.rst | 33 ++ doc/sphinx/proof-engine/proof-handling.rst | 46 +- .../proof-engine/ssreflect-proof-language.rst | 21 +- doc/sphinx/proof-engine/tactics.rst | 524 ++++++++++++--------- doc/sphinx/proof-engine/vernacular-commands.rst | 41 +- 5 files changed, 398 insertions(+), 267 deletions(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 247d5d899..009758319 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 a77b127eb..86c94bab3 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 6ddb0b027..977a5b8fa 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*. @@ -3724,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 1868f4b9d..7a45272f2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -51,7 +51,7 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. opt:: Default Goal Selector @toplevel_selector. +.. opt:: Default Goal Selector @toplevel_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 @@ -168,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. @@ -181,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. @@ -233,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. @@ -243,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. @@ -313,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 @@ -335,6 +340,7 @@ 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``. @@ -515,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 @@ -534,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 @@ -572,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: @@ -611,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 @@ -845,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. @@ -866,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 @@ -982,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 @@ -989,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. @@ -1006,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. @@ -1112,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) @@ -1121,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, @@ -1134,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 @@ -1159,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 @@ -1175,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 @@ -1416,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 `). .. 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 @@ -1442,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 @@ -1451,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. @@ -1549,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 `). .. 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, @@ -1621,6 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) (see :ref:`bindings list `). .. 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. @@ -1639,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 @@ -1649,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. @@ -1733,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 @@ -1842,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 @@ -1921,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 @@ -1948,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 :opt:`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. -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 behavior can be -turned off by setting the option :opt:`Keep Proof Equalities`. +.. opt:: 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 @@ -2110,6 +2156,7 @@ turned off by setting the option :opt:`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. @@ -2410,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 @@ -2456,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 <-`. @@ -2499,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 :opt:`Regular Subst - Tactic`. When this option is activated, subst also deals with the - following corner cases: + .. opt:: Regular Subst Tactic + + This option controls the behavior of :tacn:`subst`. When it is + activated, :tacn:`subst` also deals with the following corner cases: - + 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`. + + 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. + 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 @@ -2536,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 @@ -2697,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`. @@ -2706,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 @@ -3096,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 ` @@ -3251,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 @@ -3587,7 +3660,7 @@ non-imported hints. 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 ``...``. @@ -3601,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 @@ -3669,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 @@ -3746,13 +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 :opt:`Firstorder Solver` -option and printed using :cmd:`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} @@ -3991,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 @@ -4002,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 @@ -4270,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 @@ -4286,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 6a20c0466..d0d7d74af 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. @@ -186,9 +188,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. @@ -693,9 +703,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 @@ -761,7 +771,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 @@ -1025,16 +1035,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`). @@ -1089,7 +1096,7 @@ Controlling display This option controls the normal displaying. -.. opt:: Warnings "@ident {* , @ident }" +.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -1129,10 +1136,10 @@ Controlling display .. opt:: Printing Unfocused This option controls whether unfocused goals are displayed. Such goals are - created by focusing other goals with bullets (see :ref:`bullets`) or curly - braces (see `here `). It is off by default. + created by focusing other goals with bullets (see :ref:`bullets` or + :ref:`curly braces `). It is off by default. -.. cmd:: Printing Dependent Evars Line +.. opt:: Printing Dependent Evars Line This option controls the printing of the “(dependent evars: …)” line when ``-emacs`` is passed. @@ -1150,7 +1157,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 -- cgit v1.2.3