isabelle证明了加性的可交换性 [英] isabelle proving commutativity for add

问题描述

我正在尝试证明Isabelle/HOL中自定义add函数的可交换性.我设法证明了关联性，但我坚持这一点.

Im trying to prove commutativity in Isabelle/HOL for a self-defined add function. I managed to prove associativity but I'm stuck on this.

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​​:

After applying auto I'm left with just subgoal 3:

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

我不是在寻找答案，而是向正确的方向推.这些是《混凝土水泥学》一书中的练习.

Im not so much looking for an answer, as a push in the right direction. These are exercises from a book called Concrete Sementics.

推荐答案

我建议使证明尽可能地模块化(即证明中间引理，这将在以后帮助解决可交换性证明).为此，在应用全自动(如您的apply (auto))之前，对induct引入的子目标进行冥想通常会更有益.

I would suggest to make the proof as modular as possible (i.e., prove intermediate lemmas that will later help to solve the commutativity proof). To this end it is often more informative to meditate on the subgoals introduced by induct, before applyng full automation (like your 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. 您这样做是您的主要证明的一部分.我会说它增加了 可读性来证明以下单独的引理

1. Using the definition of add we will only be able to simplify the left-hand side, i.e., add 0 m = m. Then the question remains how to prove add m 0 = m. You did this as part of your main proof. I would argue that it increases readability to proof the following separate lemma

lemma add_0 [simp]:
  "add m 0 = m"
  by (induct m) simp_all

，然后使用[simp]将其添加到自动化工具(例如simp和auto)中.在此刻 第一个子目标可以通过simp解决，只有第二个子目标仍然存在.

and add it to the automated tools (like simp and auto) using [simp]. At this point the first subgoal can be solved by simp and only the second subgoal remains.

在应用了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)以便继续.

After applying the definition of add as well as the induction hypothesis (add k m = add m k) we will have to prove Suc (add m k) = add m (Suc k). This looks very similar to the second equation of the original definition of add, only with swapped arguments. (From that perspective, what we had to prove for the first subgoal corresponded to the first equation in the definition of add with swapped arguments.) Now, I would suggest to try to prove the general lemma add m (Suc n) = Suc (add m n) in order to proceed.

这篇关于isabelle证明了加性的可交换性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！