如何初始化空提示数据库

Question

我有几个遵循相同结构的证明。首先可以用trivial完成，其他的都可以用auto with foo_db完成，其中foo_db是一个提示数据库，在第一个证明完成后填充了提示。我想编写一个 Ltac 过程，使用auto with foo_db来解决所有这些证明。但是，当运行该 Ltac 来解决我的第一个证明时，foo_db尚不存在，因此 Coq 抱怨：Error: No such Hint database: foo_db..有没有办法初始化空的提示数据库？

Answer 1

是的，有一个命令Create HintDb可以完全按照您想要的方式执行。

Create HintDb foo_db.
Goal True.
auto with foo_db nocore. (* no hints *)
exact I.
Qed.

出于演示目的(为了避免解决目标)，我还添加了伪数据库nocore以避免使用标准库的提示。你可能只想做auto with foo_db，解决trivial本可以解决的所有目标。