Algebraic simplifications in Isabelle

Question

I have been playing around with basic examples of proofs in Isabelle.

Consider the following simple proof:

lemma
    fixes n::nat
    shows "n*(n+1) = n^2 + n"
    by simp

It seems to me that a powerful proof assistant like Isabelle should be able to prove this lemma without much guidance. However, I was surprised to find out that Isabelle actually fails at applying the rule simp here (I also tried other "generic" rules like simp_all, auto, force, blast but the result is the same).

If I replace the last line by the following, then it works out:

by (simp add: power2_eq_square)

My concern is that I feel like I shouldn't have had to tell the system about the specific rule power2_eq_square to complete this proof.

Playing around with similar trivial examples, I found that simp is able to prove

n*(n+2)=n*n+n*2

but fails with

n*(n+3)=n*n+n*3

The last example is proven

by (simp add: distrib_left)

It is a complete mystery to me why I need to specify distrib_left in that second example, but not in the first (why is that?).

I have given these examples not for their own sake, but mainly to illustrate my main question:

Is there a way to automate the verification of routine algebraic identities such as the above in Isabelle? If there isn't, then why not? What are the technical obstacles?

Answer 1

Daily proof work indeed often stumbles over »routine algebraic identities«; but after some practical experience one usually develops some intuition how to solve such problems effectively. A pattern I have developed over the years, by example:

context semidom
begin

lemma "a * (b ^ 2 + c) + 2 = a * b * b + c * a + 2"

A typical explorative proof starts with

  apply auto

Then associativity and commutative are considered also

  apply (auto simp add: ac_simps)

Then more algebaic normalizing rules are applied

  apply (auto simp add: algebra_simps)

The last gap is then easily filled by sledgehammer

  apply (simp add: power2_eq_square)

After that, the proof can be compactified

  by (simp add: algebra_simps power2_eq_square)

Answer 2

The lemma

lemma power2_eq_square: "a^2 = a * a"

is not a good rewrite rule in general, as it will easily blow up the size of terms. So it is expected that a term rewriting based automation like simp will not apply this without you telling it to.

What you want is some sort of proof search, and Isabelle provides that: After writing your lemma, you can invoke the sledgehammer tool, and it will readily and quickly find the proof for you:

Sledgehammering... 
Proof found... 
"z3": Try this: by (simp add: power2_eq_square) (1 ms) 
"cvc4": Try this: by (simp add: power2_eq_square) (5 ms)