A goal, a justification, and the resultant subgoals constitute a "proof step", sometimes called an "inference step"; the goal and subgoals are often called the "conclusion" and "premises" of the inference. A principle aim of the Nuprl system design is to assist in the relatively easy generation of "valid" inferences, i.e., inferences whose conclusions are true if their premises are, and yet to permit these inferences within a proof to be appropriate to a human reader, i.e., rather high-level.
Although ultimately inferences are justified by low level rules, one major style of proof is to formulate each step in a manner that seems evident, or at least plausible, to a human reader, and to make the "granularity" coarse enough so that the whole proof is not too tedious to read or comprehend as a whole. This is technically possible because of programs called "tactics".
Usually, for the reader of a proof, the most interesting thing about tactic code of a justification is which lemmas, definitions, or hypotheses it refers to, and what witnesses are provided (Note that hypotheses are often referred by number, negative numbers indicating counting backwards from the conclusion as zero). Sometimes the code is elided in favor of a user-created summary comment which is displayed instead (of course the tactic code is still there somewhere).
Tactics
In Nuprl, a justification is "tactic" code. Given a collection of prespecified "primitive" inference forms, a tactic is a program for reducing a desired proof goal to premises by composing primitive inferences. A tactic is essentially a program for constructing such an inference tree, and one chooses which tactics to apply according to how you want to generate subgoals from the goal. The execution of the tactic gives rise to an inference step, the premises being all the unproved leaf premises of the primitive proof tree. Further, to count as a tactic, although its execution might not terminate or might raise an exception, if it does terminate without exception, then it must be guaranteed to generate subgoals justifiable by primitive inferences.
In order to freely write heuristic tactics, one must have some practical criterion for recognizing tactics. In
The labor of justifying an inference is divided between ascertaining that the program generating the subgoals is a tactic, and checking the primitive inference rules, which are presumably formulated to make such verification feasible; primitive inference forms tend to be expressed schematically. In contrast, the justification of complex forms of inference via tactics is in terms of the generic criterion for being a tactic (i.e. that the result of execution determines a primitive proof tree), and is not schematically described.
See also
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html