Finite set theory based on fully ordered lists, by Jared Davis,
describes the set theory implementation in books/finite-set-theory/osets/. In this
library, set equality is just ACL2's 'equal' and the typical set
operations (union, intersection, difference, cardinality) are
linear-time and efficiently implemented. A fairly complete set of set
operations and rewrite rules are provided, and 'pick a point' proofs
can be used to show subset relations. Macros allow the quick
introduction of functions to quantify predicates over sets (e.g.,
'all-less-than'), and map functions over sets (e.g.,
'cons-onto-each'). More information and
slides are also available at the above page.
Finite Set Theory in ACL2, by J
Strother Moore, describes some of the features available in the
distributed book books/finite-set-theory/set-theory.lisp. The book provides
hereditarily finite sets built from ACL2 objects. Sets are represented by
lists. Sets may contain sets as elements. The usual primitives -- including
those for dealing with functions as sets of ordered pairs -- are defined and
lemmas are proved providing many algebraic properties of finite set theory.
Some common proof strategies are codified and macros are provided for
defining functions that construct certain sets from others. This book is
just a start at what could easily turn into a major effort to support finite
set theory more completely.
An Exercise in Graph Theory, J Moore, Chapter 5 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory books/workshops/1999/graph/ of the
community books, hence available at the
acl2-books project website.)
The article formalizes and proves the correctness of several
simple algorithms for determining whether a path exists between two nodes of
a finite directed graph. The ACL2 scripts referenced here provide the full
details of the results described in the article along with solutions to all
the exercises in the article.
Defthms About Zip and Tie: Reasoning About Powerlists in ACL2, Ruben
Gamboa, University of Texas Computer Sciences Technical Report No. TR97-02,
February, 1998. This work is based on Jay Misra's “powerlist” device, a
data structure well-suited to recursive, data-parallel algorithms. A
generalization of powerlists is formalized in ACL2 by Gamboa and used to
prove a variety of algorithm correct, including several sorting algorithms
(including bitonic and Batcher), a grey-code sequence generator, and a
carry-lookahead adder. ACL2 event lists are linked to the URL above.
Mechanically
Verifying the Correctness of the Fast Fourier Transform in ACL2, Ruben
Gamboa, in Third International Workshop on Formal Methods for Parallel
Programming: Theory and Applications (FMPPTA), 1998. This paper is based on
Jay Misra's work on “powerlists” (above) and formalizes Misra's
stunningly simple proof of the correctness of an FFT algorithm implemented
with powerlists. The URL above links to an ACL2 event script as well.
Defstructure
for ACL2, Bishop Brock, December, 1997. This paper serves as
documentation for the ACL2 defstructure book, which provides a
“record facility” similar to Common Lisp's defstruct and
Nqthm's add-shell.
