		Search-engine friendly clone of the ACL2 documentation.

Annotated-ACL2-scripts

Tutorial3-phonebook-example

A Phonebook Specification

The other tutorial examples are rather small and entirely self contained. The present example is rather more elaborate, and makes use of a feature that really adds great power and versatility to ACL2, namely: the use of previously defined collections of lemmas, in the form of ``books.''

This example was written almost entirely by Bill Young of Computational Logic, Inc. It was updated in December, 2024 (from the original version of about two decades ago) thanks to Andrei Koltsov, to work with recent ACL2 versions.

This example is based on one developed by Ricky Butler and Sally Johnson of NASA Langley for the PVS system, and subsequently revised by Judy Crow, et al, at SRI. It is a simple phone book specification. We will not bother to follow their versions closely, but will instead present a style of specification natural for ACL2.

The idea is to model an electronic phone book with the following properties.

Our phone book will store the phone numbers of a city.

It must be possible to retrieve a phone number, given a name.

It must be possible to add and delete entries.

Of course, there are numerous ways to construct such a model. A natural approach within the Lisp/ACL2 context is to use ``association lists'' or ``alists.'' Briefly, an alist is a list of pairs (key . value) associating a value with a key. A phone book could be an alist of pairs (name . pnum). To find the phone number associated with a given name, we merely search the alist until we find the appropriate pair. For a large city, such a linear list would not be efficient, but at this point we are interested only in modeling the problem, not in deriving an efficient implementation. We could address that question later by proving our alist model equivalent, in some desired sense, to a more efficient data structure.

We could build a theory of alists from scratch, or we can use a previously constructed theory (book) of alist definitions and facts. By using an existing book, we build upon the work of others, start our specification and proof effort from a much richer foundation, and hopefully devote more of our time to the problem at hand. Unfortunately, it is not completely simple for the new user to know what books are available and what they contain. Documentation is available for the growing collection of community-books that are typically downloaded with ACL2, and a mailing list, acl2-help, is available (see the ACL2 home page. For present purposes, the beginning user can simply take our word that a book exists containing useful alist definitions and facts. These definitions and lemmas can be introduced into the current theory using the command:

(include-book "data-structures/alist-defthms" :dir :system)

This book has been ``certified,'' which means that the definitions and lemmas have been mechanically checked and stored in a safe manner. (See books and see include-book for details.)

Including this book makes available a collection of functions including the following:

(ALISTP A)    ; is A an alist (actually a primitive ACL2 function)

(BIND X V A)  ; associate the key X with value V in alist A

(BINDING X A) ; return the value associated with key X in alist A

(BOUND? X A)  ; is key X associated with any value in alist A

(DOMAIN A)    ; return the list of keys bound in alist A

(RANGE A)     ; return the list of values bound to keys in alist A

(REMBIND X A) ; remove the binding of key X in alist A

Along with these function definitions, the book also provides a number of proved lemmas that aid in simplifying expressions involving these functions. (See rule-classes for the way in which lemmas are used in simplification and rewriting.) For example,

(defthm bound?-bind
  (equal (bound? x (bind y v a))
         (or (equal x y)
             (bound? x a))))

asserts that x will be bound in (bind y v a) if and only if: either x = y or x was already bound in a. Also,

(defthm binding-bind
  (equal (binding x (bind y v a))
         (if (equal x y)
             v
           (binding x a))))

asserts that the resulting binding will be v, if x = y, or the binding that x had in a already, if not.

Thus, the inclusion of this book essentially extends our specification and reasoning capabilities by the addition of new operations and facts about these operations that allow us to build further specifications on a richer and possibly more intuitive foundation.

However, it must be admitted that the use of a book such as this has two potential limitations:

the definitions available in a book may not be ideal for your particular problem;

it is (extremely) likely that some useful facts (especially, rewrite rules) are not available in the book and will have to be proved.

For example, what is the value of binding when given a key that is not bound in the alist? We can find out by examining the function definition. Look at the definition of the binding function (or any other defined function), using the :pe command:

ACL2 !>:pe binding
   d   1  (INCLUDE-BOOK "data-structures/alist-defthms"
                        :DIR ...)
          
          [Included books, outermost to innermost:
           ".../acl2/books/data-structures/alist-defthms.lisp"
           ".../acl2/books/data-structures/alist-defuns.lisp"
          ]
          
>V d       (DEFUN
            BINDING (X A)
            "The value bound to X in alist A."
            (DECLARE
               (XARGS :GUARD (AND (ALISTP A)
                                  (OR (EQLABLEP X) (EQLABLE-ALISTP A)))))
            (CDR (ASSOC X A)))

This tells us that binding was introduced by the given include-book form, is currently disabled in the current theory, and has the definition given by the displayed defun form. We see that binding is actually defined in terms of the primitive assoc. If we submit :pe assoc then we can see that assoc is a macro that essentially serves as an abbreviation for the primitive function assoc-equal. We say no more about assoc here but instead focus on assoc-equal. If we use :pe to look at the definition of assoc-equal:

PV    -8489  (DEFUN ASSOC-EQUAL (X ALIST)
               (DECLARE (XARGS :GUARD (ALISTP ALIST)))
               (COND ((ENDP ALIST) NIL)
                     ((EQUAL X (CAR (CAR ALIST)))
                      (CAR ALIST))
                     (T (ASSOC-EQUAL X (CDR ALIST)))))

we can see that assoc-equal returns nil upon reaching the end of an unsuccessful search down the alist. So binding returns (cdr nil) in that case, which is nil. Notice that we could also have investigated this question by trying some simple examples.

ACL2 !>(binding 'a nil)
NIL

ACL2 !>(binding 'a (list (cons 'b 2)))
NIL

