证明 add, Take 2 的交换律

Question

此问题是以下问题 isabelle proving commutativity for add 的后续问题，我的后续问题太长，无法发表评论。所述问题是显示 add 函数的交换性，定义如下：

fun add :: "nat ⇒ nat ⇒ nat" where
  "add 0 n = n" |
  "add (Suc m) n = Suc(add m n)"

正在尝试

theorem "add m n = add n m"
apply(induct_tac m)
apply(auto)

因为缺少引理而卡住（在归纳情况下）。我对这个问题很好奇，并且正在探索证明它的替代方法（尽管效率较低）。假设我们定义了引理

lemma Lemma1 [simp]: "add n (Suc 0) = Suc n

哪个伊莎贝尔可以通过归纳法自动证明那么归纳步骤就是证明

Suc (add k m) = add m (Suc k)

我们可以如下手动完成

   Suc (add k m)
=  Suc (add m k) by the IH
=  add (add m k) (Suc 0) by Lemma1 <--
=  add m (add k (Suc 0)) by associativity (already proved)
=  add m (Suc k) by the Lemma1 -->

但是，Isabelle 无法证明这一点，简化器似乎卡在了第二行。然而，使用更明显的

lemma Lemma2 [simp]: "add m (Suc n) = Suc (add m n)"

代替Lemma1，证明成功。它似乎可以在两个方向上使用 Lemma2 而不是我上面定义的 Lemma1。有谁知道为什么？我觉得我在某处忽略了一些明显的东西..

备注：我意识到简化器实际上只在一个方向上应用定义等，但使用启发式方法尝试将等式两边简化为相同的项

Answer 1

Lemma2 没有在两个方向上使用，正如您在尝试使用 subst 个步骤手动进行证明时所看到的那样：

theorem commutativity2: 
"add n m = add m n"
apply (induct n)
apply (subst Lemma0)
apply (subst add.simps(1))
apply (rule refl)

(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (Suc n) *)
apply (subst add.simps(2))
(* ⋀n. add n m = add m n ⟹ Suc (add n m) = add m (Suc n) *)
apply (erule ssubst)
(* ⋀n. Suc (add m n) = add m (Suc n) *)
apply (subst Lemma2)
(* ⋀n. Suc (add m n) = Suc (add m n) *)
apply (rule refl)
done

它只是在目标方程的右边工作，但仍然从左到右使用 Lemma1。

如果您想像手动证明那样进行证明，您也可以在 Isabelle 中轻松完成：

theorem commutativity: 
"add m n = add n m"
proof (induct m)
  show "add 0 n = add n 0" using Lemma0 by simp
next case (Suc k)
  have      "add (Suc k) n 
                 = Suc (add k n)" by simp
  also have "... = Suc (add n k)" using Suc.hyps by simp
  also have "... = add (add n k) (Suc 0)" using Lemma1 by simp
  also have "... = add n (add k (Suc 0))" using associativity by simp
  also have "... = add n (Suc k)" using Lemma1 by simp
  finally show ?case .
qed

编辑：

说明为什么这不适用于引理 1 的手动证明：在第一次重写引理 1 时必须从右到左使用（使用 [symmetric]）。

theorem commutativity3: 
"add n m = add m n"
apply (induct n)
apply (subst Lemma0)
apply (subst add.simps(1))
apply (rule refl)

(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (Suc n) *)
apply (subst Lemma1[symmetric]) back
(*  ⋀n. add n m = add m n ⟹ add (Suc n) m = add m (add n (Suc 0)) *)
apply (subst associativity)
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = add (add m n) (Suc 0) *)
apply (subst Lemma1)
(* ⋀n. add n m = add m n ⟹ add (Suc n) m = Suc (add m n) *)
apply (erule subst)
(* ⋀n. add (Suc n) m = Suc (add n m) *)
apply (subst add.simps(2))
(* ⋀n. Suc (add n m) = Suc (add n m) *)
apply (rule refl)
done

证明 add, Take 2 的交换律

Proving commutativity of add, Take 2

logic

proof

isabelle

theorem