如何初始化空提示数据库

Question

我有几个证据遵循相同的结构。其中第一个可以用trivial完成，其他所有用auto with foo_db完成，其中foo_db是在第一个证明完成后填充提示的提示数据库。我想写一个使用auto with foo_db来解决所有这些证明的Ltac程序。但是，当运行该Ltac解决我的第一个证明foo_db尚不存在，所以科克抱怨：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. 

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