csort

(in-package "ACL2")

(defun firstn
  (n l)
  "The sublist of L consisting of its first N elements."
  (declare (xargs :guard (and (true-listp l) (integerp n) (<= 0 n))))
  (cond ((endp l) nil)
    ((zp n) nil)
    (t (cons (car l) (firstn (1- n) (cdr l))))))

(defthm member-equal-car-firstn
  (implies (and (integerp n) (<= 1 n) (consp lst))
    (member-equal (car (firstn n lst)) lst)))

(defthm firstn-too-long
  (implies (and (true-listp lst) (integerp n) (<= (len lst) n))
    (equal (firstn n lst) lst)))

(defun repeat
  (n x)
  (cond ((zp n) nil) (t (cons x (repeat (1- n) x)))))

(defun evnp
  (n)
  (cond ((zp n) t) ((zp (1- n)) nil) (t (evnp (1- (1- n))))))

(defun rev
  (x)
  (cond ((endp x) nil)
    (t (append (rev (cdr x)) (list (car x))))))

(defthm car-append
  (equal (car (append a b))
    (if (consp a)
      (car a)
      (car b))))

(defthm assoc-of-append
  (equal (append (append a b) c) (append a (append b c))))

(defthm true-listp-append-rewrite
  (equal (true-listp (append a b)) (true-listp b)))

(defthm len-append
  (equal (len (append x y)) (+ (len x) (len y))))

(defthm +-constant-folding
  (implies (syntaxp (and (quotep x) (quotep y)))
    (equal (+ x (+ y z)) (+ (+ x y) z))))

(defun delete-equal
  (x lst)
  (cond ((endp lst) nil)
    ((equal x (car lst)) (cdr lst))
    (t (cons (car lst) (delete-equal x (cdr lst))))))

(defun perm
  (lst1 lst2)
  (cond ((endp lst1) (endp lst2))
    ((member-equal (car lst1) lst2) (perm (cdr lst1) (delete-equal (car lst1) lst2)))
    (t nil)))

(defthm perm-reflexive (perm x x))

(defthm perm-cons
  (implies (member-equal a x)
    (equal (perm x (cons a y)) (perm (delete-equal a x) y)))
  :hints (("Goal" :induct (perm x y))))

(defthm perm-symmetric (implies (perm x y) (perm y x)))

(defthm member-equal-delete-equal
  (implies (member-equal a (delete-equal b x))
    (member-equal a x)))

(defthm perm-member-equal
  (implies (and (perm x y) (member-equal a x))
    (member-equal a y)))

(defthm member-equal-delete-equal2
  (implies (and (member-equal a x) (not (equal a b)))
    (member-equal a (delete-equal b x))))

(defthm comm-delete-equal
  (equal (delete-equal a (delete-equal b x))
    (delete-equal b (delete-equal a x))))

(defthm perm-delete-equal
  (implies (perm x y)
    (perm (delete-equal a x) (delete-equal a y))))

(defthm perm-transitive
  (implies (and (perm x y) (perm y z)) (perm x z)))

(defequiv perm)

(defcong perm perm (cons x y) 2)

(defcong perm iff (member-equal x y) 2)

(defthm atom-perm
  (implies (not (consp x)) (perm x nil))
  :rule-classes :forward-chaining)

(defthm member-equal-append
  (iff (member-equal e (append x y))
    (or (member-equal e x) (member-equal e y))))

(defcong perm perm (append x y) 1)

(defcong perm perm (append x y) 2)

(defthm perm-append-cons
  (perm (append x (cons i y)) (cons i (append x y))))

(defcong perm equal (len x) 1)

(defthm perm-rev (perm (rev x) x))

(defthm perm-append-nil (perm (append x nil) x))

(defthm append-repeat
  (equal (append (repeat n x) (list x)) (cons x (repeat n x))))

(defthm rev-repeat (equal (rev (repeat n x)) (repeat n x)))

(defthm len-repeat (equal (len (repeat n x)) (nfix n)))

(defthm consp-repeat
  (equal (consp (repeat n x)) (not (zp n)))
  :hints (("Goal" :expand (repeat 1 x))))

(defthm car-repeat
  (equal (car (repeat n x))
    (if (zp n)
      nil
      x))
  :hints (("Goal" :expand (repeat 1 x))))

(defun data (pair) (cdr pair))

(in-theory (disable data))

(defun ordered
  (lst)
  (cond ((endp lst) t)
    ((endp (cdr lst)) t)
    ((>= (data (car lst)) (data (cadr lst))) (ordered (cdr lst)))
    (t nil)))

(defun all-gte
  (pair lst)
  (cond ((endp lst) t)
    ((and (>= (data pair) (data (car lst)))
       (all-gte pair (cdr lst))))
    (t nil)))

(defthm all-gte-delete-equal-1
  (implies (all-gte pair lst)
    (all-gte pair (delete-equal x lst))))

(defthm all-gte-delete-equal-2
  (implies (and (all-gte pair (delete-equal x lst))
      (>= (data pair) (data x)))
    (all-gte pair lst)))