These definitions aren't ideal for all purposes. For one thing, there's nothing that keeps us from having nil as a value bound to some key in the alist. Thus, if binding returns nil we don't always know if that is the value associated with the key in the alist, or if that key is not bound. We'll have to keep that ambiguity in mind whenever we use binding in our specification. Suppose instead that we wanted binding to return some error string on unbound keys. Well, then we'd just have to write our own version of binding. But then we'd lose much of the value of using a previously defined book. As with any specification technique, certain tradeoffs are necessary.

Why not take a look at the definitions of other alist functions and see how they work together to provide the ability to construct and search alists? We'll be using them rather heavily in what follows so it will be good if you understand basically how they work. Simply start up ACL2 and execute the form shown earlier, but substituting our directory name for the top-level ACL2 directory with yours. Alternatively, just

(include-book "data-structures/alist-defthms" :dir :system)

Then, you can use :pe to look at function definitions. You'll soon discover that almost all of the definitions are built on definitions of other, more primitive functions, as binding is built on assoc-equal. You can look at those as well, of course, or in many cases visit their documentation.

The other problem with using a predefined book is that it will seldom be ``sufficiently complete,'' in the sense that the collection of rewrite rules supplied won't be adequate to prove everything we'd like to know about the interactions of the various functions. If it were, there'd be no real reason to know that binding is built on top of assoc-equal, because everything we'd need to know about binding would be nicely expressed in the collection of theorems supplied with the book. However, that's very seldom the case. Developing such a collection of rules is currently more art than science and requires considerable experience. We'll encounter examples later of ``missing'' facts about binding and our other alist functions. So, let's get on with the example.

Notice that alists are mappings of keys to values; but, there is no notion of a ``type'' associated with the keys or with the values. Our phone book example, however, does have such a notion of types; we map names to phone numbers. We can introduce these ``types'' by explicitly defining them, e.g., names are strings and phone numbers are integers. Alternatively, we can partially define or axiomatize a recognizer for names without giving a full definition. A way to safely introduce such ``constrained'' function symbols in ACL2 is with the encapsulate form. For example, consider the following form.

(encapsulate
  ;; Introduce a recognizer for names and give a ``type'' lemma.
  (((namep *) => *))
  ;;
  (local (defun namep (x)
           ;; This declare is needed to tell
           ;; ACL2 that we're aware that the
           ;; argument x is not used in the body
           ;; of the function.
           (declare (ignore x))
           t))
  ;;
  (defthm namep-booleanp
    (booleanp (namep x))))

