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 # )"
lemma "length (rev xs) = length xs"
(* apply(simp add: length_suc)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and