; To certify this book
#|
(ld "defpkg.lisp")
(certify-book "set-count" 1)
|#
; Proving Things About Ordered Pairs
; It is possible to arrange things so that set theoretic ordered pairs
; are as convenient for the set theory user as ACL2's native cons
; pairs are for the ACL2 user.
; In this book, set-count.lisp, I define a function that measures the
; size of a set, taking into account the size of the elements. We
; prove that the hd and tl of a pair have smaller set-counts than the
; pair. This means it is possible to define recursive functions that
; recur by hd and tl, using set-count as the justifying measure.
; After defining a function that recurs this way, it is, of course,
; necessary to prove that it admits = as a congruence. That can be
; done conveniently using a method implemented in set-count.lisp.
; Once these preliminaries are done, it is convenient to prove
; theorems about recursive pair processing functions. For example,
; below we define a version of Lisp's append that uses ordered pairs.
(in-package "S")
(include-book "set-theory")
(defthm acl2-count-scar
(implies (not (ur-elementp a))
(e0-ord-< (acl2-count (scar a))
(acl2-count a)))
:hints (("Goal" :in-theory (enable scar ur-elementp)))
:rule-classes
((:built-in-clause)
(:linear :corollary
(implies (not (ur-elementp a))
(< (acl2-count (scdr a))
(acl2-count a))))))
(defun set-count (s)
(if (ur-elementp s)
0
(if (mem (scar s) (scdr s))
(set-count (scdr s))
(+ 1
(set-count (scar s))
(set-count (scdr s))))))
; (defx :strategy :congruence (set-count s) 1 :method :canonicalize)
; I added = to the enable hint.
(ENCAPSULATE NIL
(LOCAL (IN-THEORY (ENABLE = SCONS SCAR SCDR UR-ELEMENTP)))
(DEFTHM SET-COUNT-SET-INSERT
(IMPLIES (AND (CANONICALP E) (CANONICALP S))
(EQUAL (SET-COUNT (SET-INSERT E S))
(SET-COUNT (CONS E S))))
:HINTS
(("Goal" :INDUCT (SET-INSERT E S))))
(DEFTHM SET-COUNT-CANONICALIZE
(EQUAL (SET-COUNT (CANONICALIZE S))
(SET-COUNT S)))
(DEFCONG = EQUAL (SET-COUNT S)
1 :HINTS
(("Goal" :IN-THEORY
(DISABLE SET-COUNT-CANONICALIZE)
:USE
((:INSTANCE SET-COUNT-CANONICALIZE (S S))
(:INSTANCE SET-COUNT-CANONICALIZE
(S ACL2::S-EQUIV)))))))
(defthm set-count-mem
(implies (mem e s)
(< (set-count e) (set-count s)))
:rule-classes nil)
(defthm set-count-choose
(implies (case-split (not (ur-elementp s)))
(< (set-count (choose s)) (set-count s)))
:hints (("Goal" :use (:instance set-count-mem (e (choose s)))))
:rule-classes :linear)
(defthm e0-ordinalp-set-count
(e0-ordinalp (set-count x))
:rule-classes :built-in-clause)
(defthm set-count=0
(equal (equal (set-count x) 0)
(ur-elementp x)))
(defthm set-count-union
(implies (ur-elementp (intersection a b))
(equal (set-count (union a b))
(+ (set-count a)
(set-count b)))))
(defx subset-singleton
(implies (and (not (ur-elementp b))
(subsetp b (scons e nil)))
(= b (scons e nil)))
:rule-classes nil
:strategy :set-equivalence)
(defthm scons-diff-scons-gen
(implies (mem b1 a)
(= (scons b1 (diff a (scons b1 b)))
(if (mem b1 b)
(scons b1 (diff a b))
(diff a b)))))
; Note: This is a sort of ugly lemma and a nice proof. But the
; goal, union-diff, is quite nice.
(defthm scons-union-diff-scons
(implies (and (mem b1 a)
(subsetp b a))
(= (scons b1 (union b (diff a (scons b1 b))))
(union b (diff a b))))
:hints (("Goal" :in-theory (disable union-scons
diff-scons-1
commutativity-of-union)
:use (:instance union-scons
(e b1)
(a b)
(b (diff a (scons b1 b)))))))
(defthm union-diff
(implies (subsetp b a)
(= (union b (diff a b))
(sfix a)))
:hints (("Goal" :in-theory (disable diff-scons-1))
("Subgoal *1/3.2'" :use (:instance subset-singleton
(e SR)
(b A)))))
; These proofs are ugly because I am working in a hurry. Really, I am
; writing my report and just wanted to say it was possible to recur by
; hd and tl.
(defthm set-count-diff
(implies (subsetp b a)
(equal (set-count (diff a b))
(- (set-count a) (set-count b))))
:hints (("Goal"
:in-theory (disable set-count-union)
:use (:instance set-count-union
(a (diff a b))
(b b)))))
(defthm cardinality-2-non-ur-elementp
(implies (equal (cardinality x) 2)
(not (ur-elementp x))))
(defthm set-count-hd
(implies (pairp x)
(e0-ord-< (set-count (hd x))
(set-count x)))
:hints (("Goal"
:in-theory (enable hd pairp))
("Subgoal 1"
:in-theory (disable set-count-choose)
:use (:instance set-count-choose
(s (DIFF X (SCONS (CHOOSE X) NIL))))))
:rule-classes
((:built-in-clause)
(:linear :corollary
(implies (pairp x)
(< (set-count (hd x))
(set-count x))))))
; The next proof is even uglier than the last. I reiterate: I did
; these proofs in a hurry while writing the report, just so I could
; say it could be done.
(encapsulate
nil
(local
(defthm lemma1-helper
(IMPLIES (and (= (SCONS (CHOOSE (DIFF X (SCONS (CHOOSE X) NIL)))
NIL)
xxx)
(MEM (CHOOSE (DIFF X (SCONS (CHOOSE X) NIL)))
(CHOOSE X)))
(SUBSETP xxx
(CHOOSE X)))
:rule-classes nil))
(local
(defthm lemma1
(implies (and (equal (cardinality x) 2)
(MEM (CHOOSE (DIFF X (SCONS (CHOOSE X) NIL)))
(CHOOSE X)))
(SUBSETP (DIFF X (SCONS (CHOOSE X) NIL))
(CHOOSE X)))
:rule-classes nil
:hints
(("Goal"
:in-theory (disable elim-choose-singleton)
:use ((:instance lemma1-helper
(xxx (DIFF X (SCONS (CHOOSE X) NIL))))
(:instance elim-choose-singleton
(x (DIFF X (SCONS (CHOOSE X) NIL)))))))))
(defthm set-count-tl
(implies (pairp x)
(e0-ord-< (set-count (tl x))
(set-count x)))
:hints (("Goal"
:in-theory (enable tl pairp))
("Subgoal 1"
:in-theory (disable set-count-choose)
:use (:instance set-count-choose
(s (diff (choose x)
(DIFF X (SCONS (CHOOSE X) NIL))))))
("Subgoal 1.1"
:in-theory (disable set-count-choose set-count-diff)
:use ((:instance lemma1)
(:instance set-count-diff
(a (choose x))
(b (DIFF X (SCONS (CHOOSE X) NIL))))))
("Subgoal 1.1''"
:in-theory (enable set-count-choose)))
:rule-classes
((:built-in-clause)
(:linear :corollary
(implies (pairp x)
(< (set-count (tl x))
(set-count x)))))))
; So here is the classic theorem...
(defun pair-append (x y)
(declare (xargs :measure (set-count x)))
(if (pairp x)
(pair (hd x)
(pair-append (tl x) y))
y))
(defun pair-equal-hint (u v)
(declare (xargs :measure (set-count u)))
(if (pairp u)
(if (pairp v)
(list (pair-equal-hint (hd u) (hd v))
(pair-equal-hint (tl u) (tl v)))
(list u v))
(list u v)))
(defcong = = (pair-append x y) 1
:hints (("Goal" :induct (pair-equal-hint x acl2::x-equiv))))
(defx :strategy :congruence (pair-append x y) 2)
(defthm pair-append-is-associative
(= (pair-append (pair-append a b) c)
(pair-append a (pair-append b c))))