This encapsulate form introduces the new function namep of one argument and one result and constrains (namep x) to be Boolean, for all inputs x. More generally, an encapsulation establishes an environment in which functions can be defined and theorems and rules added without necessarily introducing those functions, theorems, and rules into the environment outside the encapsulation. To be admissible, all the events in the body of an encapsulate must be admissible. But the effect of an encapsulate is to assume only the non-local events.

The first ``argument'' to encapsulate, (((namep *) => *)) above, declares the intended signatures of new function symbols that will be ``exported'' from the encapsulation without definition. The local defun of name defines name within the encapsulation always to return t. The defthm event establishes that namep is Boolean. By making the defun local but the defthm non-local this encapsulate constrains the undefined function namep to be Boolean; the admissibility of the encapsulation establishes that there exists a Boolean function (namely the constant function returning t).

We can subsequently use namep as we use any other Boolean function, with the proviso that we know nothing about it except that it always returns either t or nil. We use namep to ``recognize'' legal keys for our phonebook alist.

We wish to do something similar to define what it means to be a legal phone number. We submit the following form to ACL2.

(encapsulate
  ;; Introduce a recognizer for phone numbers.
  (((pnump *) => *))
  ;;
  (local (defun pnump (x)
           (not (equal x nil))))
  ;;
  (defthm pnump-booleanp
    (booleanp (pnump x)))
  ;;
  (defthm nil-not-pnump
    (not (pnump nil))))

This introduces a Boolean-valued recognizer pnump, with the additional proviso that the constant nil is not a pnump. We impose this restriction to guarantee that we'll never bind a name to nil in our phone book and thereby introduce the kind of ambiguity described above regarding the use of binding.

Now a legal phone book is an alist mapping from nameps to pnumps. We can define this as follows:

(defun name-phonenum-pairp (x)
  ;; Recognizes a pair of (name . pnum).
  (and (consp x)
       (namep (car x))
       (pnump (cdr x))))

(defun phonebookp (l)
  ;; Recognizes a list of such pairs.
  (if (not (consp l))
      (null l)
    (and (name-phonenum-pairp (car l))
         (phonebookp (cdr l)))))

Thus, a phone book is really a list of pairs (name . pnum). Notice that we have not assumed that the keys of the phone book are distinct. We'll worry about that question later. (It is not always desirable to insist that the keys of an alist be distinct. But it may be a useful requirement for our specific example.)

Now we are ready to define some of the functions necessary for our phonebook example. The functions we need are:

(IN-BOOK? NM BK)          ; does NM have a phone number in BK

(FIND-PHONE NM BK)        ; find NM's phone number in phonebook BK

(ADD-PHONE NM PNUM BK)    ; give NM the phone number PNUM in BK

(CHANGE-PHONE NM PNUM BK) ; change NM's phone number to PNUM in BK

(DEL-PHONE NM PNUM)       ; remove NM's phone number from BK

Given our underlying theory of alists, it is easy to write these functions. But we must take care to specify appropriate ``boundary'' behavior. Thus, what behavior do we want when, say, we try to change the phone number of a client who is not currently in the book? As usual, there are numerous possibilities; here we'll assume that we return the phone book unchanged if we try anything ``illegal.''

Possible definitions of our phone book functions are as follows. (Remember, an include-book form such as the ones shown earlier must be executed in order to provide definitions for functions such as bound?.)

(defun in-book? (nm bk)
  (bound? nm bk))

(defun find-phone (nm bk)
  (binding nm bk))

(defun add-phone (nm pnum bk)
  ;; If nm already in-book?, make no change.
  (if (in-book? nm bk)
      bk
    (bind nm pnum bk)))

(defun change-phone (nm pnum bk)
  ;; Make a change only if nm already has a phone number.
  (if (in-book? nm bk)
      (bind nm pnum bk)
    bk))

(defun del-phone (nm bk)
  ;; Remove the binding from bk, if there is one.
  (rembind nm bk))

Notice that we don't have to check whether a name is in the book before deleting, because rembind is essentially a no-op if nm is not bound in bk.

In some sense, this completes our specification. But we can't have any real confidence in its correctness without validating our specification in some way. One way to do so is by proving some properties of our specification. Some candidate properties are:

1. A name will be in the book after we add it.

2. We will find the most recently added phone number for a client.

3. If we change a number, we'll find the change.

