*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Tue, 12 Jan 2016 05:05:34 -0500*In-reply-to*: <141FC5DA-1BD2-4EB7-9A00-77574F24EBD3@exchange.uibk.ac.at>*References*: <569414EE.60800@starkeffect.com> <5694A950.4060009@inf.ethz.ch> <141FC5DA-1BD2-4EB7-9A00-77574F24EBD3@exchange.uibk.ac.at>*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.4.0

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

**Follow-Ups**:**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Andreas Lochbihler

**References**:**[isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Eugene W. Stark

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

**Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?***From:*Thiemann, Rene

- Previous by Date: Re: [isabelle] lift_bnf Subscript exception
- Next by Date: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Previous by Thread: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Next by Thread: Re: [isabelle] Failure to prove a simple transitivity -- what could be the cause?
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list