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