Email Gateway (Aug 19 2022 at 10:33): Email Gateway (Aug 19 2022 at 10:33):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I recently spotted down a problem with SELECT_GOAL and schematic
variables. If new schematic variables are produced in the proof of the
selected goal, their names may clash with existing schematics in the
outer proof state, resulting in unexpected error messages:
inductive P for x where I: "P x"
lemma J: "P (\<lambda>_. R)" by (rule I)
schematic_lemma "\<And>a. P (?R a) \<or> P (?R)" "TERM ?R3"
apply -
apply (tactic {* SELECT_GOAL (
rtac @{thm disjI2} 1 THEN rtac @{thm J} 1
(THEN PRIMITIVE zero_var_indexes)
THEN print_tac "Proof state after inner tactic"
) 1
*})
*** exception TYPE raised (line 109 of "envir.ML"):
*** Variable "?R3" has two distinct types
*** 'c
*** 'd
What happened here is that the tactic inside SELECT_GOAL produced the
proof state: "\<And>a b. P ?R3 \<or> P (\<lambda>_. ?R3)"
And when retrofitting this into the outer proof state, ?R3 happens to
clash with the ?R3 there.
Moreover, if one directly changes schematic variables that occur in the
selected goal, like the "zero_var_indexes" does in the commented out
line of the example, the unifier runs havoc and produces errors like:
*** mk_ff_list
*** At command "apply" (line 9 of
"/home/lammich/lehre/praktWS1112/cava/Libs/Refine/Autoref/Scratch.thy")
(I also got some exceptions about "Var name confusion" from the unifier,
that I cannot reproduce any more)
These observations result in two main questions:
1. What are the conventions that tactics must stick to when
instantiating schematic variables? E.g. is it ok to do
PRIMITIVE zero_var_indexes or not?
2. Is SELECT_GOAL implemented correctly and was never supposed to
work with schematics, or should it be fixed?
Regards and thanks for any comments/workarounds on this,
Peter
Email Gateway (Aug 19 2022 at 10:37):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm afraid that I really can't answer this question without a time machine.
In the early days, I must have introduced SELECT_GOAL in the context of some specific application where it worked fine. Then it got put in the standard libraries of tacticals and more or less forgotten. I know that a lot of derivations that involve new variables in sub-proofs can go wrong as you describe. The usual method of getting around such problems was to freeze variables prior to applying the tactic, thawing them afterwards. That was a hack, but it generally worked. My impression is that Makarius has replaced such trickery by more robust methods, but it's possible that quite a lot about old code is still there and running. I'm not sure about the current best practice for dealing with this sort of situation.
Larry Paulson
Email Gateway (Aug 19 2022 at 10:37):From: Peter Lammich <lammich@in.tum.de>
Unfortunately, this problem does not only affect the (admittedly
low-level) SELECT_GOAL, but also high-level proof scripts, as the
following example demonstrates:
inductive P for x where I: "P x"
lemma J: "P (\<lambda>_. R)" by (rule I)
schematic_lemma "\<And>a b. P (?R a) \<or> P (?R)" "TERM ?R4"
apply (rule disjI2, rule J) []
*** exception TYPE raised (line 109 of "envir.ML"):
*** Variable "?R4" has two distinct types
*** 'c
*** 'd
note that everything works fine without the [].
Email Gateway (Aug 19 2022 at 10:37):From: Makarius <makarius@sketis.net>
On Fri, 22 Mar 2013, Lawrence Paulson wrote:
I'm afraid that I really can't answer this question without a time
machine.
In principle the time machine is Mercurial, but it also takes time to
study our immense history that has accumulated since changeset 0 from
Sep-16 12:20:38 1993 (and more years of unwritten history before that).
The usual method of getting around such problems was to freeze variables
prior to applying the tactic, thawing them afterwards. That was a hack,
but it generally worked. My impression is that Makarius has replaced
such trickery by more robust methods, but it's possible that quite a lot
about old code is still there and running. I'm not sure about the
current best practice for dealing with this sort of situation.
The ancient freeze_thaw and freeze_thaw_robust (which were actually both
fragile) have evolved over a long way to become the current FOCUS
combinators, which are also mentioned in the "implementation" manual.
This Isar technology for structured tactic programming is useful in many
situations, but it does not really cover the schematic goal approach that
Peter appears to use a lot. In fact, the continued retreat of genuine
logic-programming with schematic variables in Isabelle tactics over the
years had paved the way for these more recent high-level tacticals.
Readers of the old "intro" manual by Larry might remember the final Prolog
example. Such techniques are now extremely rare, so it is no surprise
that certain tools choke.
(I will have a close look later at what is actually happening here, when I
have catched up with various other open threads.)
Makarius
Email Gateway (Aug 19 2022 at 10:58):From: Makarius <makarius@sketis.net>
I've had a first round of studying 10-15 years of Isabelle source history
yesterday.
SELECT_GOAL and Subgoal.FOCUS represent different strands of tradition,
only the latter (much younger) uses high-end Isar infrastructure --
context import/export operations that vaguely resemble old "freeze_thaw"
by Larry.
SELECT_GOAL is also used for the "[...]" notation for Isar proof methods.
SELECT_GOAL was good old code by Larry in the nostalgic style of 1980-ies
Isabelle until 31-Aug-2001. Then Stefan Berghofer "Tidied function
SELECT_GOAL". I think before and after the behaviour wrt. newly invented
schematic was the same as it is still now. Much later I merely modified
its internal terminology and general setup to make it look more like
Subgoal.FOCUS, e.g. using certain "extract" and "retrofit" operations.
Beyond historical anecdotes, I have made one round of experiments to see
if SELECT_GOAL can be converged a bit more towards the way how the (very
sophisticated) Subgoal.FOCUS works, but it breaks various classic tactics.
Reasons still need to be explored, I can say more after the next round of
investigation.
Makarius
Last updated: Apr 20 2024 at 01:05 UTC