#|
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.
fast.lisp
The MBE feature in ACL2 version 2.8 provides the opportunity to
introduce functions which take advantage of the set order for good
execution efficiency, while still using simple/nice functions for
reasoning about.
This file contains efficient versions of the union, intersect, and
difference functions, and a few theorems about them. The goal is
to show that for each of these "fast" functions, when given two
sets as inputs:
(1) produces a set, and
(2) has the correct membership properties
These facts can then be used to make an equal-by-membership argu-
ment with the simple versions as required by MBE.
Note that this file is very ugly. There are many factors that con-
tribute to this problem. For one, these functions are written in
terms of cons and therefore we have to consider many cases. This
also means we have lots of subgoals when we do inductions. It is
also challenging to develop a "good" rewrite theory when it comes
to the cons function, which does not have very nice properties when
related to sets.
|#
(in-package "SETS")
(include-book "membership")
(set-verify-guards-eagerness 2)
;;; First we introduce some basic theory about cons and sets. Note
;;; that this theory is disabled at the end of this file. However, if
;;; you are introducing fast versions of new set functions, you can
;;; enable these theorems by enabling cons-theory.
(defthm cons-set
(equal (setp (cons a X))
(and (setp X)
(or (<< a (head X))
(empty X))))
:hints(("Goal" :in-theory (enable primitives-theory))))
(defthm cons-head
(implies (setp (cons a X))
(equal (head (cons a X)) a))
:hints(("Goal" :in-theory (enable primitives-theory))))
(defthm cons-to-insert-empty
(implies (and (setp X)
(empty X))
(equal (cons a X) (insert a X)))
:hints(("Goal" :in-theory (enable primitives-theory))))
(defthm cons-to-insert-nonempty
(implies (and (setp X)
(<< a (head X)))
(equal (cons a X) (insert a X)))
:hints(("Goal" :in-theory (enable primitives-theory
primitive-order-theory))))
(defthm cons-in
(implies (and (setp (cons a X))
(setp X))
(equal (in b (cons a X))
(or (equal a b)
(in b X)))))
;;; These fast versions recur on one or both of their arguments, but
;;; not always the same argument. Hence, we need to introduce a more
;;; flexible measure to prove that they terminate. Fortunately, this
;;; is still relatively simple:
(defun fast-measure (X Y)
(+ (acl2-count X) (acl2-count Y)))
;;; Fast Union
;;;
;;; We want to show that fast union always produces a set, and has the
;;; expected membership property. This is ugly because reasoning
;;; about set order is hard.
;; PATCH (0.91): David Rager noticed that as of v0.9, fast-union was not tail
;; recursive, and submitted an updated version. The original fast-union has
;; been renamed to fast-union-old, and the new fast-union replaces it.
(local (defun fast-union-old (X Y)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X) (setp Y))))
(cond ((empty X) Y)
((empty Y) X)
((equal (head X) (head Y))
(cons (head X) (fast-union-old (tail X) (tail Y))))
((<< (head X) (head Y))
(cons (head X) (fast-union-old (tail X) Y)))
(t (cons (head Y) (fast-union-old X (tail Y)))))))
(local
(encapsulate ()
(local (defthmd fast-union-old-head-weak
(implies (and (setp X)
(setp Y)
(setp (fast-union-old X Y))
(not (equal (head (fast-union-old X Y)) (head X))))
(equal (head (fast-union-old X Y)) (head Y)))
:hints(("Goal"
:in-theory (enable primitive-order-theory)
:use (:instance fast-union-old (X X) (Y Y))))))
(defthm fast-union-old-set
(implies (and (setp X) (setp Y))
(setp (fast-union-old X Y)))
:hints(("Goal"
:in-theory (enable primitive-order-theory))
("Subgoal *1/9"
:use (:instance fast-union-old-head-weak
(X X)
(Y (tail Y))))
("Subgoal *1/7"
:use (:instance fast-union-old-head-weak
(X (tail X))
(Y Y)))
("Subgoal *1/5"
:use (:instance fast-union-old-head-weak
(X (tail X))
(Y (tail Y))))))
(local (defthm fast-union-old-head-strong
(implies (and (setp X) (setp Y))
(equal (head (fast-union-old X Y))
(cond ((empty X) (head Y))
((empty Y) (head X))
((<< (head X) (head Y)) (head X))
(t (head Y)))))
:hints(("Goal"
:in-theory (enable primitive-order-theory))
("Subgoal *1/3" :use
(:instance cons-head
(a (head X))
(X (fast-union-old (tail X) (tail Y))))))))
(defthm fast-union-old-membership
(implies (and (setp X) (setp Y))
(equal (in a (fast-union-old X Y))
(or (in a X) (in a Y))))
:hints(("Goal"
:in-theory (enable primitive-order-theory))
("Subgoal *1/5"
:use (:instance cons-head
(a (head Y))
(X (fast-union-old X (tail Y)))))
("Subgoal *1/4"
:use ((:instance cons-head
(a (head X))
(X (fast-union-old (tail X) Y)))
(:instance cons-to-insert-nonempty
(a (head X))
(X (fast-union-old (tail X) Y)))
(:instance in-insert
(a a)
(b (head X))
(X (fast-union-old (tail X) Y)))))
("Subgoal *1/3"
:use (:instance cons-head
(a (head X))
(X (fast-union-old (tail X) (tail Y)))))))
))
(defun fast-union (x y acc)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp x)
(setp y)
(true-listp acc))))
(cond
((empty x) (revappend acc y))
((empty y) (revappend acc x))
((equal (head x) (head y))
(fast-union (tail x) (tail y) (cons (head x) acc)))
((<< (head x) (head y))
(fast-union (tail x) y (cons (head x) acc)))
(t
(fast-union x (tail y) (cons (head y) acc)))))
(encapsulate
()
(local (defthm lemma
(equal (fast-union x y acc)
(revappend acc (fast-union-old x y)))))
(local (defthm lemma2
(equal (fast-union x y nil)
(fast-union-old x y))))
(defthm fast-union-set
(implies (and (setp X) (setp Y))
(setp (fast-union X Y nil))))
(defthm fast-union-membership
(implies (and (setp X) (setp Y))
(equal (in a (fast-union X Y nil))
(or (in a X) (in a Y))))))
;;; Fast Intersect
;;;
;;; Again we are only interested in showing that fast-intersect
;;; creates sets and has the expected membership property. And again,
;;; the proofs are quite ugly.
;; PATCH (0.91): David Rager noticed that as of v0.9, fast-intersect was not
;; tail recursive, and submitted an updated version. The original
;; fast-intersect has been renamed to fast-intersect-old, and the new
;; fast-intersect replaces it.
(local (defun fast-intersect-old (X Y)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X) (setp Y))))
(cond ((empty X) (sfix X))
((empty Y) (sfix Y))
((equal (head X) (head Y))
(cons (head X)
(fast-intersect-old (tail X) (tail Y))))
((<< (head X) (head Y))
(fast-intersect-old (tail X) Y))
(t (fast-intersect-old X (tail Y))))))
(local
(encapsulate
()
(defthm fast-intersect-old-empty
(implies (empty X)
(equal (fast-intersect-old X Y) (sfix X))))
(local (defthm lemma
(implies (and (not (empty X))
(not (empty Y))
(not (equal (head X) (head Y)))
(not (empty (fast-intersect-old X Y)))
(not (<< (head X) (head Y))))
(not (empty (tail Y))))))
(local (defthm lemma-2
(implies (and (not (empty X))
(not (empty Y))
(not (equal (head X) (head Y)))
(not (empty (fast-intersect-old X Y)))
(<< (head X) (head Y)))
(not (empty (tail X))))))
(local (defthmd fast-intersect-old-head
(implies (and (not (empty X))
(not (empty Y))
(equal (head X) (head Y))
(not (empty (fast-intersect-old X Y))))
(equal (head (fast-intersect-old X Y))
(head X)))
:hints(("Goal" :in-theory (disable cons-set)))))
(local (defthm fast-intersect-old-order-weak
(implies (and (setp X)
(setp Y)
(not (empty X))
(not (empty Y))
(not (empty (fast-intersect-old X Y)))
(<< a (head X))
(<< a (head Y)))
(<< a (head (fast-intersect-old X Y))))
:hints(("Goal" :in-theory (enable primitive-order-theory))
("Subgoal *1/6" :use (:instance fast-intersect-old-head))
("Subgoal *1/5" :use (:instance fast-intersect-old-head))
("Subgoal *1/4" :use (:instance fast-intersect-old-head))
("Subgoal *1/3" :use (:instance fast-intersect-old-head)))))
(local (defthm fast-intersect-old-nonempty-weak
(implies (not (empty (fast-intersect-old X Y)))
(and (not (empty X))
(not (empty Y))))))
(local (defthm lemma-3
(implies (and (not (empty x))
(not (empty y))
(equal (head x) (head y))
(setp (fast-intersect-old (tail x) (tail y)))
(setp x)
(setp y))
(setp (fast-intersect-old x y)))
:hints(("Goal" :in-theory (e/d (primitive-order-theory)
(cons-set
fast-intersect-old-nonempty-weak
fast-intersect-old-order-weak))
:use ((:instance fast-intersect-old-nonempty-weak
(x (tail x))
(y (tail y)))
(:instance fast-intersect-old-order-weak
(a (head X))
(X (tail X))
(Y (tail Y))))))))
(defthm fast-intersect-old-set
(implies (and (setp X) (setp Y))
(setp (fast-intersect-old X Y)))
:hints(("Goal" :in-theory (enable primitive-order-theory))
("Subgoal *1/5" :use (:instance lemma-3))))
(defthm fast-intersect-old-membership
(implies (and (setp X) (setp Y))
(equal (in a (fast-intersect-old X Y))
(and (in a X) (in a Y))))
:hints(("Goal" :in-theory (enable primitive-order-theory
head-minimal))
("Subgoal *1/3" :use (:instance fast-intersect-old-order-weak
(a (head X))
(X (tail X))
(Y (tail Y))))))
))
(defun fast-intersect (X Y acc)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X)
(setp Y)
(true-listp acc))))
(cond ((empty X) (reverse acc))
((empty Y) (reverse acc))
((equal (head X) (head Y))
(fast-intersect (tail X)
(tail Y)
(cons (head X) acc)))
((<< (head X) (head Y))
(fast-intersect (tail X) Y acc))
(t (fast-intersect X (tail Y) acc))))
(encapsulate
()
(local (defthm lemma
(implies (true-listp acc)
(equal (fast-intersect x y acc)
(revappend acc (fast-intersect-old x y))))
:hints (("Goal" :in-theory (enable sfix empty)))))
(local (defthm lemma2
(equal (fast-intersect x y nil)
(fast-intersect-old x y))))
(defthm fast-intersect-empty
(implies (empty X)
(equal (fast-intersect X Y nil)
(sfix X))))
(defthm fast-intersect-set
(implies (and (setp X) (setp Y))
(setp (fast-intersect X Y nil))))
(defthm fast-intersect-membership
(implies (and (setp X) (setp Y))
(equal (in a (fast-intersect X Y nil))
(and (in a X) (in a Y)))))
)
;;; Fast Difference
;;;
;;; As before, we want to show that difference always creates a set
;;; and that the produced set has the expected membership properties.
;;; Also as before, these proofs are ugly.
;; PATCH (0.91): David Rager noticed that as of v0.9, fast-difference was not
;; tail recursive, and submitted an updated version. The original
;; fast-difference has been renamed to fast-difference-old, and the new
;; fast-difference replaces it.
(defun fast-difference-old (X Y)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X) (setp Y))))
(cond ((empty X) (sfix X))
((empty Y) X)
((equal (head X) (head Y))
(fast-difference-old (tail X) (tail Y)))
((<< (head X) (head Y))
(cons (head X) (fast-difference-old (tail X) Y)))
(t (fast-difference-old X (tail Y)))))
(local
(encapsulate ()
(local (defthm lemma
(implies (and (not (empty X))
(not (empty Y))
(not (empty (fast-difference-old X Y)))
(not (equal (head X) (head Y)))
(<< (head X) (head Y)))
(equal (head (fast-difference-old X Y))
(head X)))
:hints(("Goal"
:in-theory (disable cons-set)
:use (:instance cons-head
(a (head X))
(X (fast-difference-old (tail X) Y)))))))
(local (defthm lemma2
(implies (and (not (empty X))
(not (empty Y))
(not (empty (fast-difference-old X Y)))
(equal (head X) (head Y)))
(not (empty (tail X))))))
(local (defthm fast-difference-old-order-weak
(implies (and (not (empty X))
(not (empty (fast-difference-old X Y)))
(<< a (head X)))
(<< a (head (fast-difference-old X Y))))
:hints(("Goal" :in-theory (enable primitive-order-theory))
("Subgoal *1/9" :use (:instance lemma))
("Subgoal *1/8" :use (:instance lemma))
("Subgoal *1/7" :use (:instance lemma)))))
(defthm fast-difference-old-set
(implies (and (setp X) (setp Y))
(setp (fast-difference-old X Y)))
:hints(("Goal" :in-theory (enable primitive-order-theory))
("Subgoal *1/7" :use (:instance fast-difference-old-order-weak
(a (head X))
(X (tail X))
(Y Y)))))
(defthm fast-difference-old-membership
(implies (and (setp X) (setp Y))
(equal (in a (fast-difference-old X Y))
(and (in a X)
(not (in a Y)))))
:hints(("Goal" :in-theory (enable primitive-order-theory
head-minimal))
("Subgoal *1/4" :use (:instance fast-difference-old-order-weak
(a (head X))
(X (tail X))
(Y Y)))))
(defthm fast-difference-old-empty
(implies (empty X)
(equal (fast-difference-old X Y) (sfix X))))
))
(defun fast-difference (X Y acc)
(declare (xargs :measure (fast-measure X Y)
:guard (and (setp X) (setp Y) (true-listp acc))))
(cond ((empty X) (reverse acc))
((empty Y) (revappend acc X))
((equal (head X) (head Y))
(fast-difference (tail X) (tail Y) acc))
((<< (head X) (head Y))
(fast-difference (tail X) Y (cons (head X) acc)))
(t (fast-difference X (tail Y) acc))))
(encapsulate
()
(local (defthm lemma
(implies (empty x)
(not (sfix x)))
:hints(("Goal" :in-theory (enable empty sfix)))))
(local (defthm lemma2
(implies (true-listp acc)
(equal (fast-difference x y acc)
(revappend acc (fast-difference-old x y))))))
(local (defthm lemma3
(equal (fast-difference x y nil)
(fast-difference-old x y))))
(defthm fast-difference-set
(implies (and (setp X) (setp Y))
(setp (fast-difference X Y nil))))
(defthm fast-difference-membership
(implies (and (setp X) (setp Y))
(equal (in a (fast-difference X Y nil))
(and (in a X)
(not (in a Y))))))
(defthm fast-difference-empty
(implies (empty X)
(equal (fast-difference X Y nil)
(sfix X))))
)
;;; We don't really want to reason about these functions again. So,
;;; we will go ahead and disable all these theorems and put them into
;;; nice packages for the future.
(deftheory fast-union-theory
'(fast-union-set
fast-union-membership))
(deftheory fast-intersect-theory
'(fast-intersect-set
fast-intersect-membership
fast-intersect-empty))
(deftheory fast-difference-theory
'(fast-difference-set
fast-difference-membership
fast-difference-empty))
(deftheory cons-theory
'(cons-set
cons-head
cons-to-insert-empty
cons-to-insert-nonempty
cons-in))
(in-theory (disable fast-measure
fast-union
fast-intersect
fast-difference
fast-union-theory
fast-intersect-theory
fast-difference-theory
cons-theory))