4. Changing and then deleting a number is the same as just deleting.

5. A name will not be in the book after we delete it.

Let's formulate some of these properties. The first one, for example, is:

(defthm add-in-book
  (in-book? nm (add-phone nm pnum bk))).

You may wonder why we didn't need any hypotheses about the ``types'' of the arguments. In fact, add-in-book is really expressing a property that is true of alists in general, not just of the particular variety of alists we are dealing with. Of course, we could have added some extraneous hypotheses and proved

(defthm add-in-book
  (implies (and (namep nm)
                (pnump pnum)
                (phonebookp bk))
           (in-book? nm (add-phone nm pnum bk))))

but that would have yielded a weaker and less useful lemma because it would apply to fewer situations. In general, it is best to state lemmas in the most general form possible and to eliminate unnecessary hypotheses whenever possible. The reason for that is simple: lemmas are usually stored as rules and used in later proofs. For a lemma to be used, its hypotheses must be relieved (proved to hold in that instance); extra hypotheses require extra work. So we avoid them whenever possible.

There is another, more important observation to make about our lemma. Even in its simpler form (without the extraneous hypotheses), the lemma add-in-book may be useless as a rewrite rule. Notice that it is stated in terms of the non-recursive functions in-book? and add-phone. If such functions appear in the left hand side of the conclusion of a lemma, the lemma may not ever be used. Suppose in a later proof, the theorem prover encountered a term of the form:

(in-book? nm (add-phone nm pnum bk)).

Since we've already proved add-in-book, you'd expect that this would be immediately reduced to true. However, the theorem prover will often ``expand'' the non-recursive definitions of in-book? and add-phone using their definitions before it attempts rewriting with lemmas. After this expansion, lemma add-in-book won't ``match'' the term and so won't be applied. Look back at the proof script for add-in-proof and you'll notice that at the very end the prover warned you of this potential difficulty when it printed:

Warnings:  Non-rec
Time:  0.18 seconds (prove: 0.05, print: 0.00, other: 0.13)
ADD-IN-BOOK

The ``Warnings'' line notifies you that there are non-recursive function calls in the left hand side of the conclusion and that this problem might arise. Of course, it may be that you don't ever plan to use the lemma for rewriting or that your intention is to disable these functions. Disabled functions are not expanded and the lemma should apply. However, you should always take note of such warnings and consider an appropriate response. By the way, we noted above that binding is disabled. If it were not, none of the lemmas about binding in the book we included would likely be of much use for exactly the reason we just gave.

For our current example, let's assume that we're just investigating the properties of our specifications and not concerned about using our lemmas for rewriting. So let's go on. If we really want to avoid the warnings, we can add :rule-classes nil to each defthm event; see rule-classes.

Property 2 is: we always find the most recently added phone number for a client. Try the following formalization:

(defthm find-add-first-cut
  (equal (find-phone nm (add-phone nm pnum bk))
         pnum))

and you'll find that the proof attempt fails. Examining the proof attempt and our function definitions, we see that the lemma is false if nm is already in the book. We can remedy this situation by reformulating our lemma in at least two different ways:

(defthm find-add1
  (implies (not (in-book? nm bk))
           (equal (find-phone nm (add-phone nm pnum bk))
                  pnum)))

(defthm find-add2
  (equal (find-phone nm (add-phone nm pnum bk))
         (if (in-book? nm bk)
             (find-phone nm bk)
             pnum)))

For technical reasons, lemmas such as find-add2, i.e., which do not have hypotheses, are usually slightly preferable. This lemma is stored as an ``unconditional'' rewrite rule (i.e., has no hypotheses) and, therefore, will apply more often than find-add1. However, for our current purposes either version is all right.

Property 3 says: If we change a number, we'll find the change. This is very similar to the previous example. The formalization is as follows.

(defthm find-change
  (equal (find-phone nm (change-phone nm pnum bk))
         (if (in-book? nm bk)
             pnum
           (find-phone nm bk))))

Property 4 says: changing and then deleting a number is the same as just deleting. We can model this as follows.

(defthm del-change
  (equal (del-phone nm (change-phone nm pnum bk))
         (del-phone nm bk)))

