coq - 如何初始化空提示数据库

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本来就解决的目标。