Email Gateway (Aug 22 2022 at 14:19): Email Gateway (Aug 22 2022 at 14:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eisbach experts and users,
I have trouble to write a proof method that does the following:
Apply a rule called foo.
It has two premises that both contain variables that are not bound by the conclusion of
foo. Hence, the goal state consists of two goals with a schematic variable ?x in them.
Work on the first subgoal by applying rules from a named_theorems collection my_rules.
This is supposed to instantiate the variable ?x. All these rules in my_rules have one
constant C as the head term, and they have premises with the same head constant, but there
may also be premises with other terms (let's call them side conditions). As long as the
current subgoal has C as head symbol, I want to apply the rules in my_rules, and I want to
apply some proof automation (like clarsimp or auto) to the side conditions. In particular,
I want to make sure that clarsimp and auto are _never_ applied to a goal with C as head
symbol.
This should be done iteratively until either
(a) the goal arising from step 1 is solved or
(b) the current subgoal has C as head symbol, but there's no matching rule in my_rules, or
(c) one of the side conditions is not solved by clarsimp and auto.
I tried to write the proof method with Eisbach, but I failed to make the distinction based
on the head symbol. Here's my attempt:
method step =
(match conclusion in "foo p1 p2 p3" for p1 p2 p3 => rule my_rules
\<bar> H for H => \<open>solves \<open>clarsimp\<close>\<close>)
method my_method = (rule foo, (step+)?)
The problem is that the match method seems to turn the schematic variable ?x into a fixed
variable x, which the rules in my_rules can no longer instantiate.
Can I somehow achieve with Eisbach what I want?
Best,
Andreas
Email Gateway (Aug 22 2022 at 14:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dan,
Thanks for the suggestion with fail in the interesting case. That indeed gets me out of
the subgoal focus of match. Indeed, a light-weight match without subgoal focus and without
binding in the first place would be nice.
Andreas
Email Gateway (Aug 22 2022 at 14:23):From: Daniel.Matichuk@data61.csiro.au
Hi Andreas,
The incompatibility with match and schematic variables is a known limitation, and unfortunately it's actually a hard problem to solve in general. Currently the "match" method performs a subgoal focus when matching on the conclusion or premises in order to turn them into proper terms/facts. This allows you to, for example, refer to "p1" (in your example) inside your method body and have it still make sense if p1 contained a goal parameter. This focus, however, needs to turns schematics into fixed terms for a number of reasons, most of which is so that they can't suddenly depend on goal parameters that they didn't before (i.e. in the case of "!!x y. (?P x) /\ (?Q y)").
Makarius and I had some discussions about how to handle this particular situation, we were leaning towards making methods "smarter" and realising that certain fixed parameters were actually schematics in the context and knowing how to instantiate them.
The other more lightweight solution we thought of was to introduce a non-focusing match, i.e. a match that does not manipulate the goal state or try to bind goal elements. This seems more like what you would want in your current situation. It's not immediately clear how this would interact with nested matches, however.
That all being said, I believe your particular situation can be resolved simply by putting "rule my_rules" outside of the match body itself. This is not the most elegant solution, but it should get the job done.
method step =
((match conclusion in
"foo p1 p2 p3" for p1 p2 p3 ⇒ ‹fail›
¦ H for H ⇒ ‹solves ‹clarsimp››) | (rule my_rules))
The match will not backtrack past the fact that it matched "foo p1 p2 p3" and will immediately fail through to "rule my_rules".
Hopefully this resolves your issue.
-Dan
P.S.
The "_" pattern is valid in the match method, so we can make your method a bit more succinct.
method step =
((match conclusion in
"foo _ _ _" ⇒ ‹fail›
¦ _ ⇒ ‹solves ‹clarsimp››) | (rule my_rules))[1]
Last updated: Apr 20 2024 at 01:05 UTC