*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Unable to prove easy existential "directly"*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 19 Jul 2013 14:41:55 +0200*In-reply-to*: <51E931D9.3070806@gmail.com>*References*: <6c9a-51e80c80-1-5d76dd8@90856565> <51E9235A.5050403@gmail.com> <51E92A0E.1000005@in.tum.de> <51E931D9.3070806@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

Oh my, I must have missed that. Yes, in these cases, it is best to annotate variables in binders. If one does not know where the problem comes from in these cases, it can also be a good idea to enable the unification trace, which shows exactly why a role could not be applied; in this case, probably a clash between the free type variables. But be that as it may, even when one does annotate the bound variable, ".." still does not work, which then brings us back to what I said in my first reply. :) Cheers, Manuel On 07/19/2013 02:32 PM, Christian Sternagel wrote: > Dear Manuel, > > as far as I see "bijjection" is not a free variable, it was defined by > Wilmer. But you are write that my suggestion does not solve to > problem. Rather he would have to combine our two mails ;) > > cheers > > chris > > On 07/19/2013 08:59 PM, Manuel Eberl wrote: >> Hallo Christian, >> >> Are you quite sure about this? On my system, all occurences of "f" and >> "g" are displayed as having type "'a ⇒ 'b". I don't see how it could be >> any other way, seeing as bijection is a free variable and the assertion >> forces "bijection" to have the type "('a ⇒ 'b) ⇒ bool", which in turn >> forces the bound f in the "thus statement" to be of type "'a ⇒ 'b" as >> well. >> >> Cheers, >> Manuel >> >> On 07/19/2013 01:30 PM, Christian Sternagel wrote: >>> Dear Wilmer, >>> >>> I often run into the same problem ;) which is that things are too >>> polymorphic. >>> >>>> lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ >>>> 'b)))" >>>> proof >>>> assume hg : "bijection (g::'a ⇒ 'b)" >>>> thus "∃f.(bijection f)".. >>> In this line, check the type of "f" (e.g., Ctrl+hover in jEdit) which >>> outputs: >>> >>> bound "f" >>> bound variable >>> :: 'c ⇒ 'd >>> >>> i.e., the types of "f" and "g" do not match. (Try to give f an >>> explicit type in the binder.) >>> >>> hope this helps, >>> >>> chris >>> >>> On 07/19/2013 12:41 AM, Wilmer RICCIOTTI wrote: >>>> Hi all, >>>> >>>> as a beginner in the use of Isabelle/Isar, I have every day numerous >>>> clashes with the Isar way of proving theorems. The strangest one to >>>> date is related to proving an existentially quantified formula when >>>> you have the same formula with an explicit witness as a hypothesis. >>>> That is to say, something similar to this lemma: >>>> >>>> lemma fie : "P a ⟶ (∃b.(P b))" >>>> proof >>>> assume ha : "P a" >>>> thus "∃b.(P b)".. >>>> qed >>>> >>>> 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 >>>> >>>> replacing the implicit ".." with an explicit "proof (rule exI)" fails >>>> similarly, leaving me quite puzzled. >>>> (Un)Interestingly, since "foo" is an instance of "fie", we can easily >>>> prove it using "by (rule fie)" and nothing else. However this feels >>>> more like a trick to make things work than a solution. >>>> >>>> What am I doing wrong? >>>> >>>> Best, >>>> -- >>>> Wilmer Ricciotti >>>> >>> >>> >> >> > >

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

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

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

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

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

- 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