我试图在 Isabelle/HOL 中证明自定义 add
的交换性功能。我设法证明了关联性,但我坚持这一点。add
的定义:
fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"
结合性证明:
lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done
交换性证明:
theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)
我得到以下目标:
goal (3 subgoals):
1. add 0 0 = add 0 0
2. ⋀m. add 0 m = add m 0 ⟹
add 0 (Suc m) = add (Suc m) 0
3. ⋀k. add k m = add m k ⟹
add (Suc k) m = add m (Suc k)
应用 auto 后,我只剩下子目标 3:
3. ⋀k. add k m = add m k ⟹
add (Suc k) m = add m (Suc k)
编辑:我不是在寻找答案,而是朝着正确的方向前进。这些是来自名为 Concrete Sementics 的书中的练习。
最佳答案
我建议使证明尽可能模块化(即,证明中间引理,稍后将有助于解决交换性证明)。为此,冥想 induct
引入的子目标通常会提供更多信息。 ,在应用完全自动化之前(如您的 apply (auto)
)。
lemma add_comm:
"add k m = add m k"
apply (induct k)
此时的子目标是:
goal (2 subgoals):
1. add 0 m = add m 0
2. ⋀k. add k m = add m k ⟹ add (Suc k) m = add m (Suc k)
让我们分别看看它们。
add
的定义我们只能简化左边,即
add 0 m = m
.那么问题仍然是如何证明add m 0 = m
.您将其作为主要证明的一部分。我认为它会增加
证明以下单独引理的可读性
lemma add_0 [simp]:
"add m 0 = m"
by (induct m) simp_all
并使用
simp
将其添加到自动化工具(如 auto
和 [simp]
) .在此刻第一个子目标可以通过
simp
解决并且只剩下第二个子目标。 add
的定义后以及归纳假设 (add k m = add m k
) 我们必须证明 Suc (add m k) = add m (Suc k)
.这看起来与 add
的原始定义的第二个方程非常相似。 ,只有交换了参数。 (从这个角度来看,我们必须为第一个子目标证明的内容对应于 add
的定义中的第一个等式,并交换了参数。)现在,我建议尝试证明一般引理 add m (Suc n) = Suc (add m n)
为了继续。 关于logic - isabelle 证明 add 的交换性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/24815932/