Download code

Jump to: navigation, search

Back to Merge_sort_(ACL2)

Download for Windows: single file, zip

Download for UNIX: single file, zip, tar.gz, tar.bz2

mergesort.lisp

  1 ; The authors of this work have released all rights to it and placed it
  2 ; in the public domain under the Creative Commons CC0 1.0 waiver
  3 ; (http://creativecommons.org/publicdomain/zero/1.0/).
  4 ; 
  5 ; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  6 ; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  7 ; MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
  8 ; IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
  9 ; CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
 10 ; TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
 11 ; SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 12 ; 
 13 ; Retrieved from: http://en.literateprograms.org/Merge_sort_(ACL2)?oldid=8542
 14 
 15 (in-package "ACL2")
 16 
 17 ;--------------------------------------------------------
 18 ; Definitions
 19 ;--------------------------------------------------------
 20 
 21 (defun merge-ordered (x y)
 22   (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
 23   (cond ((endp x)             y)
 24 	((endp y)             x)
 25 	((< (car x) (car y))  (cons (car x) (merge-ordered (cdr x) y)))
 26 	(t                    (cons (car y) (merge-ordered x (cdr y))))))
 27 (defun split (lst)
 28   (if (endp lst)
 29       (mv nil nil)
 30     (if (endp (cdr lst))
 31 	(mv lst nil)
 32       (mv-let (list1 list2)
 33 	  (split (cdr (cdr lst)))
 34 	(mv (cons (car lst) list1) (cons (car (cdr lst)) list2))))))
 35 (defthm split-results-shorter
 36   (implies (and (consp x) (consp (cdr x)))
 37 	   (and (< (acl2-count (car (split x))) (acl2-count x))
 38 		(< (acl2-count (mv-nth 1 (split x))) (acl2-count x)))))
 39 
 40 (defun mergesort (lst)
 41   (if (or (endp lst) (endp (cdr lst)))
 42       lst
 43     (mv-let (list1 list2)
 44 	(split lst)
 45       (merge-ordered (mergesort list1) (mergesort list2)))))
 46 (defun ordered-p (lst)
 47   (or (endp lst)
 48       (endp (cdr lst))
 49       (and (<= (car lst) (car (cdr lst)))
 50            (ordered-p (cdr lst)))))
 51 (defun delete-element (a lst)
 52   (if (endp lst)
 53       lst
 54     (if (equal a (car lst))
 55         (cdr lst)
 56       (cons (car lst) (delete-element a (cdr lst))))))
 57 
 58 (defun permutation-p (left right)
 59   (or (and (endp left) (endp right))
 60       (and (consp left)
 61            (member (car left) right)
 62            (permutation-p (cdr left) (delete-element (car left) right)))))
 63 
 64 ;--------------------------------------------------------
 65 ; Initial results
 66 ;--------------------------------------------------------
 67 
 68 (defthm mergesort-ordered
 69   (ordered-p (mergesort x)))
 70 
 71 ;--------------------------------------------------------
 72 ; Show that permutation-p is an equivalence relation
 73 ;--------------------------------------------------------
 74 
 75 (defthm permutation-p-reflexive
 76   (permutation-p x x))
 77 (defthm delete-different-element-preserves-member
 78   (implies (not (equal a b))
 79 	   (iff (member a (delete-element b x))
 80 		(member a x))))
 81 (defthm permutation-p-implies-member-iff
 82   (implies (permutation-p x y)
 83 	   (iff (member a x)
 84 		(member a y))))
 85 (defthm delete-element-commutes
 86   (equal (delete-element a (delete-element b c))
 87 	 (delete-element b (delete-element a c))))
 88 
 89 (defthm delete-same-member-preserves-permutation-p
 90   (implies (and (member x a)
 91 		(member x b)
 92 		(permutation-p a b))
 93 	   (permutation-p (delete-element x a)
 94 			  (delete-element x b))))
 95 
 96 (defthm permutation-p-transitive
 97   (implies (and (permutation-p x y)
 98 		(permutation-p y z))
 99 	   (permutation-p x z)))
100 (in-theory (disable permutation-p-implies-member-iff))
101 (defthm cons-delete-permutation-of-original
102   (implies (and (member a y)
103 		(permutation-p (cons a (delete-element a y)) x))
104 	   (permutation-p y x)))
105 (defthm permutation-p-symmetric
106   (implies (permutation-p x y)
107 	   (permutation-p y x)))
108 (defequiv permutation-p)
109 
110 ;--------------------------------------------------------
111 ; Main lemmas and final result
112 ;--------------------------------------------------------
113 
114 (defthm permutation-p-implies-permutation-p-append-2
115   (implies (permutation-p y y-equiv)
116 	   (permutation-p (append x y)
117 			  (append x y-equiv)))
118   :rule-classes (:congruence))
119 (defthm member-of-append-iff-member-of-operand
120   (iff (member a (append x y))
121        (or (member a x)
122 	   (member a y))))
123 
124 (defthm permutation-p-implies-permutation-p-append-1
125   (implies (permutation-p x x-equiv)
126 	   (permutation-p (append x y)
127 			  (append x-equiv y)))
128   :rule-classes (:congruence))
129 (defthm append-commutative-wrt-permutation
130   (permutation-p (append x y)
131 		 (append y x)))
132 
133 (defthm permutation-p-implies-permutation-p-delete-2
134   (implies (permutation-p x x-equiv)
135 	   (permutation-p (delete-element a x)
136 			  (delete-element a x-equiv)))
137   :rule-classes (:congruence))
138 (defthm delete-append-deletes-from-leftmost-containing
139   (equal (delete-element a (append x y))
140 	 (if (member a x)
141 	     (append (delete-element a x) y)
142 	   (append x (delete-element a y)))))
143 (defthm merge-ordered-permutation-of-append
144   (permutation-p (merge-ordered x y)
145 		 (append x y))
146   :hints (("Goal" :induct (merge-ordered x y))))
147 (defthm append-cons-commute-under-permutation
148   (permutation-p (append x (cons a y))
149 		 (cons a (append x y))))
150 
151 (defthm append-split-permutation-of-original
152   (permutation-p (append (car (split x))
153 			 (mv-nth 1 (split x)))
154 		 x))
155 (defthm mergesort-permutation-of-input
156   (permutation-p (mergesort x) x))
157 
158 (defthm mergesort-correct
159   (and (ordered-p (mergesort x))
160        (permutation-p (mergesort x) x))
161   :rule-classes nil)
162 
163 


hijacker
hijacker
hijacker
hijacker