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

我有几个遵循相同结构的证明。第一个可以用 trivial 完成，所有其他的可以用 auto with foo_db 完成，其中 foo_db 是一个提示数据库，在第一个证明完成。我想编写一个使用 auto with foo_db 的 Ltac 过程来解决所有这些证明。然而，当运行 Ltac 来解决我的第一个证明时 foo_db 还不存在，所以 Coq 提示:Error: No such Hint database: foo_db.。有没有办法初始化一个空的提示数据库？

请您参考如下方法:

是的，有一个命令 Create HintDb 可以完全满足您的需求。

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

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