Unfortunately, our attempt to prove it failed with the following subgoal under a top-level induction.

Subgoal *1/4''
(IMPLIES (AND (CONSP BK)
              (NOT (EQUAL NM (CAR (CAR BK))))
              (NOT (BOUND?-EQUAL NM (CDR BK)))
              (BOUND?-EQUAL NM BK))
         (EQUAL (REMBIND-EQUAL NM (BIND-EQUAL NM PNUM (CDR BK)))
                (REMBIND-EQUAL NM (CDR BK))))

We have defined del-phone using rembind, and change-phone using in-book (which uses bound?) and bind; but we have ``equal'' suffixes in the subgoal. The cause is theorems of the form ***->***-equal, which are given in the included book. We can use history's :pl command to print the rules for a given name or term. Here is the part of :pl's output we are interested in now, for the rembind function:

ACL2 !>:pl rembind
...

Rune:         (:REWRITE REMBIND->REMBIND-EQUAL)
Enabled:      T
Hyps:         T
Equiv:        EQUAL
Lhs:          (REMBIND X A)
Rhs:          (REMBIND-EQUAL X A)
Backchain-limit-lst: NIL
Subclass:     ABBREVIATION

...

We can see that rewrite rule rembind->rembind-equal is enabled and that it replaces lhs with rhs. For functions bind, binding and bound? we have similar rules.

Our intuition about rembind and bind tells us that this goal should be true even without the hypotheses. We attempt to prove the following lemma.

(defthm rembind-equal-bind-equal
  (equal (rembind-equal nm (bind-equal nm pnum bk))
         (rembind-equal nm bk)))

The prover proves this by induction, and stores it as a rewrite rule. After that, the prover has no difficulty in proving del-change.

The need to prove lemma rembind-equal-bind-equal illustrates a point we made early in this example: the collection of rewrite rules supplied by a previously certified book will almost never be everything you'll need. It would be nice if we could operate purely in the realm of names, phone numbers, and phone books without ever having to prove any new facts about alists. Unfortunately, we needed a fact about the relation between rembind-equal and bind-equal that wasn't supplied with the alists theory. Hopefully, such omissions will be rare.

Let's take two steps back now (just enter the :u command twice) to get acquainted with a method that will be very useful to us. What happens if we state the previous lemma another way?

(defthm rembind-bind
  (equal (rembind name (bind name num book))
         (rembind name book)))

An attempt to prove del-change would fail then with the same subgoal as above. In this case we can give to the prover the hint to use rembind-bind as an instance of del-change (see hints and find keywords :use and :instance):

(defthm del-change-lemma-instance-example
  (equal (del-phone nm (change-phone nm pnum bk))
         (del-phone nm bk))
  :hints (("Goal" :use (:instance rembind-bind
                                  (name nm)
                                  (num pnum)
                                  (book bk)))))

As described in hints, a :use hint causes the prover to replace a goal G with new goal (IMPLIES P G), where P is the specified theorem to use. The :instance form specifies instantiation of the free variables of a previously proved theorem. See lemma-instance for more information on this subject.

Finally, let's consider our property 5 above: a name will not be in the book after we delete it. We formalize this as follows:

(defthm in-book-del
  (not (in-book? nm (del-phone nm bk))))

This proves easily. But notice that it's only true because del-phone (actually rembind) removes all occurrences of a name from the phone book. If it only removed, say, the first one it encountered, we'd need a hypothesis that said that nm occurs at most once in bk. Ah, maybe that's a property you hadn't considered. Maybe you want to ensure that any name occurs at most once in any valid phonebook.

To complete this example, let's consider adding an invariant to our specification. In particular, suppose we want to ensure that no client has more than one associated phone number. One way to ensure this is to require that the domain of the alist is a ``set'' (has no duplicates).

(defun setp (l)
  (if (atom l)
      (null l)
    (and (not (member-equal (car l) (cdr l)))
         (setp (cdr l)))))

(defun valid-phonebookp (bk)
  (and (phonebookp bk)
       (setp (domain bk))))

Now, we want to show under what conditions our operations preserve the property of being a valid-phonebookp. The operations in-book? and find-phone don't return a phone book, so we don't really need to worry about them. Since we're really interested in the ``types'' of values preserved by our phonebook functions, let's look at the types of those operations as well.

