This directory contains a demo that illustrates both high-level
strategy and lower-level tactics in the use of ACL2.  It is based on a
distributed book, books/sorting/perm.lisp, as well as a built-in
function lexorder that is a total (non-strict) order of the ACL2
universe.  The demo is however intended to be self-contained.

We set ourselves the top-level goal of proving that insertion sort
gives the same result as mergesort:

(defthm isort-is-msort
  (equal (isort x)
         (msort x)))

One might try proving this directly, but it seems difficult or
impossible to see how to do this directly by induction.  However, we
can use some high-level strategy to map out a course of action that
we feel we can carry out to completion.

Our first insight is that both isort and msort produce sorted lists
that are permutations of each other (because they are both
permutations of their common input), but because those permutations
are sorted, they must be equal!

Our high-level strategy will reflect that insight.  But we also have a
second insight.  Reasoning directly about a recursively-defined
permutation function is known to be tricky (at least if you've ever
tried it!).  So we would like to "trade" such reasoning for reasoning
about a different notion of permutation that we call the "how-many"
approach, namely: two lists are permutations of each other if and only
if every object occurs the same number of times in each.

So, we proceed as follows.

Book ordered-perms.lisp reflects our first insight.  It defines a
notion of a list being ordered, and proves that for ordered
true-lists, permutation reduces to equality.

Book convert-perm-to-how-many.lisp implements the "how-many" approach
described above, reducing the notion of permutation to the question of
whether ever object occurs the same number of times in each list.  See
convert-perm-to-how-many-annotated.lisp for a detailed discussion of
how the proof was found.

Books isort.lisp and msort.lisp define insertion sort and mergesort
(respectively), and employ the "how-many" approach to prove that each
of these produces an ordered permutation of its input.

Finally, book isort-is-msort.lisp proves that isort is equal to msort,
using the fact that both are ordered permutations of the same list.

---

An easy way to certify all books in this directory is to edit the top
of Makefile, as indicated there, and then type "make".  Type
"make clean" if you want to clean up before re-certifying.