Email Gateway (Aug 22 2022 at 16:37): Email Gateway (Aug 22 2022 at 16:37):From: Makarius <makarius@sketis.net>
Here is also the text from the "implementation" manual that has emerged
from such explanations over the years:
➧ @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
bimatch_tac}
are similar to @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
and @{ML biresolve_tac}, respectively, but do not instantiate schematic
variables in the goal state.⁋‹Strictly speaking, matching means to
treat the
unknowns in the goal state as constants, but these tactics merely discard
unifiers that would update the goal state. In rare situations (where the
conclusion and goal state have flexible terms at the same position), the
tactic will fail even though an acceptable unifier exists.› These tactics
were written for a specific application within the classical reasoner.
Flexible subgoals are not updated at will, but are left alone.
For the purposes of matching in Isar 'is' patterns etc. there is a
different front-end called Unify.matchers:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML
This has empirically evolved to something that works most of the time
for the particular applications of structured proofs (Isar) and proof
methods (Eisbach).
Makarius
Email Gateway (Aug 22 2022 at 16:43):From: Thomas.Sewell@data61.csiro.au
Thanks for the explanations, that explains what's going on entirely.
I guess that I have fallen into the habit of assuming too much from the
unifier.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 16:48):From: Thomas.Sewell@data61.csiro.au
I ran into this strange example recently.
schematic_goal "!!x y. True --> ?Q y x z"
apply clarify
apply (tactic {* match_tac @{context} [(@{thm impI})] 1 *})
apply (tactic {* resolve_tac @{context} [@{thm impI}] 1 *})
In essence, match_tac doesn't think that impI matches this goal, even
though it clearly does. This prevents clarify/clarsimp/safe from acting
on the goal. Shuffling the positions of the x/y/z premises leads to
different outcomes, with some orders allowing clarify to succeed and
others not.
This is quite strange.
I tried to dig into what Thm.biresolution is doing here, and got totally
lost. Does anyone more familiar with it want to investigate?
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 16:50):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm afraid that I have to call this behaviour correct, if weird and annoying.
Matching is implemented by performing unification and then rejecting the result if it assigns to any variables present in the goal. In your example, resolution with impI replaces ?Q in the goal by
%y x. ?Q5 x y z
This is not matching. It seems clear that there is another way to do the unification without updating ?Q, but the code doesn’t offer that option. Unification is done without knowledge of whether the user is attempting to match or not. This particular unification involves a so-called flexflex pair, a messy situation.
Larry
Last updated: Nov 21 2024 at 12:39 UTC