coq - 引用Ltac中的hintbases

Question

在我的项目中，我试图维护小型提示库以加快证明速度。然而，当我为这种架构编写 Ltac 支持时，我找不到引用各种提示库的方法。本质上，我想做以下事情:

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

事情会比这更复杂。然而，Coq 解析器似乎急切地将 db 解析为提示库的具体名称，因此会抛出这样的错误消息:

Error: No such Hint database: db.

有什么方法可以参数化 auto 系列的提示基本选项吗？

Answer 1

编辑:

您尝试做的事情目前在 Ltac 中不起作用。

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

您可以通过以下任一方式解决您的问题

• 将您的问题改写为一个单独的问题，在其中解释为什么需要这种自动化，有人可能能够帮助您以不同的方式解决最初的问题(不使用自动和数据库参数)

或

• 尝试一个较新的 Coq 策略库，例如 Ltac2

---

旧的(损坏的)答案:

在 Coq 8.7.2 中，您要寻找的是 ident 参数类型。 根据定义，Hint 数据库由 ident 引用:

Create HintDb ident [discriminated] 

(参见 https://coq.inria.fr/distrib/current/refman/tactics.html#Hints-databases 的定义)

推杆

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

对我来说效果很好。

https://coq.inria.fr/distrib/current/refman/syntax-extensions.html#hevea_command236包含允许的修饰符列表。