Isabelle/HOL：'simp' 的证明很慢，而 'value' 是瞬时的

Question

我是Isabelle/HOL的新手，还在研究prog-prov练习。同时，我正在通过将这些证明技术应用于组合词的问题来进行练习。我观察到 'value' 和 'lemma'.

之间非常不同的行为（在效率方面）

能否解释一下这两个命令之间的不同 evaluation/search 策略？

有没有办法在 'lemma' 的证明中使用 'value' 的速度？

当然，我问是因为我还没有在文档中找到答案（到目前为止）。记录和解释这种效率差异的手册是什么？

这是重现该问题的最小源代码。

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

Isabelle 社区中关于是否应该使用此选项的意见不一。有人说它类似于 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 的评论

Isabelle/HOL：'simp' 的证明很慢，而 'value' 是瞬时的

Isabelle/HOL: proof by 'simp' is slow while 'value' is instantaneous

performance

isabelle