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



On Sun, Dec 12, 2010 at 11:10 PM, Lars Noschinski <noschinl at in.tum.de> wrote:
> On 13.12.2010 05:58, Jason Dagit wrote:
>> 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).
[...]
>> 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.

Another thing to remember about the simplifier: It uses the
assumptions of the current subgoal as rewrite rules. And as always, it
only uses equalities left-to-right.

So in your proof script:

lemma "length (rev xs) = length xs"
apply(induct_tac xs)
apply (simp, simp)

you now have the following subgoal:

goal (1 subgoal):
 1. ⋀a list.
       length (rev list) = length list ⟹
       length (rev list ++ a # []) = Suc (length list)

Here the simplifier would replace any occurrences of "length (rev
list)" in the conclusion with "length list", except that "length (rev
list)" does not appear in the conclusion, so the inductive hypothesis
does not get used by the simplifier.

- Brian





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