Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
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 .
> 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" .
> 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
>> 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
>> - Gene Stark
This archive was generated by a fusion of
Pipermail (Mailman edition) and