#|
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.
map.lisp
This is an optional extension of the sets library, and is not
included by default when you run (include-book "sets").
Mappings Between Sets.
We create the macro map-function, which introduces the following
functions for any arbitrary transformation function.
map
map-list
In addition to introducing these functions, a large rewriting
strategy is developed for reasoning about the new mapping
functions.
Introductory Examples.
Here are some simple examples. These transformation functions have
only a single argument, and are guarded to operate on any inputs.
(SETS::map-function (integerp x))
- (SETS::map '(1 2 3)) = (t)
- (SETS::map-list '(1 a 2 b)) = (t nil t nil)
(defun square (x)
(declare (xargs :guard t))
(* (rfix x) (rfix x)))
(SETS::map-function (square x))
- (SETS::map '(1 2 3)) = (1 4 9)
- (SETS::map '(a b c)) = (0)
Note that you cannot use macros here. For example, you cannot map
real/rationalp, because it is not a function.
Controlling Packages.
As you can see, the new map functions are added to the SETS
package by default. If you would like them to be in a new place,
you can use the :in-package-of argument to map-function. For
example, since defthm is in the ACL2 package, we can run:
(SETS::map-function (square x)
:in-package-of defthm)
And map will be created in the ACL2 package instead of
the sets package.
Multi-Argument Transformation Functions.
You can also introduce transformations with multiple arguments.
As an example, we introduce the function square-then-add, which
first squares its input and then adds some offset to it.
(defun square-then-add (input offset)
(declare (xargs :guard t))
(+ (* (rfix input) (rfix input))
(rfix offset)))
(SETS::map-function (square-then-add input offset)
:in-package-of defthm)
(map '(1 2 3) 5) => (6 9 14)
Supporting Guards.
We can support transformation functions that require guards by
sending extra arguments to the map-function macro. As an example,
we consider what it would require to write a mapping function for
the function below.
(defun plus (x y)
(declare (xargs :guard (and (integerp x) (rationalp y))))
(+ x y))
(quantify-predicate (integerp x)) ; see quantify.lisp for explanation
(map-function (plus arg1 arg2)
:set-guard ((all ?set)) ; set's name must be ?set
:list-guard ((all-list ?list)) ; list's name must be ?list
:element-guard ((integerp a)) ; element's name must be a
:arg-guard ((rationalp arg2))) ; extra arg names specified above
|#
(in-package "SETS")
(include-book "quantify")
(set-verify-guards-eagerness 2)
; The need for the following theorems is depressing and distressing.
; I haven't figured out a way around them yet. Maybe they need to be
; added into the main sets books, but they seem to only be an issue
; here.
(defthm map-subset-helper
(implies (and (not (empty x))
(in (head x) y))
(equal (subset (tail x) y)
(subset x y)))
:hints(("Goal" :expand (subset x y))))
(defthm map-subset-helper-2
(implies (and (not (empty x))
(not (in (head x) y)))
(not (subset x y))))
; We will map an arbitrary transformation function across the set. We
; don't assume anything about transform.
(encapsulate
(((transform *) => *))
(local (defun transform (x) x)))
; Now we introduce our mapping functions. We allow the transform to
; be mapped across a list or a set. Under the hood, we use MBE to
; ensure that we first transform every element of the set, and then
; mergesort the results. This gives O(n) + O(n log n) performance
; intead of the O(n^2) required for repeated insertion. We introduce
; these functions as a constant, so we can rewrite it later to
; actually create maps.
(defconst *map-functions* '(
(defun map-list (x)
(declare (xargs :guard (true-listp x)))
(if (endp x)
nil
(cons (transform (car X))
(map-list (cdr X)))))
(defun map (X)
(declare (xargs :guard (setp X)))
(declare (xargs :verify-guards nil))
(mbe :logic (if (empty X)
nil
(insert (transform (head X))
(map (tail X))))
:exec (mergesort (map-list X))))
; A crucial component of our reasoning is the notion of the inverse of
; the transform. We define the relation (inversep a b), which is true
; if and only if a is an inverse of b under transform -- that is,
; (inversep a b) is true when (transform a) = b.
(defun inversep (a b)
(declare (xargs :guard t))
(equal (transform a) b))
))
(INSTANCE::instance *map-functions*)
(instance-*map-functions*)
; We now quantify over the predicate inversep, allowing us to talk
; about the existence of inverses in sets.
(quantify-predicate (inversep a b))
; Again we begin introducing theorems as a constant, so that we can
; instantiate concrete theories of mapping by rewriting.
(defconst *map-theorems* '(
(defthm map-setp
(setp (map X)))
(defthm map-sfix
(equal (map (sfix X))
(map X)))
; The ordered sets library works really well when you can provide a
; concise statement about membership for your new functions. Here, we
; use the idea of inverses in order to explain what it means to be a
; member in a map. Basically, (in a (map X)) is exactly equal to
; (exists X a), i.e., if there is an inverse of a in x. We
; then manually apply our "exists elimination" to make this theorem a
; little more direct.
(defthm map-in
(equal (in a (map X))
(not (all X a))))
; With this notion of membership in play, we can now use the
; properties of all in order to prove many interesting
; theorems about mappings through standard membership arguments.
(defthm map-subset
(implies (subset X Y)
(subset (map X) (map Y))))
(defthm map-insert
(equal (map (insert a X))
(insert (transform a) (map X))))
(defthm map-delete
(subset (delete (transform a) (map X))
(map (delete a X))))
(defthm map-union
(equal (map (union X Y))
(union (map X) (map Y))))
(defthm map-intersect
(subset (map (intersect X Y))
(intersect (map X) (map Y))))
(defthm map-difference
(subset (difference (map X) (map Y))
(map (difference X Y))))
(defthm map-cardinality
(<= (cardinality (map X))
(cardinality X))
:rule-classes :linear)
; We now provide some theorems about mapping over lists. These are
; somewhat nice in and of themselves, but also allow us to prove our
; mbe equivalence so that our mapping operations are more efficient.
; To begin, we prove the characteristic list membership theorem for
; mapping over lists.
(defthm map-list-in-list
(equal (in-list a (map-list X))
(exists-list X a)))
(defthm map-mergesort
(equal (map (mergesort X))
(mergesort (map-list X))))
; And finally we prove this theorem, which will be useful for
; verifying the guards of map.
(defthm map-mbe-equivalence
(implies (setp X)
(equal (mergesort (map-list X))
(map X))))
; We finish up our theory with some more, basic theorems about
; mapping over lists.
(defthm map-list-cons
(equal (map-list (cons a x))
(cons (transform a)
(map-list x))))
(defthm map-list-append
(equal (map-list (append x y))
(append (map-list x)
(map-list y))))
(defthm map-list-nth
(implies (and (integerp n)
(<= 0 n)
(< n (len x)))
(equal (nth n (map-list x))
(transform (nth n x)))))
(defthm map-list-revappend
(equal (map-list (revappend x acc))
(revappend (map-list x)
(map-list acc))))
(defthm map-list-reverse
(equal (map-list (reverse x))
(reverse (map-list x))))
))
(INSTANCE::instance *map-theorems*)
(instance-*map-theorems*)
(verify-guards map)
; This is a nice generic theory, but to be useful, we will need to be
; able to instantiate concrete theories based on it. We do this with
; the following function, for which we introduce a corresponding
; macro.
(defun map-function-fn (function in-package
set-guard
list-guard
element-guard
arg-guard)
(declare (xargs :mode :program))
(let* ((name (car function))
(extra-args (cddr function))
(wrap (app "<" (app (symbol-name name) ">")))
;; First we build up all the symbols that we will use.
(map (mksym (app "map" wrap) in-package))
(map-list (mksym (app "map-list" wrap) in-package))
(inversep (app "inversep" wrap))
(ipw (app "<" (app inversep ">")))
(not-ipw (app "")))
(inversep (mksym inversep in-package))
(all> (mksym (app "all" ipw) in-package))
(exists> (mksym (app "exists" ipw) in-package))
(find> (mksym (app "find" ipw) in-package))
(filter> (mksym (app "filter" ipw) in-package))
(all-list> (mksym (app "all-list" ipw) in-package))
(exists-list> (mksym (app "exists-list" ipw) in-package))
(find-list> (mksym (app "find-list" ipw) in-package))
(filter-list> (mksym (app "filter-list" ipw) in-package))
(all> (mksym (app "all" not-ipw) in-package))
(exists> (mksym (app "exists" not-ipw) in-package))
(find> (mksym (app "find" not-ipw) in-package))
(filter> (mksym (app "filter" not-ipw) in-package))
(all-list> (mksym (app "all-list" not-ipw) in-package))
(exists-list> (mksym (app "exists-list" not-ipw) in-package))
(find-list> (mksym (app "find-list" not-ipw) in-package))
(filter-list> (mksym (app "filter-list" not-ipw) in-package))
(subs `(((transform ?x) (,name ?x ,@extra-args))
((map ?x) (,map ?x ,@extra-args))
((map-list ?x) (,map-list ?x ,@extra-args))
((inversep ?a ?b) (,inversep ?a ?b ,@extra-args))
((all ?a ?b) (,all> ?a ?b ,@extra-args))
((exists ?a ?b) (,exists> ?a ?b ,@extra-args))
((find ?a ?b) (,find> ?a ?b ,@extra-args))
((filter ?a ?b) (,filter> ?a ?b ,@extra-args))
((all-list ?a ?b) (,all-list> ?a ?b ,@extra-args))
((exists-list ?a ?b) (,exists-list> ?a ?b ,@extra-args))
((find-list ?a ?b) (,find-list> ?a ?b ,@extra-args))
((filter-list ?a ?b) (,filter-list> ?a ?b ,@extra-args))
((all ?a ?b) (,all> ?a ?b ,@extra-args))
((exists ?a ?b) (,exists> ?a ?b ,@extra-args))
((find ?a ?b) (,find> ?a ?b ,@extra-args))
((filter ?a ?b) (,filter> ?a ?b ,@extra-args))
((all-list ?a ?b) (,all-list> ?a ?b ,@extra-args))
((exists-list ?a ?b) (,exists-list> ?a ?b ,@extra-args))
((find-list ?a ?b) (,find-list> ?a ?b ,@extra-args))
((filter-list ?a ?b) (,filter-list> ?a ?b ,@extra-args))
))
(theory (mksym (app "map-theory" wrap) in-package))
(suffix (mksym wrap in-package))
(thm-names (INSTANCE::defthm-names *map-theorems*))
(thm-name-map (INSTANCE::create-new-names thm-names suffix))
(theory-defthms (sublis thm-name-map thm-names))
)
`(encapsulate ()
(instance-*map-functions*
:subs ,(list* `((declare (xargs :guard (setp ?set)))
(declare (xargs :guard (and (setp ?set)
,@set-guard
,@arg-guard))))
`((declare (xargs :guard (true-listp ?list)))
(declare (xargs :guard (and (true-listp ?list)
,@list-guard
,@arg-guard))))
`((declare (xargs :guard t))
(declare (xargs :guard (and ,@element-guard
,@arg-guard))))
subs)
:suffix ,name)
(quantify-predicate (,inversep a b ,@extra-args)
:in-package-of ,in-package
:set-guard ,set-guard
:list-guard ,list-guard
:arg-guard ,arg-guard)
(instance-*map-theorems*
:subs ,subs
:suffix ,(mksym wrap in-package))
(verify-guards ,map)
(deftheory ,theory
(union-theories
(theory ',(mksym (app "theory" ipw) in-package))
'(,map ,map-list ,inversep
,@theory-defthms)))
)))
(defmacro map-function (function &key in-package-of
set-guard
list-guard
element-guard
arg-guard)
(map-function-fn function
(if in-package-of in-package-of 'in)
(standardize-to-package "?SET" '?set set-guard)
(standardize-to-package "?LIST" '?list list-guard)
(standardize-to-package "A" 'a element-guard)
arg-guard
))
(deftheory generic-map-theory
(union-theories (theory 'theory)
`(,@(INSTANCE::defthm-names *map-theorems*)
map
map-list
inversep)))
(in-theory (disable generic-map-theory))