伊莎贝尔:大锤发现了一个证据,但它失败了

Question

通常我有问题sledgehammer找到证据,但是当我插入它时,它不会终止.我猜sledgehammer是Isabelle最重要的部分之一,但如果证据失败则会变得很烦人.

在Sledgehammer教程中,有一个小章节"为什么Metis无法重建证明？".

它列出:

1. 尝试isar_proofs选项以获得逐步的Isar证明,其中每个步骤都是正确的metis.由于步骤相当小, metis因此更有可能重播它们.
2. 尝试使用smt证明方法而不是metis.它通常更强大,但您需要使用Z3重放证明,信任SMT求解器或使用证书.
3. 尝试blast或者auto证明方法,通过传递必要的事实unfolding,using,intro:,elim:,dest:,或simp:适当.

问题是第一个选项使证明更加冗长,并且还涉及手动干预.第二种选择很少有效.

那么第三种选择呢？我可以使用任何易于遵循的启发式方法吗？

unfolding和之间有什么区别using？也有关于如何使用的最佳做法intro:,elim:以及dest:从失败的metis证明吗？

部分例子

proof- 
  have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose) 
  then have "(det (?lm)) = [...][not shown]"
    unfolding det_transpose transpose_mat_factor_col by auto
  then show ?thesis [...][not shown]
qed

我想摆脱证明的第一行,因为这条线似乎微不足道.如果我删除了第一行,sledgehammer仍然会找到证据,但是这个证明失败了(不会终止).

Answer 1

关于你的陈述大锤是伊莎贝尔最重要的部分之一:你永远不需要大锤就能证明成功.但当然大锤非常方便,可以节省大量繁琐的推理.因此,对于那些没有花费多年时间使用它的人来说,Isabelle更有用,这绝对是一个非常重要的部分(即使是那些大锤每天都能提高效率).

来到你的问题

尝试blast或者auto证明方法,通过传递必要的事实unfolding, using,intro:,elim:,dest:,或simp:适当.
[...]
那么[这]选项怎么样？我可以使用任何易于遵循的启发式方法吗？

确实有:

unfolding:这个(递归地)展开方程,即它非常相似apply (simp only: ...).启发式是,当你没有通过simp: ...尝试获得预期结果时unfolding ...(可能是其他方程干扰的情况).

using:这用于向当前子目标添加其他假设.启发式是,只要事实不适合下面的模式之一,请尝试using改为.

intro::这用于引入规则,即,每当满足某些假设时,可以引入一些连接(或更一般地恒定)的形式.
示例:( A ==> B ==> A & B引入的常量为(&)).

elim::这用于消除规则,即,从存在某个连接词(或更一般地说是常数)的形式,某些事实可以作为附加假设得出结论.
示例:( A & B ==> (A ==> B ==> P) ==> P其中常量(&)被消除,有利于显式拥有A和B作为假设).注意结论的一般形式(与主要前提无关A & B),这对于不松散的可证明性很重要(另见dest:).

dest::这用于销毁规则,即,从存在某个常数的形式,可以直接得出一些事实.
示例:( A & B ==> B请注意,A结论中保留的信息将丢失,与elim:示例中的不同.)

simp::这用于简化规则,即(条件)方程式,它们总是从左到右应用(因此有时候添加[symmetric]到事实中是有用的,以便从右到左应用它,但要注意不确定,因为很容易以这种方式引入循环派生).

说完这些之后,通常只有经验可以让您决定在证明中最好地使用给定事实的方式.当我sledgehammer在Isar 得到一个太慢的证据时,我通常会做的是检查找到的证据使用的事实.然后按上面的方式对它们进行分类,auto适当调用,如果没有完全解决目标,sledgehammer再次应用(希望这次提供"更容易"的证明).

Answer 2

你问了很多问题，但我会把你的标题和第二段作为你主要抱怨的本质，我最终会给出一个冗长的答案，可以总结为，

• 大锤是三管齐下的武器库的一部分，
• 你变得更有经验，不断进行实验，试错是启发式的，
• 不使用 Sledgehammer 返回的许多证明是使用 Sledgehammer 的重要部分，并且
• 在minimize和preplay_timeout选项可以通过自动打回的证明，它给你定时信息，有时显示，所发现的证据将无法为你节省时间和挫折。

从你的第二段开始，你说：

很多时候我都会遇到 Sledgehammer 找到证明的问题。但后来我尝试了一下，但证明并没有终止。我猜大锤是伊莎贝尔最重要的部分之一，...

大锤很重要，但我认为它是三管齐下的武器库的一部分，其中三个部分是：

1. 使用自然演绎法的详细证明步骤。
2. 自动证明方法，如auto，simp，rule，等。这将是创建自己的很大一部分simp重写规则，并学习使用与定理rule和其他自动证明方法无数。
3. 大锤调用自动定理证明器 (ATP)。使用第 1 步和第 2 步，根据经验，用于设置 Sledgehammer。经验很重要。您可能会使用auto简化事情以使 Sledgehammer 成功，但您可能不会使用，auto因为它会将公式扩展到 Sledgehammer 没有机会成功的地方。

