0

这个问题是对以下问题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

哪个Isabelle可以通过归纳自动证明那么归纳步骤就是证明

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)"

而不是引理1，证明成功。它似乎能够在两个方向上使用 Lemma2，但不能使用我上面定义的 Lemma1。有谁知道为什么？我觉得我在某个地方忽略了一些明显的东西..

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

4

1 回答 1

1

引理 2 不是双向使用的，正如您在尝试使用以下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
于 2016-04-21T10:12:38.247 回答