*To*: <stark at cs.stonybrook.edu>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 12 Jan 2016 08:20:48 +0100*In-reply-to*: <569414EE.60800@starkeffect.com>*References*: <569414EE.60800@starkeffect.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Eugene,

have "?X = ?Y" using A by auto also have "?Y = ?Z" using 2 6 by auto finally show "?X = ?Z" . Best, Andreas On 11/01/16 21:47, Eugene W. Stark 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

**Follow-Ups**:**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Thiemann, Rene

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

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