我正在学习Coq和我正在学习的书,(CPDT)大量使用auto证明.
因为我正在学习,所以我认为确切地看到auto引擎盖下的内容可能会有所帮助(早期越少越好).有没有办法强制它显示它用于计算证据的确切策略或技术？
如果没有,是否有一个地方详细说明了什么auto呢？
Pti*_*val 15
有多种方法可以了解幕后发生的事情.
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