next up previous contents index
Next: Building Theories Up: The Metalanguage Previous: A Larger Example

Existing Tactics

This section describes some of the tactics which have been written so far. If you have a copy of the system you should find most, if not all, of the described tactics in the ML files that come with it. Since these files for the most part are fairly well documented, and since the tactic collection is not stable, we limit ourselves here to describing briefly some of the tactics which are particularly useful and which provide an example of what can be done. See the files for the exact names and types of the described tactics.

One of the most tedious parts of reasoning in Nuprl involves dealing with the numerous trivial membership subgoals which arise. Looking at the rules, one can see that many of them have subgoals of the form A in Ui. Also, applying a lemma involves using the lemma rule and then applying the elim rule to instantiate the universally quantified variables of the lemma; each such elim entails proving that the term introduced to instantiate the variable is of the appropriate type. Both these types of subgoals have the same form, t in T, and the vast majority are fairly trivial. Fortunately, the tactic written to deal with these (currently called member) has so far been able to prove almost all of them. This tactic repeatedly applies intro to the membership subgoal until the subgoal has been broken down into components with trivial enough conclusions (like x in A where x:A is a hypothesis) to be immediately justifiable from the hypotheses. The hard part is guessing the using types required by many of the intro rules; for example, the intro rule for a goal of the form >> f(a) in B takes as a parameter the type of f. It is the type--guessing component which contains the bulk of the heuristics of the tactic. A good part of the success of this tactic owes to the extensive use of extractions, which provide an important source of type information; this is discussed further in the next chapter.

There are several tactics whose function, in part, is to make the rules easier to use. Most of the primitive rules in Nuprl \ require arguments. This makes it difficult to chain them together using the tacticals, so several tactics have been written which apply an appropriate member of a class of rules and guess the arguments required. An example is the tactic intro, which handles all the introduction steps except product and set intro, where a ``witness'' term is required, and union intro, where one must decide which half to prove. These tactics also deal with noncanonical forms. That is, if a canonical form is expected, as in the case of an elimination where the hypothesis must be a canonical type, but a noncanonical form is encountered, as will often happen if one defines the basic objects of his theory to be extractions, then the tactic will first use the direct computation rules to do any necessary reduction steps.

Since the lemma rule causes the statement of the lemma to be put in the hypothesis list, proving goals whose conclusions are instances of previously proven results would be tedious without tactic support. A particularly useful tactic for this takes a theorem name and tries to match the goal's conclusion with part of the theorem in order to determine the terms with which to instantiate the theorem. If successful, the tactic will produce subgoals corresponding to the antecedents of the implication forming the theorem, the consequent of which was matched against the goal's conclusion.

Finally, we briefly discuss a set of functions which provide support for implementing term--rewriting tactics. They are slight modifications of what Paulson has written for use in LCF [Paulson 83b] and which he used to write the main tactics in his proof of the correctness of the unification algorithm [Paulson 84]. The basic idea is to use analogues of the tacticals THEN, ORELSE, etc., as the basis for constructing larger rewriting tactics from smaller ones. To this end we define a type of conversions:

    lettype conv = term -> (term # tactic).
Given a term t, a conversion will produce a term u and a tactic which should prove a goal of the form H >> t=u in T. There is a function which takes a theorem name and produces from the theorem (assuming it has the appropriate form, which is roughly that of a universally quantified chain of implications which ends in an equality) a conversion which, if it succeeds, rewrites an instance of the left--hand side of the equality of the theorem into the corresponding instance of the right--hand side. The basic combining forms are THENC, which composes two conversions, ORELSEC and REPEATC, which also work analogously to the corresponding tacticals, and SUBCONV c, which for c a conversion takes a term t and returns the term which results from applying c to the immediate subterms of t. Using these connectives we can easily define functions which take a collection of conversions and employ various strategies for applying them to the subterms of a given term until some kind of normal form is reached. They have been used to write a collection of tactics which do various kinds of algebraic simplification. In the current system, because of certain inefficiencies which will not be present in the next version of the system, it is not feasible to do any really large rewriting tasks, but it does seem that tactics based on rewriting can handle a good part of the more tedious reasoning.

next up previous contents index
Next: Building Theories Up: The Metalanguage Previous: A Larger Example

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995