Tactics

tactic Complete justifications will generate the entire proof given the goal formula because the rule name, and labeling formation and parameters are enough data to generate subgoals from the goals. So the subgoals are computable from the part of the justification that does not include the proof expression for the subproofs (the synthesized expressions). This fact suggests a way to automate interactive proof generation. Namely, a program called a refiner, takes a goal and a complete justification and produces the subgoals. Nuprl works this way.

Nuprl also adapts tactics from LCF ([55]) into the proof tree setting to get a notion of tactic-tree proof ([4,7,57]). In this setting the justifications are called primitive refinement tactics. These can be combined using procedures called tacticalstactical. For example, if a refinement r_o generates subgoals $G_1, \ldots, G_n$ when applied to sequent G_o, then the compound refinement tactic written $r_o\ \mbox{\textsc{thenl}}[r_1; \ldots; r_n]$ executes r_o, then applies r_i to subgoal G_i generated by r_o.

There are many tacticals (c.f. [65,28]); two basic ones are ORELSE and REPEAT. The ORELSE tactical relies on the idea that a refinement might fail to apply, as in trying to use $\&\!R$ on an implication. In $r_o\ \mbox{\textsc{orelse}}\ r_1$, if r_o fails to decompose the goal, then r₁ is applied.

We will use tacticals to put together compound justifications when the notation seems clear enough.