coq - "Verbose"在 Coq 中自动

Question

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

由于我正在学习，因此我认为了解确切内容可能对我有帮助 auto在幕后做(越早越好)。有没有办法强制它准确显示它用来计算证明的策略或技术？

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

Answer 1

有多种方法可以查看幕后发生的事情。

TLDR:放置 info在您的策略之前，或使用 Show Proof.在调用策略之前和之后，发现差异。

要查看特定的策略调用一直在做什么，您可以使用 info 作为前缀。 ，以显示它所采取的特定证明步骤。

(这可能会在 Coq 8.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#@tactic155

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

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

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-databases