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



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.