Coq中的“详细”自动

我正在学习Coq和我正在学习的书，（CPDT）在校样中大量使用auto。Coq中的“详细”自动

因为我正在学习，我认为这可能对我看到auto究竟在做什么（魔术越早越好）可能会有帮助。有什么办法可以强制它显示出它使用什么策略或技术来计算证明？

如果不是，有没有一个地方的细节究竟是什么auto呢？

有多种方式可以对引擎盖下发生的事情进行浏览。

TLDR：在战术前放置info，或在调用策略之前和之后使用Show Proof.，并找出差异。

要查看某个特定的策略调用一直在做，你可以前缀与info，以表明它采取具体步骤的证据。

（这可能与勒柯克8.4被打破，我看到他们提供info_版本进行了一些战术，如果你需要阅读的错误信息。）

这可能是你想要在初学者水平，已经可以相当简洁了。

另一种查看证明内容的方法是使用命令Show Proof.。它会向您显示当前建立的带洞的术语，并向您显示您当前每个目标应该填充的洞。

这可能是更先进的，尤其是如果您使用诸如induction或inversion的策略，因为正在构建的术语将会相当涉及，并且需要您了解归纳方案或相关模式匹配的基本性质（CPDT应该尽快教你）。

一旦你完成了一个证明与Qed.（或Defined.），你也可以问一下这是通过使用Print term.其中term是定理/项的名称建术语。

这通常是一个大而且丑陋的术语，需要一些培训才能阅读这些术语。特别是，如果该术语是通过使用强大的策略（例如omega,crush等）构建的，则可能无法阅读。你基本上只会用它来扫描你感兴趣的术语的某个特定位置。如果它超过10行，你甚至不会用这种粗糙的格式来阅读它！ :)

以前所有的，你可以事先使用Set Printing All.，使勒柯克打印一切的展开，明确的版本。它额外冗长，但可以帮助你想知道什么是隐式参数的值。

这些都是我能想到的在我头顶的那些，可能还有更多。

至于什么战术呢，通常的最佳答案在文档中发现：

基本上，auto尝试使用所提供的所有提示（取决于你使用的数据库），并解决您的目标，将它们组合到某个深度（您可以指定）。默认情况下，数据库为core，深度为5。

2013-02-17 04:48:23 Ptival

'info_auto'仅显示 “成功之路”。要看看'auto'尝试可以使用'debug auto.'：它显示所有失败（！）和成功。 – 2018-01-02 13:23:22

回答