I want to understand clearly affects how many steps it might take to completely proof a single goal. i.e. I want to understand the interface to the current function:
steps(goal,...) = # steps to prove goal
intuitively it must depend on the current tactic applied to
goal and the knowledge we have (e.g. environment & context).
Does this mean that the function has the following signature?
steps(goal, Tactic, Env, Context)
my hunch is that it actually only requires
since the information needed to break up the current proof obligation/goal is all in Tactic (e.g. it refers to the knowledge in the context or environment needed to correctly apply to the current goal).
Is this correct?
I guess in principle the # of steps for the current goal depends on the steps for all subsequent goals…and those might need specific knowledge that might not be current reachable from only the tactic (i.e. we do need the current context AND the environment).
As long as a proof does NOT do random imports in the middle now I believe that:
is necessary (sorry changed my mind).
Is this correct? What’s the right interface to that function?
Just curious what factors affect how long a proof is basically.