Better interaction between tactics, dependency between goals, meta variables, etc
Closed this issue · 12 comments
I think we should revamp the LCF and the auto tactic to support maybe breadth-first search and better handling of dependency.
Firstly, a tactic should be allowed to return "depending on the realizers given to other goals", a temporary failure. To achieve this, we probably need to somehow mark all the meta-variables generated for other goals, and replace the one-line pattern-matching after Abt.out with something fancier. The idea is similar to stability checking is the machine. This also applies to the match and query primitive. A more refined approach is that a temporary failure would return the index of the metavariable it needs to know, and then the framework would prioritize solving the depended goal.
Secondly, once we distinguish permanent and temporary failures, we can then apply the tactics in arbitrary orders as long as we revisit the tactics which temporarily failed. This also made it possible to try to expand or discharge goals which need fewer or simpler subgoals according to some metrics. The idea is to detect permanent failure as soon as possible before wasting too much time.
Thirdly, after all of these have been done, I wonder if we can implement breadth-first search/trying also for the par, in the spirit of trying to detect permanent failure early.
This sounds really interesting! I'm excited about your idea.
@favonia So that I can better understand what you have in mind, can you give a little example? Particularly of the "temporary failure" stuff you mentioned. This sounds very interesting to me.
@jonsterling If you apply Bool.EqTT to the goal #1 = #2 in bool where #1 and #2 are realizers of other goals, then it should temporarily fail and indicate that one of the blockers is #1 or #2 (or both) because it might succeed in the future but not right now, depending on these blockers. The distinction between permanent and temporary failures is to enable better proof search which prunes out branches with permanent failures.
For example, maybe in some branch, two goals need to be proved but there are many possible ways to prove the first goal. However, we can abort this branch if the second goal always leads to permanent failure no matter how the first goal is proved.
@favonia Ahh, I see! This sounds like something I've always wanted, but I wasn't sure the best way to formulate it.
Which part are you trying to formulate? The type (interface) of tactics or the proof search engine?
@favonia Any of it 😄
I think your Thought here sounds very immortal, and we should pursue it.
The first thing I see is to modify every rule so that it takes the set of metavariables representing the realizers of other goals. After RedPRL/sml-typed-abts#107.
@favonia I wonder if there is a way to do this more modularly, so that we don't have to change the types of rules.
Here's an idea. What if we had an exception like exception Blocked of metavar, and rules would raise this exception when the matches they perform are blocked by any metavariable, not just one which happens to represent a subgoal.
Then, in our tactics, where we have ful access to the proof state, we would catch this exception and we could check at this location whether the metavariable that blocked the rule was one of our other goals; this would allow us to decide from tactics whether a rule failure was fatal or temporary, without changing the types of rules. (I think).
How does something like this sound to you?
Alright. I was thinking that eventually you will change lots of types to support stateful proof search.
@favonia My hope is that the rules can remain with very simple types, but that the tactics may have more complicated types.
I'm opening a new ticket to track the task of making a non-broken version of auto. This ticket may be related, but I want to track that task in general, detached from a proposed solution.
Related: #558