#|
Fully Ordered Finite Sets, Version 0.91
Copyright (C) 2003-2006 by Jared Davis
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License as
published by the Free Software Foundation; either version 2 of
the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public Lic-
ense along with this program; if not, write to the Free Soft-
ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
02111-1307, USA.
outer.lisp
This file is the outermost layer of the set theory library. We
have already built up a framework for doing pick-a-point and double
containment proofs in membership.lisp, but we have not even intro-
duced a number of set functions -- deletion, union, intersect,
difference, and so forth.
Here, we introduce these functions and prove many important facts
about them. Taking a quick look through here, it should be obvious
that our automatic strategies are doing a very good job at keeping
saving us from having to provide hints.
|#
(in-package "SETS")
(include-book "fast")
(set-verify-guards-eagerness 2)
; -------------------------------------------------------------------
; Delete
(defun delete (a X)
(declare (xargs :guard (setp X)
:verify-guards nil))
(cond ((empty X) nil)
((equal a (head X)) (tail X))
(t (insert (head X) (delete a (tail X))))))
(defthm delete-set
(setp (delete a X)))
(verify-guards delete)
(defthm delete-preserves-empty
(implies (empty X)
(empty (delete a X))))
(defthm delete-in
(equal (in a (delete b X))
(and (in a X)
(not (equal a b)))))
(defthm delete-sfix-cancel
(equal (delete a (sfix X))
(delete a X)))
(defthm delete-nonmember-cancel
(implies (not (in a X))
(equal (delete a X) (sfix X))))
(defthm delete-delete
(equal (delete a (delete b X))
(delete b (delete a X)))
:rule-classes ((:rewrite :loop-stopper ((a b)))))
(defthm repeated-delete
(equal (delete a (delete a X))
(delete a X)))
(defthm delete-insert-cancel
(equal (delete a (insert a X))
(delete a X)))
(defthm insert-delete-cancel
(equal (insert a (delete a X))
(insert a X)))
(defthm subset-delete
(subset (delete a X) X))
; -------------------------------------------------------------------
; Union
(defun union (X Y)
(declare (xargs :guard (and (setp X) (setp Y))
:verify-guards nil))
(mbe :logic (if (empty X)
(sfix Y)
(insert (head X) (union (tail X) Y)))
:exec (fast-union X Y nil)))
(defthm union-set
(setp (union X Y)))
(defthm union-sfix-cancel-X
(equal (union (sfix X) Y) (union X Y)))
(defthm union-sfix-cancel-Y
(equal (union X (sfix Y)) (union X Y)))
(defthm union-empty-X
(implies (empty X)
(equal (union X Y) (sfix Y))))
(defthm union-empty-Y
(implies (empty Y)
(equal (union X Y) (sfix X))))
(defthm union-empty
(equal (empty (union X Y))
(and (empty X) (empty Y))))
(defthm union-in
(equal (in a (union X Y))
(or (in a X) (in a Y))))
(verify-guards union
:hints(("Goal" :in-theory (enable fast-union-theory))))
(defthm union-symmetric
(equal (union X Y) (union Y X))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm union-subset-X
(subset X (union X Y)))
(defthm union-subset-Y
(subset Y (union X Y)))
(defthm union-insert-X
(equal (union (insert a X) Y)
(insert a (union X Y))))
(defthm union-insert-Y
(equal (union X (insert a Y))
(insert a (union X Y))))
(defthm union-delete-X
(equal (union (delete a X) Y)
(if (in a Y)
(union X Y)
(delete a (union X Y)))))
(defthm union-delete-Y
(equal (union X (delete a Y))
(if (in a X)
(union X Y)
(delete a (union X Y)))))
(defthm union-self
(equal (union X X) (sfix X)))
(defthm union-associative
(equal (union (union X Y) Z)
(union X (union Y Z))))
(defthm union-commutative
(equal (union X (union Y Z))
(union Y (union X Z)))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm union-outer-cancel
(equal (union X (union X Z))
(union X Z)))
; -------------------------------------------------------------------
; Intersect
(defun intersect (X Y)
(declare (xargs :guard (and (setp X) (setp Y))
:verify-guards nil))
(mbe :logic (cond ((empty X) (sfix X))
((in (head X) Y)
(insert (head X) (intersect (tail X) Y)))
(t (intersect (tail X) Y)))
:exec (fast-intersect X Y nil)))
(defthm intersect-set
(setp (intersect X Y)))
(defthm intersect-sfix-cancel-X
(equal (intersect (sfix X) Y) (intersect X Y)))
(defthm intersect-sfix-cancel-Y
(equal (intersect X (sfix Y)) (intersect X Y)))
(defthm intersect-empty-X
(implies (empty X) (empty (intersect X Y))))
(defthm intersect-empty-Y
(implies (empty Y) (empty (intersect X Y))))
(encapsulate ()
(local (defthm intersect-in-Y
(implies (not (in a Y))
(not (in a (intersect X Y))))))
(local (defthm intersect-in-X
(implies (not (in a X))
(not (in a (intersect X Y))))))
(defthm intersect-in
(equal (in a (intersect X Y))
(and (in a Y) (in a X))))
)
(verify-guards intersect
:hints(("Goal" :in-theory (enable fast-intersect-theory))))
(defthm intersect-symmetric
(equal (intersect X Y) (intersect Y X))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm intersect-subset-X
(subset (intersect X Y) X))
(defthm intersect-subset-Y
(subset (intersect X Y) Y))
(defthm intersect-insert-X
(implies (not (in a Y))
(equal (intersect (insert a X) Y)
(intersect X Y))))
(defthm intersect-insert-Y
(implies (not (in a X))
(equal (intersect X (insert a Y))
(intersect X Y))))
(defthm intersect-delete-X
(equal (intersect (delete a X) Y)
(delete a (intersect X Y))))
(defthm intersect-delete-Y
(equal (intersect X (delete a Y))
(delete a (intersect X Y))))
(defthm intersect-self
(equal (intersect X X) (sfix X)))
(defthm intersect-associative
(equal (intersect (intersect X Y) Z)
(intersect X (intersect Y Z))))
(defthm union-over-intersect
(equal (union X (intersect Y Z))
(intersect (union X Y) (union X Z))))
(defthm intersect-over-union
(equal (intersect X (union Y Z))
(union (intersect X Y) (intersect X Z))))
(defthm intersect-commutative
(equal (intersect X (intersect Y Z))
(intersect Y (intersect X Z)))
:rule-classes ((:rewrite :loop-stopper ((X Y)))))
(defthm intersect-outer-cancel
(equal (intersect X (intersect X Z))
(intersect X Z)))
; -------------------------------------------------------------------
; Difference
(defun difference (X Y)
(declare (xargs :guard (and (setp X) (setp Y))
:verify-guards nil))
(mbe :logic (cond ((empty X) (sfix X))
((in (head X) Y) (difference (tail X) Y))
(t (insert (head X) (difference (tail X) Y))))
:exec (fast-difference X Y nil)))
(defthm difference-set
(setp (difference X Y)))
(defthm difference-sfix-X
(equal (difference (sfix X) Y) (difference X Y)))
(defthm difference-sfix-Y
(equal (difference X (sfix Y)) (difference X Y)))
(defthm difference-empty-X
(implies (empty X)
(equal (difference X Y) (sfix X))))
(defthm difference-empty-Y
(implies (empty Y)
(equal (difference X Y) (sfix X))))
(encapsulate ()
(local (defthm difference-in-X
(implies (in a (difference X Y))
(in a X))))
(local (defthm difference-in-Y
(implies (in a (difference X Y))
(not (in a Y)))))
(defthm difference-in
(equal (in a (difference X Y))
(and (in a X)
(not (in a Y)))))
)
(verify-guards difference
:hints(("Goal" :in-theory (enable fast-difference-theory))))
(defthm difference-subset-X
(subset (difference X Y) X))
(defthm subset-difference
(equal (empty (difference X Y))
(subset X Y)))
(defthm difference-over-union
(equal (difference X (union Y Z))
(intersect (difference X Y) (difference X Z))))
(defthm difference-over-intersect
(equal (difference X (intersect Y Z))
(union (difference X Y) (difference X Z))))
(defthm difference-insert-X
(equal (difference (insert a X) Y)
(if (in a Y)
(difference X Y)
(insert a (difference X Y)))))
(defthm difference-insert-Y
(equal (difference X (insert a Y))
(delete a (difference X Y))))
(defthm difference-delete-X
(equal (difference (delete a X) Y)
(delete a (difference X Y))))
(defthm difference-delete-Y
(equal (difference X (delete a Y))
(if (in a X)
(insert a (difference X Y))
(difference X Y))))
(defthm difference-preserves-subset
(implies (subset X Y)
(subset (difference X Z)
(difference Y Z))))
; -------------------------------------------------------------------
; Cardinality
(defun cardinality (X)
(declare (xargs :guard (setp X)
:verify-guards nil))
(mbe :logic (if (empty X)
0
(1+ (cardinality (tail X))))
:exec (length X)))
(verify-guards cardinality
;; Normally we would never want to enable the primitives theory.
;; However, here we need to show that cardinality is equal to
;; len, and for this we need to be able to reason about tail and
;; empty. Think of this as a tiny extension of "fast.lisp"
:hints(("Goal" :in-theory (enable primitives-theory))))
(defthm cardinality-type
(and (integerp (cardinality X))
(<= 0 (cardinality X)))
:rule-classes :type-prescription)
(defthm cardinality-zero-empty
(equal (equal (cardinality x) 0)
(empty x)))
(defthm cardinality-sfix-cancel
(equal (cardinality (sfix X)) (cardinality X)))
(encapsulate ()
(local (defthm cardinality-insert-empty
(implies (empty X)
(equal (cardinality (insert a X)) 1))
:hints(("Goal" :use (:instance cardinality (x (insert a X)))))))
(defthm insert-cardinality
(equal (cardinality (insert a X))
(if (in a X)
(cardinality X)
(1+ (cardinality X)))))
)
(defthm delete-cardinality
(equal (cardinality (delete a X))
(if (in a X)
(1- (cardinality X))
(cardinality X))))
; Now that we have the delete function, we can prove an interesting
; theorem, namely that if (subset X Y) and |X| = |Y|, then X = Y. In
; order to do this, we need to induct by deleting elements from both
; X and Y. This is a little ugly, but along the way we will show the
; nice theorem, subset-cardinality.
(defun double-delete-induction (X Y)
(declare (xargs :guard (and (setp X) (setp Y))))
(if (or (empty X) (empty Y))
(list X Y)
(double-delete-induction (delete (head X) X)
(delete (head X) Y))))
(defthmd subset-double-delete
(implies (subset X Y)
(subset (delete a X) (delete a Y))))
(encapsulate ()
(local (defthm subset-cardinality-lemma
(implies (and (not (or (empty x) (empty y)))
(implies (subset (delete (head x) x)
(delete (head x) y))
(<= (cardinality (delete (head x) x))
(cardinality (delete (head x) y)))))
(implies (subset x y)
(<= (cardinality x) (cardinality y))))
:hints(("goal" :use ((:instance subset-double-delete
(a (head x))
(x x)
(y y)))))))
(defthm subset-cardinality
(implies (subset X Y)
(<= (cardinality X) (cardinality Y)))
:hints(("Goal" :induct (double-delete-induction X Y)))
:rule-classes (:rewrite :linear))
)
(defthmd equal-cardinality-subset-is-equality
(implies (and (setp X)
(setp Y)
(subset X Y)
(equal (cardinality X) (cardinality Y)))
(equal (equal X Y) t))
:hints(("Goal" :induct (double-delete-induction X Y))
("Subgoal *1/2"
:use ((:instance subset-double-delete
(a (head X))
(X X)
(Y Y))
(:instance (:theorem
(implies (equal X Y)
(equal (insert a X) (insert a Y))))
(a (head X))
(X (tail X))
(Y (delete (head X) Y)))))))
(defthm intersect-cardinality-X
(<= (cardinality (intersect X Y)) (cardinality X))
:rule-classes :linear)
(defthm intersect-cardinality-Y
(<= (cardinality (intersect X Y)) (cardinality Y))
:rule-classes :linear)
; There are also some interesting properties about cardinality which
; are more precise.
(defthm expand-cardinality-of-union
(equal (cardinality (union X Y))
(- (+ (cardinality X) (cardinality Y))
(cardinality (intersect X Y))))
:rule-classes :linear)
(defthm expand-cardinality-of-difference
(equal (cardinality (difference X Y))
(- (cardinality X)
(cardinality (intersect X Y))))
:rule-classes :linear)
(defthm intersect-cardinality-subset
(implies (subset X Y)
(equal (cardinality (intersect X Y))
(cardinality X)))
:rule-classes (:rewrite :linear))
(defthm intersect-cardinality-non-subset
(implies (not (subset x y))
(< (cardinality (intersect x y))
(cardinality x)))
:rule-classes :linear)
(defthm intersect-cardinality-subset-2
(equal (equal (cardinality (intersect X Y)) (cardinality X))
(subset X Y)))
(defthm intersect-cardinality-non-subset-2
(equal (< (cardinality (intersect x y)) (cardinality x))
(not (subset x y))))