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



Thanks for the suggestions.  I've tried those, but they don't help.
Here is an abstracted version of the situation, which tries to get
rid of some of the simplifier issues by introducing definitions.
This one happens to succeed, but not in the way I would expect
(the proof shown was generated by sledgehammer).  I don't really
understand why a trivial proof (not referencing X_def and Y_def)
is not possible. The types and the fact that the expressions don't
all have the same sets of free variables might be a clue.  Perhaps it
is something to do with the way sum types are implemented in the system.

theory Barf
imports Main
begin

    definition XXX :: "'a â 'b â 'a â 'b â 'a + 'b â 'c + 'b"
    where "XXX f g x y = (Îz :: 'a + 'b. Inr y)"

    definition YYY :: "'a => 'b => 'a => 'a => 'b => 'b => 'a + 'b => 'a + 'b"
    where "YYY f g x x' y y' = id"

    definition ZZZ :: "'a â 'b â 'a â 'b â 'b â 'a + 'b â 'd + 'b"
    where "ZZZ f g x y y' = (Îz :: 'a + 'b. Inr y)"

    lemma
    assumes "XXX f g x y = YYY f g x x' y y'"
    and "YYY f g x x' y y' = ZZZ f g x y y'"
    shows "XXX f g x y = ZZZ f g x y y'"
    proof -
      have "XXX f g x y = id"
        by (simp add: YYY_def assms(1))
      then show ?thesis
        using XXX_def id_apply sum.simps(4) by (metis (full_types))
    qed

end

The same approach with definitions has not yet allowed me to prove
the original example, though, because as you can see, the proof that
does succeed is not a straight application of transitivity, but rather
uses special properties of the expressions involved.  Amusingly, when
I do try that approach on the original example, rendered as shown:

          have XY: "XXX f g x y = YYY f g x x' y y'"
            using A by (auto simp add: XXX_def YYY_def)
          moreover have YZ: "YYY f g x x' y y' = ZZZ f g x y y'"
            using 2 6 by (auto simp add: YYY_def ZZZ_def)
          ultimately have "XXX f g x y = ZZZ f g x y y'"
            using HOL.trans [of "XXX f g x y" "YYY f g x x' y y'" "ZZZ f g x y y'"]

the proof state display shows:

proof (prove)
using this:
    XXX f g x y = YYY f g x x' y y'
    YYY f g x x' y y' = ZZZ f g x y y'
    XXX f g x y = YYY f g x x' y y' â
    YYY f g x x' y y' = ZZZ f g x y y' â XXX f g x y = ZZZ f g x y y'

goal (1 subgoal):
 1. XXX f g x y = ZZZ f g x y y'


Have I maybe missed some subtle point about HOL?

						- Gene Stark



On 01/12/2016 03:05 AM, Thiemann, Rene wrote:
> 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.