Re: [isabelle] Unable to prove easy existential "directly"
On Fri, Jul 19, 2013 at 7:48 AM, Makarius <makarius at sketis.net> wrote:
> On Thu, 18 Jul 2013, Wilmer RICCIOTTI wrote:
>> 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,
>> lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
>> assume hg : "bijection (g::'a ⇒ 'b)"
>> thus "∃f.(bijection f)"..
> Here you try to make an existential introduction of a thing of function
> type. Due to the way Larry implemented HO unification some decades ago,
> this does not work in the compositional manner required by Isar. So here is
> my slightly awkward proof (again in somewhat standard form):
> definition bijection :: "('a ⇒ 'b) ⇒ bool"
> where "bijection f ⟷ (∀y. ∃!x. y = f x)"
> lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
> assume "bijection g"
> then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g])
Makarius has precisely identified the problem: Unification has trouble
when proving the existence of something with a function type. I have
come across this exact problem several times before; below is the
workaround that I have used.
lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by - (rule exI)
The "-" method serves to turn "bijection g" from a chained fact into
an ordinary assumption in the proof goal; this then affects how the
"rule" method does unification. (Writing "by - rule" will also work.)
Grep the Isabelle sources for "by - (rule exI)" to see all the places
I've had to use this trick: Some examples involve proving countability
of types, showing goals of the form "∃f::'a ⇒ nat. inj f". Other
examples occur in HOLCF when proving instances of class "bifinite",
which asserts the existence of a function with certain properties.
The same trick used to be necessary for proving things of the form
"∃A::'a set. P A", during the period when "'a set" was an abbreviation
for "'a => bool". This is no longer the case, but you can still find
one or two leftover examples of "by - (rule exI)" in
This archive was generated by a fusion of
Pipermail (Mailman edition) and