我正在学习Coq和我正在学习的书，（CPDT）在证明中大量使用auto。
由于我正在学习，我认为准确地了解auto在幕后做什么可能会对我有所帮助（早期魔法越少越好）。有什么方法可以强迫它准确地显示它用来计算证据的策略或技术吗？
如果没有，是否有一个地方详细说明了auto的作用？
有多种方法可以了解引擎盖下发生的事情。
TLDR：把info放在战术之前，或者在调用战术之前和之后使用Show Proof.，找出差异。
要查看特定策略调用一直在做什么，可以在is前面加上info，以便显示它所采取的特定证明步骤。
（Coq8.4可能会打破这一点，我看到他们提供了一些策略的info_版本，如果需要，请阅读错误消息。）
这可能是你在初级阶段想要的，它已经很简洁了。
查看校样中当前发生的情况的另一种方法是使用命令Show Proof.。它将向你展示当前构建的有漏洞的学期，并向你展示你当前目标应该填补的漏洞。
这可能更先进，尤其是如果你使用induction或inversion这样的策略，因为正在构建的术语将相当复杂，并且需要你理解归纳方案或依赖模式匹配的基本性质（CPDT应该很快教你）。
一旦你用Qed.（或Defined.）完成了一个证明，你也可以要求查看使用Print term.构建的项，其中term是定理/项的名称。
这通常是一个又大又丑的术语，需要一些培训才能阅读相关术语。特别是，如果这个术语是通过使用强大的策略（如omega、crush等）构建的，那么它可能是不可读的。你基本上只会用它来扫描你感兴趣的术语的某个特定位置。如果它超过10行长，甚至不用麻烦以如此粗糙的格式阅读！：）
对于前面的所有内容，您可以预先使用Set Printing All.，以便Coq打印所有内容的展开显式版本。它还很详细，但当您想知道隐式参数的值是什么时，它会有所帮助。
这些都是我脑海中能想到的，也许还有更多。
关于策略的作用，通常最好的答案在文档中：
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@战术155
基本上，auto尝试使用提供的所有提示（取决于您使用的数据库），并将它们组合到一定深度（您可以指定）来解决您的目标。默认情况下，数据库为core，深度为5。
更多信息可以在这里找到：
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-数据库