← 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/intermediate-to-spec.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/intermediate-to-spec.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
#|
 
4
 
 
5
 intermediate-to-spec.lisp
 
6
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
7
 
 
8
In this file we prove that the functional qsort qsort-fn is the same as
 
9
isort. Basically we show that qsort-fn is an ordered permutation, and then we
 
10
use the main spec property, anything that produces an ordered permutation is
 
11
the same as qsort, to prove the result.
 
12
 
 
13
|#
 
14
 
 
15
(include-book "intermediate-program")
 
16
(include-book "spec-properties")
 
17
 
 
18
(local
 
19
(defthm del-last-true-listp-reduction
 
20
   (true-listp (del-last x)))
 
21
)
 
22
 
 
23
(defthm snoc-del-last-reduction
 
24
  (implies (and (true-listp x)
 
25
                (consp x))
 
26
           (equal (snoc (del-last x) (last-val x))
 
27
                  x))
 
28
  :rule-classes :forward-chaining)
 
29
 
 
30
 
 
31
(local
 
32
(defthm lower-part-is-true-listp
 
33
  (implies (true-listp x) (true-listp (lower-part x e))))
 
34
)
 
35
 
 
36
(local
 
37
(defthm true-listp-cons-reduction
 
38
  (implies (true-listp x)
 
39
           (true-listp (cons e x))))
 
40
)
 
41
 
 
42
(local
 
43
(defthm true-listp-snoc-reduction
 
44
  (implies (true-listp x) 
 
45
           (true-listp (snoc x e))))
 
46
)
 
47
 
 
48
(local
 
49
(defthm true-listp-append-reduction
 
50
  (implies (and (true-listp x) (true-listp y))
 
51
           (true-listp (append x y))))
 
52
)
 
53
 
 
54
(defthm upper-part-is-true-listp
 
55
  (implies (true-listp x) 
 
56
           (true-listp (upper-part x e))))
 
57
 
 
58
(defthm qsort-fn-is-int-listp
 
59
  (implies (true-listp x)
 
60
           (true-listp (qsort-fn x))))
 
61
 
 
62
(defthm qsort-fn-is-a-permutation
 
63
  (perm (qsort-fn x) x))
 
64
 
 
65
(local
 
66
(defun lessp (e x)
 
67
  (if (endp x) T
 
68
    (if (<< (first x) e) (lessp e (rest x))
 
69
      nil)))
 
70
)
 
71
 
 
72
(local
 
73
(defun not-lessp (e x)
 
74
  (if (endp x) T
 
75
    (if (<<= e (first x)) (not-lessp e (rest x))
 
76
      nil)))
 
77
)
 
78
;; Now prove the congruences between perm, and lessp and not-lessp
 
79
 
 
80
(local
 
81
(defcong perm equal (lessp x l) 2)
 
82
)
 
83
 
 
84
(local
 
85
(defcong perm equal (not-lessp x l) 2)
 
86
)
 
87
 
 
88
;; End proof of congruences between perm, and lessp and not-lessp
 
89
 
 
90
(local
 
91
(defthm ordp-lessp-not-lessp-reduction
 
92
  (implies (and (ordp x)
 
93
                (ordp y)
 
94
                (lessp e x)
 
95
                (not-lessp e y))
 
96
           (ordp (append x (cons e y)))))
 
97
)
 
98
 
 
99
;; The next two theorems establish the correspondence of lessp and
 
100
;; not-lessp functions with the function ordp. So if you were thinking
 
101
;; what was I doing with these two functions, then it is to provide
 
102
;; the following correspondence that I was working. I would love for
 
103
;; someone to give me an easier correspondence, if they can read the
 
104
;; proof.:-)
 
105
 
 
106
(local
 
107
(defthm ordp-lessp-not-lessp-reduction-1
 
108
  (implies (and (ordp x)
 
109
                (ordp y)
 
110
                (lessp e x)
 
111
                (not-lessp e y))
 
112
           (ordp (append x y)))
 
113
  :hints (("Subgoal *1/4"
 
114
           :in-theory (enable <<))))
 
115
           
 
116
)
 
