Search code examples
coqltac

How to initialize empty hint database

I have several proofs that follow identical structure. First of them can be finished with trivial, all the other ones with auto with foo_db, where foo_db is a hint database populated with hints after the first proof is complete. I'd like to write an Ltac procedure that uses auto with foo_db to solve all these proofs. However, when running that Ltac to solve the first of my proofs foo_db does not yet exist and so Coq complains: Error: No such Hint database: foo_db.. Is there a way to initialize an empty hint database?

Solution

  • Yes, there's a command Create HintDb that does exactly what you want.

    Create HintDb foo_db.

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

    For demonstration purposes (to avoid solving the goal), I've also added the pseudo-db nocore to avoid using the standard library's hints. You probably want to just do auto with foo_db, to solve all the goals trivial would have solved.