列表和簡化規則：使用@而不是＃時更困難？

Question

在通過伊莎貝爾教程的練習中，我遇到了讓我困惑的情況。爲什麼涉及預先列表的下列引理很容易被證明：

lemma ‹count_list xs x = n ⟹ count_list (x # xs) x = Suc n› 
    by simp 

雖然這個涉及追加的不是？

lemma ‹count_list xs x = n ⟹ count_list (xs @ [x]) x = Suc n› 
    apply auto (* just does some minor rewriting *) 
    (* What should be go here? try/try0 are of no help. *) 
    done 

我認爲這事做與@如何實施比#更復雜，由於內部實現列表（#只是另一個構造而@涉及遞歸），但是是什麼讓這麼多更難以證明，你如何解釋？

Answer 1

這與'執行'@無關。這與'執行'count_list（但我會說'定義'而不是'執行'）有關。

像列表上的大部分功能，count_list是遞歸定義（使用primrec命令），其生成規則稱爲被添加到simpset（該組的該簡化器使用用於自動地重寫規則）count_list.simps。

如果您在thm count_list.simps輸入，你可能會得到這樣的事情：

count_list [] ?y = 0 
count_list (?x # ?xs) ?y = 
    (if ?x = ?y then count_list ?xs ?y + 1 else count_list ?xs ?y) 

由於他們是在simpset，被調用爲auto的一部分簡化器將永遠改寫左邊的任何實例一邊到右邊。

因此，您給出的第一個定理可以通過用這兩個規則中的第二個和更簡化來重寫的單個步驟來證明。在那張紙上，這個定理的一個等價的和更有用的公式將是count_list (x # xs) x = Suc (count_list xs x)。

同樣，我會非常建議將你的第二個引理改爲count_list (xs @ [x]) x = Suc (count_list xs x)。

現在爲什麼auto沒有解決這個問題？首先，對於這種目標，auto這個目標的唯一相關部分就是簡化器，所以你不妨在這裏寫上simp_all。而這個目標無法解決的原因是它沒有像count_list (… @ …)這樣的簡化規則。你必須自己證明這一點。

當你想證明一個遞歸定義的函數的特性，通常的做法是做鏡像遞歸定義的感應：

lemma ‹count_list (xs @ [x]) x = Suc (count_list xs x)› 
    apply (induction xs) 
    apply simp_all 
    done 

或者更簡潔：

lemma ‹count_list (xs @ [x]) x = Suc (count_list xs x)› 
    by (induction xs) simp_all 

但我實際上會推薦以下更通用的引理：

lemma ‹count_list (xs @ ys) x = count_list xs x + count_list ys x› 
    by (induction xs) simp_all 

In事實上，這是合理的給這個其實是一個名稱，並將其添加到SIMP集，因爲它使一個很好的重寫規則：

lemma count_list_append [simp]: 
    ‹count_list (xs @ ys) x = count_list xs x + count_list ys x› 
    by (induction xs) simp_all 

如果你想知道爲什麼我做了歸納於xs這裏，而不是在ys ：自的第一列表元素上count_list圖案匹配的遞歸定義，其餘的列表中，必須在第一列表上做感應（即xs），以便誘導工序談到(x # xs) @ ys，這簡化了x # (xs @ ys)然後一個可以應用歸納假設。

請注意，simp_all（或auto）足以證明上述證明中的歸納目標;一旦你告訴伊莎貝爾做誘導和什麼樣的誘導，其餘的證明再次只是簡單的重寫。