Finite set theory in ACL2

Abstract

ACL2 is a first-order, essentially quantifier free logic of computable recursive functions based on an applicative subset of Common Lisp. It supports lists as a primitive data structure. We describe how we have formalized a practical finite set theory for ACL2. Our finite set theory “book” includes set equality, set membership, the subset relation, set manipulation functions sucha s union, intersection, etc., a ch oice function, a representation of finite functions as sets of ordered pairs and a collection of useful functions for manipulating them (e.g., domain, range, apply) and others. The book provides many lemmas about these primitives, as well as macros for dealing withset comprehension and some other “higher order” features of set theory, and various strategies or tactics for proving theorems in set theory. The goal of this work is not to provide “heavy duty set theory” – a task more suited to other logics – but to allow the ACL2 user to use sets in a “light weight” fashion in specifications, while continuing to exploit ACL2’s efficient executability, built in proof techniques for certain domains, and extensive lemma libraries.