The Book

Implementing Mathematics with The Nuprl Proof Development System

See title page for important information about this reference

Next: System Description Up: Index Previous: Computation   Contents

• Refinement Tactics
• Transformation Tactics
• Writing Simple Tactics
  • The Metalanguage ML
  • Using ML from Nuprl
  • Example Tactics
  • The Auto-tactic

Proof Tactics

In the study of logic a distinction is made between the logic being studied, the object language, and the language in which the study of the logic is conducted, the metalanguage. In our case the object language is the type theory Nuprl. Thus far in this book we have conducted the discussion of Nuprl using a combination of English and mathematics as an informal metalanguage. In this chapter we introduce a formal metalanguage based upon the ML programming language [Gordon, Milner, & Wadsworth 79].

In ML the various parts of the object language--terms, declarations, proofs and rules--are data types. By defining a formal metalanguage we have made concrete the structure and elements of the object language. We can then write ML programs that manipulate objects of the object language. Thus, for example, we can write a program to return the subterms of a term or one that substitutes a term for a free variable in a term. More importantly, we can write ML functions which search for or transform proofs. We can then use such automated proof techniques and theorem-proving heuristics, tactics, while writing proofs.

A tactic is a function written in ML which partially automates the process of theorem proving in Nuprl. In any logic writing a formal proof is a combination of insightful, interesting steps and tedious ones. Being required to fill in every detail of a proof distracts one's attention from the important parts of the proof and can be quite tiresome. The refinement logic of Nuprl is no exception to this. Given undecidability, we cannot hope to fully automate the theorem-proving process. Ideally, then, we would want the user to enter only the central ideas of a proof and leave the details to be filled in by the system. Tactics offer a mechanism whereby a sketch of a proof supplied by the user can often be completed automatically and many simple proofs can be avoided altogether. Tactics can also be used to automate more difficult patterns of proofs that occur frequently so that essentially the same argument need not be repeated; a tactic for that pattern of proof would be invoked instead. The uses of tactics are many and need not be restricted to the above. There is the potential in the tactic mechanism to express any decision procedure, semidecision procedure or theorem-proving algorithm which is valid in the Nuprl logic. As will be explained in detail below, the implementation of the metalanguage makes sure that all proofs produced by tactics are in fact valid Nuprl proofs. This makes it impossible to write or use a tactic that produces an incorrect proof.^6.1

In Nuprl there are predefined tactics that are always available. These include tactics of general use in theorem proving. The user can easily add new tactics that extend the predefined tactics or are specific to the domain of theorems being proved. The next two sections describe two different kinds of tactics: refinement tactics and transformation tactics. This is followed by an introduction to the ML programming language and an explanation of writing simple tactics. Chapter 9 contains a more detailed description of the metalanguage interface and information on writing tactics and examples of more complicated tactics.

Refinement Tactics

A refinement tactic resembles a derived rule of inference. Such a tactic is invoked by typing the name of the tactic where a refinement rule is requested by the proof editor. When the tactic is applied it tries to prove the current goal. There are three possible outcomes from a tactic invocation.

1. If the tactic completely proves the current goal then the name of the tactic name is entered as the rule name, and the status of the sequent is changed to complete. This refinement generates no subgoals.

2. If the tactic produces part of a proof of the current goal then the tactic is entered as the rule name, and the status of the sequent is changed to incomplete. Each of the subgoals left unproved in the proof produced by the tactic is listed as a subgoal to the refinement.

3. If the tactic fails then an error message is displayed in the command window, and the status of the sequent is changed to bad.

The behavior of a refinement tactic resembles that of a primitive rule of inference or decision procedure (such as arith). However, although refinement tactics are similar to rules of inference, they should not be thought of as fixed rules; within the tactic, for instance, the goal can be examined and different refinements can be applied based upon this analysis. In addition, by using the failure mechanism that is primitive to the ML language a tactic may approach a goal using one technique, find that this leads to a dead-end, backtrack and try another approach. Thus while the result of a tactic may represent just a few primitive refinement steps, the method by which those few steps were arrived at may have required a substantial amount of computation.

Transformation Tactics

Whereas refinement tactics take only goals as arguments and return proofs, transformation tactics take proofs as arguments and return proofs. Transformation tactics can perform much more global analysis and change to proofs than can refinement tactics. These tactics, for instance, can complete or expand an unfinished proof, produce a new proof that is analogous to the given proof and perform various optimizations to the proof such as replacing subproofs with more elegant or concise ones, to name a few of the uses to which they have been put.

