\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Programmable proof search

## Tactics

Tactic auto nat_or_var? auto_using? hintbases?
  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 `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 with the head symbol of the goal and tries to apply one of them. This process is recursively applied to the generated subgoals.

  Within each hintbase, lower cost tactics are tried before higher-cost tactics. When multiple hintbases are specified, all hints in the first database are tried before any in the second database (and so forth) regardless of their cost (unlike `eauto` and `typeclasses eauto`).

  `nat_or_var`

    Specifies the maximum search depth. The default is 5.

  `using one_term+,`

  > Uses lemmas `one_term+,` in addition to hints. If `one_term` is an inductive type, the collection of its constructors are added as hints.

  > 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 `apply` and `auto using one_term` may fail where `apply one_term` succeeds.

  `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.

  `with ident+`

    Use the hint databases `ident+` in addition to the database `core`. Use the fake database `nocore` to omit `core`.

  If no `with` clause is given, `auto` only uses the hypotheses of the current goal and the hints of the database named `core`.

  `auto` generally either completely solves the goal or leaves it unchanged. Use `solve` `[ auto ]` if you want a failure when they don't solve the goal. `auto` will fail if `fail` or `gfail` are invoked directly or indirectly, in which case setting the `Ltac Debug` may help you debug the failure.

  Warning

  `auto` uses a weaker version of `apply` that is closer to `simple apply` so it is expected that sometimes `auto` will fail even if applying manually one of the hints would succeed.

  See also

  Hint databases for the list of pre-defined databases and the way to create or extend a database.

  Tactic info_auto nat_or_var? auto_using? hintbases?

    Behaves like `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.

> > The tactics shown in the info or debug output currently don't correspond exactly to the variants that proof search tactics such as `auto` use, but they are close.

> > Occasionally the tactics shown (after removing tactics that were backtracked) may not always work as a replacement for the proof search tactic. For example:

> > Example: `info_auto` output that isn't a valid proof

> > The output isn't accepted as a proof because the conversion constraints are solved by default after every statement but are not solved internally by `auto` as it searches for a proof.

> > Create HintDb db.
> > Hint Resolve conj : db.
> > Hint Resolve eq_refl : db.
> > Goal forall n, n=1 -> exists x y : nat, x = y /\ x = 0.
> >   1 goal ============================ forall n : nat, n = 1 -> exists x y : nat, x = y /\ x = 0
> > intros.
> >   1 goal n : nat H : n = 1 ============================ exists x y : nat, x = y /\ x = 0
> > do 2 eexists; subst. (* Fix 2: replace with "do 2 (eexists; subst)." *)
> >   1 focused goal (shelved: 2) ============================ ?x@{n:=1} = ?y@{n:=1} /\ ?x@{n:=1} = 0
> > Succeed info_auto with nocore db.
> >   (* info auto: *) simple apply conj (in db). simple apply @eq_refl (in db). simple apply @eq_refl (in db).
> > simple apply conj. (* from info_auto output *)
> >   2 focused goals (shelved: 2) ============================ ?x@{n:=1} = ?y@{n:=1} goal 2 is: ?x@{n:=1} = 0
> > Fail simple apply @eq_refl. (* Fix 1: change to "2: simple apply @eq_refl" *)
> >   The command has indeed failed with message: Unable to unify "?y@{n:=1}" with "?x@{n:=1}" (cannot satisfy constraint "?y@{n:=1}" == "?x@{n:=1}"). (while solving unification constraints, see flag "Solve Unification Constraints")
> > (* simple apply @eq_refl. *)

> > One fix is to apply the tactics to the goals in a non-default order. Another would be to add parentheses to the `do 2`, which gives a different result. The fixes are shown inline in the example.

> Tactic debug auto nat_or_var? auto_using? hintbases?

>   Behaves like `auto` but shows the tactics it tries to solve the goal, including failing paths.

Tactic trivial auto_using? hintbases?
Tactic debug trivial auto_using? hintbases?
Tactic info_trivial auto_using? hintbases?

  Like `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 `hintbases`.

Flag Info Auto
Flag Debug Auto
Flag Info Trivial
Flag Debug Trivial

  These flags enable printing of informative or debug information for the `auto` and `trivial` tactics.

