Re: [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
>> 
>> 
>> 
> 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.