如何管理所有各种证明方法

Question

是否存在Isabelle用户遵循的"通用"非正式算法,当他们试图证明某些事情未被立即证明auto或sledgehammer？如果auto需要额外的引理,由用户制定成功或者如果使用更好的一些其他证明方法,一种通用的方法.

一个相关的问题是:是否可能在某处找到一个表格,其中包含所有证明方法以及应用它们的上下文？当我阅读 编程和校对教程时,各种方法的描述(分别是某些方法的变体,例如许多变体auto)都散布在文本中,这不断让我回到文本和Isabelle代码之间(这也会导致忘记究竟用于什么),这导致工作效率非常低.

Answer 1

ammbauer 的回答已经涵盖了很多重要的内容，但这里还有一些可能对您有所帮助的内容：

• 当自动化在某个点卡住时，请查看可用的前提和该点的目标。你希望系统在那个时候做什么样的简化？为什么它没有做到？或许，相应的规则就是没有在SIMP集（与它添加simp add:）或规则的某些先决条件未能证明（在这种情况下，补充足够的事实，使他们可以证明，或者自己做的一个额外的步骤）
• Isar 证明很好。如果您有一些复杂的目标，请尝试在 Isar 中将其分解为更小的步骤。如果您有更大的辅助事实甚至可能更具有普遍意义，请尝试将它们作为辅助引理提取出来。也许你甚至可以将它们概括一下。有时，这甚至可以简化证明。
• 同样的道理：太多的信息会混淆你和伊莎贝尔。您可以在 Isar 中引入本地定义define x where "x = …"并使用 展开它们x_def。这使您的目标更小、更清晰，并降低了自动化在其证明搜索中走上无用路径的可能性。
• Isabelle 不会自动展开定义，因此如果您有definition, 并且您想展开它以进行证明，则必须自己使用unfolding foo_def或来执行此操作simp add: foo_def。
• 使用简化符 ( , , , )定义的函数的定义方程fun或primrec 正在展开的函数的定义方程，除非方程 ( ) 已从 simp 集中手动删除。（由或）simpsimp_allforceautofoo.simpslemmas [simp del] = foo.simpsdeclare [simp del] foo.simps
• 不同的证明方法擅长不同的事情，需要一定的经验才能知道在什么情况下使用什么方法。作为一般规则，任何只需要重写/简化的东西都应该用simp或来完成simp_all。任何与经典推理（即一阶逻辑或集合）相关的事物都需要blast。如果您需要重写和经典推理，请尝试auto或force。可以认为是andauto的组合，simp并且如果它不能完全解决目标blast，force则就像它的“全有或全无”变体一样auto失败。它也比 更努力一点auto。
• 大多数证明方法都可以选择。您可能已经知道add:and del:for simpand simp_all，以及等效的simp:/ simp del:for auto。然而，经典推理（auto，blast，force等）也接受intro:，dest:，elim:和相应的del:选项。这些用于声明引入、销毁和消除规则。

关于经典推理器的更多信息：

• 介绍规则是P ? Q ? R当目标具有形式时应使用的形式规则R，将其替换为P和Q
• 销毁规则是一种形式的规则，P ? Q ? R只要形式的事实存在P于前提中，就应该使用G新的目标Q和来替换目标R ? G。
• 消除规则类似于thm exE（消除存在量词）。这些就像破坏规则的概括，也允许引入新变量。这些规则经常出现在这种类似情况的区分中。
• 通过使用经典的推理auto，blast，force等会使用规则中claset（即已宣告intro/ dest/elim在适当的时候自动）。如果这样做没有得到证明，自动化将在某个时候回溯并尝试其他规则。您可以通过使用intro!:代替intro:（对于其他规则类似）来禁用特定规则的回溯。然后自动化将尽可能应用该规则，而无需回头。
• 基本的证明方法rule，drule，erule对应于将一个前奏/目标/琳规则，并且是单步推理好，例如为了找出原因自动方法不能使在某一点进步。intro就像rule但应用迭代给定的规则集，直到不再可能。
• safe并且clarify偶尔有用。前者本质上剥离了量词和逻辑连接词（在像 一样的目标上尝试?x. P x ? Q x ? R x），而后者同样试图“清理”目标。（我忘记了它到底是做什么的，我只是在我认为它可能有用的时候偶尔使用它）

Answer 2

不,没有"通用"的非正式方式.你可以用try0它尝试所有标准的证明方法(如auto,blast,fastforce,...)和/或sledgehammer哪个更先进.

之后,有趣的部分开始了.

• 这个定理可以用更简单的辅助词来表示吗？您可以使用命令"sorry"来假设引理为真.
• 我怎么在一张纸上证明这一点？然后尝试在Isabelle中做这个证明.
• 寻求帮助:)很多人在堆栈溢出,freenode上的#isabelle和Isabelle邮件列表等着你的问题.

对于你的第二个问题:不,没有这样的概述.也许有人应该写一个,但如前所述,你可以简单地使用try0.