coq - 在 Coq 证明中定位策略的定义

Question

在研究其他作者的 Coq 证明时，我经常遇到一种策略，比如“inv eq Heq”或“intro_b”。我想了解这种策略。

如何确定它是 Coq 策略还是在我当前项目的某处定义的 Tactic Notation？

其次，有没有办法找到它的定义？

我使用了 SearchAbout、Search、Locate 和 Print，但找不到上述问题的答案。

Answer 1

你应该可以使用

Print Ltac <tacticname>.

打印用户定义策略的代码（根据文档）。

---

要找到它的定义位置......我想你将需要 grep 不幸的是，Locate它似乎不适用于战术名称。

Answer 2

如前所述，Print Ltac ...打印用户定义策略的代码。

要定位用户定义的策略（即知道其定义的位置），请使用Locate Ltac .... 它为您提供完全限定的名称。然后使用Locate Library查找对应的文件。