diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 12 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sections.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 122 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 671 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 35 |
14 files changed, 428 insertions, 462 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 27ae7cea3a..039a23e8c2 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -535,11 +535,19 @@ pass additional arguments such as ``using relation``. .. tacn:: setoid_reflexivity setoid_symmetry {? in @ident } setoid_transitivity @one_term - setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @occurrences } {? in @ident } - setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @occurrences + setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @rewrite_occs } {? in @ident } + setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @rewrite_occs setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 } :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace + .. todo: move rewrite_occs to rewrite chapter when that chapter is revised + + .. insertprodn rewrite_occs rewrite_occs + + .. prodn:: + rewrite_occs ::= {+ @integer } + | @ident + The ``using relation`` arguments cannot be passed to the unprefixed form. The latter argument tells the tactic what parametric relation should be used to replace the first tactic argument with the second one. If @@ -714,6 +722,8 @@ instances are tried at each node of the search tree). To speed it up, declare your constant as rigid for proof search using the command :cmd:`Typeclasses Opaque`. +.. _strategies4rewriting: + Strategies for rewriting ------------------------ diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 98445fca1a..4143d836c4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -335,12 +335,6 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info one_pattern - - .. prodn:: - hint_info ::= %| {? @natural } {? @one_pattern } - one_pattern ::= @one_term - Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of @@ -503,7 +497,7 @@ Typeclasses Transparent, Typeclasses Opaque It is useful when some constants prevent some unifications and make resolution fail. It is also useful to declare constants which - should never be unfolded during proof-search, like fixpoints or + should never be unfolded during proof search, like fixpoints or anything which does not look like an abbreviation. This can additionally speed up proof search as the typeclass map can be indexed by such rigid constants (see @@ -555,7 +549,7 @@ Settings This can be expensive as it requires rebuilding hint clauses dynamically, and does not benefit from the invertibility status of the product introduction rule, resulting in potentially more - expensive proof-search (i.e. more useless backtracking). + expensive proof search (i.e. more useless backtracking). .. flag:: Typeclass Resolution For Conversion diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 4615a8dfca..bb78b142ca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -412,7 +412,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} - cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| + | = | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 24fa71059c..249c7794be 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -551,7 +551,7 @@ Flags, options and attributes ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann). - **Added:** - The :cmd:`Hint` commands now accept the :attr:`export` locality as + The :ref:`Hint <creating_hints>` commands now accept the :attr:`export` locality as an attribute, allowing to make import-scoped hints (`#11812 <https://github.com/coq/coq/pull/11812>`_, by Pierre-Marie Pédrot). @@ -3170,7 +3170,7 @@ Vernacular Commands `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting globally the opacity flag of variables and constants in hint databases, - overwriting the opacity set of the hint database. + overriding the opacity setting of the hint database. - Added generic syntax for "attributes", as in: `#[local] Lemma foo : bar.` - Added the `Numeral Notation` command for registering decimal numeral @@ -4045,7 +4045,7 @@ constraints can now be left floating around and be seen by the user thanks to a new option. The Keyed Unification mode has been improved by Matthieu Sozeau. -The typeclass resolution engine and associated proof-search tactic have +The typeclass resolution engine and associated proof search tactic have been reimplemented on top of the proof-engine monad, providing better integration in tactics, and new options have been introduced to control it, by Matthieu Sozeau with help from Théo Zimmermann. @@ -5140,7 +5140,7 @@ Program - Hints costs are now correctly taken into account (potential source of incompatibilities). - Documented the Hint Cut command that allows control of the - proof-search during typeclass resolution (see reference manual). + proof search during typeclass resolution (see reference manual). API @@ -5776,7 +5776,7 @@ Libraries comes first. By default, the power function now takes two BigN. - Creation of Vector, an independent library for lists indexed by their length. - Vectors' names overwrite lists' one so you should not "Import" the library. + Vectors' names override lists' one so you should not "Import" the library. All old names changed: function names follow the ocaml ones and, for example, Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing Vector.VectorNotations. @@ -6830,7 +6830,7 @@ Tactics - Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. -- Tactic "pose proof" supports name overwriting in case of specialization of an +- Tactic "pose proof" supports name overriding in case of specialization of an hypothesis. - Semi-decision tactic "jp" for first-order intuitionistic logic moved to user diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index af5d1e3a00..246568d3c1 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -188,10 +188,8 @@ nitpick_ignore = [ ('token', token) for token in [ 'conversion', 'where', 'oriented_rewriter', - 'hintbases', 'bindings_with_parameters', - 'destruction_arg', - 'clause_dft_concl' + 'destruction_arg' ]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 251b5e4955..9fda2ab1fa 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -8,14 +8,13 @@ Inductive types .. cmd:: Inductive @inductive_definition {* with @inductive_definition } - .. insertprodn inductive_definition cumul_ident_decl + .. insertprodn inductive_definition constructor .. prodn:: - inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + inductive_definition ::= {? > } @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } - cumul_ident_decl ::= @ident {? @cumul_univ_decl } This command defines one or more inductive types and its constructors. Coq generates destructors diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 54252689e1..6d96e15202 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -155,7 +155,8 @@ are now available through the dot notation. #. Interactive modules and module types can be nested. #. Interactive modules and module types can't be defined inside of :ref:`sections<section-mechanism>`. Sections can be defined inside of interactive modules and module types. - #. Hints and notations (:cmd:`Hint` and :cmd:`Notation` commands) can also appear inside interactive + #. Hints and notations (the :ref:`Hint <creating_hints>` and :cmd:`Notation` + commands) can also appear inside interactive modules and module types. Note that with module definitions like: :n:`Module @ident__1 : @module_type := @ident__2.` diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index df50dbafe3..75389bb259 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -69,7 +69,8 @@ Sections create local contexts which can be shared across multiple definitions. :undocumented: .. note:: - Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which + Most commands, such as the :ref:`Hint <creating_hints>` commands, + :cmd:`Notation` and option management commands that appear inside a section are canceled when the section is closed. .. cmd:: Let @ident_decl @def_body diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2fc3c9f748..87a367fc93 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1637,9 +1637,10 @@ Testing boolean expressions: guard .. tacn:: guard @int_or_var @comparison @int_or_var :name: guard - .. insertprodn comparison comparison + .. insertprodn int_or_var comparison .. prodn:: + int_or_var ::= {| @integer | @ident } comparison ::= = | < | <= @@ -1761,7 +1762,7 @@ Defining |Ltac| symbols "Ltac intros := idtac" seems like it redefines/hides an existing tactic, but in fact it creates a tactic which can only be called by its qualified name. This is true in - general of tactic notations. The only way to overwrite most + general of tactic notations. The only way to override most primitive tactics, and any user-defined tactic notation, is with another tactic notation. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index a46f4fb894..375129c02d 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1475,7 +1475,7 @@ Other nonterminals that have syntactic classes are listed here. * - :n:`clause` - :token:`ltac2_clause` - - :token:`clause_dft_concl` + - :token:`occurrences` * - :n:`occurrences` - :token:`q_occurrences` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4f01559cad..8f5c045929 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -466,52 +466,82 @@ Examples: .. _occurrencessets: -Occurrence sets and occurrence clauses -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -An occurrence clause is a modifier to some tactics that obeys the -following syntax: - - .. prodn:: - occurrence_clause ::= in @goal_occurrences - goal_occurrences ::= {*, @ident {? @at_occurrences } } {? |- {? * {? @at_occurrences } } } - | * |- {? * {? @at_occurrences } } - | * - at_occurrences ::= at @occurrences - occurrences ::= {? - } {* @natural } - -The role of an occurrence clause is to select a set of occurrences of a term -in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate -that occurrences have to be selected in the hypotheses named :token:`ident`. -If no numbers are given for hypothesis :token:`ident`, then all the -occurrences of :token:`term` in the hypothesis are selected. If numbers are -given, they refer to occurrences of :token:`term` when the term is printed -using the :flag:`Printing All` flag, counting from left to right. In particular, -occurrences of :token:`term` in implicit arguments -(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are -counted. - -If a minus sign is given between ``at`` and the list of occurrences, it -negates the condition so that the clause denotes all the occurrences -except the ones explicitly mentioned after the minus sign. - -As an exception to the left-to-right order, the occurrences in -the return subexpression of a match are considered *before* the -occurrences in the matched term. - -In the second case, the ``*`` on the left of ``|-`` means that all occurrences -of term are selected in every hypothesis. - -In the first and second case, if ``*`` is mentioned on the right of ``|-``, the -occurrences of the conclusion of the goal have to be selected. If some numbers -are given, then only the occurrences denoted by these numbers are selected. If -no numbers are given, all occurrences of :token:`term` in the goal are selected. - -Finally, the last notation is an abbreviation for ``* |- *``. Note also -that ``|-`` is optional in the first case when no ``*`` is given. - -Here are some tactics that understand occurrence clauses: :tacn:`set`, -:tacn:`remember`, :tacn:`induction`, :tacn:`destruct`. +Occurrence clauses +~~~~~~~~~~~~~~~~~~ + +An :gdef:`occurrence` is a subterm of a goal or hypothesis that +matches a pattern provided by a tactic. Occurrence clauses +select a subset of the ocurrences in a goal and/or in +one or more of its hypotheses. + + .. insertprodn occurrences concl_occs + + .. prodn:: + occurrences ::= at @occs_nums + | in @goal_occurrences + occs_nums ::= {? - } {+ @nat_or_var } + nat_or_var ::= {| @natural | @ident } + goal_occurrences ::= {+, @hyp_occs } {? %|- {? @concl_occs } } + | * %|- {? @concl_occs } + | %|- {? @concl_occs } + | {? @concl_occs } + hyp_occs ::= @hypident {? at @occs_nums } + hypident ::= @ident + | ( type of @ident ) + | ( value of @ident ) + concl_occs ::= * {? at @occs_nums } + + :n:`@occurrences` + The first form of :token:`occurrences` selects occurrences in + the conclusion of the goal. The second form can select occurrences + in the goal conclusion and in one or more hypotheses. + + :n:`{? - } {+ @nat_or_var }` + Selects the specified occurrences within a single goal or hypothesis. + Occurrences are numbered from left to right starting with 1 when the + goal is printed with the :flag:`Printing All` flag. (In particular, occurrences + in :ref:`implicit arguments <ImplicitArguments>` and + :ref:`coercions <Coercions>` are counted but not shown by default.) + + Specifying `-` includes all occurrences *except* the ones listed. + + :n:`{*, @hyp_occs } {? %|- {? @concl_occs } }` + Selects occurrences in the specified hypotheses and the + specified occurrences in the conclusion. + + :n:`* %|- {? @concl_occs }` + Selects all occurrences in all hypotheses and the + specified occurrences in the conclusion. + + :n:`%|- {? @concl_occs }` + Selects the specified occurrences in the conclusion. + + :n:`@goal_occurrences ::= {? @concl_occs }` + Selects all occurrences in all hypotheses and in the specified occurrences + in the conclusion. + + :n:`@hypident {? at @occs_nums }` + Omiting :token:`occs_nums` selects all occurrences within the hypothesis. + + :n:`@hypident ::= @ident` + Selects the hypothesis named :token:`ident`. + + :n:`( type of @ident )` + Selects the type part of the named hypothesis (e.g. `: nat`). + + :n:`( value of @ident )` + Selects the value part of the named hypothesis (e.g. `:= 1`). + + :n:`@concl_occs ::= * {? at @occs_nums }` + Selects occurrences in the conclusion. '*' by itself selects all occurrences. + :n:`@occs_nums` selects the specified occurrences. + + Use `in *` to select all occurrences in all hypotheses and the conclusion, + which is equivalent to `in * |- *`. Use `* |-` to select all occurrences + in all hypotheses. + +Tactics that use occurrence clauses include :tacn:`set`, +:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. .. seealso:: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 86d1d25745..e7db9cfaca 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1136,7 +1136,7 @@ Controlling the locality of commands Some commands support an :attr:`export` attribute. The effect of the attribute is to make the effect of the command available when the module containing it is imported. It is supported in - particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + particular by the :ref:`Hint <creating_hints>`, :cmd:`Set` and :cmd:`Unset` commands. .. _controlling-typing-flags: diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index cc4ab76502..472df2bd91 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -4,104 +4,87 @@ Programmable proof search ========================= -.. tacn:: auto - :name: auto +.. tacn:: auto {? @nat_or_var } {? @auto_using } {? @hintbases } - This tactic implements a Prolog-like resolution procedure to solve the + .. insertprodn auto_using hintbases + + .. prodn:: + auto_using ::= using {+, @one_term } + hintbases ::= with * + | with {+ @ident } + + Implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the :tacn:`assumption` tactic, then it reduces the goal to an atomic one using :tacn:`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. + the list of tactics associated with the head symbol of the goal and + tries to apply one of them. Lower cost tactics are tried before higher-cost + tactics. This process is recursively applied to the generated subgoals. - By default, :tacn:`auto` only uses the hypotheses of the current goal and - the hints of the database named ``core``. + :n:`@nat_or_var` + Specifies the maximum search depth. The default is 5. - .. warning:: + :n:`using {+, @one_term }` - :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to - :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will - fail even if applying manually one of the hints would succeed. + Uses lemmas :n:`{+, @one_term }` in addition to hints. If :n:`@one_term` is an + inductive type, the collection of its constructors are added as hints. - .. tacv:: auto @natural + Note that hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @one_term` + may fail where :n:`apply @one_term` succeeds. - Forces the search depth to be :token:`natural`. The maximal search depth - is 5 by default. + .. todo + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! - .. tacv:: auto with {+ @ident} + :n:`with *` + Use all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than explicitly + selecting the required databases. - Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + :n:`with {+ @ident }` + Use the hint databases :n:`{+ @ident}` in addition to the database ``core``. + Use the fake database `nocore` to omit `core`. - .. note:: + If no `with` clause is given, :tacn:`auto` only uses the hypotheses of the + current goal and the hints of the database named ``core``. - Use the fake database `nocore` if you want to *not* use the `core` - database. + :tacn:`auto` generally either completely solves the goal or + leaves it unchanged. Use :tacn:`solve` `[ auto ]` if you want a failure + when they don't solve the goal. :tacn:`auto` will fail if :tacn:`fail` + or :tacn:`gfail` are invoked directly or indirectly, in which case setting + the :flag:`Ltac Debug` may help you debug the failure. - .. tacv:: auto with * + .. warning:: - Uses all existing hint databases. Using this variant is highly discouraged - in finished scripts since it is both slower and less robust than the variant - where the required databases are explicitly listed. + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. .. seealso:: - :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of + :ref:`thehintsdatabasesforautoandeauto` for the list of pre-defined databases and the way to create or extend a database. - .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } - - Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an - inductive type, it is the collection of its constructors which are added - as hints. - - .. note:: - - The hints passed through the `using` clause are used in the same - way as if they were passed through a hint database. Consequently, - they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` - may fail where :n:`apply @qualid` succeeds. - - Given that this can be seen as counter-intuitive, it could be useful - to have an option to use full-blown :tacn:`apply` for lemmas passed - through the `using` clause. Contributions welcome! - - .. tacv:: info_auto + .. tacn:: info_auto {? @nat_or_var } {? @auto_using } {? @hintbases } Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. - .. tacv:: debug auto - :name: debug auto + .. tacn:: debug auto {? @nat_or_var } {? @auto_using } {? @hintbases } Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} - - This is the most general form, combining the various options. - -.. tacv:: trivial - :name: trivial - - This tactic is a restriction of :tacn:`auto` that is not recursive - and tries only hints that cost `0`. Typically it solves trivial - equalities like :g:`X=X`. - - .. tacv:: trivial with {+ @ident} - trivial with * - trivial using {+ @qualid} - debug trivial - info_trivial - {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} - :name: _; _; _; debug trivial; info_trivial; _ - :undocumented: +.. tacn:: trivial {? @auto_using } {? @hintbases } + debug trivial {? @auto_using } {? @hintbases } + info_trivial {? @auto_using } {? @hintbases } -.. note:: - :tacn:`auto` and :tacn:`trivial` either solve completely the goal or - else succeed without changing the goal. Use :g:`solve [ auto ]` and - :g:`solve [ trivial ]` if you would prefer these tactics to fail when - they do not manage to solve the goal. + Like :tacn:`auto`, but is not recursive + and only tries hints with zero cost. Typically used to solve goals + for which a lemma is already available in the specified :n:`hintbases`. .. flag:: Info Auto Debug Auto @@ -111,10 +94,9 @@ Programmable proof search These flags enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics. -.. tacn:: eauto - :name: eauto +.. tacn:: eauto {? @nat_or_var } {? @auto_using } {? @hintbases } - This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try + 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 internally uses a tactic close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` @@ -133,12 +115,13 @@ Programmable proof search Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. - Note that ``ex_intro`` should be declared as a hint. + `ex_intro` is declared as a hint so the proof succeeds. + .. seealso:: :ref:`thehintsdatabasesforautoandeauto` - .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} + .. tacn:: info_eauto {? @nat_or_var } {? @auto_using } {? @hintbases } - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`info_eauto` are the same as for :tacn:`info_auto`. :tacn:`eauto` also obeys the following flags: @@ -146,34 +129,55 @@ Programmable proof search Debug Eauto :undocumented: - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. tacn:: debug eauto {? @nat_or_var } {? @auto_using } {? @hintbases } + Behaves like :tacn:`eauto` but shows the tactics it tries to solve the goal, + including failing paths. + + .. tacn:: bfs eauto {? @nat_or_var } {? @auto_using } {? @hintbases } + + Like :tacn:`eauto`, but uses a + `breadth-first search <https://en.wikipedia.org/wiki/Breadth-first_search>`_. -.. tacn:: autounfold with {+ @ident} - :name: autounfold +.. tacn:: autounfold {? @hintbases } {? @occurrences } - This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` + Unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in @goal_occurrences + :n:`@occurrences` + Performs the unfolding in the specified occurrences. The :n:`at @occs_nums` + clause of :n:`@occurrences` is not supported. + +.. tacn:: autorewrite {? * } with {+ @ident } {? @occurrences } {? using @ltac_expr } + + `*` + If present, rewrite all occurrences whose side conditions are solved. - Performs the unfolding in the given clause (:token:`goal_occurrences`). + .. todo: This may not always work as described, see #4976 #7672 and + https://github.com/coq/coq/issues/1933#issuecomment-337497938 as + mentioned here: https://github.com/coq/coq/pull/13343#discussion_r527801604 -.. tacv:: autounfold with * + :n:`with {+ @ident }` + Specifies the rewriting rule bases to use. - Uses the unfold hints declared in all the hint databases. + :n:`@occurrences` + Performs rewriting in the specified occurrences. Note: the `at` clause + is currently not supported. -.. tacn:: autorewrite with {+ @ident} - :name: autorewrite + .. exn:: The "at" syntax isn't available yet for the autorewrite tactic. - This tactic carries out rewritings according to the rewriting rule - bases :n:`{+ @ident}`. + Appears when there is an `at` clause on the conclusion. - Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until + :n:`using @ltac_expr` + :token:`ltac_expr` is applied to the main subgoal after each rewriting step. + + Applies rewritings according to the rewriting rule bases :n:`{+ @ident }`. + + For each rule base, applies each rewriting 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 + changed then the rules + of this base are processed again. If the main subgoal has not changed then + the next base is processed. For the bases, the behavior is very similar to the processing of the rewriting rules. The rewriting rule bases are built with the :cmd:`Hint Rewrite` @@ -183,31 +187,13 @@ Programmable proof search This tactic may loop if you build non terminating rewriting systems. -.. tacv:: autorewrite with {+ @ident} using @tactic - - Performs, in the same way, all the rewritings of the bases :n:`{+ @ident}` - applying tactic to the main subgoal after each rewriting step. - -.. tacv:: autorewrite with {+ @ident} in @qualid - - Performs all the rewritings in hypothesis :n:`@qualid`. - -.. tacv:: autorewrite with {+ @ident} in @qualid using @tactic - - Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` - to the main subgoal after each rewriting step. - -.. tacv:: autorewrite with {+ @ident} in @goal_occurrences - - Performs all the rewriting in the clause :n:`@goal_occurrences`. - .. seealso:: - :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by + :cmd:`Hint Rewrite` for feeding the database of lemmas used by :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. + Also see :ref:`strategies4rewriting`. .. tacn:: easy - :name: easy This tactic tries to solve the current goal by a number of standard closing steps. In particular, it tries to close the current goal using the closing tactics @@ -220,45 +206,43 @@ Programmable proof search This tactic solves goals that belong to many common classes; in particular, many cases of unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. -.. tacv:: now @tactic - :name: now +.. tacn:: now @ltac_expr Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. -Controlling automation --------------------------- - .. _thehintsdatabasesforautoandeauto: The hints databases for auto and eauto -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-------------------------------------- The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database -maps head symbols to a list of hints. - -.. cmd:: Print Hint @ident +maps head symbols to a list of hints. Use the :cmd:`Print Hint` command to view +the database. - Use this command - to display the hints associated to the head symbol :n:`@ident` - (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative - integer, and an optional pattern. The hints with lower cost are tried first. A - hint is tried by :tacn:`auto` when the conclusion of the current goal matches its - pattern or when it has no pattern. +Each hint has a cost that is a nonnegative +integer and an optional pattern. Hints with lower costs are tried first. +:tacn:`auto` tries a hint when the conclusion of the current goal matches its +pattern or when the hint has no pattern. Creating Hint databases -``````````````````````` +----------------------- -One can optionally declare a hint database using the command -:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be -automatically created. +Hint databases can be created with the :cmd:`Create HintDb` command or implicitly +by adding a hint to an unknown database. We recommend you always use :cmd:`Create HintDb` +and then imediately use :cmd:`Hint Constants` and :cmd:`Hint Variables` to make +those settings explicit. -.. cmd:: Create HintDb @ident {? discriminated} +Note that the default transparency +settings differ between these two methods of creation. Databases created with +:cmd:`Create HintDb` have the default setting `Transparent` for both `Variables` +and `Constants`, while implicitly created databases have the `Opaque` setting. - This command creates a new database named :n:`@ident`. The database is +.. cmd:: Create HintDb @ident {? discriminated } + + Creates a new hint database named :n:`@ident`. The database is implemented by a Discrimination Tree (DT) that serves as an index of all the lemmas. The DT can use transparency information to decide if a constant should be indexed or not - (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), making the retrieval more efficient. The legacy implementation (the default one for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` goals), for non-Immediate hints and does not make use of transparency @@ -270,149 +254,144 @@ automatically created. from the order in which they were inserted, making this implementation observationally different from the legacy one. -.. cmd:: Hint @hint_definition : {+ @ident} +.. _creating_hints: + +Creating Hints +-------------- - The general command to add a hint to some databases :n:`{+ @ident}`. + The various `Hint` commands share these elements: - This command supports the :attr:`local`, :attr:`global` and :attr:`export` - locality attributes. When no locality is explictly given, the - command is :attr:`local` inside a section and :attr:`global` otherwise. + :n:`{? : {+ @ident } }` specifies the hint database(s) to add to. + *(Deprecated since version 8.10:* If no :token:`ident`\s + are given, the hint is added to the `core` database.) + + Outside of sections, these commands support the :attr:`local`, :attr:`export` + and :attr:`global` attributes. :attr:`global` is the default. Inside sections, + only the :attr:`local` attribute is supported because hints are local to sections. + :attr:`local` hints are never visible from other modules, even if they - require or import the current module. Inside a section, the :attr:`local` - attribute is useless since hints do not survive anyway to the closure of - sections. + :cmd:`Import` or :cmd:`Require` the current module. - + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. + + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current + module, but not when they only :cmd:`Require` it. This attribute is supported by + all `Hint` commands except for :cmd:`Hint Rewrite`. - + :attr:`global` hints are made available by merely requiring the current - module. + + :attr:`global` hints are visible from other modules when they :cmd:`Import` or + :cmd:`Require` the current module. .. deprecated:: 8.13 - The default value for hint locality is scheduled to change in a future + The default value for hint locality will change in a future release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore triggering a deprecation - warning. It is recommended to use :attr:`export` whenever possible - - The various possible :production:`hint_definition`\s are given below. - - .. cmdv:: Hint @hint_definition + specifying an explicit locality will trigger a deprecation + warning. We recommend you use :attr:`export` whenever possible. - No database name is given: the hint is registered in the ``core`` database. + The `Hint` commands are: - .. deprecated:: 8.10 + .. cmd:: Hint Resolve {+ {| @qualid | @one_term } } {? @hint_info } {? : {+ @ident } } + Hint Resolve {| -> | <- } {+ @qualid } {? @natural } {? : {+ @ident } } + :name: Hint Resolve; _ - .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident - :name: Hint Resolve + .. insertprodn hint_info one_pattern - This command adds :n:`simple apply @qualid` to the hint list with the head - symbol of the type of :n:`@qualid`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The - associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@qualid` does not start with a product the tactic added in the hint list - is :n:`exact @qualid`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @qualid` is also stored in - the hints list. If the inferred type of :n:`@qualid` contains a dependent - quantification on a variable which occurs only in the premisses of the type + .. prodn:: + hint_info ::= %| {? @natural } {? @one_pattern } + one_pattern ::= @one_term + + The first form adds each :n:`@qualid` as a hint with the head symbol of the type of + :n:`@qualid` to the specified hint databases (:n:`@ident`\s). The cost of the hint is the number of + subgoals generated by :tacn:`simple apply` :n:`@qualid` or, if specified, :n:`@natural`. The + associated pattern is inferred from the conclusion of the type of + :n:`@qualid` or, if specified, the given :n:`@one_pattern`. + + If the inferred type + of :n:`@qualid` does not start with a product, :tacn:`exact` :n:`@qualid` is added + to the hint list. If the type can be reduced to a type starting with a product, + :tacn:`simple apply` :n:`@qualid` is also added to the hints list. + + If the inferred type of :n:`@qualid` contains a dependent + quantification on a variable which occurs only in the premises 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 + unification with the goal. In this case, the hint is only used by + :tacn:`eauto` / :tacn:`typeclasses eauto`, but not by :tacn:`auto`. A + typical hint that would only be used by :tacn:`eauto` is a transitivity lemma. - .. exn:: @qualid cannot be used as a hint - - The head symbol of the type of :n:`@qualid` is a bound variable - such that this tactic cannot be associated to a constant. - - .. cmdv:: Hint Resolve {+ @qualid} : @ident + :n:`{| -> | <- }` + The second form adds the left-to-right (`->`) or right-ot-left implication (`<-`) + of an equivalence as a hint (informally + the hint will be used as, respectively, :tacn:`apply` :n:`-> @qualid` or + :tacn:`apply` :n:`<- @qualid`, + although as mentioned before, the tactic actually used is a restricted version of + :tacn:`apply`). - Adds each :n:`Hint Resolve @qualid`. + :n:`@one_term` + Permits declaring a hint without declaring a new + constant first, but this is not recommended. - .. cmdv:: Hint Resolve -> @qualid : @ident + .. warn:: Declaring arbitrary terms as hints is fragile; it is recommended to declare a toplevel constant instead + :undocumented: - Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @qualid`, although as mentioned - before, the tactic actually used is a restricted version of - :tacn:`apply`). - - .. cmdv:: Hint Resolve <- @qualid + .. exn:: @qualid cannot be used as a hint - Adds the right-to-left implication of an equivalence as a hint. + The head symbol of the type of :n:`@qualid` is a bound variable + such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Immediate @qualid : @ident - :name: Hint Immediate + .. cmd:: Hint Immediate {+ {| @qualid | @one_term } } {? : {+ @ident } } - This command adds :n:`simple apply @qualid; 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 @qualid` are + Adds :tacn:`simple apply` :n:`@qualid;` :tacn:`trivial` to the hint list for each :n:`@qualid` associated + with the head symbol of the type of :n:`@ident`. This + tactic will fail if all the subgoals generated by :tacn:`simple apply` :n:`@qualid` are not solved immediately by the :tacn:`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 + 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 want to introduce with 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. - .. exn:: @qualid cannot be used as a hint - :undocumented: + .. cmd:: Hint Constructors {+ @qualid } {? : {+ @ident } } - .. cmdv:: Hint Immediate {+ @qualid} : @ident - - Adds each :n:`Hint Immediate @qualid`. - - .. cmdv:: Hint Constructors @qualid : @ident - :name: Hint Constructors - - If :token:`qualid` is an inductive type, this command adds all its constructors as + For each :n:`@qualid` that is an inductive type, adds all its constructors as hints of type ``Resolve``. Then, when the conclusion of current goal has the form :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. .. exn:: @qualid is not an inductive type :undocumented: - .. cmdv:: Hint Constructors {+ @qualid} : @ident - - Extends the previous command for several inductive types. + .. cmd:: Hint Unfold {+ @qualid } {? : {+ @ident } } - .. cmdv:: Hint Unfold @qualid : @ident - :name: Hint Unfold - - This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :token:`qualid`. + For each :n:`@qualid`, adds the tactic :tacn:`unfold` :n:`@qualid` to the + hint list that will only be used when the head constant of the goal is :token:`qualid`. Its cost is 4. - .. cmdv:: Hint Unfold {+ @qualid} - - Extends the previous command for several defined constants. - - .. cmdv:: Hint Transparent {+ @qualid} : @ident - Hint Opaque {+ @qualid} : @ident + .. cmd:: Hint {| Transparent | Opaque } {+ @qualid } {? : {+ @ident } } :name: Hint Transparent; Hint Opaque - This adds transparency hints to the database, making :n:`@qualid` - transparent or opaque constants during resolution. This information is used + Adds transparency hints to the database, making each :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 Variables {| Transparent | Opaque } : @ident - Hint Constants {| Transparent | Opaque } : @ident - :name: Hint Variables; Hint Constants + .. cmd:: Hint {| Constants | Variables } {| Transparent | Opaque } {? : {+ @ident } } + :name: Hint Constants; Hint Variables - This sets the transparency flag used during unification of - hints in the database for all constants or all variables, - overwriting the existing settings of opacity. It is advised - to use this just after a :cmd:`Create HintDb` command. + Sets the transparency flag for constants or variables for the specified hint + databases. + These flags affect the unification of hints in the database. + We advise using this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident - :name: Hint Extern + .. cmd:: Hint Extern @natural {? @one_pattern } => @ltac_expr {? : {+ @ident } } - 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. + Extends :tacn:`auto` with tactics other than :tacn:`apply` and + :tacn:`unfold`. :n:`@natural` is the cost, :n:`@one_term` is the pattern + to match and :n:`@ltac_expr` is the action to apply. + + .. note:: + + Use a :cmd:`Hint Extern` with no pattern to do + pattern matching on hypotheses using ``match goal with`` + inside the tactic. .. example:: @@ -441,80 +420,131 @@ automatically created. .. coqtop:: all Require Import List. - Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. + 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. + info_auto. - .. cmdv:: Hint Cut @regexp : @ident - :name: Hint Cut + .. cmd:: Hint Cut [ @hints_regexp ] {? : {+ @ident } } - .. 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: + .. DISABLED insertprodn hints_regexp hints_regexp .. prodn:: - regexp ::= @ident (hint or instance identifier) + hints_regexp ::= {+ @qualid } (hint or instance identifier) | _ (any hint) - | @regexp | @regexp (disjunction) - | @regexp @regexp (sequence) - | @regexp * (Kleene star) + | @hints_regexp | @hints_regexp (disjunction) + | @hints_regexp @hints_regexp (sequence) + | @hints_regexp * (Kleene star) | emp (empty) | eps (epsilon) - | ( @regexp ) + | ( @hints_regexp ) + + Used to cut the proof search tree according to a regular + expression that matches the paths to be cut. + - 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 that :cmd:`Hint Extern`\’s do not have + During proof search, the path of + successive successful hints on a search branch is recorded as a + list of identifiers for the hints (note that :cmd:`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 :n:`Hint Cut @regexp` is to set the cut expression - to :n:`c | regexp`, the initial cut expression being `emp`. - - .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident - :name: Hint Mode - - 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 ``+``, + For each hint :n:`@qualid` in the hint database, the current path `p` + extended with :n:`@qualid` + is matched against the current cut expression `c` associated with the + hint database. If the match succeeds the hint is *not* applied. + + :n:`Hint Cut @hints_regexp` sets the cut expression + to :n:`c | @hints_regexp`. The initial cut expression is `emp`. + + The output of :cmd:`Print HintDb` shows the cut expression. + + .. warning:: + + There is no operator precedence during parsing, one can + check with :cmd:`Print HintDb` to verify the current cut expression. + + .. warning:: + + These hints currently only apply to typeclass proof search and the + :tacn:`typeclasses eauto` tactic. + + .. cmd:: Hint Mode @qualid {+ {| + | ! | - } } {? : {+ @ident } } + + Sets an optional mode of use for the identifier :n:`@qualid`. When + proof search has a goal that ends in an application of :n:`@qualid` to + arguments :n:`@arg ... @arg`, the mode tells if the hints associated with + :n:`@qualid` can be applied or not. A mode specification is a list of ``+``, ``!`` 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 + existential variables respectively, while outputs can be any term. + + The head of a term is understood here as the applicative head, or the match or projection scrutinee’s head, recursively, casts being ignored. :cmd:`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. + input forces proof search to be driven by that index of the class, with ``!`` + allowing existentials to appear in the index but not at its head. .. note:: - + One can use a :cmd:`Hint Extern` with no pattern to do - pattern matching on hypotheses using ``match goal with`` - inside the tactic. + + 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. + If you want to add hints such as :cmd:`Hint Transparent`, :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass resolution, do not forget to put them in the ``typeclass_instances`` hint database. +.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } + + :n:`{? using @ltac_expr }` + If specified, :n:`@ltac_expr` is applied to the generated subgoals, except for the + main subgoal. + + :n:`{| -> | <- }` + Arrows specify the orientation; left to right (:n:`->`) or right to left (:n:`<-`). + If no arrow is given, the default orientation is left to right (:n:`->`). + + Adds the terms :n:`{+ @one_term }` (their types must be + equalities) to the rewriting bases :n:`{* @ident }`. + Note that the rewriting bases are distinct from the :tacn:`auto` + hint bases and that :tacn:`auto` does not take them into account. + + .. cmd:: Print Rewrite HintDb @ident + + This command displays all rewrite hints contained in :n:`@ident`. + +.. cmd:: Remove Hints {+ @qualid } {? : {+ @ident } } + + Removes the hints associated with the :n:`{+ @qualid }` in databases + :n:`{+ @ident}`. Note: hints created with :cmd:`Hint Extern` currently + can't be removed. The best workaround for this is to make the hints + non global and carefully select which modules you import. + +.. cmd:: Print Hint {? {| * | @reference } } + + :n:`*` + Display all declared hints. + + :n:`@reference` + Display all hints associated with the head symbol :n:`@reference`. + + Displays tactics from the hints list. The default is to show hints that + apply to the conclusion of the current goal. The other forms with :n:`*` + and :n:`@reference` can be used even if no proof is open. + + Each hint has a cost that is a nonnegative + integer and an optional pattern. The hints with lower cost are tried first. + +.. cmd:: Print HintDb @ident + + This command displays all hints from database :n:`@ident`. + Hint databases defined in the Coq standard library -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-------------------------------------------------- Several hint databases are defined in the Coq standard library. The actual content of a database is the collection of hints declared @@ -555,76 +585,8 @@ At Coq startup, only the core database is nonempty and can be used. You are advised not to put your own hints in the core database, but use one or several databases specific to your development. -.. _removehints: - -.. cmd:: Remove Hints {+ @term} : {+ @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. - -**Variants:** - - -.. cmd:: Print Hint @ident - - This command displays only tactics associated with :n:`@ident` in the hints - list. This is independent of the goal being edited, so this command will not - fail if no goal is being edited. - -.. cmd:: Print Hint * - - This command displays all declared hints. - -.. cmd:: Print HintDb @ident - - This command displays all hints from database :n:`@ident`. - -.. _hintrewrite: - -.. cmd:: Hint Rewrite {+ @term} : {+ @ident} - - This vernacular command adds the terms :n:`{+ @term}` (their types must be - equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation - (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto` - hint bases and that :tacn:`auto` does not take them into account. - - This command is synchronous with the section mechanism (see :ref:`section-mechanism`): - when closing a section, all aliases created by ``Hint Rewrite`` in that - section are lost. Conversely, when loading a module, all ``Hint Rewrite`` - declarations at the global level of that module are loaded. - -**Variants:** - -.. cmd:: Hint Rewrite -> {+ @term} : {+ @ident} - - This is strictly equivalent to the command above (we only make explicit the - orientation which otherwise defaults to ->). - -.. cmd:: Hint Rewrite <- {+ @term} : {+ @ident} - - Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in - the bases :n:`{+ @ident}`. - -.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } - - When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the - tactic ``tactic`` will be applied to the generated subgoals, the main subgoal - excluded. - -.. cmd:: Print Rewrite HintDb @ident - - This command displays all rewrite hints contained in :n:`@ident`. - Hint locality -~~~~~~~~~~~~~ +------------- Hints provided by the ``Hint`` commands are erased when closing a section. Conversely, all hints of a module ``A`` that are not defined inside a @@ -649,7 +611,6 @@ option which accepts three flags allowing for a fine-grained handling of non-imported hints. .. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } - :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. :cmd:`Import`: @@ -668,22 +629,12 @@ non-imported hints. .. _tactics-implicit-automation: Setting implicit automation tactics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +----------------------------------- -.. cmd:: Proof with @tactic +.. cmd:: Proof with @ltac_expr {? using @section_var_expr } - 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 ``...``. - In this case the tactic command typed by the user is equivalent to - ``tactic``:sub:`1` ``;tactic``. + Starts a proof in which :token:`ltac_expr` is applied to the active goals + after each tactic that ends with `...` instead of the usual single period. + ":n:`@tactic...`" is equivalent to ":n:`@tactic; @ltac_expr.`". .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - - - .. cmdv:: Proof with @tactic using {+ @ident} - - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - - .. cmdv:: Proof using {+ @ident} with @tactic - - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 9ec568c2c7..2de6b2a18c 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -295,21 +295,21 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Performing computations --------------------------- -.. insertprodn red_expr pattern_occ +.. insertprodn red_expr pattern_occs .. prodn:: red_expr ::= red | hnf - | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | simpl {? @delta_flag } {? {| @reference_occs | @pattern_occs } } | cbv {? @strategy_flag } | cbn {? @strategy_flag } | lazy {? @strategy_flag } | compute {? @delta_flag } - | vm_compute {? @ref_or_pattern_occ } - | native_compute {? @ref_or_pattern_occ } - | unfold {+, @unfold_occ } + | vm_compute {? {| @reference_occs | @pattern_occs } } + | native_compute {? {| @reference_occs | @pattern_occs } } + | unfold {+, @reference_occs } | fold {+ @one_term } - | pattern {+, @pattern_occ } + | pattern {+, @pattern_occs } | @ident delta_flag ::= {? - } [ {+ @reference } ] strategy_flag ::= {+ @red_flag } @@ -321,16 +321,8 @@ Performing computations | cofix | zeta | delta {? @delta_flag } - ref_or_pattern_occ ::= @reference {? at @occs_nums } - | @one_term {? at @occs_nums } - occs_nums ::= {+ @nat_or_var } - | - {+ @nat_or_var } - int_or_var ::= @integer - | @ident - nat_or_var ::= @natural - | @ident - unfold_occ ::= @reference {? at @occs_nums } - pattern_occ ::= @one_term {? at @occs_nums } + reference_occs ::= @reference {? at @occs_nums } + pattern_occs ::= @one_term {? at @occs_nums } This set of tactics implements different specialized usages of the tactic :tacn:`change`. @@ -348,17 +340,6 @@ clauses) and are introduced by the keyword `in`. If no goal clause is provided, the default is to perform the conversion only in the conclusion. -The syntax and description of the various goal clauses is the -following: - -+ :n:`in {+ @ident} |-` only in hypotheses :n:`{+ @ident}` -+ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the - conclusion -+ :n:`in * |-` in every hypothesis -+ :n:`in *` (equivalent to in :n:`* |- *`) everywhere -+ :n:`in (type of @ident) (value of @ident) ... |-` in type part of - :n:`@ident`, in the value part of :n:`@ident`, etc. - For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. |