; To certify this book in raw ACL2, connect to the directory that contains your copy of
; this file, which is named quicksort.lisp, fire up ACL2, and execute:

; (certify-book "quicksort")

; To use this book after it has been certified, connect to the directory that contains your
; certified copy of this file, fire up ACL2, and then do:

; (include-book "quicksort")

; You can of course include this file while in ACL2's not connected to its original directory,
; but you'd have to type the full name of the file, e.g.,

; (include-book "/u/jones/my-acl2-stuff/quicksort")

; To simply replay all the events in this file do

; (ld "quicksort.lisp" :ld-pre-eval-print t)

(in-package "ACL2")

(DEFUN IS-SORTED (LST) ; Hyeonseo's problem
  (COND ((ENDP LST) T)
	((ENDP (CDR LST)) T)
	(T (AND (<= (CAR LST) (CADR LST))
		(IS-SORTED (CDR LST))))))

(DEFUN REMOVE-LTE (X LST)
  (IF (ENDP LST)
      NIL
      (LET ((NEXT (REMOVE-LTE X (CDR LST))))
	(IF (<= (CAR LST) X)
	    NEXT (APPEND (LIST (CAR LST)) NEXT)))))

(DEFUN REMOVE-GT (X LST)
  (IF (ENDP LST)
      NIL
      (LET ((NEXT (REMOVE-GT X (CDR LST))))
	(IF (> (CAR LST) X)
	    NEXT (APPEND (LIST (CAR LST)) NEXT)))))

(DEFUN QUICKSORT (LST)
  (IF (ENDP LST)
      NIL
      (LET ((PIVOT (CAR LST)) (REST (CDR LST)))
	(APPEND (QUICKSORT (REMOVE-GT PIVOT REST))
		(LIST PIVOT)
		(QUICKSORT (REMOVE-LTE PIVOT REST))))))

(defun all-lte (i x)
  (if (endp x)
      t
      (and (<= (car x) i)
           (all-lte i (cdr x)))))

(defun all-gt (i x)
  (if (endp x)
      t
      (and (> (car x) i)
           (all-gt i (cdr x)))))

(defthm is-sorted-append
  (implies (and (is-sorted a)
                (is-sorted b)
                (all-lte pivot a)
                (all-gt pivot b))
           (is-sorted (append a (cons pivot b)))))

(defthm all-lte-append
  (equal (all-lte i (append a b))
         (and (all-lte i a)
              (all-lte i b))))

(defthm all-gt-append
  (equal (all-gt i (append a b))
         (and (all-gt i a)
              (all-gt i b))))

(defthm all-lte-remove-lte
  (implies (<= i j)
           (equal (all-lte j (remove-lte i x))
                  (all-lte j x))))

(defthm all-lte-remove-gt
  (implies (<= i j)
           (all-lte j (remove-gt i x))))

(defthm all-gt-remove-lte
  (implies (>= i j)
           (all-gt j (remove-lte i x))))

(defthm all-gt-remove-gt
  (implies (>= i j)
           (equal (all-gt j (remove-gt i x))
                  (all-gt j x))))

(defthm all-lte-quicksort
  (equal (all-lte i (quicksort x))
         (all-lte i x)))

(defthm all-gt-quicksort
  (equal (all-gt i (quicksort x))
         (all-gt i x)))
           
(defthm prove-quicksort-correctness
  (is-sorted (quicksort x)))