Re: [isabelle] Unable to prove easy existential "directly"
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.
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
> > 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
> 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,
> 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))"
>> assume ha : "P a"
>> thus "∃b.(P b)"..
>> 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)))"
>> assume hg : "bijection (g::'a ⇒ 'b)"
>> thus "∃f.(bijection f)"..
>> 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?
>> Wilmer Ricciotti
This archive was generated by a fusion of
Pipermail (Mailman edition) and