117
 
 
118
(local
 
119
(defthm ordp-lessp-not-lessp-reduction-2
 
120
  (implies (and (ordp x)
 
121
                (not-lessp e x))
 
122
           (ordp (cons e x))))
 
123
)
 
124
 
 
125
(local
 
126
(defthm func-partition-x-is-lessp
 
127
  (lessp splitter 
 
128
         (lower-part x splitter)))
 
129
)
 
130
 
 
131
(local
 
132
(defthm func-partition-y-is-not-lessp
 
133
  (not-lessp splitter 
 
134
             (upper-part x splitter)))
 
135
)
 
136
 
 
137
(local
 
138
(defthm qsort-lower-is-lessp
 
139
  (lessp splitter 
 
140
         (qsort-fn (lower-part x splitter))))
 
141
)
 
142
 
 
143
(local
 
144
(defthm qsort-upper-is-not-lessp
 
145
  (not-lessp splitter 
 
146
             (qsort-fn (upper-part x splitter))))
 
147
)
 
148
 
 
149
(defthm if-lower-is-endp-upper-is-the-actual-list
 
150
  (implies (and (true-listp x)
 
151
                (endp (lower-part x (first x))))
 
152
           (equal (upper-part x (first x)) x))
 
153
  :rule-classes nil)
 
154
 
 
155
(local
 
156
(defthm not-lessp-implies-not-lessp-cdr
 
157
  (implies (not-lessp e x)
 
158
           (not-lessp e (rest x)))
 
159
  :rule-classes nil)
 
160
)
 
161
 
 
162
;; The proofs of the following two functions are really ugly. Just
 
163
;; look at the number of hints I had to give it. I need to talk to Rob
 
164
;; about cleaning it up.
 
165
 
 
166
(local
 
167
(defthm qsort-not-lessp-for-lower-endp
 
168
  (implies (and (true-listp x)
 
169
                (endp (lower-part x (first x))))
 
170
           (not-lessp (first x) (qsort-fn (rest x))))
 
171
  :hints (("Goal"
 
172
           :in-theory (disable lower-part qsort-fn)
 
173
           :use if-lower-is-endp-upper-is-the-actual-list)
 
174
          ("Goal'''"
 
175
           :use ((:instance not-lessp-implies-not-lessp-cdr
 
176
                            (e (car x))
 
177
                            (x (upper-part x (first x))))))))
 
178
)
 
179
 
 
180
;; The following theorem means that I am really done. The next theorem
 
181
;; should be a breeze from perm-ordp-unique.
 
182
 
 
183
(local
 
184
(defthm qsort-fn-is-ordp
 
185
  (implies (true-listp x)
 
186
           (ordp (qsort-fn x)))
 
187
  :hints (("Goal"
 
188
           :induct (qsort-fn x))
 
189
          ("Subgoal *1/4"
 
190
           :use ((:instance ordp-lessp-not-lessp-reduction-1
 
191
                            (e (car x))
 
192
                            (x (qsort-fn (lower-part x (car x))))
 
193
                            (y (qsort-fn (upper-part x (car x)))))))
 
194
          ("Subgoal *1/3"
 
195
           :use ((:instance ordp-lessp-not-lessp-reduction-2
 
196
                            (e (car x))
 
197
                            (x (qsort-fn (cdr x))))))))
 
198
)
 
199
                   
 
200
(defthm qsort-fn-equivalent-isort
 
201
  (implies (true-listp x)
 
202
           (equal (isort x)
 
203
                  (qsort-fn x)))
 
204
  :hints (("Goal"
 
205
           :use ((:instance any-ordered-permutation-of-integers-is-isort
 
206
                            (y (qsort-fn x)))))))
 
207
 
 
208
(in-theory (enable qsort-fn))
 
 
b'\\ No newline at end of file'