(encapsulate nil
  (local (defthm lemma
      (implies (and (perm lst lst-equiv)
          (syntaxp (not (term-order lst lst-equiv)))
          (all-gte pair lst))
        (all-gte pair lst-equiv))))
  (defcong perm equal (all-gte pair lst) 2))

(defthm all-gte-implies-gte-member-equal
  (implies (and (all-gte pair1 a) (member-equal pair2 a))
    (<= (data pair2) (data pair1)))
  :rule-classes :linear)

(defthm gte-car-firstn
  (implies (and (all-gte pair a)
      (perm a b)
      (integerp n)
      (<= 1 n)
      (consp b))
    (<= (data (car (firstn n b))) (data pair)))
  :rule-classes nil)

(defthm all-gte-helper
  (implies (and (all-gte pair1 lst) (<= (data pair1) (data pair2)))
    (all-gte pair2 lst)))

(defun all-all-gte
  (lst1 lst2)
  (cond ((endp lst1) t)
    (t (and (all-gte (car lst1) lst2)
        (all-all-gte (cdr lst1) lst2)))))

(defcong perm equal (all-all-gte lst1 lst2) 1)

(defcong perm equal (all-all-gte lst1 lst2) 2)

(defthm all-all-gte-cdr
  (implies (all-all-gte lst acc) (all-all-gte lst (cdr acc))))

(defthm ordered-cons
  (implies (all-gte pair1 s)
    (equal (ordered (cons pair1 s)) (ordered s))))

(defthm all-gte-append-cons
  (equal (all-gte pair1 (append s (list pair2)))
    (and (all-gte pair1 s) (>= (data pair1) (data pair2)))))

(defthm ordered-append
  (equal (ordered (append lst1 lst2))
    (and (ordered lst1) (ordered lst2) (all-all-gte lst1 lst2))))

(defthm ordered-cons-append-cons
  (implies (and (all-gte pair1 s)
      (>= (data pair1) (data pair2))
      (all-all-gte s (list pair2))
      (ordered s))
    (ordered (cons pair1 (append s (list pair2)))))
  :rule-classes nil)

(defthm all-all-gte-cons
  (implies (syntaxp (not (equal acc ''nil)))
    (equal (all-all-gte s (cons pair acc))
      (and (all-all-gte s (list pair)) (all-all-gte s acc)))))

(defthm all-all-gte-append1
  (equal (all-all-gte s (append lst1 lst2))
    (and (all-all-gte s lst1) (all-all-gte s lst2)))
  :hints (("Goal" :induct (append lst1 lst2))))

(defthm all-all-gte-append2
  (equal (all-all-gte (append lst1 lst2) lst3)
    (and (all-all-gte lst1 lst3) (all-all-gte lst2 lst3))))

(defthm all-all-gte-nil (all-all-gte lst nil))

(defthm ordered-repeat (ordered (repeat n x)))

(defthm all-all-gte-repeat
  (equal (all-all-gte (repeat n maxpair) acc)
    (or (zp n) (all-gte maxpair acc)))
  :hints (("Goal" :induct (repeat n maxpair))))

(defthm all-all-gte-repeat-2
  (implies (all-all-gte lst (list minpair))
    (all-all-gte lst (repeat n minpair))))

(defun max-pair
  (pair1 pair2)
  (cond ((<= (data pair1) (data pair2)) pair2) (t pair1)))

(defun min-pair
  (pair1 pair2)
  (cond ((<= (data pair1) (data pair2)) pair1) (t pair2)))

(defun cstep
  (acc)
  (cond ((endp acc) nil)
    ((endp (cdr acc)) acc)
    (t (cons (max-pair (cadr acc) (car acc))
        (cons (min-pair (cadr acc) (car acc)) (cstep (cddr acc)))))))

(defun cfeed
  (lst acc)
  (cond ((endp lst) acc)
    (t (cfeed (cdr lst) (cstep (cons (car lst) acc))))))

(defun cdrain
  (n acc)
  (cond ((zp n) acc)
    (t (cons (car acc) (cdrain (1- n) (cstep (cdr acc)))))))

(defun csort (lst) (cdrain (len lst) (cfeed lst nil)))

(defthm perm-cstep (perm (cstep acc) acc))

(defthm perm-cfeed
  (perm (cfeed lst acc) (append lst acc))
  :hints (("Goal" :induct (cfeed lst acc))))

(defthm perm-cdrain
  (implies (<= n (len acc)) (perm (cdrain n acc) acc)))

(defthm len-cstep (equal (len (cstep acc)) (len acc)))

(defthm len-cfeed
  (equal (len (cfeed lst acc)) (+ (len lst) (len acc))))

(defthm true-listp-cstep
  (implies (true-listp acc) (true-listp (cstep acc)))
  :hints (("Goal" :induct (cstep acc))))

(defthm true-listp-cfeed
  (implies (true-listp acc) (true-listp (cfeed lst acc))))

