Re: [isabelle] Strange eta-expansion on induction



I have complained at length about this issue before. See this thread
from August of last year:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00080.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00089.html

To summarize: In my opinion, having a proof kernel that does
eta-expansion willy-nilly is an embarrassment; I also have similar
feelings about the "eta-contract" option in the pretty-printer, which
our eta-expanding kernel makes necessary.

Unfortunately, fixing the problem properly would require modifying the
unification code in the kernel, which hardly anybody understands. It
would be hard to get anyone to trust a modified version of it.

As a workaround, perhaps someone could write a wrapper around the
induct method that would do its own unification outside the kernel,
and pre-instantiate the induction rule before applying it. This would
avoid using the kernel's unification code, thus preventing the
eta-expansion.

- Brian

On Thu, Mar 1, 2012 at 7:56 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> The induct method itself does not eta-contract or expand. It merely uses
> primitives, in particular resolution, which in turn uses higher-order
> unification. And higher-order unification does indeed eta-expand. In
> certain situations. This is intentionally not fixed and you should not
> expect or rely on a particular behaviour. That is, you may have to
> ensure eta-contraction yourself if some part of your proof method is
> sensitive to it.
>
> Tobias
>
> Am 01/03/2012 18:53, schrieb Peter Lammich:
>> Hi,
>>
>> [Referring to Isabelle-2011-1]
>>
>> I recently encountered a quite strange behavior of the induct method. It
>> seems to arbitrarily eta-expand its subgoals under certain conditions
>> (If the induction variable is nested inside higher-order context ???).
>>
>> In the boiled-down example below, the first induct method fully
>> eta-expands its subgoals. In the second induct-method, the subgoals are
>> not eta-expanded, but the generated cases are. That is, on apply-style
>> scripts, you see eta-contracted goals, and when switching to ISAR, using
>> case-commands, you get eta-expanded goals.
>>
>> Is this behavior somehow documented? Can I switch it off?
>> In my concrete application, it kills my simplifier setup, as the
>> simplifier applies rules inside the eta-expanded terms that I do not
>> expect to be applied there.
>>
>> Regards,
>>   Peter
>>
>>
>> --------------------------------------
>>
>> declare [[eta_contract = false ]] (* Configure pretty-printer not to
>> eta-contract on pretty-printing *)
>>
>> consts
>>   f :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
>>   i :: "('a list \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b
>> \<Rightarrow> bool)"
>>
>> lemma "f (i xs s)"
>>   apply (induct xs)   (* Subgoals are fully eta-expanded here *)
>>   print_cases (* Cases are eta-expanded, too*)
>>   oops
>>
>> lemma "f (i xs s)"
>>   apply (induct xs arbitrary: s) (* Subgoals are *NOT* eta-expanded here
>> *)
>>   print_cases  (* Cases are eta-expanded *)
>>   oops
>>
>>
>





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