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,
>> fails:
>>
>>  lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
>>  proof
>>    assume hg : "bijection (g::'a ⇒ 'b)"
>>    thus "∃f.(bijection f)"..
>>  qed
>
>
> 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)"
> proof
>   assume "bijection g"
>   then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g])
> qed

Hi Wilmer,

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)"
proof
   assume "bijection g"
   then show "∃f::'a ⇒ 'b. bijection f" by - (rule exI)
qed

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

- Brian




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