強制數據類型

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。