diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 40 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 740 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 89 |
4 files changed, 474 insertions, 402 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index edd83b7cee..0ea8c7be2d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -292,6 +292,7 @@ focused goals with: .. exn:: No such goal. :name: No such goal. (Goal selector) + :undocumented: .. TODO change error message index entry @@ -351,6 +352,7 @@ We can check if a tactic made progress with: goals (up to syntactical equality), then an error of level 0 is raised. .. exn:: Failed to progress. + :undocumented: Backtracking branching ~~~~~~~~~~~~~~~~~~~~~~ @@ -393,6 +395,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics: :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. + :undocumented: .. tacv:: first @expr @@ -482,6 +485,7 @@ one* success: immediately. .. exn:: This tactic has more than one success. + :undocumented: Checking the failure ~~~~~~~~~~~~~~~~~~~~ @@ -521,6 +525,7 @@ among a panel of tactics: apply :n:`v__2` and so on. It fails if there is no solving tactic. .. exn:: Cannot solve the goal. + :undocumented: .. tacv:: solve @expr @@ -576,8 +581,7 @@ Failing goals left. See the example for clarification. .. tacv:: gfail {* message_token} - - .. tacv:: gfail @num {* message_token} + gfail @num {* message_token} These variants fail with an error message or an error level even if there are no goals left. Be careful however if Coq terms have to be @@ -586,9 +590,11 @@ Failing evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed. .. exn:: Tactic Failure message (level @num). + :undocumented: .. exn:: No such goal. :name: No such goal. (fail) + :undocumented: .. example:: @@ -670,24 +676,24 @@ tactic This tactic currently does not support nesting, and will report times based on the innermost execution. This is due to the fact that it is - implemented using the tactics + implemented using the following internal tactics: .. tacn:: restart_timer @string :name: restart_timer - and + Reset a timer - .. tacn:: finish_timing {? @string} @string + .. 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 - determines the label associated with the timer for printing. + Display an optionally named timer. The parenthesized string argument + is also optional, and determines the label associated with the timer + for printing. - By copying the definition of :n:`time_constr` from the standard library, + By copying the definition of :tacn:`time_constr` from the standard library, users can achive support for a fixed pattern of nesting by passing - different :n:`@string` parameters to :n:`restart_timer` and :n:`finish_timing` - at each level of nesting. + different :token:`string` parameters to :tacn:`restart_timer` and + :tacn:`finish_timing` at each level of nesting. .. example:: @@ -967,10 +973,10 @@ Evaluation of a term can be performed with: Recovering the type of a term ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The following returns the type of term: - .. tacn:: type of @term + This tactic returns the type of :token:`term`. + Manipulating untyped terms ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1041,6 +1047,7 @@ Testing boolean expressions Fail all:let n:= numgoals in guard n=2. .. exn:: Condition not satisfied. + :undocumented: Proving a subgoal as a separate lemma ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1092,6 +1099,7 @@ Proving a subgoal as a separate lemma .. exn:: Proof is not complete. :name: Proof is not complete. (abstract) + :undocumented: Tactic toplevel definitions --------------------------- @@ -1348,6 +1356,6 @@ 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 -command :cmd:`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 + command :cmd:`Optimize Heap`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 0b059f92ee..590d71b5f3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -67,6 +67,7 @@ list of assertion commands is given in :ref:`Assertions`. The command added to the environment as an opaque constant. .. exn:: Attempt to save an incomplete proof. + :undocumented: .. note:: @@ -106,6 +107,7 @@ list of assertion commands is given in :ref:`Assertions`. The command proof was edited. .. exn:: No focused proof (No proof-editing in progress). + :undocumented: .. cmdv:: Abort @ident @@ -282,6 +284,7 @@ Navigation in the proof tree This command restores the proof editing process to the original goal. .. exn:: No focused proof to restart. + :undocumented: .. cmd:: Focus @@ -473,13 +476,14 @@ Requesting information This command displays the current goals. .. exn:: No focused proof. + :undocumented: .. cmdv:: Show @num Displays only the :token:`num`\-th subgoal. .. exn:: No such goal. - + :undocumented: .. cmdv:: Show @ident @@ -565,6 +569,7 @@ Requesting information Show Match nat. .. exn:: Unknown inductive type. + :undocumented: .. cmdv:: Show Universes :name: Show Universes diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 041f1bc966..150aadc15a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -91,6 +91,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: of ``term``. .. exn:: No such binder. + :undocumented: + A bindings list can also be a simple list of terms :n:`{* term}`. In that case the references to which these terms correspond are @@ -102,6 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: are required. .. exn:: Not the right number of missing arguments. + :undocumented: .. _occurrencessets: @@ -589,6 +591,7 @@ Applying theorems :n:`constructor 2 {? with @bindings_list }`. .. exn:: Not an inductive goal with 2 constructors. + :undocumented: .. tacv:: econstructor eexists @@ -1081,8 +1084,8 @@ Managing the local context generated by Coq. .. tacv:: epose (@ident {? @binders} := @term) - .. tacv:: epose term - :name: epose + epose @term + :name: epose; _ While the different variants of :tacn:`pose` expect that no existential variables are generated by the tactic, :tacn:`epose` @@ -1124,7 +1127,7 @@ Managing the local context Controlling the proof flow ------------------------------ -.. tacn:: assert (@ident : form) +.. tacn:: assert (@ident : @type) :name: assert This tactic applies to any goal. :n:`assert (H : U)` adds a new hypothesis @@ -1132,106 +1135,104 @@ Controlling the proof flow :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to prove. -.. exn:: Not a proposition or a type. + .. exn:: Not a proposition or a type. - Arises when the argument form is neither of type :g:`Prop`, :g:`Set` nor - :g:`Type`. + Arises when the argument :token:`type` is neither of type :g:`Prop`, + :g:`Set` nor :g:`Type`. -.. tacv:: assert form + .. tacv:: assert @type - This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by - Coq. + This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is + generated by Coq. -.. tacv:: assert @form by @tactic + .. tacv:: assert @type by @tactic - This tactic behaves like :n:`assert` but applies tactic to solve the subgoals - generated by assert. + This tactic behaves like :tacn:`assert` but applies tactic to solve the + subgoals generated by assert. - .. exn:: Proof is not complete. - :name: Proof is not complete. (assert) + .. exn:: Proof is not complete. + :name: Proof is not complete. (assert) + :undocumented: -.. tacv:: assert @form as @intro_pattern + .. tacv:: assert @type as @intro_pattern - If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), - the hypothesis is named after this introduction pattern (in particular, if - :n:`intro_pattern` is :n:`@ident`, the tactic behaves like - :n:`assert (@ident : form)`). If :n:`intro_pattern` is an action - introduction pattern, the tactic behaves like :n:`assert form` followed by - the action done by this introduction pattern. + If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), + the hypothesis is named after this introduction pattern (in particular, if + :n:`intro_pattern` is :n:`@ident`, the tactic behaves like + :n:`assert (@ident : @type)`). If :n:`intro_pattern` is an action + introduction pattern, the tactic behaves like :n:`assert @type` followed by + the action done by this introduction pattern. -.. tacv:: assert @form as @intro_pattern by @tactic + .. tacv:: assert @type as @intro_pattern by @tactic - This combines the two previous variants of :n:`assert`. + This combines the two previous variants of :tacn:`assert`. -.. tacv:: assert (@ident := @term ) + .. tacv:: assert (@ident := @term) - This behaves as :n:`assert (@ident : type) by exact @term` where :g:`type` is - the type of :g:`term`. This is deprecated in favor of :n:`pose proof`. If the - head of term is :n:`@ident`, the tactic behaves as :n:`specialize @term`. + This behaves as :n:`assert (@ident : @type) by exact @term` where + :token:`type` is the type of :token:`term`. This is equivalent to using + :tacn:`pose proof`. If the head of term is :token:`ident`, the tactic + behaves as :tacn:`specialize`. - .. exn:: Variable @ident is already declared. + .. exn:: Variable @ident is already declared. + :undocumented: -.. tacv:: eassert form as intro_pattern by tactic +.. tacv:: eassert @type as @intro_pattern by @tactic :name: eassert -.. tacv:: assert (@ident := @term) - - While the different variants of :n:`assert` expect that no existential - variables are generated by the tactic, :n:`eassert` removes this constraint. + While the different variants of :tacn:`assert` expect that no existential + variables are generated by the tactic, :tacn:`eassert` removes this constraint. This allows not to specify the asserted statement completeley before starting to prove it. -.. tacv:: pose proof @term {? as intro_pattern} +.. 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, + This tactic behaves like :n:`assert @type {? as @intro_pattern} by exact @term` + where :token:`type` is the type of :token:`term`. In particular, :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)` - and :n:`pose proof @term as intro_pattern` is the same as applying the - intro_pattern to :n:`@term`. + and :n:`pose proof @term as @intro_pattern` is the same as applying the + :token:`intro_pattern` to :token:`term`. -.. tacv:: epose proof term {? as intro_pattern} +.. tacv:: epose proof @term {? as @intro_pattern} + :name: epose proof - While :n:`pose proof` expects that no existential variables are generated by - the tactic, :n:`epose proof` removes this constraint. + While :tacn:`pose proof` expects that no existential variables are generated by + the tactic, :tacn:`epose proof` removes this constraint. -.. tacv:: enough (@ident : form) +.. tacv:: enough (@ident : @type) :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 - inserted after the initial goal rather than before it as :n:`assert` would do. + This adds a new hypothesis of name :token:`ident` asserting :token:`type` to the + goal the tactic :tacn:`enough` is applied to. A new subgoal stating :token:`type` is + inserted after the initial goal rather than before it as :tacn:`assert` would do. -.. tacv:: enough form +.. tacv:: enough @type - This behaves like :n:`enough (@ident : form)` with the name :n:`@ident` of + This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of the hypothesis generated by Coq. -.. tacv:: enough form as intro_pattern +.. tacv:: enough @type as @intro_pattern - This behaves like :n:`enough form` using :n:`intro_pattern` to name or + This behaves like :n:`enough @type` using :token:`intro_pattern` to name or destruct the new hypothesis. -.. tacv:: enough (@ident : @form) by @tactic -.. tacv:: enough @form by @tactic -.. tacv:: enough @form as @intro_pattern by @tactic +.. tacv:: enough (@ident : @type) by @tactic + enough @type {? as @intro_pattern } by @tactic - This behaves as above but with :n:`tactic` expected to solve the initial goal - after the extra assumption :n:`form` is added and possibly destructed. If the - :n:`as intro_pattern` clause generates more than one subgoal, :n:`tactic` is + This behaves as above but with :token:`tactic` expected to solve the initial goal + after the extra assumption :token:`type` is added and possibly destructed. If the + :n:`as @intro_pattern` clause generates more than one subgoal, :token:`tactic` is applied to all of them. -.. tacv:: eenough (@ident : form) by tactic - :name: eenough - -.. tacv:: eenough form by tactic +.. tacv:: eenough @type {? as @intro_pattern } {? by @tactic } + eenough (@ident : @type) {? by @tactic } + :name: eenough; _ -.. tacv:: eenough form as intro_pattern by tactic + While the different variants of :tacn:`enough` expect that no existential + variables are generated by the tactic, :tacn:`eenough` removes this constraint. - 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 @type :name: cut This tactic applies to any goal. It implements the non-dependent case of @@ -1240,11 +1241,11 @@ Controlling the proof flow subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the list of remaining subgoal to prove. -.. tacv:: specialize (ident {* @term}) {? as intro_pattern} -.. tacv:: specialize ident with @bindings_list {? as intro_pattern} - :name: specialize +.. tacv:: specialize (@ident {* @term}) {? as @intro_pattern} + specialize @ident with @bindings_list {? as @intro_pattern} + :name: specialize; _ - The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The + This tactic works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments :n:`{* @term}` or from a :ref:`bindings list <bindingslist>`. @@ -1254,15 +1255,18 @@ Controlling the proof flow uninstantiated arguments are inferred by unification if possible or left quantified in the hypothesis otherwise. With the :n:`as` clause, the local hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis - is introduced as specified by the :n:`intro_pattern`. The name :n:`@ident` + is introduced as specified by the :token:`intro_pattern`. The name :n:`@ident` can also refer to a global lemma or hypothesis. In this case, for - compatibility reasons, the behavior of :n:`specialize` is close to that of - :n:`generalize`: the instantiated statement becomes an additional premise of - the goal. The :n:`as` clause is especially useful in this case to immediately + compatibility reasons, the behavior of :tacn:`specialize` is close to that of + :tacn:`generalize`: the instantiated statement becomes an additional premise of + the goal. The ``as`` clause is especially useful in this case to immediately introduce the instantiated statement as a local hypothesis. .. exn:: @ident is used in hypothesis @ident. + :undocumented: + .. exn:: @ident is used in conclusion. + :undocumented: .. tacn:: generalize @term :name: generalize @@ -1343,8 +1347,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident -.. tacv:: instantiate ( @num := @term ) in ( value of @ident ) -.. tacv:: instantiate ( @num := @term ) in ( type of @ident ) + instantiate ( @num := @term ) in ( value of @ident ) + instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. @@ -1360,13 +1364,13 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. .. tacn:: admit :name: admit -The admit tactic allows temporarily skipping a subgoal so as to -progress further in the rest of the proof. A proof containing admitted -goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. + This tactic allows temporarily skipping a subgoal so as to + progress further in the rest of the proof. A proof containing admitted + goals cannot be closed with :cmd:`Qed` but only with :cmd:`Admitted`. .. tacv:: give_up - Synonym of :n:`admit`. + Synonym of :tacn:`admit`. .. tacn:: absurd @term :name: absurd @@ -1387,7 +1391,8 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory hypotheses. -.. exn:: No such assumption. + .. exn:: No such assumption. + :undocumented: .. tacv:: contradiction @ident @@ -1602,6 +1607,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) induction n. .. exn:: Not an inductive product. + :undocumented: .. exn:: Unable to find an instance for the variables @ident ... @ident. @@ -1672,10 +1678,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Show 2. .. tacv:: induction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences + einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences -.. tacv:: einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences - - These are the most general forms of ``induction`` and ``einduction``. It combines the + These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the effects of the with, as, using, and in clauses. .. tacv:: elim @term @@ -1709,7 +1714,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) existential variables to be resolved later on. .. tacv:: elim @term using @term -.. tacv:: elim @term using @term with @bindings_list + elim @term using @term with @bindings_list Allows the user to give explicitly an induction principle :n:`@term` that is not the standard one for the underlying inductive type of :n:`@term`. The @@ -1717,15 +1722,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`@term`. .. tacv:: elim @term with @bindings_list using @term with @bindings_list -.. tacv:: eelim @term with @bindings_list using @term with @bindings_list + eelim @term with @bindings_list using @term with @bindings_list - These are the most general forms of ``elim`` and ``eelim``. It combines the + These are the most general forms of :tacn:`elim` and :tacn:`eelim`. It combines the effects of the ``using`` clause and of the two uses of the ``with`` clause. -.. tacv:: elimtype @form +.. tacv:: elimtype @type :name: elimtype - The argument :n:`form` must be inductively defined. :n:`elimtype I` is + The argument :token:`type` must be inductively defined. :n:`elimtype I` is equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s). Conversely, if :g:`t` is a :n:`@term` of (inductive) type :g:`I` that does @@ -1879,7 +1884,10 @@ and an explanation of the underlying technique. .. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` .. exn:: Cannot find induction information on @qualid. + :undocumented: + .. exn:: Not the right number of induction arguments. + :undocumented: .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list @@ -1913,7 +1921,10 @@ and an explanation of the underlying technique. :n:`intros until @ident`. .. exn:: No primitive equality found. + :undocumented: + .. exn:: Not a discriminable equality. + :undocumented: .. tacv:: discriminate @num @@ -1927,11 +1938,11 @@ and an explanation of the underlying technique. bindings to instantiate parameters or hypotheses of :n:`@term`. .. tacv:: ediscriminate @num -.. tacv:: ediscriminate @term {? with @bindings_list} - :name: ediscriminate + 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 + This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the + type of the hypothesis referred to by :token:`num`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: discriminate @@ -1942,6 +1953,7 @@ and an explanation of the underlying technique. :n:`intro @ident; discriminate @ident`. .. exn:: No discriminable equalities. + :undocumented: .. tacn:: injection @term :name: injection @@ -1994,9 +2006,16 @@ and an explanation of the underlying technique. context using :n:`intros until @ident`. .. exn:: Not a projectable equality but a discriminable one. - .. exn:: Nothing to do, it is an equality between convertible @terms. + :undocumented: + + .. exn:: Nothing to do, it is an equality between convertible terms. + :undocumented: + .. exn:: Not a primitive equality. + :undocumented: + .. exn:: Nothing to inject. + :undocumented: .. tacv:: injection @num @@ -2010,8 +2029,8 @@ and an explanation of the underlying technique. instantiate parameters or hypotheses of :n:`@term`. .. tacv:: einjection @num - :name: einjection - .. tacv:: einjection @term {? with @bindings_list} + 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 @@ -2023,21 +2042,22 @@ and an explanation of the underlying technique. :n:`intro @ident; injection @ident`. .. exn:: goal does not satisfy the expected preconditions. + :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern} - .. tacv:: injection @num as {+ intro_pattern} - .. tacv:: injection as {+ intro_pattern} - .. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern} - .. tacv:: einjection @num as {+ intro_pattern} - .. tacv:: einjection as {+ intro_pattern} - - These variants apply :n:`intros {+ @intro_pattern}` after the call to - :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in - the context of hypotheses. The number of :n:`@intro_pattern` must not exceed - the number of equalities newly generated. If it is smaller, fresh - names are automatically generated to adjust the list of :n:`@intro_pattern` - to the number of new equalities. The original equality is erased if it - corresponds to a hypothesis. + injection @num as {+ intro_pattern} + injection as {+ intro_pattern} + einjection @term {? with @bindings_list} as {+ intro_pattern} + einjection @num as {+ intro_pattern} + einjection as {+ intro_pattern} + + These variants apply :n:`intros {+ @intro_pattern}` after the call to + :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in + the context of hypotheses. The number of :n:`@intro_pattern` must not exceed + the number of equalities newly generated. If it is smaller, fresh + names are automatically generated to adjust the list of :n:`@intro_pattern` + to the number of new equalities. The original equality is erased if it + corresponds to a hypothesis. .. flag:: Structural Injection @@ -2444,8 +2464,10 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. subgoals. .. exn:: The @term provided does not end with an equation. + :undocumented: .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + :undocumented: .. tacv:: rewrite -> @term @@ -2522,6 +2544,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. .. exn:: Terms do not have convertible types. + :undocumented: .. tacv:: replace @term with @term’ by @tactic @@ -2544,8 +2567,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. the form :n:`@term’ = @term` .. tacv:: replace @term {? with @term} in clause {? by @tactic} - .. tacv:: replace -> @term in clause - .. tacv:: replace <- @term in clause + replace -> @term in clause + replace <- @term in clause Acts as before but the replacements take place in the specified clause (see :ref:`performingcomputations`) and not only in the conclusion of the goal. The @@ -2658,6 +2681,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. convertible. .. exn:: Not convertible. + :undocumented: .. tacv:: change @term with @term’ @@ -2670,6 +2694,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. .. exn:: Too few occurrences. + :undocumented: .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident @@ -2712,12 +2737,9 @@ following: For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. -.. tacn:: cbv {* flag} - :name: cbv -.. tacn:: lazy {* flag} - :name: lazy -.. tacn:: compute - :name: compute +.. tacn:: cbv {* @flag} + lazy {* @flag} + :name: cbv; lazy These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In @@ -2765,7 +2787,8 @@ the conversion in hypotheses :n:`{+ @ident}`. evaluating purely computational expressions (i.e. with little dead code). .. tacv:: compute -.. tacv:: cbv + cbv + :name: compute; _ These are synonyms for ``cbv beta delta iota zeta``. @@ -2774,17 +2797,17 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. .. tacv:: compute {+ @qualid} -.. tacv:: cbv {+ @qualid} + cbv {+ @qualid} These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. .. tacv:: compute -{+ @qualid} -.. tacv:: cbv -{+ @qualid} + cbv -{+ @qualid} These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. .. tacv:: lazy {+ @qualid} -.. tacv:: lazy -{+ @qualid} + lazy -{+ @qualid} These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` and :n:`lazy beta delta -{+ @qualid} iota zeta`. @@ -2864,9 +2887,8 @@ the conversion in hypotheses :n:`{+ @ident}`. on transparency and opacity). .. tacn:: cbn - :name: cbn -.. tacn:: simpl - :name: simpl + simpl + :name: cbn; simpl These tactics apply to any goal. They try to reduce a term to something still readable instead of fully normalizing it. They perform @@ -2962,7 +2984,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`succ t` is reduced to :g:`S t`. .. tacv:: cbn {+ @qualid} -.. tacv:: cbn -{+ @qualid} + cbn -{+ @qualid} These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta` and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`). @@ -2978,16 +3000,17 @@ the conversion in hypotheses :n:`{+ @ident}`. matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. + :undocumented: .. tacv:: simpl @qualid -.. tacv:: simpl @string + simpl @string - This applies ``simpl`` only to the applicative subterms whose head occurrence + This applies :tacn:`simpl` only to the applicative subterms whose head occurrence is the unfoldable constant :n:`@qualid` (the constant can be referred to by its notation using :n:`@string` if such a notation exists). .. tacv:: simpl @qualid at {+ @num} -.. tacv:: simpl @string at {+ @num} + simpl @string at {+ @num} This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). @@ -3008,6 +3031,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :math:`\beta`:math:`\iota`-normal form. .. exn:: @qualid does not denote an evaluable constant. + :undocumented: .. tacv:: unfold @qualid in @ident @@ -3025,8 +3049,10 @@ the conversion in hypotheses :n:`{+ @ident}`. unfolded. Occurrences are located from left to right. .. exn:: Bad occurrence number of @qualid. + :undocumented: .. exn:: @qualid does not occur. + :undocumented: .. tacv:: unfold @string @@ -3117,6 +3143,7 @@ Conversion tactics applied to hypotheses Example: :n:`unfold not in (type of H1) (type of H3)`. .. exn:: No such hypothesis: @ident. + :undocumented: .. _automation: @@ -3127,38 +3154,41 @@ Automation .. tacn:: auto :name: auto -This tactic implements a Prolog-like resolution procedure to solve the -current goal. It first tries to solve the goal using the assumption -tactic, then it reduces the goal to an atomic one using intros and -introduces the newly generated hypotheses as hints. Then it looks at -the list of tactics associated to the head symbol of the goal and -tries to apply one of them (starting from the tactics with lower -cost). This process is recursively applied to the generated subgoals. + This tactic implements a Prolog-like resolution procedure to solve the + current goal. It first tries to solve the goal using the assumption + tactic, then it reduces the goal to an atomic one using intros and + introduces the newly generated hypotheses as hints. Then it looks at + the list of tactics associated to the head symbol of the goal and + tries to apply one of them (starting from the tactics with lower + cost). This process is recursively applied to the generated subgoals. -By default, auto only uses the hypotheses of the current goal and the -hints of the database named core. + By default, auto only uses the hypotheses of the current goal and the + hints of the database named core. .. tacv:: auto @num - Forces the search depth to be :n:`@num`. The maximal search depth - is `5` by default. + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. .. tacv:: auto with {+ @ident} - Uses the hint databases :n:`{+ @ident}` in addition to the database core. See - :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of - pre-defined databases and the way to create or extend a database. + Uses the hint databases :n:`{+ @ident}` in addition to the database core. + + .. seealso:: + :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of + pre-defined databases and the way to create or extend a database. .. tacv:: auto with * - Uses all existing hint databases. See - :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + Uses all existing hint databases. + + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` -.. tacv:: auto using {+ @lemma} +.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses :n:`{+ @lemma}` in addition to hints (can be combined with the with - :n:`@ident` option). If :n:`@lemma` is an inductive type, it is the - collection of its constructors which is added as hints. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. .. tacv:: info_auto @@ -3184,13 +3214,24 @@ hints of the database named core. equalities like :g:`X=X`. .. tacv:: trivial with {+ @ident} + :undocumented: + .. tacv:: trivial with * + :undocumented: + .. tacv:: trivial using {+ @lemma} + :undocumented: + .. tacv:: debug trivial :name: debug trivial + :undocumented: + .. tacv:: info_trivial :name: info_trivial + :undocumented: + .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :undocumented: .. note:: :tacn:`auto` either solves completely the goal or else leaves it @@ -3210,26 +3251,26 @@ the :tacn:`auto` and :tacn:`trivial` tactics: .. tacn:: eauto :name: eauto -This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try -resolution hints which would leave existential variables in the goal, -:tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` -where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` -can solve such a goal: + This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try + resolution hints which would leave existential variables in the goal, + :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` + where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + can solve such a goal: -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Hint Resolve ex_intro. - Goal forall P:nat -> Prop, P 0 -> exists n, P n. - eauto. + Hint Resolve ex_intro. + Goal forall P:nat -> Prop, P 0 -> exists n, P n. + eauto. -Note that ``ex_intro`` should be declared as a hint. + Note that ``ex_intro`` should be declared as a hint. .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for eauto are the same as for auto. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. :tacn:`eauto` also obeys the following options: @@ -3243,13 +3284,12 @@ Note that ``ex_intro`` should be declared as a hint. .. tacn:: autounfold with {+ @ident} :name: autounfold - -This tactic unfolds constants that were declared through a ``Hint Unfold`` -in the given databases. + This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` + in the given databases. .. tacv:: autounfold with {+ @ident} in clause - Performs the unfolding in the given clause. + Performs the unfolding in the given clause. .. tacv:: autounfold with * @@ -3258,18 +3298,18 @@ in the given databases. .. tacn:: autorewrite with {+ @ident} :name: autorewrite -This tactic [4]_ carries out rewritings according to the rewriting rule -bases :n:`{+ @ident}`. + This tactic [4]_ carries out rewritings according to the rewriting rule + bases :n:`{+ @ident}`. -Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until -it fails. Once all the rules have been processed, if the main subgoal has -progressed (e.g., if it is distinct from the initial main goal) then the rules -of this base are processed again. If the main subgoal has not progressed then -the next base is processed. For the bases, the behavior is exactly similar to -the processing of the rewriting rules. + Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until + it fails. Once all the rules have been processed, if the main subgoal has + progressed (e.g., if it is distinct from the initial main goal) then the rules + of this base are processed again. If the main subgoal has not progressed then + the next base is processed. For the bases, the behavior is exactly similar to + the processing of the rewriting rules. -The rewriting rule bases are built with the ``Hint Rewrite vernacular`` -command. + The rewriting rule bases are built with the :cmd:`Hint Rewrite` + command. .. warning:: @@ -3435,6 +3475,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is itself. .. exn:: @term cannot be used as a hint + :undocumented: .. cmdv:: Immediate {+ @term} @@ -3448,6 +3489,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. .. exn:: @ident is not an inductive type + :undocumented: .. cmdv:: Hint Constructors {+ @ident} @@ -3616,16 +3658,16 @@ use one or several databases specific to your development. .. cmd:: Remove Hints {+ @term} : {+ @ident} -This command removes the hints associated to terms :n:`{+ @term}` in databases -:n:`{+ @ident}`. + This command removes the hints associated to terms :n:`{+ @term}` in databases + :n:`{+ @ident}`. .. _printhint: .. cmd:: Print Hint -This command displays all hints that apply to the current goal. It -fails if no proof is being edited, while the two variants can be used -at every moment. + This command displays all hints that apply to the current goal. It + fails if no proof is being edited, while the two variants can be used + at every moment. **Variants:** @@ -3753,17 +3795,17 @@ Decision procedures .. tacn:: tauto :name: tauto -This tactic implements a decision procedure for intuitionistic propositional -calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff -:cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an -intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and -logical equivalence but does not unfold any other definition. - -The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would -fail: + This tactic implements a decision procedure for intuitionistic propositional + calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff + :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an + intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and + logical equivalence but does not unfold any other definition. .. example:: + The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would + fail: + .. coqtop:: reset all Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. @@ -3799,27 +3841,24 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. .. tacn:: intuition @tactic :name: intuition -The tactic :tacn:`intuition` takes advantage of the search-tree built by the -decision procedure involved in the tactic :tacn:`tauto`. It uses this -information to generate a set of subgoals equivalent to the original one (but -simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If -this tactic fails on some goals then :tacn:`intuition` fails. In fact, -:tacn:`tauto` is simply :g:`intuition fail`. + The tactic :tacn:`intuition` takes advantage of the search-tree built by the + decision procedure involved in the tactic :tacn:`tauto`. It uses this + information to generate a set of subgoals equivalent to the original one (but + simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If + this tactic fails on some goals then :tacn:`intuition` fails. In fact, + :tacn:`tauto` is simply :g:`intuition fail`. -For instance, the tactic :g:`intuition auto` applied to the goal - -:: - - (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O + .. example:: + For instance, the tactic :g:`intuition auto` applied to the goal:: -internally replaces it by the equivalent one: -:: + (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O - (forall (x:nat), P x), B |- P O + internally replaces it by the equivalent one:: + (forall (x:nat), P x), B |- P O -and then uses :tacn:`auto` which completes the proof. + and then uses :tacn:`auto` which completes the proof. Originally due to César Muñoz, these tactics (:tacn:`tauto` and :tacn:`intuition`) have been completely re-engineered by David Delahaye using @@ -3849,25 +3888,25 @@ some incompatibilities. .. tacn:: rtauto :name: rtauto -The :tacn:`rtauto` tactic solves propositional tautologies similarly to what -:tacn:`tauto` does. The main difference is that the proof term is built using a -reflection scheme applied to a sequent calculus proof of the goal. The search -procedure is also implemented using a different technique. + The :tacn:`rtauto` tactic solves propositional tautologies similarly to what + :tacn:`tauto` does. The main difference is that the proof term is built using a + reflection scheme applied to a sequent calculus proof of the goal. The search + procedure is also implemented using a different technique. -Users should be aware that this difference may result in faster proof-search -but slower proof-checking, and :tacn:`rtauto` might not solve goals that -:tacn:`tauto` would be able to solve (e.g. goals involving universal -quantifiers). + Users should be aware that this difference may result in faster proof-search + but slower proof-checking, and :tacn:`rtauto` might not solve goals that + :tacn:`tauto` would be able to solve (e.g. goals involving universal + quantifiers). -Note that this tactic is only available after a ``Require Import Rtauto``. + Note that this tactic is only available after a ``Require Import Rtauto``. .. tacn:: firstorder :name: firstorder -The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to -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 tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to + 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. .. opt:: Firstorder Solver @tactic :name: Firstorder Solver @@ -3906,20 +3945,20 @@ inductive definition. .. tacn:: congruence :name: congruence -The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard -Nelson and Oppen congruence closure algorithm, which is a decision procedure -for ground equalities with uninterpreted symbols. It also includes -constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal -is a non-quantified equality, congruence tries to prove it with non-quantified -equalities in the context. Otherwise it tries to infer a discriminable equality -from those in the context. Alternatively, congruence tries to prove that a -hypothesis is equal to the goal or to the negation of another hypothesis. - -:tacn:`congruence` is also able to take advantage of hypotheses stating -quantified equalities, but you have to provide a bound for the number of extra -equalities generated that way. Please note that one of the sides of the -equality must contain all the quantified variables in order for congruence to -match against it. + The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard + Nelson and Oppen congruence closure algorithm, which is a decision procedure + for ground equalities with uninterpreted symbols. It also includes + constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal + is a non-quantified equality, congruence tries to prove it with non-quantified + equalities in the context. Otherwise it tries to infer a discriminable equality + from those in the context. Alternatively, congruence tries to prove that a + hypothesis is equal to the goal or to the negation of another hypothesis. + + :tacn:`congruence` is also able to take advantage of hypotheses stating + quantified equalities, but you have to provide a bound for the number of extra + equalities generated that way. Please note that one of the sides of the + equality must contain all the quantified variables in order for congruence to + match against it. .. example:: @@ -3980,7 +4019,10 @@ succeeds, and results in an error otherwise. conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. + :undocumented: + .. exn:: Not equal (due to universes). + :undocumented: .. tacn:: constr_eq_strict @term @term :name: constr_eq_strict @@ -3990,7 +4032,10 @@ succeeds, and results in an error otherwise. constraints. .. exn:: Not equal. + :undocumented: + .. exn:: Not equal (due to universes). + :undocumented: .. tacn:: unify @term @term :name: unify @@ -3999,6 +4044,7 @@ succeeds, and results in an error otherwise. instantiating existential variables. .. exn:: Unable to unify @term with @term. + :undocumented: .. tacv:: unify @term @term with @ident @@ -4013,6 +4059,7 @@ succeeds, and results in an error otherwise. by :tacn:`eapply` and some other tactics. .. exn:: Not an evar. + :undocumented: .. tacn:: has_evar @term :name: has_evar @@ -4022,6 +4069,7 @@ succeeds, and results in an error otherwise. scans all subterms, including those under binders. .. exn:: No evars. + :undocumented: .. tacn:: is_var @term :name: is_var @@ -4030,6 +4078,7 @@ succeeds, and results in an error otherwise. the current goal context or in the opened sections. .. exn:: Not a variable or hypothesis. + :undocumented: .. _equality: @@ -4041,45 +4090,46 @@ Equality .. tacn:: f_equal :name: f_equal -This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n` -:g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`. Using :tacn:`f_equal` on such a goal -leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up -to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones -(e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically -solved by :tacn:`f_equal`. + This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n` + :g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`. Using :tacn:`f_equal` on such a goal + leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up + to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones + (e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically + solved by :tacn:`f_equal`. .. tacn:: reflexivity :name: reflexivity -This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` -and `u` are convertible and then solves the goal. It is equivalent to -``apply refl_equal``. + This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` + and `u` are convertible and then solves the goal. It is equivalent to + ``apply refl_equal``. -.. exn:: The conclusion is not a substitutive equation. + .. exn:: The conclusion is not a substitutive equation. + :undocumented: -.. exn:: Unable to unify ... with ... + .. exn:: Unable to unify ... with ... + :undocumented: .. tacn:: symmetry :name: symmetry -This tactic applies to a goal that has the form :g:`t=u` and changes it into -:g:`u=t`. + This tactic applies to a goal that has the form :g:`t=u` and changes it into + :g:`u=t`. .. tacv:: symmetry in @ident - If the statement of the hypothesis ident has the form :g:`t=u`, the tactic - changes it to :g:`u=t`. - + If the statement of the hypothesis ident has the form :g:`t=u`, the tactic + changes it to :g:`u=t`. .. tacn:: transitivity @term :name: transitivity -This tactic applies to a goal that has the form :g:`t=u` and transforms it -into the two subgoals :n:`t=@term` and :n:`@term=u`. + This tactic applies to a goal that has the form :g:`t=u` and transforms it + into the two subgoals :n:`t=@term` and :n:`@term=u`. Equality and inductive sets @@ -4133,10 +4183,10 @@ symbol :g:`=`. instantiate parameters or hypotheses of :n:`@term`. .. tacv:: esimplify_eq @num -.. tacv:: esimplify_eq @term {? with @bindings_list} - :name: esimplify_eq + 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 + This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the type of the hypothesis referred to by :n:`@num`, has uninstantiated parameters, these parameters are left as existential variables. @@ -4168,35 +4218,35 @@ Inversion .. tacn:: functional inversion @ident :name: functional inversion -:tacn:`functional inversion` is a tactic that performs inversion on hypothesis -:n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid -{+ @term}` where :n:`@qualid` must have been defined using Function (see -:ref:`advanced-recursive-functions`). Note that this tactic is only -available after a ``Require Import FunInd``. + :tacn:`functional inversion` is a tactic that performs inversion on hypothesis + :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid + {+ @term}` where :n:`@qualid` must have been defined using Function (see + :ref:`advanced-recursive-functions`). Note that this tactic is only + available after a ``Require Import FunInd``. + .. exn:: Hypothesis @ident must contain at least one Function. + :undocumented: -.. exn:: Hypothesis @ident must contain at least one Function. -.. exn:: Cannot find inversion information for hypothesis @ident. + .. exn:: Cannot find inversion information for hypothesis @ident. - This error may be raised when some inversion lemma failed to be generated by - Function. + This error may be raised when some inversion lemma failed to be generated by + Function. -.. tacv:: functional inversion @num + .. tacv:: functional inversion @num - This does the same thing as :n:`intros until @num` folowed by - :n:`functional inversion @ident` where :token:`ident` is the - identifier for the last introduced hypothesis. + This does the same thing as :n:`intros until @num` folowed by + :n:`functional inversion @ident` where :token:`ident` is the + identifier for the last introduced hypothesis. -.. tacv:: functional inversion ident qualid -.. tacv:: functional inversion num qualid + .. tacv:: functional inversion @ident @qualid + functional inversion @num @qualid - If the hypothesis :n:`@ident` (or :n:`@num`) has a type of the form - :n:`@qualid`:sub:`1` :n:`@term`:sub:`1` ... :n:`@term`:sub:`n` :n:`= - @qualid`:sub:`2` :n:`@term`:sub:`n+1` ... :n:`@term`:sub:`n+m` where - :n:`@qualid`:sub:`1` and :n:`@qualid`:sub:`2` are valid candidates to - functional inversion, this variant allows choosing which :n:`@qualid` is - inverted. + If the hypothesis :token:`ident` (or :token:`num`) has a type of the form + :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where + :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to + functional inversion, this variant allows choosing which :token:`qualid` + is inverted. Classical tactics ----------------- @@ -4206,15 +4256,14 @@ loaded. A few more tactics are available. Make sure to load the module using the ``Require Import`` command. .. tacn:: classical_left - :name: classical_left -.. tacv:: classical_right - :name: classical_right + classical_right + :name: classical_left; classical_right - The tactics ``classical_left`` and ``classical_right`` are the analog of the - left and right but using classical logic. They can only be used for - disjunctions. Use ``classical_left`` to prove the left part of the + These tactics are the analog of :tacn:`left` and :tacn:`right` + but using classical logic. They can only be used for + disjunctions. Use :tacn:`classical_left` to prove the left part of the disjunction with the assumption that the negation of right part holds. - Use ``classical_right`` to prove the right part of the disjunction with + Use :tacn:`classical_right` to prove the right part of the disjunction with the assumption that the negation of left part holds. .. _tactics-automating: @@ -4226,93 +4275,92 @@ Automating .. tacn:: btauto :name: btauto -The tactic :tacn:`btauto` implements a reflexive solver for boolean -tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are -constructed over the following grammar: + The tactic :tacn:`btauto` implements a reflexive solver for boolean + tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are + constructed over the following grammar: -.. _btauto_grammar: + .. _btauto_grammar: - .. productionlist:: `sentence` - t : x - :∣ true - :∣ false - :∣ orb t1 t2 - :∣ andb t1 t2 - :∣ xorb t1 t2 - :∣ negb t - :∣ if t1 then t2 else t3 + .. productionlist:: `sentence` + t : x + :∣ true + :∣ false + :∣ orb t1 t2 + :∣ andb t1 t2 + :∣ xorb t1 t2 + :∣ negb t + :∣ if t1 then t2 else t3 - Whenever the formula supplied is not a tautology, it also provides a - counter-example. + Whenever the formula supplied is not a tautology, it also provides a + counter-example. - Internally, it uses a system very similar to the one of the ring - tactic. + Internally, it uses a system very similar to the one of the ring + tactic. - Note that this tactic is only available after a ``Require Import Btauto``. + Note that this tactic is only available after a ``Require Import Btauto``. -.. exn:: Cannot recognize a boolean equality. + .. exn:: Cannot recognize a boolean equality. - The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` - doesn't introduce variables into the context on its own. + The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` + doesn't introduce variables into the context on its own. .. tacn:: omega :name: omega -The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision -procedure for Presburger arithmetic. It solves quantifier-free -formulas built with `~`, `\/`, `/\`, `->` on top of equalities, -inequalities and disequalities on both the type :g:`nat` of natural numbers -and :g:`Z` of binary integers. This tactic must be loaded by the command -``Require Import Omega``. See the additional documentation about omega -(see Chapter :ref:`omega`). + The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision + procedure for Presburger arithmetic. It solves quantifier-free + formulas built with `~`, `\/`, `/\`, `->` on top of equalities, + inequalities and disequalities on both the type :g:`nat` of natural numbers + and :g:`Z` of binary integers. This tactic must be loaded by the command + ``Require Import Omega``. See the additional documentation about omega + (see Chapter :ref:`omega`). .. tacn:: ring :name: ring + + This tactic solves equations upon polynomial expressions of a ring + (or semiring) structure. It proceeds by normalizing both hand sides + of the equation (w.r.t. associativity, commutativity and + distributivity, constant propagation) and comparing syntactically the + results. + .. tacn:: ring_simplify {+ @term} :name: ring_simplify -The :n:`ring` tactic solves equations upon polynomial expressions of a ring -(or semiring) structure. It proceeds by normalizing both hand sides -of the equation (w.r.t. associativity, commutativity and -distributivity, constant propagation) and comparing syntactically the -results. - -:n:`ring_simplify` applies the normalization procedure described above to -the given terms. The tactic then replaces all occurrences of the terms -given in the conclusion of the goal by their normal forms. If no term -is given, then the conclusion should be an equation and both hand -sides are normalized. + This tactic applies the normalization procedure described above to + the given terms. The tactic then replaces all occurrences of the terms + given in the conclusion of the goal by their normal forms. If no term + is given, then the conclusion should be an equation and both hand + sides are normalized. See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to declare new ring structures. All declared field structures can be printed with the ``Print Rings`` command. .. tacn:: field - :name: field -.. tacn:: field_simplify {+ @term} - :name: field_simplify -.. tacn:: field_simplify_eq - :name: field_simplify_eq - -The field tactic is built on the same ideas as ring: this is a -reflexive tactic that solves or simplifies equations in a field -structure. The main idea is to reduce a field expression (which is an -extension of ring expressions with the inverse and division -operations) to a fraction made of two polynomial expressions. - -Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` -replaces the provided terms by their reduced fraction. -:n:`field_simplify_eq` applies when the conclusion is an equation: it -simplifies both hand sides and multiplies so as to cancel -denominators. So it produces an equation without division nor inverse. - -All of these 3 tactics may generate a subgoal in order to prove that -denominators are different from zero. - -See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to -declare new field structures. All declared field structures can be -printed with the Print Fields command. + field_simplify {+ @term} + field_simplify_eq + :name: field; field_simplify; field_simplify_eq + + The field tactic is built on the same ideas as ring: this is a + reflexive tactic that solves or simplifies equations in a field + structure. The main idea is to reduce a field expression (which is an + extension of ring expressions with the inverse and division + operations) to a fraction made of two polynomial expressions. + + Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` + replaces the provided terms by their reduced fraction. + :n:`field_simplify_eq` applies when the conclusion is an equation: it + simplifies both hand sides and multiplies so as to cancel + denominators. So it produces an equation without division nor inverse. + + All of these 3 tactics may generate a subgoal in order to prove that + denominators are different from zero. + + See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to + declare new field structures. All declared field structures can be + printed with the Print Fields command. .. example:: @@ -4373,16 +4421,16 @@ Non-logical tactics .. tacn:: revgoals :name: revgoals -This tactics reverses the list of the focused goals. + This tactics reverses the list of the focused goals. -.. example:: + .. example:: - .. coqtop:: all reset + .. coqtop:: all reset - Parameter P : nat -> Prop. - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: revgoals. + Parameter P : nat -> Prop. + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: revgoals. .. tacn:: shelve :name: shelve diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a69cf209c7..4bc85f386d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -20,10 +20,13 @@ Displaying Error messages: .. exn:: @qualid not a defined object. + :undocumented: .. exn:: Universe instance should have length @num. + :undocumented: .. exn:: This object does not support universe names. + :undocumented: .. cmdv:: Print Term @qualid @@ -81,9 +84,9 @@ and tables: * A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`. * An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. * A :production:`table` contains a set of strings or qualids. -* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`. +* In addition, some commands provide settings, such as :cmd:`Extraction Language`. -.. FIXME Convert `Extraction Language OCaml` to an option. +.. FIXME Convert "Extraction Language" to an option. Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. @@ -538,8 +541,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard will use the default extension ``.v``. .. cmdv:: Load Verbose @ident - - .. cmdv:: Load Verbose @string + Load Verbose @string Display, while loading, the answers of |Coq| to each command (including tactics) contained in @@ -548,10 +550,13 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard .. seealso:: Section :ref:`controlling-display`. .. exn:: Can’t find file @ident on loadpath. + :undocumented: .. exn:: Load is not supported inside proofs. + :undocumented: .. exn:: Files processed by Load cannot leave open proofs. + :undocumented: .. _compiled-files: @@ -620,6 +625,7 @@ file is a particular case of module called *library file*. comes from a given package by making explicit its absolute root. .. exn:: Cannot load qualid: no physical path bound to dirpath. + :undocumented: .. exn:: Cannot find library foo in loadpath. @@ -684,8 +690,10 @@ file is a particular case of module called *library file*. where they occur, even if outside a section. .. exn:: File not found on loadpath: @string. + :undocumented: .. exn:: Loading of ML object file forbidden in a native Coq. + :undocumented: .. cmd:: Print ML Modules @@ -812,6 +820,7 @@ interactively, they cannot be part of a vernacular file loaded via over the name of a module or of an object inside a module. .. exn:: @ident: no such entry. + :undocumented: .. cmdv:: Reset Initial @@ -953,6 +962,7 @@ Quitting and debugging it prints a message indicating that the failure did not occur. .. exn:: The command has not failed! + :undocumented: .. _controlling-display: @@ -1136,6 +1146,7 @@ described first. variable nor a constant. .. exn:: The reference is not unfoldable. + :undocumented: .. cmdv:: Print Strategies @@ -1166,41 +1177,41 @@ Controlling the locality of commands .. cmd:: Local @command -.. cmd:: Global @command - -Some commands support a Local or Global prefix modifier to control the -scope of their effect. There are four kinds of commands: - - -+ Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. For these - commands, the Local modifier limits the effect of the command to the - current section or module it occurs in. As an example, the :cmd:`Coercion` - and :cmd:`Strategy` commands belong to this category. -+ Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the Local modifier limits the - effect of the command to the current module if the command does not occur in a - section and the Global modifier extends the effect outside the current - sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong - to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global modifier is not - applicable to them. -+ Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the ``Global`` - modifier extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` - (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands - belong to this category. -+ Commands whose default behavior is to extend their effect outside - sections but not outside modules when they occur in a section and to - extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier - limits the effect to the current section or module while the Global - modifier extends the effect outside the module even when the command - occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this - category. + Global @command + + Some commands support a Local or Global prefix modifier to control the + scope of their effect. There are four kinds of commands: + + + + Commands whose default is to extend their effect both outside the + section and the module or library file they occur in. For these + commands, the Local modifier limits the effect of the command to the + current section or module it occurs in. As an example, the :cmd:`Coercion` + and :cmd:`Strategy` commands belong to this category. + + Commands whose default behavior is to stop their effect at the end + of the section they occur in but to extend their effect outside the module or + library file they occur in. For these commands, the Local modifier limits the + effect of the command to the current module if the command does not occur in a + section and the Global modifier extends the effect outside the current + sections and current module if the command occurs in a section. As an example, + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + to this category. Notice that a subclass of these commands do not support + extension of their scope outside sections at all and the Global modifier is not + applicable to them. + + Commands whose default behavior is to stop their effect at the end + of the section or module they occur in. For these commands, the ``Global`` + modifier extends their effect outside the sections and modules they + occur in. The :cmd:`Transparent` and :cmd:`Opaque` + (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + belong to this category. + + Commands whose default behavior is to extend their effect outside + sections but not outside modules when they occur in a section and to + extend their effect outside the module or library file they occur in + when no section contains them.For these commands, the Local modifier + limits the effect to the current section or module while the Global + modifier extends the effect outside the module even when the command + occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this + category. .. _exposing-constants-to-ocaml-libraries: |