Next: Mathematics Libraries Up: Building Theories Previous: Sets and Quotients

# Theories

In  section 10.2 the use of extractions to keep the size of objects down was described; we now describe another important advantage of this scheme. The conclusion of the theorem from which an object is extracted gives a type for the object, and this type is used by a special tactic which proves the numerous ``membership'' subgoals (i.e., those of the form H>>t in T) that arise in virtually every proof. As briefly mentioned in chapter 9, this tactic works by repeatedly breaking down the conclusion using intro rules until the goals are trivial. Some of the intro rules require using terms as parameters, and these require types to be assigned to components of the conclusion of the goal; this task can be much easier when the extraction scheme is used, since it in effect supplies types for the important objects of the theory. When a theory is structured in this way, the membership tactic is able to prove most, and in some cases all (as in the theory of regular sets described in the next chapter), of the membership subgoals.

Proving such subgoals is tedious, and they arise often, so the use of extractions as previously described is almost a necessity for any serious user. Also, because a reference to an extraction contains the name of the theorem extracted from, tactics examining terms have ``hooks'' into the library available to them. Certain kinds of facts are naturally associated with defined objects. For example, a defined object which is a function may also be functional over a domain with a different equality. Using conventions for the naming or placement of such facts can allow tactics to locate required information for themselves without requiring the user to explicitly supply lemma names. The convention could be that such facts are named using a certain extension to the name of the theorem extracted from, or that such facts are located in the library close to that theorem. Obviously this is far from being a solution to the problem of knowledge management; in the design of the future versions of the Nuprl system this problem will receive considerable attention.

There are a few minor points to keep in mind when putting together a substantial theory. First, be careful with the ordering  of library objects. Other objects which are referenced in a given object must precede the given object in the library. ML objects can be particularly troublesome: if you modify and recheck  an ML function then the change will not be reflected in an ML function which references it. There will be nothing to indicate that the second object should be rechecked, and until it is it will continue to refer to the old version of the modified function. Another problem is that deleting an ML object from the library does not undo the bindings created therein. Thus you can check the entire library (using, say, check first-last) without an error but then have errors occur when the same library is loaded into a fresh session. Currently, the only way to solve these problems is by being careful of organization and by keeping track of the dependencies yourself.

Next: Mathematics Libraries Up: Building Theories Previous: Sets and Quotients

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