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.