Isabelle/HOL：'simp'的證明是緩慢的，'value'是瞬時的

Question

我是Isabelle/HOL的新手，仍然在研究鍛鍊練習。與此同時，我正在通過將這些證明技巧應用於組合詞的問題來鍛鍊。我觀察到一個非常不同的行爲（效率方面），在'價值'和'引理'之間。

能解釋兩個命令之間的不同評估/搜索策略嗎？

有沒有一種方法可以在「引理」的證明中使用「價值」的速度？

當然，我在問，因爲我還沒有在文檔中找到答案（到目前爲止）。什麼是手冊，這種效率差異將被記錄和解釋？

下面是重現問題的最小源代碼。

theory SlowLemma 
imports Main 
begin 

(* Alphabet for Motzkin words. *) 
datatype alphabet = up | lv | dn 

(* Keep the [...] notation for lists. *) 
no_notation Cons (infixr "#" 65) and append (infixr "@" 65) 

primrec count :: "'a ⇒ 'a list ⇒ nat" where 
"count _ Nil = 0" | 
"count s (Cons h q) = (if h = s then Suc (count s q) else count s q)" 

(* prefix n l simply returns undefined if n > length l. *) 
fun prefix :: "'a list ⇒ nat ⇒ 'a list" where 
"prefix _ 0 = []" | 
"prefix (Cons h q) (Suc n) = Cons h (prefix q n)" 

definition M_ex_7 :: "alphabet list" where 
"M_ex_7 ≡ [lv, lv, up, up, lv, dn, dn]" 
definition M_ex_19 :: "alphabet list" where 
"M_ex_19 ≡ [lv, lv, up, up, lv, up, lv, dn, lv, dn, lv, up, dn, dn, lv, up, dn, lv, lv]" 

fun height :: "alphabet list ⇒ int" where 
"height w = (int (count up w + count up w)) - (int (count dn w + count dn w))" 

primrec is_pre_M :: "alphabet list ⇒ nat ⇒ bool" where 
"is_pre_M _ (0 :: nat) = True" 
| "is_pre_M w (Suc n) = (let w' = prefix w (Suc n) in is_pre_M w' n ∧ height w' ≥ 0)" 

fun is_M :: "alphabet list ⇒ bool" where 
"is_M w = (is_pre_M w (length w) ∧ height w = 0)" 

(* These two calls to value are fast. *) 
value "is_M M_ex_7" 
value "is_M M_ex_19" 

(* This first lemma goes fast. *) 
lemma is_M_M_ex_7: "is_M M_ex_7" 
by (simp add: M_ex_7_def) 

(* This second lemma takes five minutes. *) 
lemma is_M_M_ex_19: "is_M M_ex_19" 
by (simp add: M_ex_19_def) 

end 

Answer 1

simp的是通過證明內核，即，每一步必須被合理的去證明方法。對於長時間重寫鏈，這可能是相當昂貴的。

另一方面，value在可能的情況下使用code generator。所有使用的常量都被轉換成ML代碼，然後執行。你必須相信結果，即它沒有經過內核，可能是錯誤的。

作爲證明方法的value的等價物是eval。因此，一個簡單的方法，以加快您的證明就是用這樣的：

lemma is_M_M_ex_19: "is_M M_ex_19" 
by eval 

意見在伊莎貝爾社區關於這是否應該使用不同。有人說它與axiomatization類似（因爲你必須相信它），但其他人認爲這是一個合理的方式，如果通過內核速度過於緩慢。大家都同意，儘管你必須非常小心代碼生成器的自定義設置（你還沒有完成，所以它應該沒問題）。

有中間地帶：在code_simp方法將設立simp使用只否則將由eval使用的公式。這意味着：對於simp而言，規則要小得多，同時還要經歷內核。根據你的情況，它實際上是相同的速度by eval，所以我會強烈建議這樣做：

lemma is_M_M_ex_19: "is_M M_ex_19" 
by code_simp 

在你的情況，爲什麼code_simp比simp快得多的原因是因爲有指數運行時simproc的在嵌套的let表達式中。因此，另一種解決方案是使用simp add: Let_def來展開let表達式。

---

編輯由Andreas Lochbihler