Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

1 files changed, 1132 insertions, 0 deletions

diff --git a/books/defsort/generic.lisp b/books/defsort/generic.lisp
new file mode 100644
index 0000000..774e085
--- /dev/null
+++ b/books/defsort/generic.lisp
@@ -0,0 +1,1132 @@
+; Defsort - Defines a stable sort when given a comparison function
+; Copyright (C) 2008 Centaur Technology
+;
+; Contact:
+;   Centaur Technology Formal Verification Group
+;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
+;   http://www.centtech.com/
+;
+; License: (An MIT/X11-style license)
+;
+;   Permission is hereby granted, free of charge, to any person obtaining a
+;   copy of this software and associated documentation files (the "Software"),
+;   to deal in the Software without restriction, including without limitation
+;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
+;   and/or sell copies of the Software, and to permit persons to whom the
+;   Software is furnished to do so, subject to the following conditions:
+;
+;   The above copyright notice and this permission notice shall be included in
+;   all copies or substantial portions of the Software.
+;
+;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
+;   DEALINGS IN THE SOFTWARE.
+;
+; Original author: Jared Davis <jared@centtech.com>
+
+(in-package "ACL2")
+(include-book "std/lists/list-defuns" :dir :system)
+(include-book "std/lists/abstract" :dir :system)
+(include-book "tools/save-obligs" :dir :system)
+(include-book "misc/without-waterfall-parallelism" :dir :system)
+(local (include-book "std/lists/take" :dir :system))
+(local (include-book "std/lists/nthcdr" :dir :system))
+(local (include-book "std/lists/list-fix" :dir :system))
+(local (include-book "std/lists/revappend" :dir :system))
+(local (include-book "std/lists/equiv" :dir :system))
+(local (include-book "std/lists/no-duplicatesp" :dir :system))
+(local (include-book "ihs/ihs-lemmas" :dir :system))
+(local (in-theory (disable floor mod take-redefinition nthcdr)))
+
+(defthmd comparable-mergesort-admission-nthcdr
+  (implies (consp (cdr x))
+           (< (len (nthcdr (floor (len x) 2) x))
+              (len x)))
+  :rule-classes :linear)
+
+(defthmd comparable-mergesort-admission-take
+  (implies (consp (cdr x))
+           (< (len (take (floor (len x) 2) x))
+              (len x)))
+  :rule-classes :linear)
+
+(defthmd fast-mergesort-admission-1
+  (implies (and (not (zp len))
+                (not (equal len 1)))
+           (< (nfix (+ len (- (ash len -1))))
+              (nfix len)))
+  :rule-classes :linear)
+
+(defthmd fast-mergesort-admission-2
+  (implies (and (not (zp len))
+                (not (equal len 1)))
+           (< (nfix (ash len -1))
+              (nfix len)))
+  :rule-classes :linear)
+
+(local (in-theory (disable ash)))
+
+(local (defthm ash-neg-1
+         (implies (natp x)
+                  (equal (ash x -1)
+                         (floor x 2)))
+         :hints(("Goal" :in-theory (enable ash*)))))
+
+(encapsulate
+ (((comparablep *) => *)
+  ((compare< * *) => *))
+
+ (local (defun comparablep (x)
+          (declare (xargs :guard t))
+          (natp x)))
+
+ (local (defun compare< (x y)
+          (declare (xargs :guard (and (comparablep x)
+                                      (comparablep y))))
+          (< x y)))
+
+ (defthm type-of-comparablep
+   (or (equal (comparablep x) t)
+       (equal (comparablep x) nil))
+   :rule-classes :type-prescription)
+
+ (defthm type-of-compare<
+   (or (equal (compare< x y) t)
+       (equal (compare< x y) nil))
+   :rule-classes :type-prescription)
+
+ (defthm compare<-transitive
+   (implies (and (compare< x y)
+                 (compare< y z))
+            (compare< x z))))
+
+
+
+
+(defund comparable-listp (x)
+  (declare (xargs :guard t))
+  (if (consp x)
+      (and (comparablep (car x))
+           (comparable-listp (cdr x)))
+    (element-list-final-cdr-p x)))
+
+(local
+ (progn
+   (defthm comparable-listp-when-not-consp
+     (implies (not (consp x))
+              (equal (comparable-listp x)
+                     (element-list-final-cdr-p x)))
+     :hints(("Goal" :in-theory (enable comparable-listp))))
+
+   (defthm comparable-listp-of-cons
+     (equal (comparable-listp (cons a x))
+            (and (comparablep a)
+                 (comparable-listp x)))
+     :hints(("Goal" :in-theory (enable comparable-listp))))
+
+   (defthm comparable-listp-of-take
+     (implies (and (force (comparable-listp x))
+                   (force (<= (nfix n) (len x))))
+              (comparable-listp (take n x)))
+     :hints(("Goal"
+             :in-theory (enable take-redefinition)
+             :induct (take n x))))
+
+   (defthm comparable-listp-of-nthcdr
+     (implies (force (comparable-listp x))
+              (comparable-listp (nthcdr n x)))
+     :hints(("Goal"
+             :in-theory (enable (:induction nthcdr))
+             :induct (nthcdr n x)
+             :expand ((nthcdr n x)))))
+
+   (defthm comparable-listp-of-cdr
+     (implies (comparable-listp x)
+              (comparable-listp (cdr x)))
+     :hints(("Goal" :in-theory (disable (comparable-listp)))))
+
+   (defthm comparablep-of-car
+     (implies (comparable-listp x)
+              (equal (comparablep (car x))
+                     (or (consp x)
+                         (comparablep nil)))))))
+
+
+
+
+(defund comparable-merge (x y)
+  (declare (xargs :measure (+ (len x)
+                              (len y))
+                  :guard (and (comparable-listp x)
+                              (comparable-listp y))
+                  :verify-guards nil))
+  (cond ((atom x)
+         y)
+        ((atom y)
+         x)
+        ((compare< (car y) (car x))
+         (cons (car y) (comparable-merge x (cdr y))))
+        (t
+         ;; Either (car x) < (car y) or they are equivalent.  In either case,
+         ;; for stability, take (car x) first.
+         (cons (car x) (comparable-merge (cdr x) y)))))
+
+(verify-guards comparable-merge)
+
+(defthm len-of-comparable-merge
+  (equal (len (comparable-merge x y))
+         (+ (len x) (len y)))
+  :hints(("Goal" :in-theory (enable comparable-merge))))
+
+
+(defthm comparable-listp-of-comparable-merge
+  (implies (and (force (comparable-listp x))
+                (force (comparable-listp y)))
+           (equal (comparable-listp (comparable-merge x y))
+                  t))
+  :hints(("Goal" :in-theory (enable comparable-merge))))
+
+(local
+ (progn
+   (defthm comparable-merge-when-not-consp-left
+     (implies (not (consp x))
+              (equal (comparable-merge x y)
+                     y))
+     :hints(("Goal" :in-theory (enable comparable-merge))))
+
+   (defthm comparable-merge-when-not-consp-right
+     (implies (not (consp y))
+              (equal (comparable-merge x y)
+                     (if (consp x)
+                         x
+                       y)))
+     :hints(("Goal" :in-theory (enable comparable-merge))))
+
+   (in-theory (disable floor-bounded-by-/
+                       take-of-len-free
+                       true-listp-when-element-list-p-rewrite))))
+
+
+
+
+
+
+
+(defund comparable-merge-tr (x y acc)
+  (declare (xargs :measure (+ (len x)
+                              (len y))
+                  :guard (and (comparable-listp x)
+                              (comparable-listp y))
+                  :verify-guards nil))
+  (cond ((atom x)
+         (revappend-without-guard acc y))
+        ((atom y)
+         (revappend-without-guard acc x))
+        ((compare< (car y) (car x))
+         (comparable-merge-tr x (cdr y) (cons (car y) acc)))
+        (t
+         ;; Either (car x) < (car y) or they are equivalent.  In either case,
+         ;; for stability, take (car x) first.
+         (comparable-merge-tr (cdr x) y (cons (car x) acc)))))
+
+(verify-guards comparable-merge-tr)
+
+(local
+ (encapsulate
+   ()
+   (local (defthm comparable-merge-tr-removal-lemma
+            (equal (comparable-merge-tr x y acc)
+                   (revappend acc (comparable-merge x y)))
+            :hints(("Goal"
+                    :induct (comparable-merge-tr x y acc)
+                    :in-theory (enable comparable-merge-tr
+                                       comparable-merge
+                                       revappend)))))
+
+   (defthm comparable-merge-tr-removal
+     (equal (comparable-merge-tr x y nil)
+            (comparable-merge x y)))))
+
+
+
+
+
+;; (encapsulate
+;;  ()
+;;  (defund first-half-len (len)
+;;    (declare (xargs :guard (natp len)))
+;;    (floor (nfix len) 2))
+
+;;  (defthm natp-of-first-half-len
+;;    (natp (first-half-len len))
+;;    :rule-classes :type-prescription)
+
+;;  (defthm first-half-len-less
+;;    (implies (< 0 len)
+;;             (< (first-half-len len) len))
+;;    :rule-classes (:rewrite :linear)
+;;    :hints(("Goal" :in-theory (enable first-half-len))))
+
+;;  (defthm first-half-len-zero
+;;    (equal (equal (first-half-len len) 0)
+;;           (or (zp len)
+;;               (= len 1)))
+;;    :hints(("Goal" :in-theory (enable first-half-len))))
+
+;;  (defund second-half-len (len)
+;;    (declare (xargs :guard (natp len)))
+;;    (- (nfix len) (floor (nfix len) 2)))
+
+;;  (defthm natp-of-second-half-len
+;;    (natp (second-half-len len))
+;;    :hints(("Goal" :in-theory (enable second-half-len)))
+;;    :rule-classes :type-prescription)
+
+;;  (defthm second-half-len-less
+;;    (implies (and (natp len)
+;;                  (not (= 0 len))
+;;                  (not (= 1 len)))
+;;             (< (second-half-len len) len))
+;;    :rule-classes (:rewrite :linear)
+;;    :hints(("Goal" :in-theory (enable second-half-len))))
+
+;;  (defthm second-half-len-zero
+;;    (equal (equal (second-half-len len) 0)
+;;           (zp len))
+;;    :hints(("Goal" :in-theory (enable second-half-len zp))))
+
+;;  (defthm first-plus-second-half
+;;    (implies (natp len)
+;;             (equal (+ (first-half-len len)
+;;                       (second-half-len len))
+;;                    len))
+;;    :hints(("Goal" :in-theory (enable first-half-len second-half-len)))))
+
+
+;; (defund comparable-mergesort-spec2 (x)
+;;   (declare (xargs :measure (len x)
+;;                   :hints(("Goal"
+;;                           :use ((:instance comparable-mergesort-spec-admission))
+;;                           :in-theory (enable first-half-len)))))
+;;   (cond ((atom x)
+;;          nil)
+;;         ((atom (cdr x))
+;;          (list (car x)))
+;;         (t
+;;          (let ((half (first-half-len (len x))))
+;;            (comparable-merge
+;;             (comparable-mergesort-spec2 (take half x))
+;;             (comparable-mergesort-spec2 (nthcdr half x)))))))
+
+;; (defthm true-listp-of-comparable-merge
+;;   (implies (and (true-listp y)
+;;                 (true-listp x))
+;;            (true-listp (comparable-merge x y)))
+;;   :rule-classes :type-prescription
+;;   :hints(("Goal" :in-theory (enable comparable-merge))))
+
+;; (defthm true-listp-of-comparable-mergesort-spec2
+;;   (true-listp (comparable-mergesort-spec2 x))
+;;   :rule-classes :type-prescription
+;;   :hints(("Goal" :in-theory (enable comparable-mergesort-spec2))))
+
+;; (defthm len-of-comparable-mergesort-spec2
+;;   (equal (len (comparable-mergesort-spec2 x))
+;;          (len x))
+;;   :hints(("Goal" :in-theory (enable comparable-mergesort-spec2))))
+
+;; (defthm consp-of-comparable-mergesort-spec2
+;;   (equal (consp (comparable-mergesort-spec2 x))
+;;          (consp x))
+;;   :hints(("Goal" :in-theory (enable comparable-mergesort-spec2))))
+
+
+
+;; (defthm comparable-mergesort-spec-redefinition
+;;   (equal (comparable-mergesort-spec x)
+;;          (comparable-mergesort-spec2 x))
+;;   :hints(("Goal" :in-theory (enable comparable-mergesort-spec
+;;                                     comparable-mergesort-spec2
+;;                                     first-half-len))))
+
+;; (defthm comparable-listp-of-comparable-mergesort-spec2
+;;   (implies (force (comparable-listp x))
+;;            (comparable-listp (comparable-mergesort-spec2 x)))
+;;   :hints(("Goal" :in-theory (e/d (comparable-mergesort-spec2)
+;;                                  ((comparable-listp))))))
+
+;; (defthm comparable-listp-of-comparable-mergesort-spec
+;;   (implies (force (comparable-listp x))
+;;            (comparable-listp (comparable-mergesort-spec x))))
+
+
+
+
+; Refinement 2.  Our efficient sorting routine only tries to sort the first n
+; elements of the list.  This allows us to implicitly partition the list
+; without having to do any consing.
+
+
+;; (defun comparable-mergesort-spec3 (x len)
+;;   (declare (xargs :guard (and (comparable-listp x)
+;;                               (<= len (len x)))
+;;                   :measure (nfix len)
+;;                   :verify-guards nil)
+;;            (type integer len))
+
+;; ; This computes (comparable-mergesort-spec (take len x)).
+
+;;   (cond ((zp len)
+;;          nil)
+;;         ((eql len 1)
+;;          (list (car x)))
+;;         (t
+;;          (let* ((len1  (ash len -1))
+;;                 (len2  (- len len1))
+;;                 (part1 (comparable-mergesort-spec3 x len1))
+;;                 (part2 (comparable-mergesort-spec3 (nthcdr len1 x) len2)))
+;;            (comparable-merge part1 part2)))))
+
+;; (encapsulate
+;;  ()
+;;  ;; (local (defthm +-collect-consts
+;;  ;;          (implies (syntaxp (and (quotep a) (quotep b)))
+;;  ;;                   (equal (+ a b c)
+;;  ;;                          (+ (+ a b) c)))))
+
+;;  ;; (local (defthm +-collect-consts
+;;  ;;          (implies (syntaxp (and (quotep a) (quotep b)))
+;;  ;;                   (equal (+ a b c)
+;;  ;;                          (+ (+ a b) c)))))
+
+;;  (local (defthm take-of-cdr
+;;           (equal (take n (cdr x))
+;;                  (cdr (take (+ 1 n) x)))
+;;           :hints(("Goal" :expand ((take (+ 1 n) x))))))
+
+;;  (local (defthm crock
+;;           (implies (and (natp len1)
+;;                         (natp len2))
+;;                    (equal (NTHCDR len1 (TAKE (+ len1 len2) X))
+;;                           (TAKE len2 (NTHCDR len1 X))))
+;;           :hints(("Goal" :in-theory (e/d (take-redefinition nthcdr)
+;;                                          (open-small-nthcdr
+;;                                           nthcdr-of-cdr))
+;;                   :induct (nthcdr len1 x)))
+;;           :rule-classes nil))
+
+;;  (local (defthm nthcdr-of-take
+;;           (implies (and (natp len1)
+;;                         (natp len2)
+;;                         (<= len1 len2))
+;;                    (equal (nthcdr len1 (take len2 x))
+;;                           (take (- len2 len1) (nthcdr len1 x))))
+;;           :hints (("goal" :use ((:instance crock
+;;                                  (len2 (- len2 len1))))))))
+
+;;  ;; (local (defthm crock2
+;;  ;;          (implies (and (natp len)
+;;  ;;                        (<= len (len x)))
+;;  ;;                   (equal (NTHCDR (FIRST-HALF-LEN LEN) (TAKE LEN X))
+;;  ;;                          (TAKE (SECOND-HALF-LEN LEN)
+;;  ;;                                (NTHCDR (FIRST-HALF-LEN LEN) X))))
+;;  ;;          :hints(("Goal"
+;;  ;;                  :in-theory (disable crock)
+;;  ;;                  :use ((:instance crock
+;;  ;;                                   (len1 (first-half-len len))
+;;  ;;                                   (len2 (second-half-len len))))))))
+
+;;  (local (defthm crock3
+;;           (implies (< 1 (len x))
+;;                    (consp (cdr x)))))
+
+;;  (local (in-theory (disable nthcdr-of-nthcdr)))
+;;  (local (in-theory (enable floor-bounds)))
+
+;;  (defthm comparable-mergesort-spec3-redefinition
+;;    (implies (and (<= len (len x))
+;;                  (natp len))
+;;             (equal (comparable-mergesort-spec3 x len)
+;;                    (comparable-mergesort-spec (take len x))))
+;;    :hints(("Goal"
+;;            :do-not '(generalize eliminate-destructors)
+;;            :induct (comparable-mergesort-spec3 x len)
+;;            :in-theory (disable (:d comparable-mergesort-spec3))
+;;            :expand ((comparable-mergesort-spec (take len x))
+;;                     (:free (a b) (comparable-mergesort-spec (cons a b)))
+;;                     (comparable-mergesort-spec3 x len)
+;;                     (comparable-mergesort-spec3 x 1)
+;;                     (comparable-mergesort-spec3 x 0))))))
+
+
+; Refinement 3.  We now add fixnum and integer declarations, in order to make
+; the arithmetic faster.
+
+(defund fast-comparable-mergesort-fixnums (x len)
+  (declare (xargs :guard (and (comparable-listp x)
+                              (natp len)
+                              (<= len (len x)))
+                  :measure (nfix len)
+                  :verify-guards nil)
+           (type (signed-byte 30) len))
+  (cond ((mbe :logic (zp len)
+              :exec (eql (the (signed-byte 30) len) 0))
+         nil)
+
+        ((eql (the (signed-byte 30) len) 1)
+         (list (car x)))
+
+        (t
+         (let* ((len1  (the (signed-byte 30)
+                         (ash (the (signed-byte 30) len) -1)))
+                (len2  (the (signed-byte 30)
+                         (- (the (signed-byte 30) len)
+                            (the (signed-byte 30) len1))))
+                (part1 (fast-comparable-mergesort-fixnums x len1))
+                (part2 (fast-comparable-mergesort-fixnums (rest-n len1 x) len2)))
+           (comparable-merge-tr part1 part2 nil)))))
+
+
+(local
+ (defthm comparable-listp-of-fast-comparable-mergesort-fixnums
+   (implies (and (<= len (len x))
+                 (force (comparable-listp x)))
+            (comparable-listp (fast-comparable-mergesort-fixnums x len)))
+   :hints(("Goal" :in-theory (enable fast-comparable-mergesort-fixnums)))))
+
+
+(without-waterfall-parallelism
+(def-saved-obligs fast-comparable-mergesort-fixnums-guards
+  :proofs ((fast-comparable-mergesort-fixnums-guards))
+  (verify-guards fast-comparable-mergesort-fixnums))
+)
+
+
+(defmacro mergesort-fixnum-threshold () 536870912)
+
+
+(defund fast-comparable-mergesort-integers (x len)
+  (declare (xargs :guard (and (comparable-listp x)
+                              (natp len)
+                              (<= len (len x)))
+                  :measure (nfix len)
+                  :verify-guards nil)
+           (type integer len))
+  (cond ((mbe :logic (zp len)
+              :exec (eql (the integer len) 0))
+         nil)
+
+        ((eql (the integer len) 1)
+         (list (car x)))
+
+        (t
+         (let* ((len1  (the integer (ash (the integer len) -1)))
+                (len2  (the integer
+                         (- (the integer len) (the integer len1))))
+                (part1 (if (< (the integer len1) (mergesort-fixnum-threshold))
+                           (fast-comparable-mergesort-fixnums x len1)
+                         (fast-comparable-mergesort-integers x len1)))
+                (part2 (if (< (the integer len2) (mergesort-fixnum-threshold))
+                           (fast-comparable-mergesort-fixnums (rest-n len1 x) len2)
+                         (fast-comparable-mergesort-integers (rest-n len1 x) len2))))
+           (comparable-merge-tr part1 part2 nil)))))
+
+(local
+ (defthm comparable-listp-of-fast-comparable-mergesort-integers
+   (implies (and (<= len (len x))
+                 (force (comparable-listp x)))
+            (comparable-listp (fast-comparable-mergesort-integers x len)))
+   :hints(("Goal" :in-theory (e/d ((:i fast-comparable-mergesort-integers))
+                                  ((force)))
+           :induct (fast-comparable-mergesort-integers x len)
+           :expand ((fast-comparable-mergesort-integers x len)
+                    (fast-comparable-mergesort-integers x 1))))))
+
+
+(without-waterfall-parallelism
+(encapsulate
+  ()
+  (local (defthm crock
+           (equal (fast-comparable-mergesort-fixnums x len)
+                  (fast-comparable-mergesort-integers x len))
+           :hints(("Goal" :in-theory (e/d (fast-comparable-mergesort-integers
+                                           fast-comparable-mergesort-fixnums))))))
+
+  (def-saved-obligs fast-comparable-mergesort-integers-guards
+    :proofs ((fast-comparable-mergesort-integers-guards))
+    (verify-guards fast-comparable-mergesort-integers)))
+)
+
+
+(defund comparable-mergesort (x)
+  (declare (xargs :measure (len x)
+                  :guard (comparable-listp x)
+                  :verify-guards nil))
+  (mbe :logic (cond ((atom x)
+                     nil)
+                    ((atom (cdr x))
+                     (list (car x)))
+                    (t
+                     (let ((half (floor (len x) 2)))
+                       (comparable-merge
+                        (comparable-mergesort (take half x))
+                        (comparable-mergesort (nthcdr half x))))))
+       :exec (let ((len (len x)))
+               (if (< len (mergesort-fixnum-threshold))
+                   (fast-comparable-mergesort-fixnums x len)
+                 (fast-comparable-mergesort-integers x len)))))
+
+
+;; We now establish that sorting preserves the duplicities of elements.  In
+;; other words, the output is a permutation of its input.
+(local
+ (defthm duplicity-of-pieces
+   (implies (<= (nfix n) (len x))
+            (equal (+ (duplicity a (nthcdr n x))
+                      (duplicity a (take n x)))
+                   (duplicity a x)))
+   :hints(("Goal" :in-theory (enable take-redefinition nthcdr)))))
+
+(defthm duplicity-of-comparable-merge
+  (equal (duplicity a (comparable-merge x y))
+         (+ (duplicity a x)
+            (duplicity a y)))
+  :hints(("Goal" :in-theory (enable comparable-merge))))
+
+(defthm duplicity-of-comparable-mergesort
+  (equal (duplicity a (comparable-mergesort x))
+         (duplicity a x))
+  :hints(("Goal" :in-theory (e/d (comparable-mergesort
+                                  floor-bounded-by-/)
+                                 (len)))))
+
+
+(defthm true-listp-of-comparable-merge
+  (implies (and (true-listp y)
+                (true-listp x))
+           (true-listp (comparable-merge x y)))
+  :rule-classes :type-prescription
+  :hints(("Goal" :in-theory (enable comparable-merge))))
+
+(defthm true-listp-of-comparable-mergesort
+  (true-listp (comparable-mergesort x))
+  :rule-classes :type-prescription
+  :hints(("Goal" :in-theory (enable comparable-mergesort))))
+
+(defthm len-of-comparable-mergesort
+  (equal (len (comparable-mergesort x))
+         (len x))
+  :hints(("Goal" :in-theory (e/d ((:i comparable-mergesort)
+                                  floor-bounded-by-/)
+                                 (take-redefinition nthcdr))
+          :induct (comparable-mergesort x)
+          :expand ((comparable-mergesort x)))))
+
+(defthm consp-of-comparable-mergesort
+  (equal (consp (comparable-mergesort x))
+         (consp x))
+  :hints(("Goal" :in-theory (e/d ((:i comparable-mergesort))
+                                 (take-redefinition nthcdr))
+          :induct (comparable-mergesort x)
+          :expand ((comparable-mergesort x)))))
+
+(defthm comparable-listp-of-comparable-mergesort
+  (implies (force (comparable-listp x))
+           (comparable-listp (comparable-mergesort x)))
+  :hints(("Goal" :in-theory (e/d ((:i comparable-mergesort)
+                                  floor-bounded-by-/)
+                                 ((comparable-listp)))
+          :induct (comparable-mergesort x)
+          :expand ((comparable-mergesort x)))))
+
+(defthm comparable-mergesort-of-list-fix
+  (equal (comparable-mergesort (list-fix x))
+         (comparable-mergesort x))
+  :hints(("Goal"
+          :in-theory (e/d (comparable-mergesort))
+          :induct (comparable-mergesort x)
+          :expand ((comparable-mergesort (list-fix x))))))
+
+
+(local
+ (encapsulate
+   ()
+   ;; (local (defthm +-collect-consts
+   ;;          (implies (syntaxp (and (quotep a) (quotep b)))
+   ;;                   (equal (+ a b c)
+   ;;                          (+ (+ a b) c)))))
+
+   ;; (local (defthm +-collect-consts
+   ;;          (implies (syntaxp (and (quotep a) (quotep b)))
+   ;;                   (equal (+ a b c)
+   ;;                          (+ (+ a b) c)))))
+
+   (local (defthm take-of-cdr
+            (equal (take n (cdr x))
+                   (cdr (take (+ 1 n) x)))
+            :hints(("Goal" :expand ((take (+ 1 n) x))))))
+
+   (local (defthm crock
+            (implies (and (natp len1)
+                          (natp len2))
+                     (equal (NTHCDR len1 (TAKE (+ len1 len2) X))
+                            (TAKE len2 (NTHCDR len1 X))))
+            :hints(("Goal" :in-theory (e/d (take-redefinition nthcdr)
+                                           (open-small-nthcdr
+                                            nthcdr-of-cdr))
+                    :induct (nthcdr len1 x)))
+            :rule-classes nil))
+
+   (local (defthm nthcdr-of-take
+            (implies (and (natp len1)
+                          (natp len2)
+                          (<= len1 len2))
+                     (equal (nthcdr len1 (take len2 x))
+                            (take (- len2 len1) (nthcdr len1 x))))
+            :hints (("goal" :use ((:instance crock
+                                   (len2 (- len2 len1))))))))
+
+   (local (in-theory (disable take-of-cdr)))
+
+   (local (defthm crock3
+            (implies (< 1 (len x))
+                     (consp (cdr x)))))
+
+   (local (in-theory (disable nthcdr-of-nthcdr)))
+   (local (in-theory (enable floor-bounded-by-/)))
+
+   (defthm fast-comparable-mergesort-fixnums-redefinition
+     (equal (fast-comparable-mergesort-fixnums x len)
+            (comparable-mergesort (take len x)))
+     :hints(("Goal"
+             :in-theory (e/d ((:i fast-comparable-mergesort-fixnums)
+                              comparable-mergesort))
+             :induct (fast-comparable-mergesort-fixnums x len)
+             :expand ((fast-comparable-mergesort-fixnums x len)
+                      (fast-comparable-mergesort-fixnums x 1)
+                      (fast-comparable-mergesort-fixnums x 0)
+                      (comparable-mergesort (take len x))))))
+
+   (defthm fast-comparable-mergesort-integers-redefinition
+     (equal (fast-comparable-mergesort-integers x len)
+            (comparable-mergesort (take len x)))
+     :hints(("Goal"
+             :in-theory (e/d ((:i fast-comparable-mergesort-integers)
+                              comparable-mergesort))
+             :induct (fast-comparable-mergesort-integers x len)
+             :expand ((fast-comparable-mergesort-integers x len)
+                      (fast-comparable-mergesort-integers x 1)
+                      (fast-comparable-mergesort-integers x 0)
+                      (comparable-mergesort (take len x))))))))
+
+(defthm fast-comparable-mergesort-fixnums-of-len-is-spec
+  (equal (fast-comparable-mergesort-fixnums x (len x))
+         (comparable-mergesort x)))
+
+(defthm fast-comparable-mergesort-integers-of-len-is-spec
+  (equal (fast-comparable-mergesort-integers x (len x))
+         (comparable-mergesort x)))
+
+(without-waterfall-parallelism
+(def-saved-obligs comparable-mergesort-guard
+  :proofs ((comparable-mergesort-guard
+            :hints ((and stable-under-simplificationp
+                         '(:expand ((comparable-mergesort x)))))))
+  (verify-guards comparable-mergesort))
+)
+
+
+
+
+; We now establish that the sort returns produces an ordered list.  There may
+; be "equivalent" elements in the list, where we simultaneously have:
+;
+;    (compare< a b) = nil
+;    (compare< b a) = nil
+;
+; For instance, when sorting integers with <, if there are any duplicates in
+; the input list then we will have this situation.  So we only want to ensure
+; that, for every A which preceeds B in the list, either A < B, or A === B in
+; the above sense.
+
+(defund comparable-orderedp (x)
+  (declare (xargs :guard (comparable-listp x)))
+  (cond ((atom x)
+         t)
+        ((atom (cdr x))
+         t)
+        ((compare< (first x) (second x))
+         (comparable-orderedp (cdr x)))
+        (t
+         (and (not (compare< (second x) (first x)))
+              (comparable-orderedp (cdr x))))))
+
+
+(local
+ (progn
+   (defthm comparable-orderedp-when-not-consp
+     (implies (not (consp x))
+              (comparable-orderedp x))
+     :hints(("Goal" :in-theory (enable comparable-orderedp))))
+
+   (defthm comparable-orderedp-when-not-consp-of-cdr
+     (implies (not (consp (cdr x)))
+              (comparable-orderedp x))
+     :hints(("Goal" :in-theory (enable comparable-orderedp))))))
+
+(defthm comparable-orderedp-of-comparable-merge
+  (implies (and (comparable-orderedp x)
+                (comparable-orderedp y))
+           (comparable-orderedp (comparable-merge x y)))
+  :hints(("Goal" :in-theory (enable comparable-merge comparable-orderedp))))
+
+(defthm comparable-orderedp-of-comparable-mergesort
+  (comparable-orderedp (comparable-mergesort x))
+  :hints(("Goal" :in-theory (enable comparable-mergesort))))
+
+
+(defthm no-duplicatesp-equal-of-comparable-mergesort
+  (equal (no-duplicatesp-equal (comparable-mergesort x))
+         (no-duplicatesp-equal x))
+  :hints(("Goal"
+          :use ((:functional-instance
+                 no-duplicatesp-equal-same-by-duplicity
+                 (duplicity-hyp (lambda () t))
+                 (duplicity-lhs (lambda () (comparable-mergesort x)))
+                 (duplicity-rhs (lambda () x)))))))
+
+
+
+
+;; To prove that the sort is stable (and therefore equivalent to a simpler
+;; one), we need additional properties of the comparison function.
+
+(defun-sk compare<-negation-transitive ()
+  ;; This says that the negation of the comparison relation is also transitive.
+  ;; One big effect of it is that incomparable elements -- where (not (compare<
+  ;; x y)) and (not (compare< y x)) -- are all in an equivalence class under
+  ;; the comparison function.  (Transitivity of compare< shows that elements
+  ;; with (compare< x y) and (compare< y x) are in an equivalence class as
+  ;; well.)
+  (forall (x y z)
+          (implies (and (not (compare< x y))
+                        (not (compare< y z)))
+                   (not (compare< x z))))
+  :rewrite :direct)
+
+(defun-sk compare<-strict ()
+  ;; We need this property of the comparison to make our merge functions
+  ;; stable; if we don't know that either compare< or its negation is strict,
+  ;; then it doesn't suffice to do only one comparison per element merged.
+  (forall (x) (not (compare< x x)))
+  :rewrite :direct)
+
+
+
+
+(local
+ (progn
+   (in-theory (disable compare<-negation-transitive compare<-strict))
+
+   (defthm compare<-reverse-when-strict
+     (implies (and (compare<-strict)
+                   (compare< x y))
+              (not (compare< y x)))
+     :hints (("goal" :use ((:instance compare<-transitive
+                            (x x) (z x) (y y)))
+              :in-theory (disable compare<-transitive))))
+
+
+   (defund compare-equiv-elts (elt x)
+     ;; Extract elements of x that are compare<-equivalent to elt, in order.
+     (if (atom x)
+         nil
+       (if (iff (compare< elt (car x))
+                (compare< (car x) elt))
+           (cons (car x) (compare-equiv-elts elt (cdr x)))
+         (compare-equiv-elts elt (cdr x)))))
+
+   (defthm compare-equiv-elts-empty-case
+     (implies (and (comparable-orderedp x)
+                   ;; (comparable-listp x)
+                   (compare<-negation-transitive)
+                   ;; (comparablep elt)
+                   (compare< elt (car x))
+                   (not (compare< (car x) elt)))
+              (equal (compare-equiv-elts elt x) nil))
+     :hints(("Goal" :in-theory (enable compare-equiv-elts comparable-orderedp
+                                       comparable-listp))))
+
+   ;; (defthm compare<-by-equiv
+   ;;   (implies (and (compare<-negation-transitive)
+   ;;                 (not (compare< x y))
+   ;;                 (not (compare< y x))
+   ;;                 ;; (comparablep x)
+   ;;                 ;; (comparablep y)
+   ;;                 ;; (comparablep z)
+   ;;                 )
+   ;;            (and (implies (compare< y z)
+   ;;                          (compare< x z))
+   ;;                 (implies (not (compare< y z))
+   ;;                          (not (compare< x z)))
+   ;;                 (implies (compare< z y)
+   ;;                          (compare< z x))
+   ;;                 (implies (not (compare< z y))
+   ;;                          (not (compare< z x))))))
+
+   ;; (defthm not-compare<-by-strict
+   ;;   (implies (and (compare<-strict)
+   ;;                 ;; (comparablep x)
+   ;;                 ;; (comparablep y)
+   ;;                 (compare< y x))
+   ;;            (not (compare< x y))))
+
+   ;; (defthm compare<-by-negated-trans
+   ;;   (implies (and (compare<-negation-transitive)
+   ;;                 (compare< x y)
+   ;;                 (not (compare< z y))
+   ;;                 (comparablep x)
+   ;;                 (comparablep y)
+   ;;                 (comparablep z))
+   ;;            (compare< x z)))
+
+
+   (defthm compare-negation-transitive-implies
+     (implies (compare<-negation-transitive)
+              (implies (and (not (compare< b c))
+                            (compare< a c))
+                       (compare< a b))))
+
+   (defthm compare-transitive-implies
+     (implies (and (not (compare< a c))
+                   (compare< a b))
+              (not (compare< b c))))
+
+   (defthm compare-equiv-elts-of-comparable-merge
+     (implies (and (compare<-negation-transitive)
+                   (compare<-strict)
+                   (comparable-orderedp x)
+                   (comparable-orderedp y)
+                   ;; (comparable-listp x)
+                   ;; (comparable-listp y)
+                   ;; (comparablep elt)
+                   )
+              (equal (compare-equiv-elts elt (comparable-merge x y))
+                     (append (compare-equiv-elts elt x)
+                             (compare-equiv-elts elt y))))
+     :hints(("Goal" :in-theory (enable (:i comparable-merge)
+                                       compare-equiv-elts
+                                       comparable-orderedp
+                                       comparable-listp)
+             :induct (comparable-merge x y)
+             :expand ((comparable-merge x y)
+                      ;; (:free (a b) (compare-equiv-elts elt (cons a b)))
+                      ;; (compare-equiv-elts elt nil)
+                      ))
+            (and stable-under-simplificationp
+                 (cond ((member-equal '(compare< (car y) (car x)) clause)
+                        '(:cases ((consp (cdr x)))
+                          ;; :expand ((compare-equiv-elts elt x)
+                          ;;          (compare-equiv-elts elt nil))
+                          ))
+                       (t ;; (member-equal '(not (compare< (car y) (car x))) clause)
+                        '(:cases ((consp (cdr y)))
+                          ;; :expand ((compare-equiv-elts elt y)
+                          ;;          (compare-equiv-elts elt nil))
+                          ))
+                       ;; (t '(:expand ((compare-equiv-elts elt x)
+                       ;;               (compare-equiv-elts elt y)
+                       ;;               (compare-equiv-elts elt nil))))
+                       ))))
+
+   (defthm compare-equiv-elts-of-append
+     (equal (compare-equiv-elts elt (append x y))
+            (append (compare-equiv-elts elt x)
+                    (compare-equiv-elts elt y)))
+     :hints(("Goal" :in-theory (enable compare-equiv-elts))))
+
+   (defthm append-compare-extracts-of-take/nthcdr
+     (implies (< (nfix n) (len x))
+              (equal (append (compare-equiv-elts elt (take n x))
+                             (compare-equiv-elts elt (nthcdr n x)))
+                     (compare-equiv-elts elt x)))
+     :hints (("goal" :use ((:instance compare-equiv-elts-of-append
+                            (x (take n x)) (y (nthcdr n x))))
+              :in-theory (disable compare-equiv-elts-of-append
+                                  (force)))))
+
+   (defthm compare-equiv-elts-of-comparable-mergesort
+     (implies (and (compare<-negation-transitive)
+                   (compare<-strict)
+                   ;; (comparable-listp x)
+                   ;; (comparablep elt)
+                   )
+              (equal (compare-equiv-elts elt (comparable-mergesort x))
+                     (compare-equiv-elts elt x)))
+     :hints(("Goal" :in-theory (e/d ((:i comparable-mergesort)
+                                     floor-bounded-by-/)
+                                    ((force) (comparable-mergesort)
+                                     compare-equiv-elts-empty-case))
+             :expand ((comparable-mergesort x))
+             :induct (comparable-mergesort x))
+            (and stable-under-simplificationp
+                 '(:in-theory (e/d (compare-equiv-elts)
+                                   ((force) (comparable-mergesort)
+                                    compare-equiv-elts-empty-case))))))
+
+   ;; Canoncity: Two truelists are equal if they are both ordered and the
+   ;; extract-equivalents of any element from the two lists are equal (as long as
+   ;; the comparison function is good.)
+
+   (defun-sk compare-elts-equiv (x y)
+     (forall elt
+             (equal (compare-equiv-elts elt x)
+                    (compare-equiv-elts elt y)))
+     :rewrite :direct)
+
+   (defun unequal-lists-badguy (x y)
+     (if (atom x)
+         (car y)
+       (if (atom y)
+           (car x)
+         (if (equal (car x) (car y))
+             (unequal-lists-badguy (cdr x) (cdr y))
+           (if (compare< (car x) (car y))
+               (car x)
+             (car y))))))
+
+   ;; (defthm comparablep-of-unequal-lists-badguy
+   ;;   (implies (not (equal (list-fix x) (list-fix y)))
+   ;;            (comparablep (unequal-lists-badguy x y)))
+   ;;   :hints(("Goal" :in-theory (enable list-fix))))
+
+   (defthm compare-equiv-elts-when-not-consp
+     (implies (not (consp x))
+              (equal (compare-equiv-elts elt x) nil))
+     :hints(("Goal" :in-theory (enable compare-equiv-elts))))
+
+   (defthm compare-equiv-elts-when-past
+     (implies (and (comparable-orderedp x)
+                   (compare< elt (car x))
+                   (not (compare< (car x) elt))
+                   (compare<-negation-transitive))
+              (equal (compare-equiv-elts elt x) nil))
+     :hints(("Goal" :in-theory (enable comparable-orderedp
+                                       compare-equiv-elts))))
+
+
+   (defthm compare-equiv-elts-of-unequal-lists
+     (implies (and (compare<-negation-transitive)
+                   ;; (comparable-listp x)
+                   ;; (comparable-listp y)
+                   ;; (true-listp x)
+                   ;; (true-listp y)
+                   (comparable-orderedp x)
+                   (comparable-orderedp y)
+                   (not (equal (list-fix x) (list-fix y))))
+              (not (equal (compare-equiv-elts (unequal-lists-badguy x y) x)
+                          (compare-equiv-elts (unequal-lists-badguy x y) y))))
+     :hints (("goal" :induct (unequal-lists-badguy x y)
+              :expand ((:free (elt) (compare-equiv-elts elt x))
+                       (:free (elt) (compare-equiv-elts elt y)))
+              :in-theory (e/d (comparable-orderedp)))))))
+
+
+(defund comparable-insert (elt x)
+  (declare (xargs :guard (and (comparablep elt)
+                              (comparable-listp x))))
+  (if (atom x)
+      (list elt)
+    (if (compare< (car x) elt)
+        (cons (car x) (comparable-insert elt (cdr x)))
+      (cons elt x))))
+
+(local
+ (progn
+   (defthm compare-equiv-elts-of-comparable-insert
+     (implies (and (compare<-negation-transitive)
+                   (compare<-strict))
+              (equal (compare-equiv-elts a (comparable-insert b x))
+                     (if (iff (compare< a b)
+                              (compare< b a))
+                         (cons b (compare-equiv-elts a x))
+                       (compare-equiv-elts a x))))
+     :hints(("Goal" :in-theory (enable compare-equiv-elts comparable-insert))))
+
+   (defthm comparable-orderedp-of-comparable-insert
+     (implies (and (comparable-orderedp x))
+              (comparable-orderedp (comparable-insert elt x)))
+     :hints(("Goal" :in-theory (enable comparable-orderedp comparable-insert))))
+
+   (defthm comparable-listp-of-comparable-insert
+     (implies (and (comparable-listp x)
+                   (comparablep elt))
+              (comparable-listp (comparable-insert elt x)))
+     :hints(("Goal" :in-theory (enable comparable-insert))))
+
+   (defthm true-listp-of-comparable-insert
+     (implies (true-listp x)
+              (true-listp (comparable-insert elt x)))
+     :hints(("Goal" :in-theory (enable comparable-insert))))))
+
+
+(defund comparable-insertsort (x)
+  (declare (xargs :guard (comparable-listp x)
+                  :verify-guards nil))
+  (if (atom x)
+      nil
+    (comparable-insert (car x)
+                       (comparable-insertsort (cdr x)))))
+
+(defthm comparable-listp-of-comparable-insertsort
+  (implies (comparable-listp x)
+           (comparable-listp (comparable-insertsort x)))
+  :hints(("Goal" :in-theory (e/d (comparable-insertsort)
+                                 ((comparable-listp))))))
+
+(without-waterfall-parallelism
+(def-saved-obligs comparable-insertsort-guard
+  :proofs ((comparable-insertsort-guard))
+  (verify-guards comparable-insertsort))
+)
+
+(local
+ (progn
+   (defthm compare-equiv-elts-of-comparable-insertsort
+     (implies (and (compare<-negation-transitive)
+                   (compare<-strict))
+              (equal (compare-equiv-elts a (comparable-insertsort x))
+                     (compare-equiv-elts a x)))
+     :hints(("Goal" :in-theory (e/d (comparable-insertsort)
+                                    ((comparable-insertsort)))
+             :induct (comparable-insertsort x)
+             :expand ((compare-equiv-elts a x)
+                      (compare-equiv-elts a nil)
+                      (comparable-listp x)))))
+
+   (defthm comparable-orderedp-of-comparable-insertsort
+     (comparable-orderedp (comparable-insertsort x))
+     :hints(("Goal" :in-theory (e/d (comparable-insertsort)
+                                    ((comparable-orderedp)
+                                     (comparable-insertsort))))))
+
+
+   (defthm true-listp-of-comparable-insertsort
+     (true-listp (comparable-insertsort x))
+     :hints(("Goal" :in-theory (enable comparable-insertsort))))))
+
+
+(defthm comparable-mergesort-equals-comparable-insertsort
+  (implies (and (compare<-negation-transitive)
+                (compare<-strict))
+           (equal (comparable-mergesort x)
+                  (comparable-insertsort x)))
+  :hints (("goal" :use ((:instance compare-equiv-elts-of-unequal-lists
+                         (x (comparable-mergesort x))
+                         (y (comparable-insertsort x))))
+           :in-theory (disable compare-equiv-elts-of-unequal-lists))))
+