; 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)))