Finite Set Theory based on Fully Ordered Lists
This is a relatively minor release for efficiency improvements and minor tweaks to the reasoning strategy.
Certain operations are now tail recursive. Previously, functions such as fast-union, fast-intersect, fast-difference, were not implemented tail recursively. This could cause overflows on very large lists. Thanks to David Rager for identifying this problem and for submitting patches to make these functions tail recursive, eliminating the problem. Also made split-list tail recursive, at David Rager's suggestion.
Cardinality has been given a speed boost. The executable version of cardinality now calls length instead of len.
Subset is now enabled. Disabling the subset function was causing some problems in finishing pick a point proofs. It is now enabled by default.
Added :built-in-clause rules about the acl2-count of head and tail.
Added the rule in-head, rewriting (in (head X) X) to (not (empty X)).
This is a major release.
The library now requires ACL2 2.9.
The set order has been changed. We now use the same << as the total-order book. Effectively, we make fewer assumptions about the set order, no longer requiring that nil be the greatest element. This change might allow us to consider custom set orders in the future. This was a bit of an undertaking. Many proofs in membership.lisp and fast.lisp have been changed to avoid relying on nil's maximality. There are also some changes in other low level theorems, such as head-insert. There should be little or no impact on user theorems, unless you were reasoning "from first principles", e.g., for "fast" functions defined using cons and so forth.
Computed hints are now automatically managed. Previously, the macros enable/disable-set-reasoning were used to turn on the computed hint for conducting pick-a-point proofs. These macros have been removed and are no longer necessary, and pick-a-point proofs are automatically enabled. (To disable them, disable the "tagging" theorem, pick-a-point-subset-strategy, instead.) Thanks to Matt Kaufmann for modifying ACL2 to permit this change.
Membership.lisp has been cleaned up. The support for computed hints have been separated out and put into its own package, COMPUTED-HINTS. The encapsulate event which the pick-a-point subset strategy was based on is now more general and can be used with the new extensions in this release. The pick-a-point method is now developed earlier in the membership.lisp file, and is used in order to prove many of the theorems which used to be based on induction arguments, e.g., subset-reflexive.
A new package, INSTANCE, has been added to support the new extensions. Users should not need to use this package directly.
New extension: constructive quantification. This extension (in quantify.lisp) completely replaces typed sets with a more general and powerful theory of constructive quantification. Given a k-ary (k > 1) predicate P, you can now quickly introduce a theory of quantification for that predicate over sets and lists.
New extension: mappings. Building off the base provided by constructive quantification, mappings allow you to discuss the images of sets under some arbitrary k-ary function, F, where (k > 1). As with constructive quantification, an elaborate rewriting strategy is also introduced for reasoning about mappings. Mappings are also implemented more efficiently (via MBE) than the naive implementation using repeated insertion.
Mergesort is easier to reason about. Mergesort now has a new logical definition via MBE, so that you can reason about it as if it were a simple, recursive insert sort. Of course, it still acts as an efficient mergesort under the hood. Thanks to Serita Nelesen for pointing out the deficiencies with the previous approach. I've also done away with the use of member-equal, and instead a new in-list function has been added which returns a boolean instead of part of the list.
Cardinality reasoning has been improved. This is particularly true with regards to the cardinalities of intersections. Added theorems cardinality-zero-empty, intersect-cardinality-non-subset, intersect-cardinality-subset-2, and intersect-cardinality-non-subset-2. Also changed intersect-cardinality-subset to also be a :rewrite rule in addition to being :linear. Thanks to Robert Krug and Hanbing Liu for their input in these changes.
Subset reasoning has been improved. Added the theorem subset-tail at Hanbing Liu's suggestion, which is useful for induction-style proofs of subset. Also, the theorems difference-preserves-subset and subset-delete, have been added at Omar El-Domeiri's suggestion. Finally, subset-insert has been added, and parallels subset-delete.
This is a minor release to merge the library with ACL2.
Matt Kaufmann has integreated the library with ACL2. The library will now be part of the standard books released with ACL2. The build system has been modified to work nicely with ACL2's makefiles, changed the computed hints functions to be program mode in order to fix some problems with the new, more stringent guard checking in ACL2 2.8. He has also updated the README to be more accurate about what is built, and cleaned up the stray parentheses in membership.lisp. Thanks, Matt!
This is a significant release, involving significant cleanup work and a few new theorems.
The build system has been significantly improved. A file package.lisp has been added, and now contains the defpkg event for the set theory books, so you can now simply "ld" this file to get the set theory package. The .acl2 have been changed so that they do not contain include-book events, and sets.lisp now includes the other books locally and then redefines events from those books. This approach makes loading sets.lisp faster, allows us to export events in a better order, and hides all of the local proofs. These changes have all been made at the suggestion of Eric Smith. Thanks!
A mergesort has been added. This allows you to quickly create a set from an unordered list which may contain duplicates, and its performance seems quite good.
Optional set order reasoning is now available. The file set-order.lisp has been added and can be optionally included to help with reasoning about the set order. Of course, this should only be done if you are arguing from "first principles" that your functions create sets, and should otherwise generally be avoided.
Double containment is now a rewrite rule. A new theorem, double-containment, has been added in order to explicitly rewrite equalities between sets into mutual subset statements. The computed hints which previously performed double containment proofs have been removed.
Computed hints can now be easily disabled. The macro disable-set-reasoning has been added, and can be used to turn off the pick-a-point proofs that enable-set-reasoning turns on.
Some new theorems help fill out the rewriting strategy. In particular, the theorems difference-insert-X/Y and difference-delete-X/Y were added.
This is a minor release, mainly introducing a new extension.
A new induction scheme is now used for insert. This induction scheme rephrases insert's operation in terms of membership rather than the set order, allowing inductive proofs over the definition of insert to avoid introducing the set order into proofs.
New extension: typed sets. This extension allows you to introduce a theory about sets which contain elements of a fixed type, e.g., integerp.
This is the first publically available version of the set theory library.