← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2004/davis/support/membership.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2004/davis/support/membership.lisp
 
1
; Fully Ordered Finite Sets, Version 0.9
 
2
; Copyright (C) 2003, 2004 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
;
 
31
; Original author: Jared Davis <jared@kookamara.com>
 
32
;
 
33
;
 
34
; membership.lisp
 
35
;
 
36
; We are now getting into more interesting territory.  The primitive set
 
37
; functions nicely contain the potential messes that we would have to face if
 
38
; we were implementing sets just using the primitive list functions.  However,
 
39
; they are still plagued with order.
 
40
;
 
41
; The end user of the set library should not have to care that the elements of
 
42
; the set are ordered or not.  (Well, with the exception that if they are
 
43
; trying to make a fast version of a function, they might decide to exploit
 
44
; that order.)
 
45
;
 
46
; Set reasoning should be done in terms of membership.  In traditional
 
47
; mathematics, subsets are defined through quantification over membership, as
 
48
; is set equailty, and so forth.  But right now, the best we can do is induct
 
49
; over insert, which is somewhat messy.
 
50
;
 
51
; This file introduces the notions of set membership and subset.  We also go
 
52
; into an abstract argument which will form the basis for quantification.  The
 
53
; goal is to transform the insertion induction proofs into more traditional
 
54
; pick-a-point and double containment proofs.
 
55
;
 
56
; At the end of this file, we will disable all of the theorems that pertain to
 
57
; the order of elements, providing an entirely membership-based reasoning
 
58
; environment for the outer level.
 
59
 
 
60
(in-package "SET")
 
61
(include-book "primitives")
 
62
(include-book "computed-hints")
 
63
(set-verify-guards-eagerness 2)
 
64
 
 
65
 
 
66
 
 
67
;;; Set Membership.
 
68
;;;
 
69
;;; We could go ahead and write another version of in, which could use
 
70
;;; the total order to stop early if it ever encountered an element
 
71
;;; too big.  I.e., looking for 1 in the list '(2 3 4), it could say
 
72
;;; that since 1 << 2, we are done.
 
73
;;;
 
74
;;; Should we do so?  Really the only question is whether or not it
 
75
;;; would be faster.  Certainly we can contrive situations in which it
 
76
;;; would be better, i.e. (in 1 '(2 3 4 .... 100000)), where we would
 
77
;;; save 100,000 calls to in.  But we can also contrive situations
 
78
;;; that it would be slower, for example (in 100001 '(1 2 3 4
 
79
;;; ... 100000)), where we would incur the extra cost of 100,000 calls
 
80
;;; to <<.
 
81
;;;
 
82
;;; I have arbitrarily decided not to implement short-circuiting.  My
 
83
;;; reasoning is that (1) it is not clear which would be faster, (2)
 
84
;;; it is not clear what "typical" usage behavior of in would be, so
 
85
;;; even if we wanted to benchmark the two solutions, we could
 
86
;;; probably not come up with a good benchmarking suite, (3) both
 
87
;;; solutions are O(n) anyway so I don't think there's much to be
 
88
;;; gained here, and (4) the current method is arguably "no less
 
89
;;; efficient" than an unordered implementation.
 
90
 
 
91
(defun in (a X)
 
92
  (declare (xargs :guard (setp X)))
 
93
  (and (not (empty X))
 
94
       (or (equal a (head X))
 
95
           (in a (tail X)))))
 
96
 
 
97
(defthm in-type
 
98
  (or (equal (in a X) t)
 
99
      (equal (in a X) nil))
 
100
  :rule-classes :type-prescription)
 
101
 
 
102
(encapsulate ()
 
103
 
 
104
  (local (defthm lemma
 
105
    (implies (> (acl2-count x) (acl2-count y))
 
106
             (not (in x y)))))
 
107
 
 
108
  (defthm not-in-self
 
109
    (not (in x x)))
 
110
 
 
111
)
 
112
 
 
113
(defthm in-sfix-cancel
 
114
  (equal (in a (sfix X)) (in a X)))
 
