← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/defexec/other-apps/qsort/programs.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/defexec/other-apps/qsort/programs.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#|
 
4
    
 
5
    programs.lisp
 
6
    ~~~~~~~~~~~~~
 
7
 
 
8
We consider an example of how to write an in-situ quicksort function in
 
9
ACL2. For efficiency, we would like to use a common store which holds the array
 
10
we are sorting in place. This leads us to write a quicksort using stobjs. Our
 
11
spec is the standard insertion sort, and we would like to prove that the
 
12
quicksort produces the same answer as the insertion sort.
 
13
 
 
14
The present version has been updated from the original 2002 ACL2 Workshop
 
15
supporting materials to incorporate stobjs inlining.
 
16
 
 
17
|#
 
18
 
 
19
(set-verify-guards-eagerness 1)
 
20
 
 
21
(include-book "total-order")
 
22
(include-book "nth-update-nth")
 
23
(include-book "arithmetic/top-with-meta" :dir :system)
 
24
 
 
25
;(defthm natp-compound-recognizer
 
26
;  (iff (natp n)
 
27
;       (and (integerp n)
 
28
;           (>= n 0)))
 
29
;  :rule-classes :compound-recognizer)
 
30
 
 
31
(in-theory (disable natp))
 
32
 
 
33
(local
 
34
(defthm len-resize-list
 
35
  (equal (len (resize-list l n d))
 
36
         (nfix n))))
 
37
 
 
38
;; The store just has one field: objs
 
39
 
 
40
(defstobj qstor 
 
41
  (objs :type (array T (0)) 
 
42
        :initially nil
 
43
        :resizable t)
 
44
  :inline t)
 
45
 
 
46
(local 
 
47
(defthm objsp-is-true-listp
 
48
  (equal (objsp x) (true-listp x))))
 
49
 
 
50
(defthm nth-update-nth-diff-objsi
 
51
  (implies (not (equal (nfix n) (nfix m)))
 
52
           (equal (objsi n (update-objsi m v l)) (objsi n l))))
 
53
 
 
54
(defthm nth-update-nth-same-objsi
 
55
  (implies (equal (nfix n) (nfix m))
 
56
           (equal (objsi n (update-objsi m v l)) v)))
 
57
 
 
58
(defthm update-nth-update-nth-same-objsi
 
59
  (equal (update-objsi n v (update-objsi n x l))
 
60
         (update-objsi n v l)))
 
61
 
 
62
(defthm update-nth-update-nth-diff-objsi
 
63
  (implies (not (equal (nfix n) (nfix m)))
 
64
           (equal (update-objsi n v (update-objsi m x l))
 
65
                  (update-objsi m x (update-objsi n v l))))
 
66
  :rule-classes ((:rewrite :loop-stopper ((n m)))))
 
67
 
 
68
(in-theory (disable objsi update-objsi))
 
69
 
 
70
(defun alloc-qs (N qstor)
 
71
  (declare (xargs :stobjs qstor))
 
72
  (resize-objs N qstor))
 
73
 
 
74
(local
 
75
(defthm alloc-qs-qstorp
 
76
  (implies (qstorp qs)
 
77
           (qstorp (alloc-qs N qs)))))
 
78
 
 
79
(local
 
80
(defthm objs-length-alloc-qs
 
81
  (equal (objs-length (alloc-qs N qs))
 
82
         (nfix N))))
 
83
 
 
84
(local
 
85
(defthm objs-length-update-objs
 
86
  (equal (len (nth 0 (update-objsi m x l)))
 
87
         (len (update-nth m x (nth 0 l))))
 
88
  :hints (("Goal" :in-theory (enable update-objsi)))))
 
89
 
 
90
(defun load-qs (x lo N qstor)
 
91
  (declare (xargs :guard (and (true-listp x)
 
92
                              (natp lo)
 
93
                              (natp N)
 
94
                              (<= (+ N lo)
 
95
                                  (objs-length qstor)))
 
96
                  :stobjs qstor))
 
97
  (if (zp N) qstor
 
98
    (let ((qstor (update-objsi lo (first x) qstor)))
 
99
      (load-qs (rest x) (1+ lo) (1- N) qstor))))
 
