Proving commutativity of add, Take 2

Question

This question is a follow up to the following question isabelle proving commutativity for add, my followup was too long to be a comment. The problem as stated was to show the commutativity of the add function defined as follows:

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

Trying

theorem "add m n = add n m"
apply(induct_tac m)
apply(auto)

gets stuck (on the inductive case) because of a missing lemma. I got curious about this problem, and was exploring alternative (albeit less efficient) way of proving it. Suppose we defined the Lemma

lemma Lemma1 [simp]: "add n (Suc 0) = Suc n

which Isabelle can automatically prove by induction Then the inductive step is to prove

Suc (add k m) = add m (Suc k)

which we could do by hand as follows

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

However, Isabelle is unable to prove this, and it appears the simplifier is stuck at the 2nd line. However, using the more obvious

lemma Lemma2 [simp]: "add m (Suc n) = Suc (add m n)"

instead of Lemma1, the proof succeeds. It seems to be able to use Lemma2 in both directions but not the Lemma1 I defined above. Does anyone know why? I feel like I am overlooking something obvious somewhere..

Remarks: I realize the simplifier actually only applies definitions etc in one direction but uses heuristics to try and reduce both sides of the equation to the same term

To make it easier to help you without firing up Isabelle, can you also paste the proof state a the point where proofs are failing, e.g. where you say “gets stuck because of a missing lemma”? — Joachim Breitner

Peter Zeller Peter Zeller · Accepted Answer · 2016-04-21T10:12:38

Lemma2 is not used in both directions, as you can see when you try to do the proof manually with subst steps:

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

It is just working on the right hand side of the goal-equation, but still using Lemma1 from left to right.

If you want to do the proof as in your manual proof you can also easily do it in 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

EDIT:

A manual proof showing why this does not work with Lemma1: In the first rewrite Lemma 1 has to be used from right to left (using [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

Proving commutativity of add, Take 2

1 Answers