*To*: stark at cs.stonybrook.edu*Subject*: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Tue, 12 Jan 2016 13:43:05 +1100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <569414EE.60800@starkeffect.com>*References*: <569414EE.60800@starkeffect.com>*Sender*: ramana.kumar at gmail.com

Something to do with mismatching types or type classes I'd expect. On 12 January 2016 at 07:47, Eugene W. Stark <isabelle-users at starkeffect.com > wrote: > I am stumped. I have a proof block of the following form: > > proof - > ...a bunch of stuff that proves A "2" and "6"... > > let ?X = "...a modestly sized expression..." > let ?Y = "...another expression of similar size..." > let ?Z = "...yet another expression similar to the first..." > > have "?X = ?Y" using A by auto > also have "?Y = ?Z" using 2 6 by auto > finally show "?X = ?Z" by auto > qed > > The proofs of "?X = ?Y" and "?Y = ?Z" succeed. > > The proof of "?X = ?Z" does not (the final "auto" is underlined > with a red squiggle and the output window says "Failed to apply > initial proof method", though the "using this" and "goal" > expressions are identical). > > I introduced the "lets" after encountering the original problem, > to make sure that there wasn't some subtle difference in the > expressions or that they were being interpreted in different ways > if they occurred multiple times. > > The "show" is in blue, indicating that it matches the statement > to be proved in the current block. It doesn't matter if I change > "show" to "have", the proof still fails. It also doesn't matter > if I change "have ... also have ... finally" to > "have ... moreover have ... ultimately show". > I also tried rewriting it as: > > have XY: "?X = ?Y" using A by auto > have YZ: "?Y = ?Z" using 2 6 by auto > thus "?X = ?Z" by (metis XY YZ) > > and metis does not terminate. > > Does anyone have any idea what could cause this? I can't really > distill the example better because it's embedded in thousands of > lines of context. As I indicated, I tried ways of rewriting it > that seemed to me like they might work around the problem, to no > avail. > > - Gene Stark > > > >

**References**:**[isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] lift_bnf Subscript exception
- Next by Date: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Previous by Thread: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Next by Thread: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Cl-isabelle-users January 2016 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