File: TUTORIAL3-PHONEBOOK-EXAMPLE.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (853 lines) | stat: -rw-r--r-- 32,615 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
<html>
<head><title>TUTORIAL3-PHONEBOOK-EXAMPLE.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>TUTORIAL3-PHONEBOOK-EXAMPLE</h3>A Phonebook Specification
<pre>Major Section:  <a href="TUTORIAL-EXAMPLES.html">TUTORIAL-EXAMPLES</a>
</pre><p>

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 ``<a href="BOOKS.html">books</a>.''<p>

This example was written almost entirely by Bill Young of
Computational Logic, Inc.
<p>
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, <i>et al</i>, 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.<p>

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

<blockquote><p>

Our phone book will store the phone numbers of a city.<p>

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

It must be possible to add and delete entries. <p>

</blockquote>
<p>

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 <code>(key .  value)</code> associating a value with a key.  A phone
book could be an alist of pairs <code>(name . pnum)</code>.  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 <strong>modeling</strong> 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.<p>

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 <a href="BOOKS.html">books</a> are available and what they contain.  We hope later
to improve the documentation of the growing collection of <a href="BOOKS.html">books</a>
available with the ACL2 distribution; for now, the reader is
encouraged to look in the README file in the <code>books</code> subdirectory.
For present purposes, the beginning user can simply take our word
that a book exists containing useful alist definitions and facts.
On our local machine, these definitions and lemmas can be introduced
into the current theory using the <a href="COMMAND.html">command</a>:

<pre><p>

  (include-book "/slocal/src/acl2/v1-9/books/public/alist-defthms")<p>

</pre>

This book has been ``certified,'' which means that the definitions
and lemmas have been mechanically checked and stored in a safe
manner.  (See <a href="BOOKS.html">books</a> and see <a href="INCLUDE-BOOK.html">include-book</a> for details.)<p>

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

<pre><p>

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

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

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

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

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

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

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

</pre>

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

<pre><p>

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

</pre>

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

<pre><p>

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

</pre>

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

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.<p>

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

<blockquote><p>

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

it is (extremely) likely that some useful facts (especially, <a href="REWRITE.html">rewrite</a>
rules) are not available in the book and will have to be proved.<p>

</blockquote>

For example, what is the value of <code>binding</code> 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 <code>binding</code>
function (or any other defined function), using the <code>:</code><code><a href="PE.html">pe</a></code> command:

<pre><p>

  ACL2 !&gt;:pe binding
     d     33  (INCLUDE-BOOK
                    "/slocal/src/acl2/v1-9/books/public/alist-defthms")
               
  &gt;V d          (DEFUN BINDING (X A)
                       "The value bound to X in alist A."
                       (DECLARE (XARGS :GUARD (ALISTP A)))
                       (CDR (ASSOC-EQUAL X A)))<p>

</pre>
<p>

This tells us that <code>binding</code> was introduced by the given
<code><a href="INCLUDE-BOOK.html">include-book</a></code> form, is currently <a href="DISABLE.html">disable</a>d in the current
theory, and has the definition given by the displayed <code><a href="DEFUN.html">defun</a></code> form.
We see that <code>binding</code> is actually defined in terms of the primitive
<code><a href="ASSOC-EQUAL.html">assoc-equal</a></code> function.  If we look at the definition of
<code><a href="ASSOC-EQUAL.html">assoc-equal</a></code>:

<pre><p>

  ACL2 !&gt;:pe assoc-equal
   V     -489  (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)))))<p>

</pre>
<p>

we can see that <code><a href="ASSOC-EQUAL.html">assoc-equal</a></code> returns <code>nil</code> upon reaching the end
of an unsuccessful search down the alist.  So <code>binding</code> returns
<code>(cdr nil)</code> in that case, which is <code>nil</code>.  Notice that we could also
have investigated this question by trying some simple examples.

<pre><p>

  ACL2 !&gt;(binding 'a nil)
  NIL<p>

  ACL2 !&gt;(binding 'a (list (cons 'b 2)))
  NIL<p>

</pre>
<p>

These definitions aren't ideal for all purposes. For one thing,
there's nothing that keeps us from having <code>nil</code> as a value bound to
some key in the alist.  Thus, if <code>binding</code> returns <code>nil</code> 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 <code>binding</code> in our specification.
Suppose instead that we wanted <code>binding</code> to return some error
string on unbound keys.  Well, then we'd just have to write our own
version of <code>binding</code>.  But then we'd lose much of the value of
using a previously defined book.  As with any specification
technique, certain tradeoffs are necessary.<p>

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, the following should work if you start
up ACL2 in the directory of the ACL2 sources:

<pre><p>

  (include-book "books/public/alist-defthms")<p>

</pre>