Tactic eauto nat_or_var? auto_using? hintbases?

  Generalizes `auto`. While `auto` does not try resolution hints which would leave existential variables in the goal, `eauto` will try them. Also, `eauto` internally uses `eassumption` instead of `assumption` and, when needed, a tactic similar to `simple eapply` instead of a tactic similar to `simple apply`. As a consequence, `eauto` can solve goals such as:

  Example

  Hint Resolve ex_intro : core.
    The hint ex_intro will only be used by eauto, because applying ex_intro would leave variable x as unresolved existential variable.
  Goal forall P:nat -> Prop, P 0 -> exists n, P n.
    1 goal ============================ forall P : nat -> Prop, P 0 -> exists n : nat, P n
  eauto.
    No more goals.

  `ex_intro` is declared as a hint so the proof succeeds.

  See also

  Hint databases

  Tactic info_eauto nat_or_var? auto_using? hintbases?

    The various options for `info_eauto` are the same as for `info_auto`. Note that the tactics shown (after removing tactics that were backtracked) may not always work as a replacement for the proof search tactic. See here.

  `eauto` uses the following flags:

  Flag Info Eauto
  Flag Debug Eauto
  Tactic debug eauto nat_or_var? auto_using? hintbases?

    Behaves like `eauto` but shows the tactics it tries to solve the goal, including failing paths.

Tactic autounfold hintbases? simple_occurrences?

  Unfolds constants that were declared through a `Hint Unfold` in the given databases.

  `simple_occurrences`

    Performs the unfolding in the specified occurrences.

Tactic autounfold_one hintbases? in ident?

Tactic autorewrite *? with ident+ occurrences? using ltac_expr?
  `*`

    If present, rewrite all occurrences whose side conditions are solved.

  `with ident+`

    Specifies the rewriting rule bases to use.

  `occurrences`

    Performs rewriting in the specified occurrences. Note: the `at` clause is currently not supported.

    Error The "at" syntax isn't available yet for the autorewrite tactic.

      Appears when there is an `at` clause on the conclusion.

  `using ltac_expr`

    `ltac_expr` is applied to the main subgoal after each rewriting step.

  Applies rewritings according to the rewriting rule bases `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 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 `Hint Rewrite` command.

Warning

This tactic may loop if you build non-terminating rewriting systems.

See also

`Hint Rewrite` for feeding the database of lemmas used by `autorewrite` and `autorewrite` for examples showing the use of this tactic. Also see Strategies for rewriting.

Here are two examples of `autorewrite` use. The first one ( Ackermann function) shows actually a quite basic use where there is no conditional rewriting. The second one ( Mac Carthy function) involves conditional rewritings and shows how to deal with them using the optional tactic of the `Hint Rewrite` command.

Example: Ackermann function

Parameter Ack : nat -> nat -> nat.
  Ack is declared

Axiom Ack0 : forall m:nat, Ack 0 m = S m.
  Ack0 is declared
Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1.
  Ack1 is declared
Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
  Ack2 is declared

Create Rewrite HintDb base0.
Global Hint Rewrite Ack0 Ack1 Ack2 : base0.

Lemma ResAck0 : Ack 3 2 = 29.
  1 goal ============================ Ack 3 2 = 29

autorewrite with base0 using try reflexivity.
  No more goals.

Example: MacCarthy function

This example requires the Stdlib library.

From Stdlib Require Import Arith Lia.
  Toplevel input, characters 27-32: > From Stdlib Require Import Arith Lia. > ^^^^^ Error: Cannot find a physical path bound to logical path Arith with prefix Stdlib.

Parameter g : nat -> nat -> nat.
  g is declared

Axiom g0 : forall m:nat, g 0 m = m.
  g0 is declared
Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
  g1 is declared
Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
  g2 is declared

Create Rewrite HintDb base1.
Global Hint Rewrite g0 g1 g2 using lia : base1.
  Toplevel input, characters 35-38: > Global Hint Rewrite g0 g1 g2 using lia : base1. > ^^^ Error: The reference lia was not found in the current environment.

Lemma Resg0 : g 1 110 = 100.
  1 goal ============================ g 1 110 = 100

Show.
  1 goal ============================ g 1 110 = 100

autorewrite with base1 using reflexivity || simpl.

Qed.
  Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof Resg0): Attempt to save an incomplete proof (there are remaining open goals).

Lemma Resg1 : g 1 95 = 91.
  Toplevel input, characters 0-26: > Lemma Resg1 : g 1 95 = 91. > ^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.

autorewrite with base1 using reflexivity || simpl.

Qed.
  Toplevel input, characters 0-4: > Qed. > ^^^^ Error: (in proof Resg0): Attempt to save an incomplete proof (there are remaining open goals).

Tactic 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 `trivial`, `reflexivity`, `symmetry`, `contradiction` and `inversion` of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal using `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.

