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