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