4

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

4

2 回答 2

8

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

让我们分别看看它们。

  1. 使用 的定义，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，只剩下第二个子目标。

  2. 在应用 的定义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)以便继续。

于 2014-07-18T11:39:59.930 回答
3

我在评论克里斯的回答时回答了 RainyCats 的问题：“伊莎贝尔如何证明”。我add在 Isar 中手动和一步一步地详细证明了关联性。

通过对 k 的归纳，手动进行关联性：

  • 对于k=0我们必须证明add (add 0 m) z = add 0 (add m z).

    我们用 的定义重写add：

    • add (add 0 m) z⇢add m z
    • add 0 (add m z)⇢add m z

    然后目标由 的自反性证明=。

  • 对于k=Suc k'

    • 我们假设add (add k' m) z = add k' (add m z)。
    • 我们必须证明add (add (Suc k') m) z = add (Suc k') (add m z)。

    我们用 的定义重写add：

    • add (add (Suc k') m) z⇢ add (Suc (add k' m)) z⇢Suc (add (add k' m) z)
    • add (Suc k') (add m z)⇢Suc (add k' (add m z))

    通过归纳假设：Suc (add (add k' m) z)⇢Suc (add k' (add m z))

    然后目标由 的反身性证明=。

在具有这种详细程度的 Isar 中，这将给出：

lemma add_Associative: "add(add k m) z = add k (add m z)"
proof (induction k)
  case 0
    have "add (add 0 m) z = add m z" by (subst add.simps, intro refl)
    moreover have "add 0 (add m z) = add m z" by (subst add.simps, intro refl)
    ultimately show ?case by (elim ssubst, intro refl)
next
  case (Suc k')
    have "add (add (Suc k') m) z = add (Suc (add k' m)) z" by (subst add.simps, intro refl)
    also have "… = Suc (add (add k' m) z)" by (subst add.simps, intro refl)
    also have "… = Suc (add k' (add m z))" by (subst Suc, intro refl)
    moreover have "add (Suc k') (add m z) = Suc (add k' (add m z))" by (subst add.simps, intro refl)
    ultimately show ?case by (elim ssubst, intro refl)
qed

在哪里我已经使最小的步骤成为可能，并且所有的by ...都可以替换为by simp.

于 2014-07-19T21:25:49.233 回答