如何在Ltac中引用自定义hintbase？Coq解析报错求助

这个问题我之前也碰到过，Coq的Tactic Notation在处理hint base参数时，直接写变量名会被解析成具体的hintbase名称去查找，所以才会抛出"No such Hint dat..."的错误。要实现你想要的功能，关键是要明确指定参数的类型为标识符（ident），让Coq把它当作变量捕获而不是直接解析。

基础实现 #

先看最贴近你需求的基础版本，只需要给参数加上ident类型声明即可：

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

这样定义后，你就可以像调用auto一样使用myauto，比如：

(* 假设你有自定义的hintbase my_hints *)
myauto core.
myauto my_hints.

扩展到复杂逻辑 #

如果你的实际逻辑更复杂（比如添加预处理策略、组合多个hintbase、或者做失败回退），可以把逻辑放在ltac:(...)块里，比如：

Tactic Notation "myauto" ident(db) :=
  ltac:(
    (* 这里可以添加任意复杂的Ltac逻辑 *)
    repeat rewrite -> some_lemma;
    auto with db;
    try solve [exact I | apply my_helper_lemma]
  ).

支持多个Hintbase #

如果需要同时支持多个hintbase参数，只需要添加多个ident类型的参数即可：

Tactic Notation "myauto" ident(db1) ident(db2) := auto with db1 db2.

(* 调用示例 *)
myauto core my_hints.

如果想要支持可变数量的hintbase，可以用Coq的可变参数语法（注意版本兼容性，Coq 8.10+支持）：

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

为什么原来的写法不行？ #

你之前写的Tactic Notation "myauto" ???(db) := auto with db.没有指定参数类型，Coq会默认把db当作一个具体的hintbase名称去查找，而不是一个变量参数，自然会找不到对应的hintbase而报错。通过ident(db)明确告诉Coq：这是一个标识符参数，需要捕获后面的输入作为变量使用。

内容的提问来源于stack exchange，提问作者Jason Hu