Then, you can use <code>:</code><a href="PE.html">pe</a> 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 <code>binding</code> is
built on <code><a href="ASSOC-EQUAL.html">assoc-equal</a></code>.  You can look at those as well, of course,
or in many cases visit their documentation.<p>

The other problem with using a predefined book is that it will
seldom be ``sufficiently complete,'' in the sense that the
collection of <a href="REWRITE.html">rewrite</a> 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
<code>binding</code> is built on top of <code><a href="ASSOC-EQUAL.html">assoc-equal</a></code>, because everything
we'd need to know about <code>binding</code> 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 <code>binding</code> and
our other alist functions.  So, let's get on with the example.<p>

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 <strong>partially define</strong> 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 <code><a href="ENCAPSULATE.html">encapsulate</a></code> form.  For example, consider the
following form.

<pre><p>

  (encapsulate
    ;; Introduce a recognizer for names and give a ``type'' lemma.
    (((namep *) =&gt; *))
    ;;
    (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))))<p>

</pre>
 <p>

This <code><a href="ENCAPSULATE.html">encapsulate</a></code> form introduces the new function <code>namep</code> of one
argument and one result and constrains <code>(namep x)</code> to be Boolean,
for all inputs <code>x</code>.  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.<p>

The first ``argument'' to <code>encapsulate</code>, <code>((namep (x) t))</code> above,
declares the intended <a href="SIGNATURE.html">signature</a>s of new function symbols that
will be ``exported'' from the encapsulation without definition.  The
<code><a href="LOCAL.html">local</a></code> <code><a href="DEFUN.html">defun</a></code> of <code>name</code> defines name within the encapsulation
always to return <code>t</code>.  The <code>defthm</code> event establishes that
<code>namep</code> is Boolean.  By making the <code>defun</code> local but the <code>defthm</code>
non-<code>local</code> this encapsulate constrains the undefined function
<code>namep</code> to be Boolean; the admissibility of the encapsulation
establishes that there exists a Boolean function (namely the
constant function returning <code>t</code>).<p>

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

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

<pre><p>

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

</pre>

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

Now a legal phone book is an alist mapping from <code>namep</code>s to
<code>pnump</code>s.  We can define this as follows:

<pre><p>

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

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

</pre>

Thus, a phone book is really a list of pairs <code>(name . pnum)</code>.
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.)<p>

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


<pre><p>

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

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

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

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

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

</pre>
<p>

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.''<p>

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

<pre><p>

  (defun in-book? (nm bk)
    (bound? nm bk))<p>

  (defun find-phone (nm bk)
    (binding nm bk))<p>

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

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

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

</pre>

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

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:

<blockquote><p>

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

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

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

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

5. A name will not be in the book after we delete it.
</blockquote>
<p>

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

<pre><p>

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

</pre>

You may wonder why we didn't need any hypotheses about the ``types''
of the arguments.  In fact, <code>add-in-book</code> 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:

<pre><p>

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

</pre>

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. <p>

There is another, more important observation to make about our
lemma.  Even in its simpler form (without the extraneous
hypotheses), the lemma <code>add-in-book</code> may be useless as a
<a href="REWRITE.html">rewrite</a> rule.  Notice that it is stated in terms of the
non-recursive functions <code>in-book?</code> and <code>add-phone</code>.  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 <a href="TERM.html">term</a> of the form:

<pre><p>

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

</pre>

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

<pre><p>

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

</pre>

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
<a href="DISABLE.html">disable</a> these functions.  <a href="DISABLE.html">Disable</a>d 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 <code>binding</code> is <a href="DISABLE.html">disable</a>d.  If it
were not, none of the lemmas about <code>binding</code> in the book we
included would likely be of much use for exactly the reason we just
gave.<p>

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 <code>:rule-classes nil</code> to each
<code>defthm</code> event; see <a href="RULE-CLASSES.html">rule-classes</a>.<p>

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

<pre><p>

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

</pre>

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 <code>nm</code> is already in the book.  We can remedy this situation by
reformulating our lemma in at least two different ways:

<pre><p>

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

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

</pre>

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

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.

<pre><p>

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

</pre>

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

<pre><p>

  (defthm del-change
    (equal (del-phone nm (change-phone nm pnum bk))
           (del-phone nm bk)))<p>

</pre>

Unfortunately, when we try to prove this, we encounter subgoals that
seem to be true, but for which the prover is stumped.  For example,
consider the following goal.  (Note:  <code>endp</code> holds of lists that
are empty.)

<pre><p>

  Subgoal *1/4
  (IMPLIES (AND (NOT (ENDP BK))
                (NOT (EQUAL NM (CAAR BK)))
                (NOT (BOUND? NM (CDR BK)))
                (BOUND? NM BK))
           (EQUAL (REMBIND NM (BIND NM PNUM BK))
                  (REMBIND NM BK))).<p>

