logic - isabelle 证明 add 的交换性

Question

我试图在 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 的书中的练习。

Answer 1

我建议使证明尽可能模块化(即，证明中间引理，稍后将有助于解决交换性证明)。为此，冥想 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)为了继续。