isabelle证明add的交换性

Question

我试图证明一个自定义add函数在Isabelle/HOL中的交换性。我设法证明了联想，但我还是坚持住了。

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)

申请汽车后，我只剩下次级目标3：

3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

编辑:我与其说是在寻找答案，不如说是在朝正确的方向前进。这是一本叫做“具体符号学”的书中的练习。

Answer 1

我建议尽可能地使证明成为模(即证明中间引理，这将有助于解决交换性证明)。为此，在应用程序完全自动化(如您的induct )之前，先考虑一下induct引入的子目标，这通常会提供更多的信息。

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。你这样做是你的主要证据之一。我认为它增加了证明下列独立引理的可读性 引理add_0 simp："add m 0= m“(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)，以便继续。

Answer 2

我在对克里斯回答的评论中回答了雨猫的问题：“伊莎贝尔是如何证明的”。给出了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'

- we assume `add (add k' m) z = add k' (add m z)`.
- we have to prove `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))

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

在具有这一详细程度的会计准则中，这将提供：

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所取代。