115
 
 
116
(defthm never-in-empty
 
117
  (implies (empty X) (not (in a X))))
 
118
 
 
119
(defthm in-set
 
120
  (implies (in a X) (setp X)))
 
121
 
 
122
(defthm in-tail
 
123
  (implies (in a (tail X)) (in a X)))
 
124
 
 
125
(defthm in-tail-or-head
 
126
  (implies (and (in a X)
 
127
                (not (in a (tail X))))
 
128
           (equal (head X) a)))
 
129
 
 
130
 
 
131
;;; We now begin to move away from set order.
 
132
 
 
133
(encapsulate ()
 
134
 
 
135
  (local (defthm lemma
 
136
           (implies (and (not (empty X))
 
137
                         (not (equal a (head X)))
 
138
                         (not (<< a (head (tail X))))
 
139
                         (<< a (head X)))
 
140
                    (not (in a X)))
 
141
           :hints(("Goal"
 
142
                   :in-theory (enable primitive-order-theory)
 
143
                   :cases ((empty (tail X)))))))
 
144
 
 
145
  (defthm head-minimal
 
146
    (implies (<< a (head X))
 
147
             (not (in a X)))
 
148
    :hints(("Goal"
 
149
            :in-theory (enable primitive-order-theory))))
 
150
 
 
151
  (defthm head-minimal-2
 
152
    (implies (in a X)
 
153
             (not (<< a (head X)))))
 
154
 
 
155
)
 
156
 
 
157
(encapsulate ()
 
158
 
 
159
  (local (defthm lemma
 
160
           (implies (empty (tail X))
 
161
                    (not (in (head X) (tail X))))))
 
162
 
 
163
  (local (defthm lemma-2
 
164
           (implies (not (empty (tail X)))
 
165
                    (not (in (head X) (tail X))))
 
166
           :hints(("Goal" :in-theory (enable primitive-order-theory)))))
 
167
 
 
168
  ;; This is an interesting theorem, which gives us a concept of
 
169
  ;; uniqueness without using the set order to state it!
 
170
 
 
171
  (defthm head-unique
 
172
    (not (in (head X) (tail X)))
 
173
    :hints(("Goal"
 
174
            :use ((:instance lemma)
 
175
                  (:instance lemma-2)))))
 
176
)
 
177
 
 
178
 
 
179
(defthm insert-identity
 
180
  (implies (in a X)
 
181
           (equal (insert a X) X))
 
182
  :hints(("Goal" :in-theory (enable insert-induction-case))))
 
183
 
 
184
 
 
185
(defthm in-insert
 
186
  (equal (in a (insert b X))
 
187
         (or (in a X)
 
188
             (equal a b)))
 
189
  :hints(("Goal" :in-theory (enable primitive-order-theory)
 
190
                 :induct (insert b X))))
 
191
 
 
192
 
 
193
 
 
194
 
 
195
;;; The behavior of insert is, of course, determined by the set order.
 
196
;;; Yet, we often need to induct upon insert's definition to prove
 
197
;;; theorems.  So, here we introduce a new induction scheme which
 
198
;;; hides the set order, yet still allows us to induct on insert very
 
199
;;; nicely.  We then disable the induction scheme that insert normally
 
200
;;; uses, and set up an induction hint so that weak-insert-induction
 
201
;;; will automatically be used instead.
 
202
 
 
203
(defthm weak-insert-induction-helper-1
 
204
  (implies (and (not (in a X))
 
205
                (not (equal (head (insert a X)) a)))
 
206
           (equal (head (insert a X)) (head X)))
 
207
  :hints(("Goal" :in-theory (enable primitive-order-theory))))
 
208
 
 
209
(defthm weak-insert-induction-helper-2
 
210
  (implies (and (not (in a X))
 
211
                (not (equal (head (insert a X)) a)))
 
212
           (equal (tail (insert a X)) (insert a (tail X))))
 
213
  :hints(("Goal" :in-theory (enable primitive-order-theory))))
 
