; To certify this book #| (ld "defpkg.lisp") (certify-book "recursion-by-choose" 1) |# ; Recursion by Choose ; J Strother Moore ; Abstract ; This book shows an alternative way to define recursive functions on ; sets in the ACL2 finite set theory. We call this ``recursion by ; choose'' and contrast it to ``recursion by scdr,'' which is the ; preferred style. Recursion by choose is nice because it is entirely ; set theoretic while scdr is not. ; Discussion ; The definition of set union provided in ACL2 set theory is ; (defun union (a b) ; (if (ur-elementp a) ; (sfix b) ; (scons (scar a) (union (scdr a) b)))) ; It is defined in terms of the functions scar and scdr which do not ; admit = as a congruence. As noted, we prefer such recursive ; definitions because scar/scdr recursions ``ripple'' through of nests ; of similarly defined functions during induction. Induction and ; recursion are extremely important in this setting since they embody ; the basic set builder notation and allow us to deduce properties of ; the constructed sets. ; In this appendix we illustrate an alternative approach to recursive ; definition which is ``more pure'' from the set theoretic ; perspective. ; Here is a definition of set union defined in a purely set theoretic ; way. By that we mean that the definition in no way exposes the ; underlying list representation of sets. The key is to use (choose ; s) as a way to select an element from a set and to delete it from ; the set upon recursion. The function abc (which stands for ``All ; But Choose'') deletes the element from the set, using diff. ; (defun abc (s) ; (diff s (brace (choose s)))) ; (defun un (a b) ; (declare (xargs :measure (cardinality a))) ; (if (ur-elementp a) ; (sfix b) ; (scons (choose a) (un (abc a) b)))) ; The definition is admitted because the cardinality of the set a ; decreases. ; Now consider proving ; (defthm un-assoc ; (= (un (un a b) c) (un a (un b c)))) ; The corresponding theorem about union is proved by induction in ACL2 ; set theory. The proof is trivial: as easy as the inductive proof of ; the associativity of append --- indeed, it is the associativity of ; append. ; But an inductive proof of un-assoc is more complicated until certain ; groundwork is established. The inductive hypothesis of an induction ; on a is (= (un (un (abc a) b) c) (un (abc a) (un b c))). The trick ; is getting (un (un a b) c) to simplify to something involving (un ; (un (abc a) b) c). The problem is that the inner un expression, (un ; a b), recurs by removing (choose a) from its first argument. But ; the outer un expression recurs by removing (choose (un a b)), which ; is generally different from (choose a). This makes it very ; difficult to deal with un inductively because as similarly defined ; nested applications expand, they decompose successive outputs in ; different ways, i.e., recursions do not ``ripple up'' in the choose ; style because different elements are chosen at each level. ; The key to proving theorems about un is to prove the following lemma ; (= (un (scons e a) b) ; (scons e (un a b))). ; This basically eliminates the use of the recursive definition and its ; ``preference'' to use choose. ; The key to proving this is to prove the following ; fundamental fact: ; (implies (not (ur-elementp a)) ; (= (scons (choose a) (abc a)) a)) ; That is, any set can be thought of as the scons of its choose and ; its abc. ; In order prove the key theorem relating un and scons it is necessary ; to consider both (choose (scons e a)) and (abc (scons e a)). The ; weak choose-scons property is sufficient to handle the first. How ; the second simplifies depends on which element is chosen by the ; first. The following lemma describes both cases, without ; introducing mention of our total order. ; (defthm choose-dichotomy ; (implies (not (ur-elementp a)) ; (or (and (= (choose (scons x a)) x) ; (= (abc (scons x a)) ; (if (= x (choose a)) ; (abc a) ; a))) ; (and (= (choose (scons x a)) (choose a)) ; (= (abc (scons x a)) ; (if (= x (choose a)) ; (abc a) ; (scons x (abc a)))))))) ; If this lemma were part of our set-theory book (it is not, but we ; prove here), and coded so as to be an effective rewrite rule, then ; proofs about functions defined using recursion by choose are no more ; difficult than those defined using scar and scdr. ; In particular, this book configures ACL2 so that it is easy to ; prove: ; (defthm associativity-of-un ; (= (un (un a b) c) (un a (un b c)))) ; (defthm commutativity-of-un ; (= (un a b) (un b a))) ; (defthm union-un ; (= (un a b) (union a b))) ; suggesting that we can deal reasonably well with the alternative scheme. ; We personally prefer the scar and scdr recursion and induction, ; because it so completely converts the set theory problems into the ; domain where ACL2 is most powerful. The = relation is responsible ; for ignoring duplications and order, and so we might as well regard ; our sets as ordered when it makes inductive proofs easier. (in-package "S") (include-book "set-theory") (defun abc (s) (diff s (brace (choose s)))) (defcong = = (abc s) 1) (defthm choose-abc-elim (implies (not (ur-elementp a)) (= (scons (choose a) (abc a)) a)) :rule-classes :elim) (defthm cardinality-abc (implies (not (ur-elementp a)) (< (cardinality (abc a)) (cardinality a))) :rule-classes (:rewrite (:built-in-clause :corollary (implies (not (ur-elementp a)) (e0-ord-< (cardinality (abc a)) (cardinality a)))))) (defthm choose-dichotomy (implies (not (ur-elementp a)) (or (and (= (choose (scons x a)) x) (= (abc (scons x a)) (if (= x (choose a)) (abc a) a))) (and (= (choose (scons x a)) (choose a)) (= (abc (scons x a)) (if (= x (choose a)) (abc a) (scons x (abc a))))))) :rule-classes nil :hints (("Goal" :use ((:instance choose-scons (e x) (a a)) (:instance diff-scons (s a) (e x) (y nil))) :in-theory (disable choose-abc-elim choose-scons diff-scons)))) (defthm abc-singleton (= (abc (scons x nil)) nil)) (in-theory (disable abc)) (defthm e0-ordinalp-cardinality (e0-ordinalp (cardinality a)) :rule-classes :built-in-clause) (defun un (a b) (declare (xargs :measure (cardinality a))) (if (ur-elementp a) (sfix b) (scons (choose a) (un (abc a) b)))) (defthm setp-un (setp (un a b))) ; I have had to prove theorems similar to the one below before. ; But this theorem follows immediately from the one above. ; (thm (implies (setp a) (equal (ur-elementp a) (equal a nil)))) ; Furthermore, I cannot prove the more pure: ; (thm (implies (setp a) (= (ur-elementp a) (= a nil)))) ; Look into this. (defthm ur-elementp-un (equal (ur-elementp (un a b)) (equal (un a b) nil))) (defthm mem-un (equal (mem x (un a b)) (or (mem x a) (mem x b)))) (defx :strategy :congruence (un a b) 1 :method :subsetp) (defx :strategy :congruence (un a b) 2) (defthm L3 (= (un (scons x a) b) (scons x (un a b))) :hints (("Subgoal *1/2'" :use choose-dichotomy))) (defthm associativity-of-un (= (un (un a b) c) (un a (un b c)))) (defthm commutativity-of-un (= (un a b) (un b a))) (defthm union-un (= (un a b) (union a b)))