Nuprl provides the facility for a distinguished transformation tactic known as the auto--tactic . This tactic is invoked automatically on the results of each primitive refinement step. After each primitive refinement performed in the refinement editor the auto--tactic is run on the subgoals as a transformation tactic. There is a default auto--tactic, but any refinement or transformation tactic may be used. For example, to set the auto--tactic to a transformation tactic called transform_tac, the following ML code is used:
set_auto_tactic `transform_tac`;;This code could be used either in an ML interactive window or placed in an ML object (and checked). To see what auto_tactic is currently set to, type
show_auto_tactic ();;
in the ML interactive window.
In general, an auto_tactic should either completely prove a subgoal or leave it unchanged. To ensure this the COMPLETE tactical can be applied to the intended tactic. This tactical changes the argument tactic so that partial results (i.e., those that still have unproved subgoals) are turned into failure. For example, to use transform_tac as the auto--tactic and to make it so that partial results are not used, use the command
set_auto_tactic `COMPLETE transform_tac`;;To set auto_tactic to a refinement tactic immediate where partial results are not used, use the following:
set_auto_tactic `COMPLETE
(refine (tactic \`immediate\`))`;;
This is the default setting of auto_tactic
. When the auto--tactic
fails the failure is not reported; rather, the subgoal is just unchanged. By
watching the status characters on subgoals one can tell which have been
proved by the auto--tactic and which still need to be proved.
The auto--tactic is applied to subgoals of primitive refinements only when a proof is being edited. When performing a library load or when using a tactic while editing a proof, the auto--tactic is inhibited.