Email Gateway (Aug 19 2022 at 11:37): Email Gateway (Aug 19 2022 at 11:37):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I stumbled upon some odd behaviour of match_tac. When match_tac
- must match a schematic variable in the rule against a schematic
variable in the goal and the schematic variable,
- the schematic in the goal has bound variables as parameters,
- one of these bound variables x occurs at least twice in the
parameters, and
- there is another bound variable between the occurences of x,
then match_tac fails (i.e. empty proof sequence / failed to apply proof
method).
Has anyone got an explanation for this behaviour? I would have expected
that the implementation of matching for this quasi-first-order case is
complete.
This behaviour occurs both in Isabelle 2012 and in a current development
snapshot (0cd62cb233e0).
definition "TT ≡ λx. True"
lemma TT_I: "TT x" unfolding TT_def by simp
schematic_lemma "⋀x y. TT (?P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
(* fails *)
oops
schematic_lemma "⋀x y. TT (?P x y )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
schematic_lemma "⋀x y. TT (?P x x y )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
schematic_lemma "⋀x y. TT (P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
schematic_lemma "⋀x. TT (?P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
-- Lars
Email Gateway (Aug 19 2022 at 11:38):From: Makarius <makarius@sketis.net>
Larry is the one to explain what really happens.
When I came across match_tac for the first time as a very young student in
1993, I was already wondering about it -- but it was always document in
the manner of what is now in "implementation" manual (section 4.2.1):
\item @{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.
Flexible subgoals are not updated at will, but are left alone.
Strictly speaking, matching means to treat the unknowns in the goal
state as constants; these tactics merely discard unifiers that would
update the goal state.
This sounds like it is better not to lean out of the window too far.
Makarius
Email Gateway (Aug 19 2022 at 11:38):From: Lawrence Paulson <lp15@cam.ac.uk>
Sorry but I have totally forgotten about these. They are relics from a remote past.
Larry
Email Gateway (Aug 19 2022 at 11:38):From: Tobias Nipkow <nipkow@in.tum.de>
It is the documentation that is leaning too far out of the window. The
difference between
schematic_lemma "⋀x y. TT (?P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
(* fails *)
oops
and
schematic_lemma "⋀x y. TT (P x y x )"
apply (tactic {* match_tac @{thms TT_I} 1 *})
done
shows that in some situations it is not doing what it claims: "matching means to
treat the unknowns in the goal state as constants".
Tobias
Email Gateway (Aug 19 2022 at 11:38):From: Makarius <makarius@sketis.net>
The documentation is also going back to Larry.
I don't complain about anything he did there many years ago. One needs to
be realistic about what certain parts of a system can do and what not.
Makarius
Email Gateway (Aug 19 2022 at 11:38):From: Lawrence Paulson <lp15@cam.ac.uk>
I see that match_tac is basically part of the classical reasoner. It is for applying rules safely without affecting the proof state. Any significant change in its behaviour would breaks lots of things, but it's conceivable that there's a bug in this example. Or else the documentation isn't quite accurate.
Larry
Email Gateway (Aug 19 2022 at 11:38):From: Tobias Nipkow <nipkow@in.tum.de>
Am 12/08/2013 22:39, schrieb Lawrence Paulson:
I see that match_tac is basically part of the classical reasoner. It is for applying rules safely without affecting the proof state. Any significant change in its behaviour would breaks lots of things, but it's conceivable that there's a bug in this example. Or else the documentation isn't quite accurate.
The term "match" has precisely the definition you quote in the documentation,
and that should be the specifiation of anything called "match". If the
implementation does not conform, it should be fixed. I agree this may be hard in
this case and it is not a top priority. Alternatively the documentation should
carry a warning.
Tobias
Larry
On 12 Aug 2013, at 19:09, Makarius <makarius@sketis.net> wrote:
The documentation is also going back to Larry.
I don't complain about anything he did there many years ago. One needs to be realistic about what certain parts of a system can do and what not.
Email Gateway (Aug 19 2022 at 11:39):From: Lars Noschinski <noschinl@in.tum.de>
Peter and I did some investigation and this seems to be the source of
this behaviour: If two schematic variables (with only bound variables as
arguments) are to be unified, Unifiers.unify will always provide a
single unifier with the schematic variables reordered.
It might be interesting to note that also Unify.matchers is not able to
match such term.
theory Scratch imports Main begin (* Isabelle 2013 *)
ML {*
val pat = @{cpat "⋀x y. ?P x y"}
val term = @{cpat "⋀x y. ?Q x y x"}
val pair = [(term_of pat, term_of term)]
fun maxidx_of_cterm ct = case rep_cterm ct of
{maxidx, ...} => maxidx
val maxidx = Int.max (maxidx_of_cterm pat, maxidx_of_cterm term)
*}
ML {*
fun pretty_subst ctxt ((name,_), (typ, term)) =
[Pretty.str name, Syntax.pretty_typ ctxt typ, Syntax.pretty_term
ctxt term]
|> Pretty.list "" ""
val pretty_env =
Envir.term_env #> Vartab.dest #> map (pretty_subst @{context}) #>
Pretty.big_list "Unifier"
val pretty_env_list = map pretty_env #> Pretty.big_list "Unifiers"
*}
ML {*
Unify.unifiers (@{theory}, Envir.empty maxidx, pair)
|> Seq.list_of
|> map fst
|> pretty_env_list
|> Pretty.string_of
|> tracing
*}
ML {*
Unify.matchers @{theory} pair |> Seq.list_of |> pretty_env_list |>
Pretty.string_of |> tracing
*}
Email Gateway (Aug 19 2022 at 11:39):From: Makarius <makarius@sketis.net>
Larry is of course welcome to reformulate this snippet of the
documentation to fit better to the implementation, whatever it really is.
A warning like "the documentation might be inaccurate" does not make any
sense, because this always applies by default to any documentation.
Whenever someone sees a function somewhere, and some documentation
elsewhere, maybe together with some real-world uses of it in some working
application, one always needs to apply common-sense to estimate if it will
do a different job in a different context.
This principle applies to any complex software system, library, framework,
etc. For Isabelle the level of precision is actually above average -- I
am working routinely with more industrial things like the Java Standard
libraries that are much worse. And what Apple, Oracle, IBM usually do in
cases of uncertainty is to adapt the manual only.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC