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

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 MHonArc.