.. _automation: ========================= Programmable proof search ========================= .. 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 :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. By default, :tacn:`auto` only uses the hypotheses of the current goal and the hints of the database named ``core``. .. warning:: :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. .. tacv:: auto @natural Forces the search depth to be :token:`natural`. The maximal search depth is 5 by default. .. tacv:: auto with {+ @ident} Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. .. note:: Use the fake database `nocore` if you want to *not* use the `core` database. .. tacv:: auto with * 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. .. seealso:: :ref:`The Hints Databases for auto and eauto ` 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 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 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: .. 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. .. flag:: Info Auto Debug Auto Info Trivial Debug Trivial These flags enable printing of informative or debug information for 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 internally uses a tactic close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: .. coqtop:: none Set Warnings "-deprecated-hint-without-locality". .. coqtop:: all Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. Note that ``ex_intro`` should be declared as a hint. .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} The various options for :tacn:`eauto` are the same as for :tacn:`auto`. :tacn:`eauto` also obeys the following flags: .. flag:: Info Eauto Debug Eauto :undocumented: .. seealso:: :ref:`The Hints Databases for auto and eauto ` .. tacn:: autounfold with {+ @ident} :name: autounfold This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. .. tacv:: autounfold with {+ @ident} in @goal_occurrences Performs the unfolding in the given clause (:token:`goal_occurrences`). .. tacv:: autounfold with * Uses the unfold hints declared in all the hint databases. .. tacn:: autorewrite with {+ @ident} :name: autorewrite This tactic 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. The rewriting rule bases are built with the :cmd:`Hint Rewrite` command. .. warning:: 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 ` for feeding the database of lemmas used by :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. .. 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 :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` and :tacn:`inversion` of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal using :tacn:`split` and recursing. 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 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 Use this command to display the hints associated to the head symbol :n:`@ident` (see :ref:`Print Hint `). 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. 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. .. cmd:: Create HintDb @ident {? discriminated} This command creates a new 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 `), 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 hints, putting more work on the unification that is run after retrieval (it keeps a list of the lemmas in case the DT is not used). The new implementation enabled by the discriminated option makes use of DTs in all cases and takes transparency information into account. However, the order in which hints are retrieved from the DT may differ from the order in which they were inserted, making this implementation observationally different from the legacy one. .. cmd:: Hint @hint_definition : {+ @ident} The general command to add a hint to some databases :n:`{+ @ident}`. 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. + :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. + :attr:`export` are visible from other modules when they import the current module. Requiring it is not enough. + :attr:`global` hints are made available by merely requiring the current module. .. deprecated:: 8.13 The default value for hint locality is scheduled to 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 No database name is given: the hint is registered in the ``core`` database. .. deprecated:: 8.10 .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident :name: Hint Resolve 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 and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. .. 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 Adds each :n:`Hint Resolve @qualid`. .. cmdv:: Hint Resolve -> @qualid : @ident 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 Adds the right-to-left implication of an equivalence as a hint. .. cmdv:: Hint Immediate @qualid : @ident :name: Hint Immediate 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 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 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: .. 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 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. .. 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`. 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 :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 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 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. .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a :n:`@tactic` to execute. .. example:: .. coqtop:: none Set Warnings "-deprecated-hint-without-locality". .. coqtop:: in Hint Extern 4 (~(_ = _)) => discriminate : core. Now, when the head of the goal is a disequality, ``auto`` will try discriminate if it does not manage to solve the goal with hints with a cost less than 4. One can even use some sub-patterns of the pattern in the tactic script. A sub-pattern is a question mark followed by an identifier, like ``?X1`` or ``?X2``. Here is an example: .. example:: .. coqtop:: reset none Set Warnings "-deprecated-hint-without-locality". .. coqtop:: all Require Import List. Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. Info 1 auto with eqdec. .. cmdv:: Hint Cut @regexp : @ident :name: Hint Cut .. 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: .. prodn:: regexp ::= @ident (hint or instance identifier) | _ (any hint) | @regexp | @regexp (disjunction) | @regexp @regexp (sequence) | @regexp * (Kleene star) | emp (empty) | eps (epsilon) | ( @regexp ) 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 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 ``+``, ``!`` or ``-`` items that specify if an argument of the identifier is to be treated as an input (``+``), if its head only is an input (``!``) or an output (``-``) of the identifier. For a mode to match a list of arguments, input terms and input heads *must not* contain existential variables or be existential variables respectively, while outputs can be any term. Multiple modes can be declared for a single identifier, in that case only one mode needs to match the arguments for the hints to be applied. The head of a term is understood here as the applicative head, or the match or projection scrutinee’s head, recursively, casts being ignored. :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. .. note:: + One can use a :cmd:`Hint Extern` with no pattern to do pattern matching on hypotheses using ``match goal with`` inside the tactic. + 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. 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 to belong to this database in each of the various modules currently loaded. Especially, requiring new modules may extend the database. At Coq startup, only the core database is nonempty and can be used. :core: This special database is automatically used by ``auto``, except when pseudo-database ``nocore`` is given to ``auto``. The core database contains only basic lemmas about negation, conjunction, and so on. Most of the hints in this database come from the Init and Logic directories. :arith: This database contains all lemmas about Peano’s arithmetic proved in the directories Init and Arith. :zarith: contains lemmas about binary signed integers from the directories theories/ZArith. The database also contains high-cost hints that call :tacn:`lia` on equations and inequalities in ``nat`` or ``Z``. :bool: contains lemmas about booleans, mostly from directory theories/Bool. :datatypes: is for lemmas about lists, streams and so on that are mainly proved in the Lists subdirectory. :sets: contains lemmas about sets and relations from the directories Sets and Relations. :typeclass_instances: contains all the typeclass instances declared in the environment, including those used for ``setoid_rewrite``, from the Classes directory. :fset: internal database for the implementation of the ``FSets`` library. :ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), mainly used in the ``FSets`` and ``FMaps`` libraries. 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 section (and not defined with option ``Local``) become available when the module ``A`` is required (using e.g. ``Require A.``). As of today, hints only have a binary behavior regarding locality, as described above: either they disappear at the end of a section scope, or they remain global forever. This causes a scalability issue, because hints coming from an unrelated part of the code may badly influence another development. It can be mitigated to some extent thanks to the :cmd:`Remove Hints` command, but this is a mere workaround and has some limitations (for instance, external hints cannot be removed). A proper way to fix this issue is to bind the hints to their module scope, as for most of the other objects Coq uses. Hints should only be made available when the module they are defined in is imported, not just required. It is very difficult to change the historical behavior, as it would break a lot of scripts. We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` 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`: - "Lax": this is the default, and corresponds to the historical behavior, that is, hints defined outside of a section have a global scope. - "Warn": outputs a warning when a non-imported hint is used. Note that this is an over-approximation, because a hint may be triggered by a run that will eventually fail and backtrack, resulting in the hint not being actually useful for the proof. - "Strict": changes the behavior of an unloaded hint to a immediate fail tactic, allowing to emulate an import-scoped hint mechanism. .. _tactics-implicit-automation: Setting implicit automation tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Proof with @tactic 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``. .. 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`