I was curious to know what (minimum) knowledge/information was necessary to reverse the application of a tactic.
Let’s say I only have a goal and the tactic application (perhaps atomic tactic) that lead that goal. What information do we need to be able to compute goals that could have lead to that result?
My guess is that we need all the imports (what I cal environment, not sure if that is the right terminology), resulting context and resulting goal. i.e.
parent_goal = ReverseCoq(child_goal, tactic_leading_to_child_goal, env, child_context)
is enough to compute the (possible) parents goals that lead to a specific
I am alright with returning a list of possible goals (or more likely goals). I am aware that the problem might be ill-posed so I’m flexible with solutions.
But I guess the only thing that is more of a stricter requirement that any goal in the parent goals should always return the child_goal. i.e.
g_parent \in parent_goal(s)
I do want
child_goal = Coq(g_parent, tactic_leading_to_child_goal, context_parent, env)
That should be satisfied/returned.