强制数据类型

Question

我在伊莎贝尔

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是不同的？

更新：作为曼努埃尔EBERL在答案注释所建议的，问题是由错误的简化规则引起的（引理与[simp]属性，这里省略），其提出的简化过程回路，因此忽略该自动生成的简化规则B≠C,C≠B（发现于bs_t.simps，正如克里斯在他的回答中所指出的那样）。正如在gc44的回答中，simp足以证明在正常情况下的引理。

Answer 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)) 

我以前​​，因为我曾在 “插件选项/伊莎贝尔/常规” 选中Auto Methods。很多时候在选项中，除了大锤之外，我还检查了所有的汽车工具箱。

您可以使用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规则。简化器有一个以上的石头来杀死这只鸟，所以我放弃了。

要记住的一件事是，您可以使用simp与方法如auto和fastforce，如apply(auto simp add: stufferThm)。特别是如果auto，如果simp规则不足以证明一个定理，它可能会诉诸使用blast，它不会显示在simp跟踪。在使用only时，知道这一点非常重要，因此您不会对auto找到的证明所需的全部规则感到满意。

这里我对你的评论发表一些评论。如Eberl提到的那样，如果simp保持紫色很长时间，则必须进行大量简化，或者它处于非终止循环中。要么是坏的。我不认为40秒simp证明了一个很好的证据。

基本上，很容易让simp进入循环，或者任何其他调用simp的方法，尤其是如果您要定义自己的simp规则。当它工作时，simp方法很容易。如果没有，你可能需要为你的逻辑工作。

使用​​，当没有证据被发现，它会给你的自动证明方法的列表进行实验，像force，fastforce，auto等。如果simp与auto循环，您可能会fastforce尝试。试验很重要。

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

[更新 140109_0750：进行概括总是有风险的。展开定义将多次阻止大锤找到证据。通过匹配高级定理，Sledgehammer可以很好地工作，所以一个绝望的扩展公式会多次失败。即使是一个巨大的扩展公式也会导致其他自动方法无法找到证明。然而，对于基于方程的计算性质的事物，扩展定义可以允许完全减少巨大的，复杂的表达式。你必须知道什么时候握住他们，什么时候展开他们。伟大的事情是很容易以合理的速度尝试很多事情。]

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

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

这不是小问题。简单的事情不一定很容易证明。一旦你学会了如何使用汽车工具，所需要的打字就是微不足道的。

Answer 2

创建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获得。）

通过这些简化规则，可以解决您的引理by simp。