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

**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

>> E* list -> E* BY explicit intro \x. list_ind(x;nil;h,t,v.h@v)The definitions of containment, ``

<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(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

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 | | | +------------------------------------------+

Thu Sep 14 08:45:18 EDT 1995