Email Gateway (Aug 18 2022 at 19:17): Email Gateway (Aug 18 2022 at 19:17):From: Peter Lammich <lammich@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:18):From: Makarius <makarius@sketis.net>
This is the normal order of things. Combinations of simplification with
rule applications of the resolution family (intro/elim/dest) can lead to
eta-expansion and thus more reductions than first anticipated.
The above simpset is a bit fragile in that sense, as you have observed
already. If you do not want to add more rules, but want to retain control
of lambda equivalences, you can try to wrap up some App or Abs nodes in
auxiliary operators; similar to Collect/member for 'a set in HOL.
Makarius
Email Gateway (Aug 18 2022 at 19:18):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:19):From: Brian Huffman <huffman@in.tum.de>
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.
Email Gateway (Aug 18 2022 at 19:20):From: Makarius <makarius@sketis.net>
As Tobias points out, the Pure Isabelle system conceptually works modulo
eta (and beta and alpha) conversion -- although there are well known
traps. So to continue the thread, I would also like to see the other part
-- the proof tool by Peter that fails here.
Makarius
Email Gateway (Aug 18 2022 at 19:21):From: Lawrence Paulson <lp15@cam.ac.uk>
Eta-expansion is an intrinsic part of the higher-order unification algorithm. Following each unification by an eta-contraction step would be inefficient, and equally arbitrary. The “problem" that must be “fixed" is any code that cannot exist with this basic fact of nature.
Larry Paulson
Email Gateway (Aug 18 2022 at 19:23):From: Brian Huffman <huffman@in.tum.de>
On Fri, Mar 2, 2012 at 9:28 AM, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Eta-expansion is an intrinsic part of the higher-order unification algorithm. Following each unification by an eta-contraction step would be inefficient, and equally arbitrary. The “problem" that must be “fixed" is any code that cannot exist with this basic fact of nature.
By this reasoning, the Isabelle simplifier is a "problem" that must be "fixed".
The simplifier does not respect eta-equivalence of terms. I don't
think I would want one that did.
On 1 Mar 2012, at 20:15, Brian Huffman wrote:
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.htmlTo 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.
Email Gateway (Aug 18 2022 at 19:23):From: Peter Lammich <lammich@in.tum.de>
It's no custom "proof tool" involved here. My setting is roughly like
this:
I have assertions of type "heap => addr set => bool", and hoare-tripels
of type "assertion => program => assertion => bool" (syntax: {P} S {Q})
I defined the assertion
definition [simp]: "false h as == False"
Moreover, I have a rule
lemma [simp]: "{false} S {Q}"
The proof that fails has the form:
lemma "{is_list xs p} S Q" proof (induct xs arbitrary: p)
case Nil show ?case by (cases p, simp_all)
...
Here, depending on the case for p, "is_list [] p" simplifies to false,
which is then simplified to \lambda _ _. False, before the rule for
{false} S {Q} is applied.
So, if I have to expect eta-expansion at any point, I have to add
additional rules to the simpset to make it confluent again. This
certainly works, but may blow up the simpset.
Just as a remark: The simpset setup from the standard library has such
problems, too --- for example there is id_apply, that happily simplifies
"%x. id x" to "%x. x", but not "id" (I already had problems with that).
Last updated: Nov 21 2024 at 12:39 UTC