Email Gateway (Aug 23 2022 at 09:14): Email Gateway (Aug 23 2022 at 09:14):From: Peter Lammich <lammich@in.tum.de>
Hi,
resolution (i.e. apply (rule x)) seems to sometimes introduce seemingly
arbitrary eta-expansions into the result. In my case, these will then
confuse subsequent tactics that depend on the term syntax.
Questions:
Do I always have to assume that resolution introduces eta-
contractions?
Are there conventions like
"all tactics should work independently of eta-expansions in the goal",
and in consequence, "all tactics may arbitrarily eta-expand or contract
the goal"?
Is there an easier way to get rid of eta-expansions, other than
using "tactic ‹PRIMITIVE (Conv.fconv_rule Thm.eta_conversion)›" after
each resolution/before each tactic that depends on the term syntax?
Email Gateway (Aug 23 2022 at 09:14):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,
Questions:
1. Do I always have to assume that resolution introduces eta-
contractions [read: expansions]?
I believe this originates from the higher-order unification algorithm. See e.g.
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-August/msg00089.html
- Are there conventions like
"all tactics should work independently of eta-expansions in the goal",
If there is such a convention, it is more honored in the breach than in the observance. The above link (and a moment's thought) reveals that "simp" violates it. So does, incidentally, the "tactic that depends on the term syntax" you describe below.
and in consequence, "all tactics may arbitrarily eta-expand or contract
the goal"?
Not "in consequence", but "in practice" I guess they do, for some definition of "arbitrarily".
- Is there an easier way to get rid of eta-expansions, other than
using "tactic ‹PRIMITIVE (Conv.fconv_rule Thm.eta_conversion)›" after
each resolution/before each tactic that depends on the term syntax?
That's what I would do if the tactic works well on eta-reduced terms. (Or I'd introduce some proof method if "tactic ‹PRIMITIVE ...›" is something you have to write often in Isar.)
Isabelle's limitations in this respect seem hard to avoid. Even provers like Coq and Lean that work up to computation (including beta-eta-conversion) have tactics like "simp" that inspect the term structure and that behave differently (up to beta-eta-equivalence classes) on different beta-eta-representatives.
Nonetheless, better documentation of the status quo could help, and at the cost of some complications (and the risk of introducing bugs and for sure incompatibilities), unification could in principle be changed so that it doesn't eta-expand.
Cheers,
Jasmin
Email Gateway (Aug 23 2022 at 09:14):From: Lawrence Paulson <lp15@cam.ac.uk>
The basic higher-order unification search process expects fully expanded terms, a form it maintains as it traverses the two structures. Since resolution is still one of the most heavily used proof methods, contracting after each resolution step would degrade performance significantly.
Larry
Last updated: Apr 24 2024 at 20:16 UTC