coq - Coq 中的“详细”自动

Question

我正在学习 Coq 和我正在学习的书，( CPDTauto )在证明中大量使用。

由于我正在学习，我认为准确了解幕后工作可能对我有所帮助auto（早期的魔法越少越好）。有什么方法可以强制它准确显示它用于计算证明的策略或技术吗？

如果没有，是否有一个地方详细说明了什么auto？

score 18 · Accepted Answer

有多种方法可以一目了然地了解引擎盖下发生的事情。

TLDR：放在info你的策略之前，或者Show Proof.在调用策略之前和之后使用并发现差异。

要查看特定策略调用一直在做什么，您可以在 is 前加上info，以显示它已采取的特定证明步骤。

（这可能会被 Coq 8.4 破坏，我看到他们提供info_了一些策略的版本，如果需要，请阅读错误消息。）

这可能是初学者想要的，它已经很简洁了。

另一种查看证明中当前情况的方法是使用命令Show Proof.。它将向您显示当前构建的带有漏洞的术语，并告诉您当前的每个目标应该填补哪个漏洞。

这可能更高级，特别是如果您使用诸如inductionor之类的策略inversion，因为正在构建的术语将相当复杂，并且需要您了解归纳方案或依赖模式匹配的基本性质（CPDT 应该教您很快就好了）。

Qed.用(or )完成证明后Defined.，您还可以要求查看通过使用Print term.where termis the theorem/term 的名称构建的术语。

这通常是一个又大又丑的术语，它需要一些培训才能阅读这些涉及的术语。特别是，如果该术语是通过使用强大的策略（例如omega、crush等）构建的，则它可能会变得不可读。您基本上只会使用它来扫描您感兴趣的术语的某个特定位置。如果它超过 10 行，甚至不用费心以如此粗略的格式阅读它！:)

对于之前的所有内容，您可以Set Printing All.预先使用，以便 Coq 打印所有内容的展开、显式版本。它也很冗长，但当您想知道隐式参数的值是什么时会有所帮助。

这些都是我能想到的，但可能还有更多。

至于策略的作用，通常的最佳答案可以在文档中找到：

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

更多信息可以在这里找到：

1 回答 1