Изабель: Доказательство разницы между 2 списками

Question

Я новичок в доказательстве теоремы и Изабель. Я пытаюсь доказать простую (?) Теорему в Изабель о списках.

Вот теория:

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 доказательств, и я использовал Sledgehammer, чтобы доказать, что они двое. Затем я выбил 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