伊莎贝尔：证明两个名单之间的差异

Question

我是新定理证明和伊莎贝尔。我试图在Isabelle中列举一个简单的（？）定理。

这是理论：

theory Scratch 
imports 
    Main 
    Option 
    String 
begin 

fun list_difference :: "string list => string list => nat" 
where 
    "list_difference [] [] = 0" 
| "list_difference [] x = length x" 
| "list_difference x [] = length x" 
| "list_difference (x#d1) (y#d2) = (if (x=y) then list_difference d1 d2 else (1 + list_difference d1 d2))" 

fun modify :: "string list ⇒ nat ⇒ string list" 
where 
"modify list n = list[n:=''somethingnew'']" 

这些配套引理

lemma diff_zero [simp]: 
shows "list_difference somelist somelist = 0" 
apply(induct_tac somelist, auto) 
done 

lemma sub1 [simp]: 
shows "modify [] 0 = []" 
apply(auto) 
done 

lemma diff_zero_basecase [simp]: 
shows "list_difference somelist (modify somelist 0) <= 1" 
apply(induct_tac somelist, auto) 
done 

此我想原来的定理证明

(*Description : modify will change only one or zero elements.. so diff should be <= 1*) <br> 
lemma modification_lemma [simp]: 
shows "list_difference somelist (modify somelist index) ≤ 1" 
apply(induct_tac somelist, auto) 
apply(cases index, auto) 
oops 

如何继续证明这个定理？

我的另一个问题是如何从这些情况下通常尝试证明定理？我尝试了以下Isabelle教程，但我无法获得关于此的一般建议。

Answer 1

我给你一个证明，并解释一些我用来获得结果的基本技巧，但是用一种相当无心的方式。其他人可能想要提供一个解释，使您更好地了解该主题：涉及nat和list的归纳。

我缩短了一些标识符，我把整个理论放在下面。在需要证明的公式中基本上有两个自由变量，ls和idx。

因此，对于证据的目标，在努力的事情，我在做的很多事情我旁边展示，或一些变化，有可能cases为induct：

(*MINDLESS_TECHNIQUE_1*) 
apply(induct ls, auto) 
apply(induct idx, auto) 

在某一点上，auto正在采取很长一段时间，这意味着由于simp规则，它也许循环不好，你曾在。

我消除了simp规则，并插入他们只在需要的地方，它摆脱了auto循环。

这是第一个进步点，它让我进入MINDLESS_TECHNIQUE_2，将验证目标分解为lemma，与MINDLESS_TECHNIQUE_1一起使用，并与Sledgehammer一起使用。

在这一点上，对于你的modification_lemma，在使用apply之后，我有3个证明目标，我用大锤证明其中两个。然后我打出了如下所示的第三个证明目标，这很容易通过by(induct ls, auto)来证明。

更新：使用亚历山大的尖端去同一个目标证明为损出引理上面，我添加了一个证明，在下面的源，在那里我解开了两个绑定变量。这仍然是一个丑陋的解决方案，所以也许有更好的办法比结束绑定变量。

使用auto或simp_all为我做什么，我不能盲目与by(induct ls, auto)得到最终结果的原因是因为变量idx和ls是由元所有，!!约束。如果没有自动工具可以做证明工作，我们需要解开它（我猜），这会让事情变得非常混乱。

theory c2 
imports Main Option String 
begin 

fun list_diff :: "string list => string list => nat" where 
    "list_diff [] [] = 0" 
|"list_diff [] x = length x" 
|"list_diff x [] = length x" 
|"list_diff (x#d1) (y#d2) = 
    (if (x=y) then list_diff d1 d2 else (1 + list_diff d1 d2))" 

fun modify :: "string list => nat => string list" where 
    "modify ls n = ls[n := ''abc'']" 

lemma diff_zero: 
    "list_diff ls ls = 0" 
by(induct_tac ls, auto) 

lemma sub1: 
    "modify [] 0 = []" 
by(auto) 

lemma diff_zero_basecase: 
    "list_diff ls (modify ls 0) <= 1" 
by(induct_tac ls, auto simp add: diff_zero) 

(*****************************************************************************) 
lemma the_mindless_result_of_eliminating_simp_rules_and_breaking_out_goals: 
    "(!!a ls. list_diff ls (ls[idx := ''abc'']) <= Suc 0 ==> 
    list_diff (a # ls) 
    (case idx of 0 => ''abc'' # ls | Suc j => a # ls[j := ''abc'']) <= Suc 0) 
    ==> list_diff ls (ls[Suc idx := ''abc'']) <= Suc 0 ==> 
     list_diff ls (ls[idx := ''abc'']) <= Suc 0" 
by(induct ls, auto) 

lemma modification_lemma: 
    "list_diff ls (modify ls idx) <= 1" 
apply(induct ls, auto) 
apply(induct idx, auto) 
apply(metis diff_zero le0) 
apply(metis diff_zero) (*The goal I broke out to the above lemma.*) 
by (metis the_mindless_result_of_eliminating_simp_rules_and_breaking_out_goals) 

(*****************************************************************************) 
(*Update: After the third 'apply', I can't mindlessly do 'by(induct ls, auto)', 
    because variables 'ls' and 'idx' are bound by '!!. If I use 'auto' like I 
    did, and I don't want to break out the proof goal, I need to unwrap the 
    variables 'idx' and 'ls, as shown below.*) 

lemma unwrapping_variables: 
    "list_diff ls (modify ls idx) <= 1" 
apply(induct ls, simp_all) 
apply(induct idx, simp_all) 
apply(simp_all add: diff_zero) 
proof- 
    fix idx 
show "!!ls. ((!!a ls. list_diff ls (ls[idx := ''abc'']) <= Suc 0 ==> 
    list_diff (a # ls) 
    (case idx of 0 => ''abc'' # ls | Suc j => a # ls[j := ''abc'']) <= Suc 0) 
    ==> list_diff ls (ls[Suc idx := ''abc'']) <= Suc 0 ==> 
     list_diff ls (ls[idx := ''abc'']) <= Suc 0)" 
    proof- 
    fix ls 
    show "(!!a ls. list_diff ls (ls[idx := ''abc'']) <= Suc 0 ==> 
    list_diff (a # ls) 
    (case idx of 0 => ''abc'' # ls | Suc j => a # ls[j := ''abc'']) <= Suc 0) 
    ==> list_diff ls (ls[Suc idx := ''abc'']) <= Suc 0 ==> 
     list_diff ls (ls[idx := ''abc'']) <= Suc 0" 
    by(induct ls, auto) 
    qed 
qed 

thm unwrapping_variables 

end