(defthm true-listp-cdrain
  (implies (true-listp acc) (true-listp (cdrain n acc))))

(defthm len-cdrain
  (implies (and (integerp n) (<= n (len acc)))
    (equal (len (cdrain n acc)) (len acc))))

(defthm cfeed-opener
  (equal (cfeed (cons pair lst) acc)
    (cfeed lst (cstep (cons pair acc)))))

(defthm cstep-append1
  (implies (evnp (len a))
    (equal (cstep (append a b)) (append (cstep a) (cstep b))))
  :rule-classes nil
  :hints (("Goal" :induct (cstep a))))

(defthm cstep-noop
  (implies (and (true-listp acc) (ordered acc))
    (equal (cstep acc) acc))
  :hints (("Goal" :induct (cstep acc))))

(defthm cstep-append2
  (implies (and (true-listp b) (ordered b) (all-all-gte a b))
    (equal (cstep (append a b)) (append (cstep a) b)))
  :hints (("Goal" :induct (cstep a))))

(defun phi
  (acc)
  (cond ((endp acc) t)
    ((endp (cdr acc)) t)
    (t (and (all-gte (car acc) (cdr acc)) (phi (cddr acc))))))

(defthm all-gte-cstep
  (implies (all-gte x acc) (all-gte x (cstep acc)))
  :hints (("Goal" :induct (cstep acc))))

(defthm phi-cstep
  (implies (phi (cdr acc)) (phi (cstep acc))))

(defthm phi-cons
  (equal (phi (cons pair acc))
    (or (endp acc) (and (all-gte pair acc) (phi (cdr acc))))))

(defthm phi-cfeed
  (implies (phi acc) (phi (cfeed lst acc)))
  :hints (("Goal" :induct (cfeed lst acc) :in-theory (disable cstep))))

(defthm perm-csort (perm (csort acc) acc))

(defthm ordered-firstn-cdrain
  (implies (and (integerp n) (<= n (len acc)) (phi acc))
    (ordered (firstn (+ 2 n) (cdrain n acc))))
  :hints (("Subgoal *1/5" :use (:instance gte-car-firstn
       (a (cdr acc))
       (b (cdrain (+ -1 n) (cstep (cdr acc))))
       (pair (car acc))
       (n (+ 1 n)))) ("Subgoal *1/1" :expand ((firstn (+ 2 n) acc) (firstn (+ 1 n) (cdr acc))))))

(defthm ordered-csort
  (ordered (csort lst))
  :hints (("Goal" :use (:instance ordered-firstn-cdrain
       (n (len lst))
       (acc (cfeed lst nil))))))

(defthm bridge
  (implies (and (all-gte pair1 s)
      (>= (data pair1) (data pair2))
      (all-all-gte s (list pair2))
      (evnp (len s))
      (ordered s))
    (equal (cstep (cons pair1 (append s (cons pair2 acc))))
      (cons pair1 (append s (cons pair2 (cstep acc))))))
  :hints (("Goal" :use ((:instance cstep-append1
        (a (cons pair1 (append s (list pair2))))
        (b acc)) (:instance ordered-cons-append-cons
         (pair1 pair1)
         (s s)
         (pair2 pair2))))))

(defun positive-infinity-hint
  (lst s acc)
  (cond ((endp lst) (list s acc))
    (t (positive-infinity-hint (cdr lst)
        (cons (car lst) (append s (list (car acc))))
        (cstep (cdr acc))))))

(defthm positive-infinity-gen
  (implies (and (<= (len lst) (len acc))
      (evnp (len s))
      (ordered s)
      (ordered (rev lst))
      (phi acc)
      (all-all-gte lst s)
      (all-all-gte lst acc)
      (all-all-gte s acc))
    (equal (cfeed lst (append s acc))
      (append (rev lst) s (cdrain (len lst) acc))))
  :hints (("Goal" :induct (positive-infinity-hint lst s acc)))
  :rule-classes nil)

(defthm positive-infinity
  (implies (and (integerp n)
      (<= n (len acc))
      (all-gte maxpair acc)
      (phi acc))
    (equal (cfeed (repeat n maxpair) acc)
      (append (repeat n maxpair) (cdrain n acc))))
  :hints (("Goal" :use (:instance positive-infinity-gen
       (lst (repeat n maxpair))
       (s nil)
       (acc acc)))))

(defthm negative-infinity-gen
  (implies (and (true-listp acc)
      (all-all-gte lst acc)
      (all-all-gte s acc)
      (ordered acc))
    (equal (cfeed lst (append s acc))
      (append (cfeed lst s) acc)))
  :hints (("Goal" :induct (cfeed lst s)))
  :rule-classes nil)

(defthm negative-infinity
  (implies (all-all-gte lst (list minpair))
    (equal (cfeed lst (repeat n minpair))
      (append (cfeed lst nil) (repeat n minpair))))
  :hints (("Goal" :use (:instance negative-infinity-gen
       (lst lst)
       (s nil)
       (acc (repeat n minpair))))))