Search code examples
coqcoq-tactic

Refer to hintbases in Ltac

In my project, I am attempting to maintain small hintbases in order to speed up proofs. However, when I am writing Ltac support for such architecture, I couldn't find a way to refer to the various hintbases. Essentially, I want to do the following:

Tactic Notation "myauto" ???(db) := auto with db.

It will be more complicated than that. However, Coq parser seems eagerly parse db to be the concrete name of the hint base, and therefore error message like this will be thrown:

Error: No such Hint database: db.

Any way I can parameterize the hint base option for auto family?

Solution

  • EDIT:

    What you are trying to do is currently not working in Ltac.

    https://github.com/coq/coq/issues/2417

    You can get around your issue by either

    • rephrasing your issue into a separate question where you give some explanation why you need this kind of automation, where someone might be able to help you solving the initial problem in a different way (not using auto and database parameters)

    or

    • trying out one of the newer Coq tactic libraries, like Ltac2

    Old (broken) answer:

    In Coq 8.7.2 what you are looking for is the ident argument type. According to the definition, a Hint database is referenced by an ident:

    Create HintDb ident [discriminated]

    (see https://coq.inria.fr/distrib/current/refman/tactics.html#Hints-databases for the definition)

    Putting

    Tactic Notation "test" ident(db) :=
  auto with db.

    works fine for me.

    https://coq.inria.fr/distrib/current/refman/syntax-extensions.html#hevea_command236 contains a list of allowed modifiers.