(defthm in-book-booleanp
  (booleanp (in-book? nm bk)))

(defthm in-book-namep
  (implies (and (phonebookp bk)
                (in-book? nm bk))
           (namep nm))
  :hints (("Goal" :in-theory (enable bound?-equal))))

(defthm find-phone-pnump
  (implies (and (phonebookp bk)
                (in-book? nm bk))
           (pnump (find-phone nm bk)))
  :hints (("Goal" :in-theory (enable bound?-equal
                                     binding-equal))))

Note the ``:hints'' on the last two lemmas. Neither of these would prove without these hints, because once again there are some facts about bound?-equal and binding-equal not available in our current context. Now, we could figure out what those facts are and try to prove them. Alternatively, we can enable bound?-equal and binding-equal and hope that by opening up these functions, the conjectures will reduce to versions that the prover does know enough about, perhaps using proof by induction. In this case, this strategy works. The hints tell the prover to enable the functions in question when considering the designated goal and any subgoals of it.

It's important to understand that it's not enough to enable the bound? and binding functions. That's because rewrite rules of the form ***->***-equal (mentioned above) will replace enabled functions with disabled ones for which there are not sufficient rules to complete the proof. We can use history's very informative command :pl to get a lot of information about rules for a given name.

Below we develop the theorems showing that add-phone, change-phone, and del-phone preserve our proposed invariant. Notice that along the way we have to prove some subsidiary facts, some of which are pretty ugly. It would be a good idea for you to try, say, add-phone-preserves-invariant without introducing the following four lemmas first. Perhaps you will use the instantiation of lemmas method, described above. See if you can develop the proof and only add these lemmas as you need assistance. Then try change-phone-preserves-invariant and del-phone-preserves-invariant. They will be easier. It is illuminating to think about why del-phone-preserves-invariant does not need any ``type'' hypotheses.

(defthm bind-preserves-phonebookp
  (implies (and (phonebookp bk)
                (namep nm)
                (pnump num))
           (phonebookp (bind nm num bk))))

(defthm member-equal-strip-cars-bind-equal
  (implies (and (not (equal x y))
                (not (member-equal x (strip-cars a))))
           (not (member-equal x (strip-cars (bind-equal y z a))))))

(defthm bind-equal-preserves-domain-setp
  (implies (and (alistp bk)
                (setp (domain bk)))
           (setp (domain (bind-equal nm num bk))))
  :hints (("Goal" :in-theory (enable domain))))

Let's take two steps back (using :u twice) and prove the following instead of member-equal-strip-cars-bind-equal:

(defthm member-equal-strip-cars-bind
  (implies (and (not (equal x y))
                (not (member-equal x (strip-cars a))))
           (not (member-equal x (strip-cars (bind y z a))))))

Then bind-equal-preserves-domain-setp fails:

Subgoal *1/5''
(IMPLIES (AND (CONSP BK)
         (NOT (EQUAL NM (CAR (CAR BK))))
         (SETP (STRIP-CARS (BIND-EQUAL NM NUM (CDR BK))))
         (CONSP (CAR BK))
         (ALISTP (CDR BK))
         (NOT (MEMBER-EQUAL (CAR (CAR BK))
                            (STRIP-CARS (CDR BK))))
         (SETP (STRIP-CARS (CDR BK))))
    (NOT (MEMBER-EQUAL (CAR (CAR BK))
                       (STRIP-CARS (BIND-EQUAL NM NUM (CDR BK))))))

We can use a lemma-instance to prove it:

(defthm bind-equal-preserves-domain-setp
  (implies (and (alistp bk)
                (setp (domain bk)))
           (setp (domain (bind-equal nm num bk))))
  :hints (("Goal" :in-theory (enable domain))
          ("Subgoal *1/5''" :use (:instance
                                  member-equal-strip-cars-bind
                                  (x (car (car bk)))
                                  (y nm)
                                  (z num)
                                  (a (cdr bk))))))

The use of lemma-instance is somewhat artificial in this example, but this method gives great opportunities to lead ACL2 in proving theorems. That said, it is generally preferable to avoid :use hints in favor of developing a useful set of rewrite rules, since those rules can help to automate future proof attempts.

