Email Gateway (Aug 18 2022 at 15:13): Email Gateway (Aug 18 2022 at 15:13):From: Andrei Borac <zerosum42@gmail.com>
First off, sorry for not posting the actual real problem at hand, but
there quite a number of definitions that would have to be brought in.
I have a subgoal that can be solved by "force" if I first specify a
universal instantiation (UI) of an expression with three variables:
apply(erule_tac x="..." in meta_allE)
apply(erule_tac x="..." in meta_allE)
apply(erule_tac x="..." in meta_allE)
apply(force)
"force" has been able to do universal instantiation in the past ...
however, this time:
(1) there is a lot of stuff in the assumptions block
(2) some amount of simplification is required after UI including
following the appropriate branch of nested case expressions
Is there a way to get force to try harder, or use some other kind of
automated method? Note that I have tried ATPs but it seems as they
have difficulty doing the simplifications required after UI (just a
guess, I don't actually know how these tools work). To split the
case/options before instantiation cannot be done by simp split and
would have to be done semi-manually (to split into multiple
universally quantified expressions) which I might try but looks
tedious at best and might not even help.
Any ideas?
-Andrei
Email Gateway (Aug 18 2022 at 15:13):From: Lawrence Paulson <lp15@cam.ac.uk>
Looking at the code, I see that force has no search depth, but performs a best-first search. You haven't stated whether it gives up or runs forever, but I would expect the latter. If you can make it work by instantiating a couple of quantifiers, that's probably the simplest thing to do. Tuning a reasoning tactic to your specific requirements would probably take quite a long time.
Larry Paulson
Email Gateway (Aug 18 2022 at 15:23):From: Andrei Borac <zerosum42@gmail.com>
Well, if it is doing a best-first search, which I take to be
exhaustive, it does not seem as if the search is over all possible
UIs. Applying force to the unrefined subgoal gives up (rather quickly)
... manually instantiating the quantifiers is not really an option, as
there are 269 subgoals ... I got here because I assumed that force can
find the instantiation that works (and it has been able to do similar
proofs, this one just has slightly more complex stuff under the
quantifier).
Additionally, I found that simp is sufficient to solve the subgoal
after manual instantiation:
apply(erule_tac x="..." in meta_allE)
apply(erule_tac x="..." in meta_allE)
apply(erule_tac x="..." in meta_allE)
apply(simp)
So, my speculation at this point is that force does not blindly try
UIs, but looks for some correlation between the stuff in the UI and
the other facts in the assumption block. What I am thinking is the
best option at this point is to write some kind of control program
that will interact with Isabelle, first inserting the thy file up the
current point and then try all possible (type-sane) instantiations
followed by force until one succeeds ... after a long time, I will
have a long script that can be cut & paste into the thy file ...
perhaps it would even be possible to run regular expressions on the
assumption facts to make good guesses at the required UI.
At this point, it would sorta help me out if I knew the incantation to
turn on "quick and dirty mode" in the Isabelle shell.
Or perhaps someone can give me few pointers to places in Isabelle's
source or code samples that are relevant to writing such a trial and
error tactic in ML?
-Andrei
Email Gateway (Aug 18 2022 at 15:26):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Andrei Borac wrote:
It all rather depends on the nature of your problem, but I find that you
can often pick out the easy subgoals in a way which will give you the
right instantiations.
Things like this
(TRYALL (ares_tac [refl])), (TRYALL (eresolve_tac wf_cc_Ds)),
tend to be sprinkled throughout my proofs, and I don't have to do much
instantiating by "hand", or, for that matter, waiting for Force_tac to
finish.
So far as I know these tactics have no equivalent in Isar. Opinions
seem to vary as to whether that is a reason for not using them
Regards
Jeremy
Email Gateway (Aug 18 2022 at 15:27):From: Lawrence Paulson <lp15@cam.ac.uk>
I assume that by UI you mean universal instantiation. Isabelle instantiates quantifiers solely by unification. It could be interesting to investigate whether some proofs would benefit from automated explicit substitution of candidate terms.
As Jeremy mentioned, at the ML level Isabelle provides a flexible tactic language in which you can express various search strategies that may be able to automate your proofs, and there are ways of inserting ML tactics into Isar proofs or encapsulating them as Isar methods.
Larry Paulson
Last updated: Apr 19 2024 at 16:20 UTC