A user invokes a transformation tactic by editing the theorem of interest and traversing the proof until the goal heading the desired subproof is displayed. The user then types , and Nuprl will prompt for the name of the transformation tactic which is to be applied. The tactic is applied to the proof consisting of the current goal and anything that is below it, that is, any subgoals and proofs below the subgoals. The transformation tactic, if it succeeds, will return a proof which has the same goal as the argument proof tree. Unlike those of refinement tactics, the name of the transformation tactic is not entered into the proof; the tactic serves as an operation on proofs, transforming one proof to another. Upon termination the proof returned may bear little resemblance to the original proof, except that a transformation tactic cannot change the proof above the root of the argument, nor can it change the goal of the root of the subproof. The only exception to this rule is if the subproof is the whole proof--the tactic was called from the top goal. In this case the transformation tactic may replace the goal of the proof; thus a transformation tactic can map one theorem into another. These constraints are enforced by the implementation and need not be the concern of the tactic designer or user.

Writing Simple Tactics

The Metalanguage ML

Writing complicated tactics requires a thorough knowledge of the ML programming language [Gordon, Milner, & Wadsworth 79] and the information contained in chapter 9. It is an easy matter, however, to write simple tactics and to combine existing tactics with a minimal subset of ML. ML is a functional programming language with three important characteristics which make it a good language for expressing tactics:

1. ML has an extensible, polymorphic type discipline with secure types. This allows type constraints on the arguments and results of functions to be expressed and enforced. For example, the result of a function may be constrained to be of type proof.

2. ML has a mechanism for raising and handling exceptions (or, in the terminology of ML, throwing and catching failures). This is a convenient way to incorporate backtracking into tactics.

3. ML is fully higher-order; functions are objects in the language. This allows tactics (which are functions) to be combined using combining forms called tacticals, all of which are written in ML.

In order to understand the example tactics presented below it is not necessary to know many of the details of ML. The following summarizes some of the more important and less obvious language constructs. Functions in ML are defined as in

        let divides x y = ((x/y)*y = x);;

This function has type intintbool; that is, it maps integers to functions from integers to boolean values. There is also an explicit abstraction operator, , which stands for the more conventional . The previous function could have been defined as

        let divides = \ x . \ y  . ((x/y)*y = x);;

Exceptions are raised using the expression ``fail'' and handled (caught) using ``?''. The result of evaluating exp1?exp2 is the result of evaluating exp1 unless a failure is encountered, in which case it is the result of evaluating exp2. For example, the following function returns false if .

        let divides x y = (if y = 0 then fail
                          else (y*(x/y)=x)
                          ) ? false;;

In fact, because dividing by causes a failure, we could define the same function with

        let divides x y = (y*(x/y)=x)?false;;

Using ML from Nuprl

From Nuprl the user can request that ML be run interactively by entering the command ml in the command window. Nuprl will respond with a M> prompt in the command window. Any input typed after this prompt is processed by ML. This facility allows for the examination of variables and constants in ML and for the tracing, definition and debugging of tactics. The user leaves the interactive ML mode by typing .

Although definitions can be entered interactively using this mode, the definitions entered are only temporary. Once the current Nuprl session has been concluded, any changes to the ML state disappear. If more permanent definitions are desired an ML object can be created and edited using the text-editing facilities of Nuprl, and the ML commands in this ML object can be evaluated by ML. To do this a library object of type ``ML'' is created and then edited in Nuprl. Once complete this ML object can be checked, during which process the commands of the ML object are evaluated sequentially by ML. If there are no errors in the object it is marked as good, and any changes in the ML state implicit in the commands will remain in effect throughout the remainder of the Nuprl session. Should an error be encountered while evaluating the ML object an error message will be displayed, and evaluation of the ML object will be discontinued. Any error-free commands that preceded the one with an error will have been evaluated with any changes in state remaining in effect. The user may then view the ML object, make the necessary corrections and recheck it. The commands in an ML object will also be evaluated when it is loaded or restored to the library.

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 Nuprl. 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.

The Auto-tactic

        set_auto_tactic `transform_tac`;;

        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`;;

        set_auto_tactic `COMPLETE
                        (refine (tactic \`immediate\`))`;;

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.

Footnotes

... proof.^6.1

A tactic may fail to produce any proof at all, but it will not produce an invalid proof.

---

Next: System Description Up: Index Previous: Computation   Contents