Как инициализировать пустую базу данных подсказок

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 решил бы.