100
 
 
101
(local
 
102
(defthm load-qs-qstorp
 
103
  (implies (qstorp qs)
 
104
           (qstorp (load-qs x i N qs)))
 
105
  :hints (("Goal" :in-theory (enable update-objsi)))))
 
106
 
 
107
(local
 
108
(defthm load-qs-objs-length
 
109
  (implies (and (natp i)
 
110
                (natp N)
 
111
                (<= (+ i N) (objs-length qs)))
 
112
           (= (objs-length (load-qs x i N qs))
 
113
              (objs-length qs)))
 
114
  :hints (("Goal" :in-theory (enable update-objsi)))))
 
115
 
 
116
(defun extract-qs (lo hi qstor)
 
117
  (declare (xargs :guard (and (natp lo)
 
118
                              (natp hi)
 
119
                              (< hi (objs-length qstor)))
 
120
                  :stobjs qstor
 
121
                  :measure (nfix (1+ (- hi lo)))))
 
122
  (if (and (natp lo)
 
123
           (natp hi)
 
124
           (<= lo hi))
 
125
      (cons (objsi lo qstor) 
 
126
            (extract-qs (1+ lo) hi qstor))
 
127
    nil))
 
128
 
 
129
(defun swap (i j qstor)
 
130
  (declare (xargs :guard (and (natp i)
 
131
                              (natp j)
 
132
                              (< i (objs-length qstor))
 
133
                              (< j (objs-length qstor)))
 
134
                  :stobjs qstor))
 
135
  (let* ((temp (objsi i qstor))
 
136
         (qstor (update-objsi i (objsi j qstor) qstor))
 
137
         (qstor (update-objsi j temp qstor)))
 
138
    qstor))
 
139
 
 
140
(local
 
141
(defthm swap-preserves-qstorp
 
142
  (implies (qstorp qs)
 
143
           (qstorp (swap i j qs)))
 
144
  :hints (("Goal" :in-theory (enable update-objsi)))))
 
145
 
 
146
(local
 
147
(defthm swap-preserves-objs-length
 
148
  (implies (and (natp i)
 
149
                (natp j)
 
150
                (< i (objs-length qs))
 
151
                (< j (objs-length qs)))
 
152
           (= (objs-length (swap i j qs))
 
153
              (objs-length qs)))
 
154
  :hints (("Goal" :in-theory (enable update-objsi)))))
 
155
 
 
156
(local
 
157
(in-theory (disable alloc-qs swap qstorp objs-length)))
 
158
 
 
159
(defun ndx< (x y)
 
160
  (declare (xargs :guard t))
 
161
  (if (and (natp x)
 
162
           (natp y))
 
163
      (< x y)
 
164
    t))
 
165
 
 
166
(defun ndx<= (x y)
 
167
  (declare (xargs :guard t))
 
168
  (if (and (natp x)
 
169
           (natp y))
 
170
      (<= x y)
 
171
    t))
 
172
 
 
173
(verify-guards <<)
 
174
 
 
175
(defun split-qs (lo hi splitter qstor)
 
176
  (declare (xargs :guard (and (integerp lo)
 
177
                              (integerp hi)
 
178
                              (<= lo (objs-length qstor))
 
179
                              (< hi (objs-length qstor)))
 
180
                  :stobjs qstor
 
181
                  :measure (nfix (1+ (- hi lo)))))
 
182
  (if (ndx< hi lo)
 
183
      (mv lo qstor)
 
184
    (let* ((swap-lo (<<= splitter (objsi lo qstor)))
 
185
           (swap-hi (<< (objsi hi qstor) splitter))
 
186
           (qstor (if (and swap-lo swap-hi)
 
187
                      (swap lo hi qstor)
 
188
                    qstor)))
 
189
      (split-qs (if (implies swap-lo swap-hi)
 
190
                    (1+ lo)
 
191
                  lo)
 
192
                (if (implies swap-hi swap-lo)
 
193
                    (1- hi)
 
194
                  hi)
 
195
                splitter qstor))))
 
196
 
 
197
(local
 
198
(defthm qstorp-split-qs
 
199
  (implies (qstorp qs)
 
200
           (qstorp (cadr (split-qs lo hi x qs))))))
 
201
 
 
202
(local
 
203
(defthm objs-length-split-qs
 
204
  (implies (and (natp lo)
 
205
                (natp hi)
 
206
                (<= lo (objs-length qs))
 
207
                (< hi (objs-length qs)))
 
208
           (= (objs-length (cadr (split-qs lo hi x qs)))
 
209
              (objs-length qs)))))
 