...但是如果证明失败，那就很烦人了。

所以在这里，你和我对 Sledgehammer 的期望是不同的。这些天，如果我生气，我会生气，因为我将不得不工作 30 秒以上来证明一个定理。如果我对某个特定的 Sledgehammer 证明失败感到非常失望，那是因为我一直试图证明一个定理几个小时或几天没有成功。

用 Sledgehammer 不是找证明，而是找好的证明

自动化有时可以减轻挫折感。单击 Sledgehammer 证明，却发现它失败了，这令人沮丧。这是我目前使用 Sledgehammer 的方式，除非我开始急于求证：

sledgehammer_params[minimize=smart,preplay_timeout=10,timeout=60,verbose=true,
                    max_relevant=smart,provers="
  remote_vampire  metis  remote_satallax  z3_tptp  remote_e
  remote_e_tofof  spass  remote_e_sine    e        z3       yices
"]

选项minimize=smart和preplay_timeout=10与 Sledgehammer 在找到它们后回放校样有关。不使用 Sledgehammer 找到的许多证明是使用 Sledgehammer 的重要组成部分，而证明回放是剔除证明的重要组成部分。

就我个人而言，我不太会处理不终止的 Sledgehammer 证明，但这可能是因为我有选择性地开始。

我对 Sledgehammer 证明的第一个标准是它相当快，所以当 Sledgehammer 报告说它找到了一个超过 3 秒长的证明时，我什至不会尝试使用它，除非我非常想知道定理可以证明。

我对 Sledgehammer 的使用通常是这样的：

• 陈述一个定理，看看我是否幸运地使用了 Sledgehammer。
• 如果 Sledgehammer 给我的证明时间为 30 毫秒或更短，那么我认为这是一个很好的证明，但我仍在尝试使用tryisar-ref.pdf 第 208 页第 9.4.4 节中的自动证明方法。很多时候，我可以在 5 毫秒或更短的时间内获得证明。
• 一个metis超过100ms的总时间证明，我愿意工作30分钟以上，试图获得更快的证明。
• 一个metis200毫秒的500毫秒来证明，我会求助于我知道，试图把它降低到低于100毫秒，其多次手段转化为详细的证明一切。
• A smtormetis大于1秒的证明我只认为好的作为临时证明。
• Sledgehammer 报告大于 3 秒的输出面板中的证明，我通常什至不尝试，因为即使最终成功，我也将不得不努力寻找另一个证明，所以我会而是花时间在前面试图找到一个好的证明。

选项 3 启发式

你说，

那么第三个选项呢。是否有任何我可以应用的易于遵循的启发式方法？

启发式是：

• “作为适当的”，

也就是说，启发式是“使用大锤作为三管齐下的武器库的一部分”。

启发式也是“阅读大量教程和文档，以便您有很多其他东西可以与 Sledgehammer 一起使用”。Sledgehammer 是强大的，但它不是无限强大的，对于一些定理，你可以使用自己的simp规则在 0ms 内证明apply(simp)或者apply(auto)Sledgehammer 永远不会证明的。

对我自己来说，我有大约 150 到 200 个定理，所以“酌情”对我来说比过去更有意义。基本上，您尝试按照需要设置的方式设置 Sledgehammer。

Sledgehammer 需要设置的方式有时意味着运行auto或simp首先，但有时不是，因为多次运行auto或simp将注定 Sledgehammer 失败。

但有时，您甚至不需要metisSledgehammer的证明，除非作为初步证明，直到您找到更好的证明，对我来说，这通常意味着使用自动证明方法更快地证明。

我不是 Sledgehammer 的权威，但 Sledgehammer 似乎擅长匹配旧定理的假设和结论，并将假设和结论用于新定理。它不擅长的是证明我通过使用simp和大大扩展的公式auto。

我继续以 Sledgehammer 为中心的冗长启发式：

• 使用 Sledgehammer 启动证明过程，通过使用 Sledgehammer 证明一些您不知道如何证明的定理。
• 把你的定理这是换算公式为simp带自动证明的方法，如使用重写规则simp，auto，fastforce等，在tutorial.pdf的第9章描述。
• 将您的一些定理用于条件重写规则，以便与intro和一起使用rule。
• 最后两个步骤用于完全解决证明步骤或用于“根据需要”设置 Sledgehammer。大锤永远有用，不管你知道多少，当你知道的不多时它非常有用，但仅靠大锤不是成功之路。
• 如果 Sledgehammer 不能证明一个定理，那就求助于详细的证明，从一个简单的详细证明开始。有时，当 Sledgehammer 无法证明 if-and-only-if 时，将 if-and-only-if 分解为两个条件可以让 Sledgehammer 轻松证明这两个条件。
• 在你证明了很多东西之后，回去优化你的证明。有时，所有的重写规则您创建，simp并auto会奇迹般地被证明的东西，你将摆脱一些metis证据，可以证明大锤找到您。有时，您会使用 Sledgehammer 找到metis更快的证明。

使用此命令优化时序：

ML_command "Toplevel.timing := true"

还有另一个 SO 帖子提供了有关它的更多详细信息。