</pre>

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

<pre><p>

  (defthm rembind-bind 
    (equal (rembind nm (bind nm pnum bk))
           (rembind nm bk)))<p>

</pre>

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

The need to prove lemma <code>rembind-bind</code> illustrates a point we made
early in this example:  the collection of <a href="REWRITE.html">rewrite</a> 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 <code>rembind</code> and <code>bind</code> that
wasn't supplied with the alists theory.  Hopefully, such omissions
will be rare.<p>

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:

<pre><p>

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

</pre>

This proves easily.  But notice that it's only true because
<code>del-phone</code> (actually <code>rembind</code>) removes <strong>all</strong> 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 <code>nm</code> occurs at
most once in <code>bk</code>.  Ah, maybe that's a property you hadn't
considered.  Maybe you want to ensure that <strong>any</strong> name occurs at
most once in any valid phonebook.<p>

To complete this example, let's consider adding an <strong>invariant</strong> to
our specification.  In particular, suppose we want to assure 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).

<pre><p>

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

  (defun valid-phonebookp (bk)
    (and (phonebookp bk)
         (setp (domain bk))))<p>

</pre>

Now, we want to show under what conditions our operations preserve
the property of being a <code>valid-phonebookp</code>.  The operations
<code>in-book?</code>  and <code>find-phone</code> 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.

<pre><p>

  (defthm in-book-booleanp
    (booleanp (in-book? nm bk)))<p>

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

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

</pre>

Note the ``<code>:</code><code><a href="HINTS.html">hints</a></code>'' on the last two lemmas.  Neither of these
would prove without these <a href="HINTS.html">hints</a>, because once again there are
some facts about <code>bound?</code> and <code>binding</code> not available in our
current context.  Now, we could figure out what those facts are and
try to prove them.  Alternatively, we can <a href="ENABLE.html">enable</a> <code>bound?</code> and
<code>binding</code> and hope that by opening up these functions, the
conjectures will reduce to versions that the prover does know enough
about or can prove by induction.  In this case, this strategy works.
The hints tell the prover to <a href="ENABLE.html">enable</a> the functions in question
when considering the designated goal.<p>

Below we develop the theorems showing that <code>add-phone</code>,
<code>change-phone</code>, and <code>del-phone</code> 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, <code>add-phone-preserves-invariant</code> without introducing the
following four lemmas first.  See if you can develop the proof and
only add these lemmas as you need assistance.  Then try
<code>change-phone-preserves-invariant</code> and <code>del-phone-preserves-invariant</code>.
They will be easier.  It is illuminating to think about why
<code>del-phone-preserves-invariant</code> does not need any ``type''
hypotheses.

<pre><p>

  (defthm bind-preserves-phonebookp
    (implies (and (phonebookp bk)
                  (namep nm)
                  (pnump num))
             (phonebookp (bind nm num bk))))
  
  (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))))))
  
  (defthm bind-preserves-domain-setp 
    (implies (and (alistp bk)
                  (setp (domain bk)))
             (setp (domain (bind nm num bk))))
    :hints (("Goal" :in-theory (enable domain))))
  
  (defthm phonebookp-alistp
    (implies (phonebookp bk)
             (alistp 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))))
  
  (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))))
  
  (defthm remove-equal-preserves-setp
    (implies (setp l)
             (setp (remove-equal x l))))
  
  (defthm rembind-preserves-phonebookp 
    (implies (phonebookp bk)
             (phonebookp (rembind nm bk))))
  
  (defthm DEL-PHONE-PRESERVES-INVARIANT
    (implies (valid-phonebookp bk)
             (valid-phonebookp (del-phone nm bk))))
</pre>
<p>

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.

<blockquote><p>

1. Define the appropriate invariant.  (Hint: remember the function
<code>range</code>.)<p>

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

3. Study the definition of the function <code>range</code> and notice that it
is defined in terms of the function <code><a href="STRIP-CDRS.html">strip-cdrs</a></code>.  Understand how
this defines the range of an alist.<p>

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 <code><a href="STRIP-CDRS.html">strip-cdrs</a></code>
analogous to the lemma <code>member-equal-strip-cars-bind</code> above.<p>

</blockquote>
<p>

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 <code>add-phone</code> and
<code>change-phone</code>, 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.

<pre><p>

  (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 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? x a))
                  (alistp a))
             (equal (strip-cdrs (bind x y a))
                    (append (strip-cdrs a) (list y))))
    :hints (("Goal" :in-theory (enable bound?))))
  
  (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
    (implies (and (not (member-equal z (strip-cdrs a)))
                  (not (equal z y)))
             (not (member-equal z (strip-cdrs (bind 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))))
</pre>


<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>