next up previous contents index
Next: Real Analysis Up: Mathematics Libraries Previous: Cardinality

Regular Sets

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 gif 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 gif 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 gif 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.                  
           & 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                          |
|                                          |

next up previous contents index
Next: Real Analysis Up: Mathematics Libraries Previous: Cardinality

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