214
 
 
215
(defthm weak-insert-induction-helper-3
 
216
  (implies (and (not (in a X))
 
217
                (equal (head (insert a X)) a))
 
218
           (equal (tail (insert a X)) (sfix X)))
 
219
  :hints(("Goal" :in-theory (enable primitive-order-theory))))
 
220
 
 
221
(defun weak-insert-induction (a X)
 
222
  (declare (xargs :guard (setp X)))
 
223
  (cond ((empty X) nil)
 
224
        ((in a X) nil)
 
225
        ((equal (head (insert a X)) a) nil)
 
226
        (t (list (weak-insert-induction a (tail X))))))
 
227
 
 
228
(in-theory (disable (:induction insert)))
 
229
 
 
230
(defthm use-weak-insert-induction t
 
231
  :rule-classes ((:induction
 
232
                  :pattern (insert a X)
 
233
                  :scheme (weak-insert-induction a X))))
 
234
 
 
235
 
 
236
 
 
237
 
 
238
 
 
239
;;; Subset Testing.
 
240
;;;
 
241
;;; Now we introduce subset.  This becomes complicated because we want
 
242
;;; to use MBE to make it fast.  The fast-subset function is a tail
 
243
;;; re- cursive, linear pass through both lists.  Subset, by
 
244
;;; comparison, is a nice to reason about definition and much simpler,
 
245
;;; but would require quadratic time if we didn't use MBE here.
 
246
 
 
247
(defun fast-subset (X Y)
 
248
  (declare (xargs :guard (and (setp X) (setp Y))))
 
249
  (cond ((empty X) t)
 
250
        ((empty Y) nil)
 
251
        ((<< (head X) (head Y)) nil)
 
252
        ((equal (head X) (head Y)) (fast-subset (tail X) (tail Y)))
 
253
        (t (fast-subset X (tail Y)))))
 
254
 
 
255
(defun subset (X Y)
 
256
  (declare (xargs :guard (and (setp X) (setp Y))
 
257
                  :verify-guards nil))
 
258
  (mbe :logic (if (empty X)
 
259
                  t
 
260
                (and (in (head X) Y)
 
261
                     (subset (tail X) Y)))
 
262
       :exec (fast-subset X Y)))
 
263
 
 
264
(defthm subset-type
 
265
  (or (equal (subset X Y) t)
 
266
      (equal (subset X Y) nil))
 
267
  :rule-classes :type-prescription)
 
268
 
 
269
(encapsulate ()
 
270
 
 
271
  (local (defthmd lemma
 
272
           (implies (not (in (head Y) X))
 
273
                    (equal (subset X Y) (subset X (tail Y))))))
 
274
 
 
275
  (local (defthm case-1
 
276
           (implies (and (not (empty X))
 
277
                         (not (empty Y))
 
278
                         (not (<< (head X) (head Y)))
 
279
                         (not (equal (head X) (head Y)))
 
280
                         (implies (and (setp X) (setp (tail Y)))
 
281
                                  (equal (fast-subset X (tail Y))
 
282
                                         (subset X (tail Y)))))
 
283
                    (implies (and (setp X) (setp Y))
 
284
                             (equal (fast-subset X Y)
 
285
                                    (subset X Y))))
 
286
           :hints(("Goal" :in-theory (enable primitive-order-theory)
 
287
                   :use (:instance lemma)))))
 
288
 
 
289
  (local (defthm case-2
 
290
           (implies (and (not (empty x))
 
291
                         (not (empty y))
 
292
                         (not (<< (head x) (head y)))
 
293
                         (equal (head x) (head y))
 
294
                         (implies (and (setp (tail x)) (setp (tail y)))
 
295
                                  (equal (fast-subset (tail x) (tail y))
 
296
                                         (subset (tail x) (tail y)))))
 
297
                    (implies (and (setp x) (setp y))
 
298
                             (equal (fast-subset x y)
 
299
                                    (subset x y))))
 
300
           :hints(("Goal" :in-theory (enable primitive-order-theory)
 
301
                   :use (:instance lemma (X (tail X)))))))
 
302
 
 
303
  (local (defthm fast-subset-equivalence
 
304
           (implies (and (setp X) (setp Y))
 
305
                    (equal (fast-subset X Y) (subset X Y)))
 
306
           :hints(("Goal" :in-theory (enable primitive-order-theory)
 
307
                   :induct (fast-subset X Y)))))
 
308
 
 
309
  (verify-guards subset)
 
310
 
 
311
)
 
