Coq中的“Verbose”自动模式

Question

17

我正在学习Coq，并且使用的教材是 (CPDT)，在证明中广泛使用了 auto。

由于我正在学习，因此我认为看到 auto 在幕后执行的确切步骤可能会对我有所帮助（起初尽量减少神秘感）。是否有任何方法可以强制它显示计算证明时使用的确切策略或技术？

如果没有，请问是否有地方详细介绍了 auto 所做的事情？

- user2079615

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Ptival · Accepted Answer

有多种方法可以一瞥内部运行情况。

TLDR: 在你的策略之前加上info，或在调用策略之前和之后使用Show Proof.，以便发现差异。

要查看特定策略调用的运行情况，可以在其前缀中加上info，以显示它所采取的特定证明步骤。

（这可能会在Coq 8.4中出现问题，我看到他们提供了info_版本的某些策略，请阅读错误消息如果需要。）

对于初学者来说，这可能是您想要的，因为它已经非常简洁。

另一种查看证明过程中正在进行的情况的方法是使用命令Show Proof.。它将向您显示带有空洞的当前构建术语，并向您显示每个当前目标应该填充的空洞。

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

完成使用Qed。（或Defined.）的证明后，您还可以使用Print term.来查看构建的术语，其中term是定理/术语的名称。

这通常是一个庞大而丑陋的术语，需要一些训练才能阅读涉及的术语。特别是，如果该术语是通过使用强大的策略（如omega、crush等）构建的，则可能无法阅读。基本上，您只会在感兴趣的术语的某个特定位置上扫描它。如果超过10行，请不要试图以这种粗略的格式阅读它！ :)

关于这些内容，您可以在使用 Set Printing All 之前，让 Coq 打印所有展开、显式版本的内容。虽然这样会变得更加冗长，但它可以帮助您了解隐含参数的值。

这些是我能够想到的所有内容，但可能还有更多。

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

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

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