Tactic now ltac_expr

  Run `tactic` followed by `easy`. This is a notation for `tactic; easy`.

## Hint databases

Hints used by `auto`, `eauto` and other tactics are stored in hint databases. Each database maps head symbols to a list of hints. Use the `Print Hint` command to view a database.

Each hint has a cost and an optional pattern. Hints with lower cost are tried first. (Cost is not used to limit the scope of searches.) `auto` tries a hint when the conclusion of the current goal matches its pattern or when the hint has no pattern.

### Creating hint databases

Use `Create HintDb` command to create hint databases. The new databases have the default setting `Transparent` for `Constants`, `Projections` and `Variables`. We recommend using `Hint Constants`, `Hint Projections` and `Hint Variables` immediately after `Create HintDb` to make these settings explicit.

Alternatively, adding a hint to an unknown database creates the latter implicitly, but this behavior is deprecated as of Rocq 9.2. Implicitly created databases have the `Opaque` setting for `Constants`, `Projections` and `Variables`.

The proof search tactics use unification to choose which tactics to try, for example whether the goal unifies with a theorem given by `Hint Resolve`.

Use `Hint Opaque` and `Hint Transparent` to control the opacity of individual items during this initial unification. These settings are distinct from the non-hint `Opaque` and `Transparent` settings. Hint opacity settings influence which hints the search tactics try, but in some cases they also affect how selected tactics are executed. (In particular, `typeclasses eauto` uses the equivalent of `autoapply` when applying `Hint Resolve` hints, which explicitly use the hint opacity settings. `auto` and `eauto` don't do this.)

Command Create HintDb ident discriminated?

  If there is no hint database named `ident`, creates a new hint database with that name. Otherwise, does nothing.

  All constants, variables and projections are set to default to unfoldable (use `Hint Constants`, `Hint Projections` and `Hint Variables` to change this). For better performance, we recommend setting each of these to `Opaque` and then using `Hint Transparent` for specific items when necessary.

  By default, hint databases are undiscriminated. We recommend using `discriminated` because it generally performs better.

### Deciding which hints to try

The proof search tactics decide which hints to try by first selecting hints whose pattern has the same head constant as the goal. Then the selected hints are tried as follows:

- For hints other than `Hint Extern`: If the database is discriminated, only matching hints are tried. Hints match if all compared items that are opaque in both the goal and the pattern are identical. Marking definitions as Hint Opaque reduces the number of matches, but it may cause some proof searches that previously worked to fail.

  Otherwise (if not discriminated), all hints will be tried. (Therefore, use `discriminated` databases whenever possible.)

- For `Extern` hints: If the hint has a pattern, hints matching the goal will be tried. In this case, matching uses a form of syntactic unification), treating everything as hint opaque.

  Otherwise (if there is no pattern), all hints will be tried. (Therefore, provide a pattern in `Extern` hints whenever possible.)

Command Create Rewrite HintDb ident

  Like above, but creates a database for `Hint Rewrite` declarations instead.

### Hint databases defined in the Rocq standard library

Several hint databases are defined in the Rocq standard library. The database contains the hints declared for it in the currently loaded modules (subject to locality attributes) as well as any added in the current module. Requiring additional modules (`Require`) may add more hints.

At Rocq startup, only the core database is nonempty and ready to be used immediately.

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:

  all lemmas about Peano’s arithmetic proved in the directories Init and Arith.

zarith:

  lemmas about binary signed integers from the directories theories/ZArith. The database also contains high-cost hints that call `lia` on equations and inequalities in `nat` or `Z`.

bool:

  lemmas about booleans, mostly from directory theories/Bool.

datatypes:

  lemmas about lists, streams and so on that are mainly proved in the Lists subdirectory.

sets:

  lemmas about sets and relations from the directories Sets and Relations.

typeclass_instances:

  special database containing all 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 instead to use one or more databases specific to your development.

## Creating Hints

> The various `Hint` commands share these elements:

