Coq 中的“详细”自动答案

【问题标题】："Verbose" auto in CoqCoq 中的“详细”自动
【发布时间】：2013-02-01 18:18:50
【问题描述】：

我正在学习 Coq，我正在学习的书 (CPDT) 在证明中大量使用了 auto。

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

如果没有，是否有地方详细说明 auto 的作用？

【问题讨论】：

标签： coq verbose

【解决方案1】：

有多种方法可以一目了然。

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

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

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

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

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

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

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

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

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

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

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

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

【讨论】：