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
(* apply(simp add: length_suc)
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

  apply(simp add: length_suc[symmetric])

but I suggest you change the definition of length suc. As a rule of thumb, rules to be used by the simplifier should be "simpler" on the right hand side than on the left hand side.

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.