312
 
 
313
 
 
314
 
 
315
 
 
316
;;; Quantification over Sets.
 
317
;;;
 
318
;;; Up until version 0.81, we used an explicit argument to reduce subset
 
319
;;; proofs to pick-a-point style membership arguments.  Starting in 0.9,
 
320
;;; we generalize this argument to arbitrary predicates instead.
 
321
;;;
 
322
;;; I'll begin with some background on what we historically wanted to
 
323
;;; do.  The "ultimate goal" was to use pick-a-point reasoning to
 
324
;;; prove subset relationships.  In traditional mathematics, subset is
 
325
;;; defined using quantification over members, e.g., as follows:
 
326
;;;
 
327
;;;    (subset X Y) iff "forall a : (in a X) implies (in a Y)"
 
328
;;;
 
329
;;; Traditionally, one would prove the membership part of this
 
330
;;; statement, and use it to conclude whether or not (subset X Y) is
 
331
;;; true.  But, in ACL2, we cannot write a theorem of the following
 
332
;;; form, because all variables are implicitly universally quantified.
 
333
;;;
 
334
;;;    [ "forall a : (in a ...) implies (in a ___)" ]
 
335
;;;       =>
 
336
;;;    (subset ... ___)
 
337
;;;
 
338
;;; However, we can take the contrapositive of this theorem, which
 
339
;;; looks like the following:
 
340
;;;
 
341
;;;    ~(subset ... ___) => "exists a : (in a ...) ^ ~(in a ___)
 
342
;;;
 
343
;;; And we can prove this, by using a new function to search for an
 
344
;;; element which satisfies the existential predicate.
 
345
;;;
 
346
;;; Once we prove the above, we still need to be able to "reduce" a
 
347
;;; proof of (subset X Y) to a proof of (in a X) => (in a Y).  While
 
348
;;; we can't do this with a direct rewrite rule, we can sort of fake
 
349
;;; it using functional instantiation.  In other words, we set up an
 
350
;;; encapsulated event with (in a X) => (in a Y) as its constraint,
 
351
;;; then we can use this constraint to prove that (subset X Y).  By
 
352
;;; functionally instantiating the resulting theorem, we can reduce
 
353
;;; the subset problem to a membership problem.
 
354
;;;
 
355
;;; All of this was an explicit argument until version 0.9.  But, now
 
356
;;; the process is generalized.  First notice that subset is really
 
357
;;; nothing more than "forall a, (in a x) => (in a Y)."  If you let (P
 
358
;;; x) = (in a Y), then this is "forall a, (in a x) => (P a)".  This
 
359
;;; is a more general concept which can capture not only subset, but
 
360
;;; also many other ideas by simply changing the meaning of (P x).
 
361
;;; For example, if P = integerp, then we can test if every element in
 
362
;;; the set is an integer, and so forth.  So, starting in v0.9, we use
 
363
;;; this more general form of encapsulate instead of the more specific
 
364
;;; version used in previous versions.
 
365
;;;
 
366
;;; We begin by introducing a completely arbitrary predicate.  Based
 
367
;;; on this generic predicate we will introduce a new function, all,
 
368
;;; which checks to see if every member in a set satisfies a
 
369
;;; predicate.  We also introduce find-not, which can be used to find
 
370
;;; us a witness for proving all-by-membership.  Finally, we set up an
 
371
;;; encapsulate which allows us to assume that if some hypotheses are
 
372
;;; true, then any member of some set satisfies the predicate, and use
 
373
;;; this constraint to prove that if those same hypotheses are
 
