*To*: Jason Dagit <dagitj at gmail.com>*Subject*: Re: [isabelle] Beginner question: Symmetry of equality in proofs?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 13 Dec 2010 09:05:12 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTimNW5ZsmUnqtpNhnY40UL5zDCzAywkzFUJwBofZ@mail.gmail.com>*References*: <AANLkTimNW5ZsmUnqtpNhnY40UL5zDCzAywkzFUJwBofZ@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

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

**References**:**[isabelle] Beginner question: Symmetry of equality in proofs?***From:*Jason Dagit

- Previous by Date: [isabelle] PhD position in Computational Logic at the University of Innsbruck
- Next by Date: [isabelle] Post-doctoral position in coalgebraic logic at DFKI Bremen
- Previous by Thread: Re: [isabelle] Beginner question: Symmetry of equality in proofs?
- Next by Thread: [isabelle] PhD position in Computational Logic at the University of Innsbruck
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list