Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
Something to do with mismatching types or type classes I'd expect.
On 12 January 2016 at 07:47, Eugene W. Stark <isabelle-users at starkeffect.com
> 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