374
;;; satisfied, then all is true for the same set.
 
375
 
 
376
(encapsulate
 
377
 (((predicate *) => *))
 
378
  (local (defun predicate (x) x)))
 
379
 
 
380
(defun all (set-for-all-reduction)
 
381
  (declare (xargs :guard (setp set-for-all-reduction)))
 
382
  (if (empty set-for-all-reduction)
 
383
      t
 
384
    (and (predicate (head set-for-all-reduction))
 
385
         (all (tail set-for-all-reduction)))))
 
386
 
 
387
(defun find-not (X)
 
388
  (declare (xargs :guard (setp X)))
 
389
  (cond ((empty X) nil)
 
390
        ((not (predicate (head X))) (head X))
 
391
        (t (find-not (tail X)))))
 
392
 
 
393
 
 
394
 
 
395
(encapsulate
 
396
 (((all-hyps) => *)
 
397
  ((all-set) => *))
 
398
 
 
399
 (local (defun all-hyps () nil))
 
400
 (local (defun all-set () nil))
 
401
 
 
402
 (defthmd membership-constraint
 
403
   (implies (all-hyps)
 
404
            (implies (in arbitrary-element (all-set))
 
405
                     (predicate arbitrary-element))))
 
406
)
 
407
 
 
408
(encapsulate ()
 
409
 
 
410
  (local (defthm lemma-find-not-is-a-witness
 
411
           (implies (not (all x))
 
412
                    (and (in (find-not x) x)
 
413
                         (not (predicate (find-not x)))))))
 
414
 
 
415
  (defthmd all-by-membership
 
416
    (implies (all-hyps)
 
417
             (all (all-set)))
 
418
    :hints(("Goal"
 
419
            :use (:instance membership-constraint
 
420
                            (arbitrary-element (find-not (all-set)))))))
 
421
)
 
422
 
 
423
 
 
424
;;; The theorem all-by-membership is massively important.  It is the basis
 
425
;;; for reducing subset arguments to membership arguments.  It also has a
 
426
;;; sufficiently general character that we can reuse it to make similar
 
427
;;; reductions for problems other than subset.
 
428
;;;
 
429
;;; However, for the time being, it's important that we actually do apply
 
430
;;; this theorem to the subset function, which is a particularly useful
 
431
;;; way of reasoning about sets.  Two important questions are: how can we
 
432
;;; apply the theorem, and when should we apply it?
 
433
;;;
 
434
;;; To support these notions, a framework is introduced in the file
 
435
;;; computed-hints.lisp.  Basically, we introduce a "trigger" function
 
436
;;; which is nothing more than an alias for subset.  We then use the
 
437
;;; "tagging theorem" pick-a-point-subset-strategy in order to rewrite
 
438
;;; subsets into subset-triggers.  This theorem is constrained so that
 
439
;;; it will only rewrite conclusions and it will not apply while
 
440
;;; backchaining, via syntaxp hypotheses.  This process is described
 
441
;;; in more detail in computed-hints.lisp.
 
442
 
 
443
(defun subset-trigger (X Y)
 
444
  (declare (xargs :guard (and (setp X) (setp Y))))
 
445
  (subset X Y))
 
