isabelle proving commutativity for add

Question

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.

Baluchi

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

Junie

Thanks that helped! Just a question, I don't think I really understand how Isabelle proves. I know how the induction hypothesis works, but if you asked me to prove this manually I wouldn't be able to. Are there any good resources (books/online lessons) for learning this branch of mathematics? What would you call this branch of mathematics anyways. – Baluchi

If you understand induction, the remaining parts are solved by the simplifier, which rewrites terms according to the equational lemmas contained in the so-called simpset. A lemma is added to the simpset by 'primrec' and 'fun' (the equations of the definition) and manually via the '[simp]' attribute. The rewriting is oriented, always from left to right, so the right hand side should be 'simpler' than the left hand side and should avoid cycles. – Yokefellow

I added more details in an answer. – Yokefellow

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

Yokefellow