Example Tactics

We  now examine how some simple tactics are written. One should think of tactics as mappings from proofs to proofs which may take additional arguments. The simplest tactics are formed using the ML function refine_using_prl_rule .   This function takes two arguments, a token (the ML equivalent of a string) and a proof. The token is parsed as a rule, and then the goal of the proof is refined by this rule. Conceptually the result is a proof with the top goal refined by the rule indicated by the token and with the appropriate subgoals for this refinement. Thus refine_using_prl_rule is a procedural embodiment of the primitive refinement rules of . The function refine_using_prl_rule is an example of a tactic.

Atomic refinement steps and existing tactics may be combined using a combining form called a tactical . For example, the following tactic refines a goal by intro; then, each of the resultant subgoals is again refined by intro. To each of the subgoals of this the predefined tactic immediate is applied.

        let two_intro proof = 
          (refine_using_prl_rule `intro` THEN
            refine_using_prl_rule `intro` THEN
              immediate) proof;;

The tactical  THEN is an infix operator; it takes two tactics and produces a new tactic. When applied to a proof this new tactic applies the tactic on the left--hand side of the THEN and then, to each of the subgoals resulting from the left--hand tactic, the right--hand tactic. Note that two_intro will only work if it makes sense to perform two levels of introductions. For example, if the tactic is applied to a dependent product (where an intro rule requires an object of the left type) the refinement will fail, causing the tactic to fail.

In addition to THEN , two other tacticals are of general usefulness: REPEAT   and ORELSE

 . The tactical REPEAT will repeatedly apply a tactic until the tactic fails (or fails to do anything). That is, the tactic is applied to the argument proof, and then to the children produced by tactics, and so on. The REPEAT tactical will catch all failures of the argument tactic and can not generate a failure. For example,

        let intros = REPEAT (refine_using_prl_rule `intro`);;

will perform (simple) introduction until it no longer applies. The ORELSE tactical takes two tactics as arguments and produces a tactic that applies the --hand tactic to a proof and, if that tactic fails, the right--hand tactic. The following tactic performs all simple introductions and eliminations which are possible.

        let goal_simplify =
          REPEAT ((refine_using_prl_rule `intro`) 
                  ORELSE (refine_using_prl_rule `elim`));;

Using refine_using_prl_rule  , the four tacticals given here and the predefined tactics, many useful tactics can be written. We hope that tactics are easy enough to write and convenient enough to use that the user will be encouraged to experiment with them. In particular, we hope that the user will write tactics for any aspect of theorem proving that is repetitious, stylized or routine.

The power and flexibility of the tactic mechanism go well beyond these simple examples. In chapter 9 we continue the discussion begun here.