空のヒントデータベースを初期化する方法

Question

同じ構造に従ういくつかの証明があります。最初はtrivialで終わることができ、他のすべてはauto with foo_dbで終わることができます。foo_dbは、最初の証明が完了した後にヒントが埋め込まれたヒントデータベースです。私はauto with foo_dbを使用してこれらの証明をすべて解決するLtacプロシージャを作成したいと思います。しかし、その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. 

（目標を解く回避するために）、私はまた、標準ライブラリのヒントを使用して回避するために、疑似DB nocoreを追加しました。あなたはおそらくauto with foo_dbをやりたいだけで、すべての目標を解決するにはtrivialが解決しました。