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



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










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