*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 13:59:10 +0200*In-reply-to*: <51E9235A.5050403@gmail.com>*References*: <6c9a-51e80c80-1-5d76dd8@90856565> <51E9235A.5050403@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

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

- 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