We continue now with proofs that our operations preserve the phonebook' invariant.

(defthm phonebookp-alistp
  (implies (phonebookp bk)
           (alistp bk)))

(defthm bind-equal-preserves-phonebookp
  (implies (and (phonebookp bk)
                (namep nm)
                (pnump num))
           (phonebookp (bind-equal nm num bk))))

(defthm add-phone-preserves-invariant
  (implies (and (valid-phonebookp bk)
                (namep nm)
                (pnump num))
           (valid-phonebookp (add-phone nm num bk)))
  :hints (("Goal" :in-theory (disable domain-bind-equal))))

(defthm change-phone-preserves-invariant
  (implies (and (valid-phonebookp bk)
                (namep nm)
                (pnump num))
           (valid-phonebookp (change-phone nm num bk)))
  :hints (("Goal" :in-theory (disable domain-bind-equal))))

(defthm member-remove-equal
  (implies (and (not (equal a b))
                (not (member a x)))
           (not (member a (remove-equal b x)))))

(defthm remove-equal-preserves-setp
  (implies (setp l)
           (setp (remove-equal x l))))

(defthm del-phone-preserves-invariant
  (implies (valid-phonebookp bk)
           (valid-phonebookp (del-phone nm bk))))

As a final test of your understanding, try to formulate and prove an invariant that says that no phone number is assigned to more than one name. The following hints may help.

1. Define the appropriate invariant. (Hint: remember the function range.)

2. Do our current definitions of add-phone and change-phone necessarily preserve this property? If not, consider what hypotheses are necessary in order to guarantee that they do preserve this property.

3. Study the definition of the function range and notice that it is defined in terms of the function strip-cdrs. Understand how this defines the range of an alist.

4. Formulate the correctness theorems and attempt to prove them. You'll probably benefit from studying the invariant proof above. In particular, you may need some fact about the function strip-cdrs analogous to the lemma member-equal-strip-cars-bind above.

Below is one solution to this exercise. Don't look at the solution, however, until you've struggled a bit with it. Notice that we didn't actually change the definitions of add-phone and change-phone, but added a hypothesis saying that the number is ``new.'' We could have changed the definitions to check this and return the phonebook unchanged if the number was already in use.

(defun pnums-in-use (bk)
  (range bk))

(defun phonenums-unique (bk)
  (setp (pnums-in-use bk)))

(defun new-pnump (pnum bk)
  (not (member-equal pnum (pnums-in-use bk))))

(defthm member-equal-strip-cdrs-rembind
  (implies (not (member-equal x (strip-cdrs y)))
           (not (member-equal x (strip-cdrs
                                 (rembind-equal z y))))))

(defthm del-phone-preserves-phonenums-unique
  (implies (phonenums-unique bk)
           (phonenums-unique (del-phone nm bk)))
  :hints (("Goal" :in-theory (enable range))))

(defthm strip-cdrs-bind-non-member
  (implies (and (not (bound?-equal x a))
                (alistp a))
           (equal (strip-cdrs (bind-equal x y a))
                  (append (strip-cdrs a) (list y))))
  :hints (("Goal" :in-theory (enable bound?-equal))))

(defthm member-append
  (iff (member e (append x y))
       (or (member e x)
           (member e y))))

(defthm setp-append-list
  (implies (setp l)
           (equal (setp (append l (list x)))
                  (not (member-equal x l)))))

(defthm add-phone-preserves-phonenums-unique
  (implies (and (phonenums-unique bk)
                (new-pnump pnum bk)
                (alistp bk))
           (phonenums-unique (add-phone nm pnum bk)))
  :hints (("Goal" :in-theory (enable range))))

(defthm member-equal-strip-cdrs-bind-equal
  (implies (and (not (member-equal z (strip-cdrs a)))
                (not (equal z y)))
           (not (member-equal z (strip-cdrs
                                 (bind-equal x y a))))))

(defthm change-phone-preserves-phonenums-unique
  (implies (and (phonenums-unique bk)
                (new-pnump pnum bk)
                (alistp bk))
           (phonenums-unique (change-phone nm pnum bk)))
  :hints (("Goal" :in-theory (enable range))))