证明生成列表的属性

Question

我的目标是证明包含生成模式的列表的属性。在第一个示例中，模式只是一个 0 序列，引理 pattern_0_len 证明生成列表的长度确实等于生成器函数的长度参数。

theory pattern_0
imports Main
begin

fun pattern_0 :: "nat ⇒ nat list" where
"pattern_0 0 = []" |
"pattern_0 len =  (pattern_0 (len - 1)) @ [0]"

lemma pattern_0_len [simp]: "length (pattern_0 lng) = lng"
apply(induction lng)
apply(simp)
apply(auto)
done

end

在第二个示例中，生成器生成一个包含 0、1 个项目的序列。

theory pattern_0_1
imports Main
begin

fun pattern_0_1 :: "nat ⇒ nat ⇒ nat list" where
"pattern_0_1 0 item  = []" |
"pattern_0_1 len item =  (pattern_0_1 (len - 1) (if item = 0 then 1 else 0)) @ [item]"

lemma pattern_0_1_len [simp]: "length (pattern_0_1 lng item) = lng"
apply(induction lng)
apply(simp)
apply(auto)
done

end

不幸的是，pattern_0_1_len 没有证明（在 simp 之后目标正是归纳步骤），我想了解不证明的原因。 'confuses' Isabelle 是否存在项目参数？在这种情况下可以做什么，最好不要声明任何关于模式是如何生成的？

Answer 1

确实是附加参数的问题。例如，考虑这个子目标：

1. ⋀lng. length (pattern_0_1 lng 0) = lng ⟹ item = 0 ⟹ length (pattern_0_1 lng (Suc 0)) = lng

你看到归纳假设只适用于零，但你需要它。

修复很简单：

apply(induction lng arbitrary: item)

这指示归纳法首先概括变量item。然后，归纳假设变得更广泛适用。

证明生成列表的属性

Proving properties of generated lists

isabelle