210
 
 
211
;; I do not like to write defthms in the middle of function definitions, but I
 
212
;; do it here, simply because the sort-qs function defined soon below is a pain in
 
213
;; the butt to go thru....
 
214
 
 
215
(local
 
216
(in-theory (enable alloc-qs swap qstorp objs-length)))
 
217
 
 
218
(defthm property-of-swap
 
219
  (implies (and (natp i)
 
220
                (natp lo)
 
221
                (natp hi))
 
222
           (equal (objsi i (swap lo hi qs))
 
223
                  (if (equal i lo)
 
224
                      (objsi hi qs)
 
225
                    (if (equal i hi)
 
226
                        (objsi lo qs)
 
227
                      (objsi i qs)))))
 
228
  :hints (("Subgoal 3"
 
229
           :cases ((equal lo hi)))))
 
230
 
 
231
(in-theory (disable swap))
 
232
 
 
233
(local
 
234
(defthm arith-001
 
235
  (implies (and (not (natp (1- hi)))
 
236
                (natp hi))
 
237
           (equal hi 0))
 
238
  :rule-classes :forward-chaining)
 
239
)
 
240
 
 
241
(local
 
242
(defthm split-qs-returns-a-value-<=-hi+1
 
243
  (implies (and (natp lo)
 
244
                (natp hi)
 
245
                (<= lo hi))               
 
246
  (<= (mv-nth 0 (split-qs lo hi splitter qs))
 
247
      (1+ hi)))
 
248
  :hints (("Goal"
 
249
           :induct (split-qs lo hi splitter qs)
 
250
           :do-not-induct t)))
 
251
)
 
252
 
 
253
(defthm split-qs-returns-natp
 
254
  (implies (and (natp lo)
 
255
                (natp hi))
 
256
           (natp (mv-nth 0 (split-qs lo hi splitter qs)))))
 
257
 
 
258
(local
 
259
(defthm arith-002
 
260
  (implies (and (<= i hi)
 
261
                (natp i))
 
262
           (<= i (1+ hi)))
 
263
  :rule-classes :forward-chaining)
 
264
)
 
265
 
 
266
(local
 
267
(defthm arith-004
 
268
  (implies (and (<= i hi)
 
269
                (natp i)
 
270
                (natp hi))
 
271
           (not (equal i (1+ hi))))
 
272
  :rule-classes :forward-chaining)
 
273
)
 
274
 
 
275
(local
 
276
(defthm if-splitter-is-lo-then-split-qs-neq-hi+1
 
277
  (implies (and (natp lo)
 
278
                (natp hi)
 
279
                (<= lo hi)
 
280
                (equal splitter (objsi lo qs)))
 
281
           (not (equal (mv-nth 0 (split-qs lo hi splitter qs)) (1+ hi))))
 
282
  :hints (("Goal" ; needed for v2-8 addition of natp-posp book
 
283
           :in-theory (disable natp-posp--1))
 
284
           ("Subgoal *1/5"
 
285
           :do-not-induct t
 
286
           :in-theory (disable split-qs-returns-a-value-<=-hi+1))
 
287
          ("Subgoal *1/5.1"
 
288
           :use ((:instance split-qs-returns-a-value-<=-hi+1
 
289
                            (hi (1- hi))
 
290
                            (splitter (objsi lo qs)))))
 
291
 
 
292
          ("Subgoal *1/5.2"
 
293
           :use ((:instance split-qs-returns-a-value-<=-hi+1
 
294
                             (lo (1+ lo))
 
295
                             (hi (1- hi))
 
296
                             (qs (swap lo hi qs))
 
297
                             (splitter (objsi lo qs)))))))
 
298
)
 
299
 
 
300
(local
 
301
(defthm arith-003
 
302
  (implies (and (<= i (1+ hi))
 
303
                (natp i)
 
304
                (natp hi)
 
305
                (not (equal i (1+ hi))))
 
306
           (<= i hi))
 
307
  :rule-classes nil)
 
308
)
 
