2

我在 Isabelle 中定义了以下数据类型

datatype bc_t =  B | C

并且看不到如何证明以下基本引理

lemma "∀ x::bc_t . (x=B ⟶ x≠C)"

在假设下B≠C，证明通过：

lemma "⟦B≠C; x=B⟧ ⟹ x≠C"
by metis

有没有一种方法可以在没有明确假设的情况下证明引理B并且C是不同的？

更新：正如 Manuel Eberl 在对答案的评论中建议的那样，问题是由错误的简化规则（带有[simp]属性的引理，此处省略）导致简化过程循环并因此忽略自动生成的简化规则B≠C，C≠B（在bs_t.simps,正如克里斯在他的回答中指出的那样）。正如 gc44 的回答一样，simp在正常情况下足以证明引理。

4

2 回答 2

1

你可以让汽车工具给你一个很大的开端。告诉你从自动工具获得反馈的多种方法比我证明定理需要更多的工作。

datatype bc_t =  B | C

lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
try0
using[[simp_trace]] 
using [[simp_trace_depth_limit=100]]
apply(simp)
done

lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"
sledgehammer
by (metis bc_t.distinct(1))

我使用try0是因为我Auto Methods在“插件选项/伊莎贝尔/常规”中未选中。很多时候，在选项中，除了 Sledgehammer 之外，我都选中了所有的自动工具框。

您可以使用sledgehammer我在此处显示的内容，也可以在 PIDE 的 Sledgehammer 面板中使用它。使用simp_trace，当您将光标放在 的行上时apply(simp)，您可以了解该simp方法如何证明它，这将基于替换规则。

更新 140108_1305

自动工具对于帮助我们快速工作很重要，但有时理解证明的基本逻辑也很重要。这是simp_trace该方法的其他属性simp可能有用的地方。阅读tutorial.pdf，prog-prove.pdf并isar-ref.pdf了解有关使用的一些详细信息和课程simp。

simp用于控制该方法的三个此类属性是add、del和only。

在您的示例中，我想使用simp_trace和only来明确使用哪些规则，以帮助我理解逻辑。

Sledgehammer的metis证明看起来simp可能只使用了一些规则。我查看simp跟踪，simp只使用可以从控制面板剪切和粘贴的规则。我数了 4 条命名规则，这实际上并不是值得做的事情，尽管我必须找到它。

[更新140101_0745：尽量不过度分析情况，我最终使用了，del因为我的宏伟使用计划only没有奏效。在下面simp only的地方simp del，该apply方法失败并出现错误，这意味着它不能仅使用这四个规则来简化目标。auto simp only而不是这种情况simp only。该auto方法不受方式simp的限制，它可能会做很多它不会告诉你的事情，例如调用blast.]

lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"    
using[[simp_trace]] 
using [[simp_trace_depth_limit=100]]
apply(simp del: 
    bc_t.distinct(1)
    simp_thms(8)
    simp_thms(17)
    simp_thms(35)
    ) 
oops

好吧，现在当我查看最新的simp踪迹时，还有更多simp规则。简化器有超过1个石头可以杀死鸟，所以我放弃了。

要记住的一件事是，您可以使用simp诸如auto和之fastforce类的方法apply(auto simp add: stufferThm)。auto特别是，如果simp规则不足以证明一个定理，它可能会求助于 using blast，这不会出现在跟踪simp中。在使用 时了解这一点很重要only，因此您不会认为simp规则就是 . 找到的证明所需要的全部内容auto。

在这里，我在下面对您的评论发表一些评论。

如 Eberl 所提到的，如果simp长时间保持紫色，则必须进行大量简化，或者处于非终止循环中。要么不好。我不认为 40 秒simp的证明是一个好的证明。

基本上，很容易进入simp循环或任何其他调用 的方法simp，尤其是在您定义自己的simp规则时。该simp方法在起作用时很容易。如果没有，您可能必须按照自己的逻辑工作。

使用try0，当没有找到证明时，它会给你一个自动证明方法的列表来试验，比如force, fastforce,auto等。如果simp是循环的auto，你可以尝试使用fastforce。实验很重要。

要记住的另一件重要的事情是展开不是simp规则的定义。大锤有时可以找到定义，但有时最简单的定理无法证明，因为尚未展开定义。

[更新140109_0750：进行概括总是有风险的。展开定义会多次阻止 Sledgehammer 找到证据。大锤通过匹配高级定理而运作良好，因此一个绝望的扩展公式将多次注定它会失败。即使是一个极大扩展的公式也可能导致其他自动方法无法找到证明。然而，对于基于方程的计算性质的事物，扩展定义可以simp完全减少庞大而复杂的表达式。您必须知道何时握住它们，何时展开它们。最棒的是很容易以相当快的速度尝试很多事情。]

definition stuffTrue :: "bool" where
  "stuffTrue = True"

theorem "stuffTrue"
  apply(unfold stuffTrue_def)
  by(simp)

这不是微不足道的问题。简单的事情不一定容易证明。一旦您学习了如何使用自动工具，就需要进行打字，这是微不足道的。

于 2014-01-08T14:14:38.213 回答
0

在创建datatype一堆简化规则时会自动派生（在名称下<datatype-name>.simps）并添加到简化器中。在您的示例中，它将是

datatype bc_t =  B | C
thm bc_t.simps

B ≠ C
C ≠ B
(case B of B ⇒ ?f1.0 | C ⇒ ?f2.0) = ?f1.0
(case C of B ⇒ ?f1.0 | C ⇒ ?f2.0) = ?f2.0
bc_t_rec ?f1.0 ?f2.0 B = ?f1.0
bc_t_rec ?f1.0 ?f2.0 C = ?f2.

其中包括B和C不同的事实。（这些事实的一个子集，仅谈论独特性，可通过名称获得bc_t.distinct。）

有了这些简化规则，就有可能解决您的 lemma by simp。

于 2014-01-09T10:14:59.000 回答