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



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.