> `: ident+?` specifies the hint database(s) to add to. (Deprecated since version 8.10: If no `ident`s are given, the hint is added to the `core` database.)

> Hints in hint databases are ordered, which is the order in which they're tried, as shown by the `Print HintDb` command. Hints with lower costs are tried first. Hints with the same cost are tried in reverse of their order of definition, i.e., last to first.

> Rewrites with theorems such as `forall n m, n+m=m+n` or `forall n m p, (n+m)+p=n+(m+p)` (eg `Hint Extern ... => rewrite ...`) should be used only in `Hint Immediate` to prevent them from wastefully being applied .

> Outside of sections, these commands support the `local`, `export` and `global` attributes. `export` is the default.

> Inside sections, some commands only support the `local` attribute. These are `Hint Immediate`, `Hint Resolve`, `Hint Constructors`, `Hint Unfold`, `Hint Extern` and `Hint Rewrite`. `local` is the default for all hint commands inside sections.

> - `local` hints are never visible from other modules, even if they `Import` or `Require` the current module.

> - `export` hints are visible from other modules when they `Import` the current module, but not when they only `Require` it.

> - `global` hints are visible from other modules when they `Require` the current module (submodules of the current module are considered `Require`d after their `End`).

> Changed in version 8.18: The default value for hint locality outside sections is now `export`. It used to be `global`.

> Deprecated since version 9.2: Implicitly creating a unknown database is now deprecated and will become an error.

> The `Hint` commands are:

> Command Hint Resolve qualid​one_term+ hint_info? : ident+?
> Command Hint Resolve ->​<- qualid+ natural? : ident+?
>   hint_info`::=`| natural? one_pattern?``one_pattern`::=`one_term``

>   The first form adds each `qualid` as a hint with the head symbol of the type of `qualid` to the specified hint databases (`ident`s). If specified, `natural` is the cost of the hint; otherwise the cost of the hint is the number of subgoals generated by `simple apply`. The associated pattern is inferred from the conclusion of the type of `qualid` or, if specified, the given `one_pattern`.

>   If the inferred type of `qualid` does not start with a product, the command adds `exact` `qualid` to the hint list. If the type reduces to a type starting with a product, the command also adds `simple apply` `qualid` to the hints list. Note that tactics printed in debug output are similar to but not exactly the same as the ones executed by proof search. Unlike `auto` and `eauto`, `typeclasses eauto` uses a tactic equivalent to `autoapply`, which behaves somewhat differently from `simple apply`. Nonetheless, that tactic's debug output and the hint database misleadingly show `simple apply`.

>   If the inferred type of `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 only used by `eauto` / `typeclasses eauto`, but not by `auto`. A typical hint that would only be used by `eauto` is a transitivity lemma.

>   `->​<-`

>     The second form adds the left-to-right (`->`) or right-ot-left implication (`<-`) of a logical equivalence (`<->`) as a hint. If needed, it defines a projection for the specified direction, which the hint applies with a restricted version of `apply`. (For example, `Hint Resolve -> and_comm` defines `and_comm_proj_l2r`.)

>   `one_term`

>     Permits declaring a hint without declaring a new constant first. This is deprecated.

>     > Warning Declaring arbitrary terms as hints is fragile and deprecated; it is recommended to declare a toplevel constant instead

>   `one_pattern`

>     Overrides the default pattern, which may occasionally be useful. For example, if a hint has the default pattern `_ = _`, you could limit the hint being tried only for `bool`s with the pattern `(@eq bool _ _)`.

>   Error qualid cannot be used as a hint

>     The head symbol of the type of `qualid` is a bound variable such that this tactic cannot be associated with a constant.

> Command Hint Immediate qualid​one_term+ : ident+?

>   For each specified `qualid`, adds the tactic `simple apply` `qualid;` `solve` `[` `trivial` `]` to the hint list associated with the head symbol of the type of `qualid`. The tactic fails if any of the subgoals generated by `simple apply` `qualid` are not solved immediately by `trivial` (which only tries tactics with cost 0). This hint is useful to allow controlled use of theorems such as `n+m=m+n` or `(n+m)+p=n+(m+p)` that otherwise could be applied repeatedly without limit. The cost of this hint (which never generates subgoals) is always 1, so it won't be used by `trivial` itself.

> Command Hint Constructors qualid+ : ident+?

>   For each `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 `(qualid ...)`, `auto` will try to apply each constructor using `exact`.

