This section describes an existing library of theorems from the theory of regular sets. The library was constructed in part to try out some general--purpose tactics which had recently been written; the most useful of these were the membership tactic (see chapter 9) and several tactics which performed computation steps and definition expansions in goals. The membership tactic was able to prove all of the membership subgoals which arose, i.e., all those of the form H >> t in T. The other tactics mentioned were heavily used but required a fair amount of user involvement; for example, the user must explicitly specify which definitions to expand. Including planning, the total time required to construct the library and finish all the proofs was about ten hours.
For the reader unfamiliar with the subject, this theory
involves a certain
class of computationally ``simple'' sets of words over some
given alphabet; the sets are those which can be built
from singleton sets using three operations, which are denoted by
r+s, r s and 
. There should be enough
explanation in what follows to make the theorems understandable
to almost everyone.
We begin with a presentation of the library; a discussion of some of
the objects will follow.
This theory uses extractions for most of the basic
objects. For example,
the right--hand side of the definition for the function flatten is
just term_of(flatten_)(<l>); the actual Nuprl
term for the
function is introduced in the theorem flatten_. As a convention in
this theory, a DEF name with ``_'' appended
is the name of the corresponding theorem that the defined object is
extracted from.
Figure 
presents the first part of the library, which contains the definitions of the basic
objects, such as basic list operations and the
usual operations on regular sets. Objects not particular to this theory,
such as the definitions of the logical connectives, are omitted. The alphabet over which our regular
sets are formed is given the name E and
is defined to be atom (although all the theorems hold for
any type). The collection of words over E, E*, is defined to
be the lists over E, and the regular sets
for the purposes of this theory are identified with their
meaning as subsets of E*:
E* == (E list)
R(E) == (E*->U1)
Note first that we have identified the subsets of E* with
the predicates over E*; for more on representing sets, see the preceding
chapter. This means that if x is a word in E*, and r
is a regular set from R(E), then the assertion that x is
a member of r is expressed as the application 
.
Figure: Definitions of Objects for the Theory of Regular Sets
Figure shows the next part of the library, which contains some lemmas expressing some
elementary properties of the defined objects. It should be noted here that the
theorems we are proving are
identities involving the basic operations, and they are true over all subsets,
not just the regular ones. This allows us to avoid cutting R(E)
down to be just the regular sets, and we end
up proving more general theorems. (It would be a straightforward
matter to add this restriction by using a recursive type
to define the regular expressions and defining an evaluation
function.)
Figure: Basic Lemmas in the Theory of Regular Sets
Figure list some lemmas expressing properties of regular sets, and
the main theorem of the library.
Figure: Lemmas and a Theorem from the Theory of Regular Sets
We now turn our attention to objects contained in the library. The following descriptions of library objects should give the flavor of the development of this theory. This proof top and DEF together give the definition of append.
>> E* -> E* -> E*
BY explicit intro \x.\y. list_ind(x;y;h,t,v.(h.v))
<l1:A list>@<l2:A list> == (term_of(append_)(<l1>)(<l2>))
We use append to define the function flatten, which
takes a list of lists and concatenates them:
>> E* list -> E*
BY explicit intro \x. list_ind(x;nil;h,t,v.h@v)
The definitions of containment, `` <'', and equality
are what one would expect, given the definition of regular sets.
<r1:R(E)> < <r2:R(E)> == All x:E*. (<r1>)(x) => (<r2>)(x)
<r1:R(E)> = <r2:R(E)> == <r1> < <r2> & <r2> < <r1>
The following three proof tops give the definitions of
r+s, r s, and 
, respectively. (Informally, plus corresponds to
union, juxtaposition to forming all possible concatenations of
a word from the first set with a word from the second set, and
star to forming all possible concatenations of words from
the set.)
>> R(E) -> R(E) -> R(E)
BY explicit intro \r.\s.\x. ( r(x) | s(x) )
>> R(E)->R(E)->R(E)
BY explicit intro
\r.\s.\x. Some u,v:E*.
u@v=x in E* & r(u) & s(v)
>> R(E) -> R(E)
BY explicit intro
\r.\x. Some y:E* list.
list_ind(y;true;h,t,v.r(h)&v)
& flatten(y)=x in E*
Note the use of list_ind to
define
a predicate recursively.
The presentation concludes with a few shapshots that should
give an idea of what the proofs in this library are like.
First, consider a few steps of the proof of
star_lemma_3p5, which states that if u is in set 
then for all sets of words in s the concatenation of all words in the set, followed by u, is also in 
. The major proof step, done
after the goal has been ``restated'' by
moving things into the hypothesis list, is induction on
the list y.
,----------------------------------------------, |* top 1 1 1 | |1. s:(R(E)) | |2. u:(E*) | |3. (s*(u)) | |4. y:(E* list ) | |>> ( list_ind(y;true;h,t,v.s(h)&v) | | => s*(flatten(y)@u)) | | | |BY elim y new p,h,t | | | |1* 1...4. | | >> ( list_ind(nil;true;h,t,v.s(h)&v) | | => s*(flatten(nil)@u)) | | | |2* 1...4 | | 5. h:E* | | 6. t:(E* list ) | | 7. p:( list_ind(t;true;h,t,v.s(h)&v) | | => s*(flatten(t)@u)) | | >> ( list_ind(h.t;true;h,t,v.s(h)&v) | | => s*(flatten(h.t)@u)) | '----------------------------------------------'
The first subgoal is disposed of by doing some computation steps on subterms of the consequent of the conclusion. The second subgoal is restated, and the last hypothesis is reduced using a tactic.
,-----------------------------------------------, |* top 1 1 1 2 1 | |1...7. | |8. ( list_ind(h.t;true;h,t,v.s(h)&v) ) | |>> ( s*(flatten(h.t)@u)) | | | |BY compute_hyp_type | | | |1* 1...7. | | 8. s(h)&list_ind(t;true;h,t,v.s(h)&v) | | >> ( s*(flatten(h.t)@u)) | '-----------------------------------------------'
The rest of the proof is just a matter of expanding a few definitions and doing some trivial propositional reasoning.
Now consider Theorem. The proof is abstract with respect to the representation of regular sets; lemmas lemma_1 to lemma_4 and the transitivity of containment are all that is needed. First, the two major branches of the proof are set up.
,-----------------------------------------------, |* top 1 | |1. r:(R(E)) | |2. s:(R(E)) | |>> ( (r*s*)*=(r+s)*) | | | |BY intro | | | |1* 1...2. | | >> ((r*s*)*<(r+s)*) | | | |2* 1...2. | | >> ((r+s)*<(r*s*)*) | '-----------------------------------------------'
The rest of the proof is just lemma application (using lemma application tactics) ; for example, the rule below is actually a definition whose right--hand side calls a tactic which computes from the goal the terms with which to instantiate the named lemma, and then attempts (successfully in this case) to finish the subproof.
+------------------------------------------+ |EDIT THM Theorem | |------------------------------------------| |* top 1 1 1 1 1 | |1. r:(R(E)) | |2. s:(R(E)) | |3. ( r*s*<(r+s)* => r*s**<(r+s)**) | |>> (r*s*<(r+s)* ) | | | |BY Lemma lemma_4 | | | +------------------------------------------+