446
 
 
447
(defthm pick-a-point-subset-strategy
 
448
  (implies (and (syntaxp (rewriting-goal-lit mfc state))
 
449
                (syntaxp (rewriting-conc-lit `(subset ,X ,Y) mfc state)))
 
450
           (equal (subset X Y)
 
451
                  (subset-trigger X Y))))
 
452
 
 
453
(in-theory (disable subset-trigger))
 
454
 
 
455
 
 
456
 
 
457
(COMPUTED-HINTS::automate-instantiation
 
458
  :new-hint-name pick-a-point-subset-hint
 
459
  :generic-theorem all-by-membership
 
460
  :generic-predicate predicate
 
461
  :generic-hyps all-hyps
 
462
  :generic-collection all-set
 
463
  :generic-collection-predicate all
 
464
  :actual-collection-predicate subset
 
465
  :actual-trigger subset-trigger
 
466
  :predicate-rewrite (((predicate ?x ?y) (in ?x ?y)))
 
467
  :tagging-theorem pick-a-point-subset-strategy
 
468
)
 
469
 
 
470
 
 
471
 
 
472
 
 
473
 
 
474
;;; We now show the basic properties of subset.  The first theorems
 
475
;;; are mundane but then we get more interesting, showing that subset
 
476
;;; is reflexive and transitive.  The goal here is to build up
 
477
;;; sufficient theorems to do pick-a-point proofs, which come next.
 
478
 
 
479
(defthm subset-sfix-cancel-X
 
480
  (equal (subset (sfix X) Y)
 
481
         (subset X Y)))
 
482
 
 
483
(defthm subset-sfix-cancel-Y
 
484
  (equal (subset X (sfix Y))
 
485
         (subset X Y)))
 
486
 
 
487
(defthm empty-subset
 
488
  (implies (empty X)
 
489
           (subset X Y)))
 
490
 
 
491
(defthm empty-subset-2
 
492
  (implies (empty Y)
 
493
           (equal (subset X Y) (empty X))))
 
494
 
 
495
(defthm subset-in
 
496
  (implies (and (subset X Y)
 
497
                (in a X))
 
498
           (in a Y)))
 
499
 
 
500
(defthm subset-in-2
 
501
  (implies (and (subset X Y)
 
502
                (not (in a Y)))
 
503
           (not (in a X))))
 
504
 
 
505
(defthm subset-insert-X
 
506
  (equal (subset (insert a X) Y)
 
507
         (and (subset X Y)
 
508
              (in a Y)))
 
509
  :hints(("Goal" :induct (insert a X))))
 
510
 
 
511
(defthm subset-reflexive
 
512
  (subset X X))
 
513
 
 
514
(defthm subset-transitive
 
515
  (implies (and (subset X Y)
 
516
                (subset Y Z))
 
517
           (subset X Z)))
 
518
 
 
519
(defthm subset-membership-tail
 
520
  (implies (and (subset X Y)
 
521
                (in a (tail X)))
 
522
           (in a (tail Y)))
 
523
  :hints(("Goal" :in-theory (enable primitive-order-theory))))
 
524
 
 
525
(defthm subset-membership-tail-2
 
526
  (implies (and (subset X Y)
 
527
                (not (in a (tail Y))))
 
528
           (not (in a (tail X))))
 
529
  :hints(("Goal" :in-theory (disable subset-membership-tail)
 
530
                 :use (:instance subset-membership-tail))))
 
531
 
 
532
(defthm subset-insert
 
533
  (subset X (insert a X)))
 
534
 
 
535
(defthm subset-tail
 
536
  (subset (tail X) X)
 
537
  :rule-classes ((:rewrite)
 
538
                 (:forward-chaining :trigger-terms ((tail x)))))
 
539
 
 
540
 
 
541
 
 
542
 
 
543
 
 
544
 
 
545
;;; Proofs of equality by double containment are also very common.  So,
 
546
;;; to support these, we want to show that double containment is the
 
547
;;; same as equality.
 
548
;;;
 
549
;;; The general argument is the following:
 
550
;;;
 
551
;;;  Suppose that we have two sets which are subsets of one another,
 
552
;;;  i.e. (subset X Y) and (subset Y X) are true.  First, we will show
 
553
;;;  that (head X) = (head Y).  Next we will show that (in a (tail X))
 
554
;;;  implies that (in a (tail Y)).  This fact is then used for a sub-
 
555
;;;  set by membership argument to show that (tail X) = (tail Y).
 
556
;;;  Now, (head X) = (head Y) and (tail X) = (tail Y) can be used
 
557
;;;  together to show that X = Y (see primitives.lisp, head-tail-same)
 
558
;;;  so we are done.
 
559
 
 
560
(encapsulate ()
 
561
 
 
562
  ;; Here are the details.  First we show that the heads are the same:
 
563
 
 
564
  (local (defthmd double-containment-lemma-head
 
565
           (implies (and (subset X Y)
 
566
                         (subset Y X))
 
567
                    (equal (head X) (head Y)))
 
568
           :hints(("Goal" :in-theory (enable primitive-order-theory)))))
 
569
 
 
570
 
 
571
  ;; Next we show that (tail X) is a subset of (tail Y), using a subset
 
572
  ;; by membership argument:
 
573
 
 
574
  (local (defthmd in-tail-expand
 
575
           (equal (in a (tail X))
 
576
                  (and (in a X)
 
577
                       (not (equal a (head X)))))))
 
578
 
 
579
  (local (defthmd double-containment-lemma-in-tail
 
580
           (implies (and (subset X Y)
 
581
                         (subset Y X))
 
582
                    (implies (in a (tail X))     ; could be "equal" instead,
 
583
                             (in a (tail Y))))   ; but that makes loops.
 
584
           :hints(("Goal"
 
585
                   :in-theory (enable primitive-order-theory)
 
586
                   :use ((:instance in-tail-expand (a a) (X X))
 
587
                         (:instance in-tail-expand (a a) (X Y)))))))
 
588
 
 
589
  (local (defthmd double-containment-lemma-tail
 
590
           (implies (and (subset X Y)
 
591
                         (subset Y X))
 
592
                    (subset (tail X) (tail Y)))
 
593
           :hints(("Goal" :in-theory (enable double-containment-lemma-in-tail)))))
 
594
 
 
595
  ;; Finally, we are ready to show that double containment is equality.
 
596
  ;; To do this, we need to induct in such a way that we consider the
 
597
  ;; tails of X and Y.  Then, we will use our fact that about the tails
 
598
  ;; being subsets of one another in the inductive case.
 
599
 
 
600
  (local (defun double-tail-induction (X Y)
 
601
           (declare (xargs :guard (and (setp X) (setp Y))))
 
602
           (if (or (empty X) (empty Y))
 
603
               (list X Y)
 
604
             (double-tail-induction (tail X) (tail Y)))))
 
605
 
 
606
  (local (defthm double-containment-is-equality-lemma
 
607
           (IMPLIES (AND (NOT (OR (EMPTY X) (EMPTY Y)))
 
608
                         (IMPLIES (AND (SUBSET (TAIL X) (TAIL Y))
 
609
                                       (SUBSET (TAIL Y) (TAIL X)))
 
610
                                  (EQUAL (EQUAL (TAIL X) (TAIL Y)) T))
 
611
                         (SETP X)
 
612
                         (SETP Y)
 
613
                         (SUBSET X Y)
 
614
                         (SUBSET Y X))
 
615
                    (EQUAL (EQUAL X Y) T))
 
616
           :hints(("Goal"
 
617
                   :use ((:instance double-containment-lemma-tail
 
618
                                    (X X) (Y Y))
 
619
                         (:instance double-containment-lemma-tail
 
620
                                    (X Y) (Y X))
 
621
                         (:instance double-containment-lemma-head
 
622
                                    (X X) (Y Y)))))))
 
623
 
 
624
  (local (defthmd double-containment-is-equality
 
625
           (implies (and (setp X)
 
626
                         (setp Y)
 
627
                         (subset X Y)
 
628
                         (subset Y X))
 
629
                    (equal (equal X Y) t))
 
630
           :hints(("Goal" :induct (double-tail-induction X Y)))))
 
631
 
 
632
  (defthm double-containment
 
633
    (implies (and (setp X)
 
634
                  (setp Y))
 
635
             (equal (equal X Y)
 
636
                    (and (subset X Y)
 
637
                         (subset Y X))))
 
638
    :hints(("Goal" :use (:instance double-containment-is-equality))))
 
639
 
 
640
)
 
641
 
 
642
 
 
643
;;; We are now done with the membership level.  We disable all of the
 
644
;;; order based reasoning that we introduced here.
 
645
 
 
646
(in-theory (disable head-minimal
 
647
                    head-minimal-2))