>   Error qualid is not an inductive type
> Command Hint Unfold qualid+ : ident+?

>   For each `qualid`, adds the tactic `unfold` `qualid` to the hint list that will only be used when the head constant of the goal is `qualid`. Its cost is 4.

> Command Hint Transparent​Opaque qualid+ : ident+?

>   Adds transparency hints to the database, making each `qualid` transparent or opaque during resolution. The proof search tactics use unification to determine whether to try most hints, for example checking if the goal unifies with the theorem used in a `Hint Resolve` hint. Currently the head constant is always treated as opaque (see example). See here for a description of how opaque and transparent affect which hints are tried. Note that transparency hints are independent of the non-hint `Opaque` and `Transparent` settings.

>   Example: Transparency with Multiple Hint Databases

>   To use different transparency settings for particular hints, put them in separate hint databases with distinct transparency settings and use `typeclasses eauto`. (This doesn't work for `auto` or `eauto`.):

>   Definition one := 1.
>     one is defined
>   Theorem thm : one = 1. reflexivity. Qed.
>     1 goal ============================ one = 1 No more goals.
>   Create HintDb db1.
>   Hint Opaque one : db1.
>   Hint Resolve thm | 1 : db1.
>   Create HintDb db2.
>   Goal 1 = 1.
>     1 goal ============================ 1 = 1
>   (* "one" is not unfolded because it's opaque in db1, where bar is *) Fail typeclasses eauto with db1 db2 nocore. (* fails with tc eauto *)
>     The command has indeed failed with message: Tactic failure: Proof search failed.
>   Succeed eauto with db1 db2 nocore. (* ignores the distinction *)
>   Succeed auto with db1 db2 nocore. (* ignores the distinction *)
>   Hint Resolve thm | 2 : db2.
>   (* "one" is unfolded because it's transparent (by default) in db2 *) Succeed typeclasses eauto with db1 db2 nocore.
>   Abort.

>   Example: Independence of Hint Opaque and Opaque

>   Definition one := 1.
>     one is defined
>   Opaque one. (* not relevant to hint selection *)
>   Theorem bar: 1=1. reflexivity. Qed.
>     1 goal ============================ 1 = 1 No more goals.
>   Create HintDb db. (* constants, etc. transparent by default *)
>   Hint Opaque one : db. (* except for "one" *)
>   Hint Resolve bar : db. (* hint is not tried if one is Hint Opaque *)
>   Set Typeclasses Debug Verbosity 1.
>   Goal one = 1.
>     1 goal ============================ one = 1
>   Fail typeclasses eauto with db nocore. (* fail: no match for (one = 1) *)
>     Debug: 1: looking for (one = 1) without backtracking Debug: 1: no match for (one = 1), 1 possibilities The command has indeed failed with message: Tactic failure: Proof search failed.
>   Hint Transparent one : db.
>   Succeed typeclasses eauto with db nocore. (* success: now bar is tried *)
>     Debug: 1: looking for (one = 1) without backtracking Debug: 1.1: exact bar on (one = 1), 0 subgoal(s)
>   Fail unfold one. (* fail: one is still Opaque *)
>     The command has indeed failed with message: one is opaque.
>   Abort.

> > Example: Head Constants are always opaque

> > Adding `Hint Unfold Tru : db` will make `auto` succeed. (If the goal was `True = Tru`, the head constant is `eq` and `Tru` will be unfolded.)

> > Definition Tru := True.
> >   Tru is defined
> > Create HintDb db.
> > Hint Constants Transparent : db.
> > Hint Resolve I : db.
> > Print HintDb db. (* For XXX -> indicates XXX is the head constant *)
> >   Non-discriminated database Unfoldable variable definitions: all Unfoldable constant definitions: all Unfoldable projection definitions: all Cut: emp For any goal -> For True -> exact I (cost 0, pattern True, id 0)
> > Goal Tru.
> >   1 goal ============================ Tru
> > Fail progress auto with db.
> >   The command has indeed failed with message: Failed to progress.
> > Hint Unfold Tru : db. (* workaround *)
> > progress info_auto with db. (* works now! *)
> >   (* info auto: *) unfold Tru (in db). exact I (in core). No more goals.
> > Abort.
> > Error Cannot coerce qualid to an evaluable reference.

> Command Hint Constants​Projections​Variables Transparent​Opaque : ident+?

>   Sets the default transparency for constants (from `Definition`s and `Example`s), projections (from `Record`s and `Structure`s) or variables (from `Hypotheses` and `Variables`) for the specified hint databases. Existing transparency settings for individual items (e.g., set with `Hint Opaque`) are dropped. Making items opaque can make proof search commands run faster (fewer unfoldings) but it can also prevent matching some hints. We recommend setting each of these to `Opaque` and then using `Hint Transparent` for specific items as needed. We advise using this command just after a `Create HintDb` command.

> Command Hint Extern natural one_pattern? => generic_tactic : ident+?

>   Extends `auto` with tactics other than `apply` and `unfold`. `natural` is the cost, `one_pattern` is the pattern to match and `ltac_expr` is the action to apply.

>   We recommend providing a pattern whenever possible. Hints with patterns are tried only if the pattern matches without unfolding transparent constants (i.e., a syntactic match). Hints without patterns are always tried.

>   Usage tip: tactics that can succeed even if they don't change the context, such as most of the conversion tactics, should be prefaced with `progress` to avoid needless repetition of the tactic.

>   Usage tip: Use a `Hint Extern` with no pattern to do pattern matching on hypotheses using `match goal with` inside the tactic.

>   Example

>   Hint Extern 4 (~(_ = _)) => discriminate : core.

>   Now, when the head of the goal is an inequality, `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

>   Require Import ListDef.
>   Create HintDb 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}.
>     1 goal ============================ forall a b : list (nat * nat), {a = b} + {a <> b}
>   info_auto with eqdec.
>     (* info auto: *) intro. intro. (*external*) (generalize X1, X2; decide equality) (in eqdec). (*external*) (generalize X1, X2; decide equality) (in eqdec). (*external*) (generalize X1, X2; decide equality) (in eqdec). (*external*) (generalize X1, X2; decide equality) (in eqdec). No more goals.
> Command Hint Cut [ hints_regexp ] : ident+?
>   hints_regexp`::=`qualid+`(hint or instance identifier)````|`_`(any hint)````|`hints_regexp | hints_regexp`(disjunction)````|`hints_regexp hints_regexp`(sequence)````|`hints_regexp *`(Kleene star)````|`emp`(empty)````|`eps`(epsilon)````|`( hints_regexp )``

>   Adds another clause to the cut regular expression in the specfied hint databases. `Hint Cut hints_regexp` sets the cut expression to `c | hints_regexp`. The initial cut expression is `emp`.

>   Typeclass proof search and the `typeclasses eauto` tactic (but not `auto` or `eauto`) use the cut expression to conditionally prevent using some hints based on the path of hints that have been successfully applied. The path is an ordered list of hint identifiers. When the path plus the identifier of a candidate hint matches the cut expression, the hint is not applied. (It is nothing like a cut in Prolog.)

>   The hint identifier is the `qualid` that appears in the various `Hint` commands (e.g. as in `Hint Resolve` `plus_O_n.`), with the following exceptions:

>   - `Hint Extern`s do not have associated identifiers

>   - For `Hint Constructors`, which creates multiple hints, the identifiers are the names of the constructors.

>   - For `Hint Resolve` `->​<- theorem`, the name is `theorem_proj_l2r` or `theorem_proj_r2l` depending on the direction of the arrow.

>   The output of `Print HintDb` shows the cut expression.

>   Warning

>   The regexp matches the entire path. Most hints will start with a leading `( _* )` to match the tail of the path. (Note that `(_*)` misparses since `*)` would end a comment.)

>   Warning

>   There is no operator precedence during parsing, one can check with `Print HintDb` to verify the current cut expression.

> Command Hint Mode qualid +​!​-+ : ident+?

>   Sets an optional mode of resolution for the identifier `qualid`. When proof search has a goal that ends in an application of `qualid` to arguments `arg ... arg`, the mode tells if the hints associated with `qualid` can be applied or not, depending on a criterion on the arguments. 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. Mode `-` matches any term, mode `+` matches a term if and only if it does not contain existential variables, while mode `!` matches a term if and only if the head of the term is not an existential variable. The head of a term is understood here as the applicative head, recursively, ignoring casts. For a mode declaration to match a list of arguments, each argument should match its corresponding mode.

>   Only `typeclasses eauto` uses these hints. `Hint Mode` is especially useful for typeclasses, when one does not want to support default instances and wants to 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 `!` allowing existentials to appear in the index but not at its head.

> Note

> - 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 `Hint Transparent`, `Hint Cut`, or `Hint Mode`, for typeclass resolution, do not forget to put them in the `typeclass_instances` hint database.

> Warning This hint is not local but depends on a section variable. It will disappear when the section is closed.

>   A hint with a non-local attribute was added inside a section, but it refers to a local variable that will go out of scope when closing the section. As a result the hint will not survive either.

> Example: Logic programming with addition on natural numbers

> This example illustrates the use of modes to control how resolutions can be triggered during proof search.

> Parameter plus : nat -> nat -> nat -> Prop.
>   plus is declared
> Create HintDb plus.
> Hint Mode plus ! - - : plus.
> Hint Mode plus - ! - : plus.
> Axiom plus0l : forall m : nat, plus 0 m m.
>   plus0l is declared
> Axiom plus0r : forall n : nat, plus n 0 n.
>   plus0r is declared
> Axiom plusSl : forall n m r : nat, plus n m r -> plus (S n) m (S r).
>   plusSl is declared
> Axiom plusSr : forall n m r : nat, plus n m r -> plus m (S m) (S r).
>   plusSr is declared
> Hint Resolve plus0l plus0r plusSl plusSr : plus.
>   The hint plusSr will only be used by eauto, because applying plusSr would leave variable n as unresolved existential variable.

> The previous commands define the addition predicate and set its mode so it can resolve goals if and only if one of the first two arguments is headed by a constructor or constant. The last argument of the predicate will be the inferred result.

> Goal exists x y, plus x y 12.
>   1 goal ============================ exists x y : nat, plus x y 12
> Proof. eexists ?[x], ?[y].
>   1 focused goal (shelved: 2) ============================ plus ?x ?y 12
> Fail typeclasses eauto with plus.
>   The command has indeed failed with message: Tactic failure: Proof search failed.
> instantiate (y := 1).
>   1 focused goal (shelved: 1) ============================ plus ?x 1 12
> typeclasses eauto with plus.
>   No more goals.
> Defined.

> In the proof script, the first call to `typeclasses eauto` fails as the two arguments are headed by an existential variable, while when we instantiate the second argument with `1`, typeclass resolution succeeds as the second declared mode is matched, and instantiates `x` with `11`.

Command Hint Rewrite ->​<-? one_term+ using generic_tactic? : ident+?
  `using generic_tactic?`

    If specified, `generic_tactic` is applied to the generated subgoals, except for the main subgoal.

  `->​<-`

    Arrows specify the orientation; left to right (`->`) or right to left (`<-`). If no arrow is given, the default orientation is left to right (`->`).

  Adds the terms `one_term+` (their types must be equalities) to the rewriting bases `ident*`. Note that the rewriting bases are distinct from the `auto` hint bases and that `auto` does not take them into account.

  Command Print Rewrite HintDb ident

    This command displays all rewrite hints contained in `ident`.

Command Remove Hints qualid+ : ident+?

  Removes the hints associated with the `qualid+` in databases `ident+`. Hints removals within sections are local to the section. Note: hints created with `Hint Extern` currently can't be removed because they aren't associated with names. The best workaround for this is to make the hints non-global and carefully select which modules you import.

Command Print Hint *​reference?
  `*`

    Display all declared hints.

  `reference`

    Display all hints associated with the head symbol `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 `*` and `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.

Command Print HintDb ident

  This command displays all hints from database `ident`. Hints are grouped by the head constants of their patterns ("For ... ->"). The groups are shown ordered alphabetically on the last component of the head constant name. Within each group, hints are shown in the order in which they will be tried (first to last). Note that hints with the same cost are tried in reverse of the order they're defined in, i.e., last defined is used first. Mode of resolution symbols, `+​!​-+`, when defined with `Hint Mode`, appear after the head constant.

## Setting implicit automation tactics

Command Proof with generic_tactic using section_var_expr?

  Starts a proof in which `generic_tactic` is applied to the active goals after each tactic that ends with `...` instead of the usual single period. "`tactic...`" is equivalent to "`tactic; generic_tactic.`".

  See also

  `Proof` in Entering and exiting proof mode.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF