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