isabelle证明了交换性

Question

我试图证明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后,我只剩下subgoal 3:

3. ?k. add k m = add m k ?
     add (Suc k) m = add m (Suc k)

编辑:我不是在寻找答案,而是朝着正确的方向努力.这些是一本名为Concrete Sementics的书的练习.

Answer 1

我建议尽可能使证明模块化(即证明中间的引理,以后将有助于解决交换性证明).为此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)以便继续进行.