# Re: [isabelle] Beginner question: Symmetry of equality in proofs?

On 13.12.2010 05:58, Jason Dagit wrote:

lemma length_suc: "Suc (length list) = length (list ++ a # [])"
apply(induct_tac list)
apply(auto)
done

[...]

lemma "length (rev xs) = length xs"
apply(induct_tac xs)
apply(simp, simp)
oops
done *)
\end{code}

What I noticed was that between the last two lemmas, the direction of the
equality makes a huge difference when proving the lemma.  The lemma"length
xs = length (rev xs)" is easy to prove but lemma "length (rev xs) =length
xs" is much harder to prove (for me at least).



You don't need to prove this for yourself. If you name the second lemma e.g. rev_length, then the third lemma is just rev_length[symmetric].


I would expect "=" to be symmetric.  Is that not the case?  Is there
something else going on here?



The simplifier applies equalities only from left to right. In your case the problem is the formulation of length_suc: The right hand side contains a variable which does not occur on the left hand side, so the simplifier does not apply this rule, as it does not know how to instantiate this variable.

A proof easily succeeds by