isabelle proving commutativity for 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.

The definition of add:

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

The proof of associativity:

lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done

The proof of commutativity:

theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)

I get the following goals:

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)

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)

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

回答1:

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)

At this point the subgoals are:

 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)

Lets look at them separately.

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
   

   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.

2. 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.

回答2:

I answer the RainyCats's question in a comment of the chris's answer: "How Isabelle proves". I give a detailed proof of the associativity of add both manually and step by step in Isar.

Manually for associativity, by induction on k:

• for k = 0 we have to prove add (add 0 m) z = add 0 (add m z).

  We rewrite with definition of add:

  • add (add 0 m) z ⇢ add m z
  • add 0 (add m z) ⇢ add m z

  Then the goal is proven by reflexivity of =.

• for 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).

  We rewrite with definition of 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))

  By induction hypothesis: Suc (add (add k' m) z) ⇢ Suc (add k' (add m z))

  And then then goal is proven by reflexivity of =.

In Isar with this level of detail, this would give:

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

where I have made the smallest steps possible and where all the by ... could be replaced by by simp.