*To*: Wilmer RICCIOTTI <Wilmer.Ricciotti at irit.fr>, Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Unable to prove easy existential "directly"*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Fri, 19 Jul 2013 10:34:05 -0700*Cc*: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1307191628140.15169@macbroy21.informatik.tu-muenchen.de>*References*: <6c9a-51e80c80-1-5d76dd8@90856565> <alpine.LNX.2.00.1307191628140.15169@macbroy21.informatik.tu-muenchen.de>

On Fri, Jul 19, 2013 at 7:48 AM, Makarius <makarius at sketis.net> wrote: > On Thu, 18 Jul 2013, Wilmer RICCIOTTI wrote: >> Unsurprisingly, this proof doesn't pose any challenge at all. However I >> can slightly complicate the formula by means of a definition, and this >> obvious proof technique won't work any more. Specifically, I define >> >> definition bijection :: "('a ⇒ 'b) ⇒ bool" where >> "bijection f = (∀y::'b.∃!x::'a. y = f x)" >> >> and then the same proof as before, with bijection in place of a generic P, >> fails: >> >> lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))" >> proof >> assume hg : "bijection (g::'a ⇒ 'b)" >> thus "∃f.(bijection f)".. >> qed > > > Here you try to make an existential introduction of a thing of function > type. Due to the way Larry implemented HO unification some decades ago, > this does not work in the compositional manner required by Isar. So here is > my slightly awkward proof (again in somewhat standard form): > > > definition bijection :: "('a ⇒ 'b) ⇒ bool" > where "bijection f ⟷ (∀y. ∃!x. y = f x)" > > lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)" > proof > assume "bijection g" > then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g]) > qed Hi Wilmer, Makarius has precisely identified the problem: Unification has trouble when proving the existence of something with a function type. I have come across this exact problem several times before; below is the workaround that I have used. lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)" proof assume "bijection g" then show "∃f::'a ⇒ 'b. bijection f" by - (rule exI) qed The "-" method serves to turn "bijection g" from a chained fact into an ordinary assumption in the proof goal; this then affects how the "rule" method does unification. (Writing "by - rule" will also work.) Grep the Isabelle sources for "by - (rule exI)" to see all the places I've had to use this trick: Some examples involve proving countability of types, showing goals of the form "∃f::'a ⇒ nat. inj f". Other examples occur in HOLCF when proving instances of class "bifinite", which asserts the existence of a function with certain properties. The same trick used to be necessary for proving things of the form "∃A::'a set. P A", during the period when "'a set" was an abbreviation for "'a => bool". This is no longer the case, but you can still find one or two leftover examples of "by - (rule exI)" in Multivariate_Analysis. - Brian

**Follow-Ups**:**Re: [isabelle] Unable to prove easy existential "directly"***From:*Makarius

**References**:**[isabelle] Unable to prove easy existential "directly"***From:*Wilmer RICCIOTTI

**Re: [isabelle] Unable to prove easy existential "directly"***From:*Makarius

- Previous by Date: Re: [isabelle] Unable to prove easy existential "directly"
- Next by Date: Re: [isabelle] Unable to prove easy existential "directly"
- Previous by Thread: Re: [isabelle] Unable to prove easy existential "directly"
- Next by Thread: Re: [isabelle] Unable to prove easy existential "directly"
- Cl-isabelle-users July 2013 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