309
 
 
310
 
 
311
(defthm split-qs-returns-a-number-<=hi
 
312
  (implies (and (natp lo)
 
313
                (natp hi)
 
314
                (equal splitter (objsi lo qs))
 
315
                (<= lo hi))
 
316
           (<= (mv-nth 0 (split-qs lo hi splitter qs))
 
317
               hi))
 
318
  :hints (("Goal"
 
319
           :in-theory (disable split-qs)
 
320
           :use ((:instance arith-003
 
321
                            (i (mv-nth 0 (split-qs lo hi (objsi lo qs) qs)))))))
 
322
  :rule-classes :linear)
 
323
 
 
324
(defun sort-qs (lo hi qstor)
 
325
  (declare (xargs :guard (and (natp lo)
 
326
                              (natp hi)
 
327
                              (<= lo (objs-length qstor))
 
328
                              (< hi (objs-length qstor)))
 
329
                  :verify-guards nil
 
330
                  :stobjs qstor
 
331
                  :measure (nfix (- hi lo))
 
332
                  :hints (("Goal"
 
333
                           :in-theory (enable natp)
 
334
                           :induct (split-qs lo hi splitter qs)))))
 
335
   (if (ndx<= hi lo)
 
336
       qstor
 
337
     (mv-let (index qstor)
 
338
         (split-qs lo hi (objsi lo qstor) qstor)
 
339
       (if (ndx<= index lo)
 
340
           (sort-qs (1+ lo) hi qstor)
 
341
         (let* ((qstor (sort-qs index hi qstor))
 
342
                (qstor (sort-qs  lo (1- index) qstor)))
 
343
           qstor)))))
 
344
 
 
345
(local
 
346
(in-theory (disable alloc-qs swap qstorp objs-length)))
 
347
 
 
348
(local
 
349
(defthm split-qs-<=-objs-length
 
350
  (implies (and (integerp lo)
 
351
                (integerp hi)
 
352
                (< lo (objs-length qs))
 
353
                (< hi (objs-length qs)))
 
354
           (<= (car (split-qs lo hi x qs))
 
355
               (objs-length qs)))
 
356
  :rule-classes :linear))
 
357
 
 
358
(local
 
359
(defthm mv-nth-0-is-car
 
360
  (equal (mv-nth 0 x) (car x))
 
361
  :hints (("Goal" :in-theory (enable mv-nth)))))
 
362
 
 
363
(local
 
364
(defthm mv-nth-1-is-cadr
 
365
  (equal (mv-nth 1 x) (cadr x))
 
366
  :hints (("Goal" :in-theory (enable mv-nth)))))
 
367
 
 
368
(local
 
369
(defthm qstorp-sort-qs
 
370
  (implies (qstorp qs)
 
371
           (qstorp (sort-qs lo hi qs)))))
 
372
 
 
373
(local
 
374
(defthm objs-length-sort-qs
 
375
  (implies (and (natp lo)
 
376
                (natp hi)
 
377
                (<= lo (objs-length qs))
 
378
                (< hi (objs-length qs)))
 
379
           (= (objs-length (sort-qs lo hi qs))
 
380
              (objs-length qs)))))
 
381
 
 
382
(verify-guards sort-qs)
 
383
 
 
384
(local (in-theory (disable mv-nth-0-is-car mv-nth-1-is-cadr)))
 
385
 
 
386
(defun qsort (x)
 
387
  (declare (xargs :guard (true-listp x)))
 
388
  (if (endp x) ()
 
389
    (with-local-stobj qstor
 
390
      (mv-let (rslt qstor)
 
391
          (let* ((size (length x))
 
392
                 (qstor (alloc-qs size qstor))
 
393
                 (qstor (load-qs x 0 size qstor))
 
394
                 (qstor (sort-qs 0 (1- size) qstor)))
 
395
            (mv (extract-qs 0 (1- size) qstor)
 
396
                qstor))
 
397
        rslt))))
 
398
 
 
399
;; Now we define the abstract spec.
 
400
 
 
401
(defun insert (e x)
 
402
  (declare (xargs :guard t))
 
403
  (if (or (atom x)
 
404
          (<< e (first x)))
 
405
      (cons e x)
 
406
    (cons (first x)
 
407
          (insert e (rest x)))))
 
408
 
 
409
(defun isort (x)
 
410
  (declare (xargs :guard t))
 
411
  (if (atom x) ()
 
412
    (insert (first x)
 
413
            (isort (rest x)))))
 
414
 
 
415
 
 
416