*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Tue, 12 Jan 2016 08:05:10 +0000*Accept-language*: de-DE, de-AT, en-US*Cc*: "stark at cs.stonybrook.edu" <stark at cs.stonybrook.edu>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5694A950.4060009@inf.ethz.ch>*References*: <569414EE.60800@starkeffect.com> <5694A950.4060009@inf.ethz.ch>*Thread-index*: AQHRTQtrF8NHkBtWSEuqaXvlxcK7D573dQ8A*Thread-topic*: [isabelle] Failure to prove a simple transitivity -- what could be the cause?

Dear Eugene, another potential failure reason: is ?Y a subexpression of ?X ? Then it might be the case that the â?Y = ?Zâ also modifies the ?X. To prevent this you can try def X = ?X def Z = ?Z have âX = ?Yâ unfolding X_def using A by auto also have â?Y = Zâ unfolding Z_def using 2 6 by auto finally have â?X = ?Zâ unfolding X_def Z_def . Cheers, RenÃ > Am 12.01.2016 um 08:20 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>: > > Dear Eugene, > > Another cause might be eta-expansion which happens occasionally during resolution and is not shown in the proof state by default (attribute eta_contract). When this happens, the simplifier can go into very different directions. Have you tried the following? > > 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:*Eugene W. Stark

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

**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Andreas Lochbihler

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