diff options
Diffstat (limited to 'books/workshops/2004/davis')
17 files changed, 6181 insertions, 0 deletions
diff --git a/books/workshops/2004/davis/set-theory.pdf.gz b/books/workshops/2004/davis/set-theory.pdf.gz Binary files differnew file mode 100644 index 0000000..3b659f9 --- /dev/null +++ b/books/workshops/2004/davis/set-theory.pdf.gz diff --git a/books/workshops/2004/davis/support/CHANGES.html b/books/workshops/2004/davis/support/CHANGES.html new file mode 100644 index 0000000..8130a8f --- /dev/null +++ b/books/workshops/2004/davis/support/CHANGES.html @@ -0,0 +1,184 @@ +<html> +<head> +<title>Osets Change Log</title> +<link rel="stylesheet" href="http://www.cs.utexas.edu/users/jared/style.css" + type="text/css"/> +</head> +<body> + +<table border="0" width="100%" bgcolor="#f0f0f0" class="logo" + cellpadding="8"> +<tr> +<td align="center" class="logoText"> +Finite Set Theory based on Fully Ordered Lists<br/> +</td> +</tr> +</table> + +<h3>Change Log</h3> + +<h4>Version 0.9, October 22, 2004</h4> + +<p>This is a major release.</p> + + <p><em>The library now requires ACL2 2.9.</em></p> + + <p><em>The set order has been changed.</em> We now use the same + <tt><<</tt> as the total-order book. Effectively, we make + fewer assumptions about the set order, no longer requiring that nil + be the greatest element. This change might allow us to consider + custom set orders in the future. This was a bit of an undertaking. + Many proofs in <tt>membership.lisp</tt> and <tt>fast.lisp</tt> have + been changed to avoid relying on <tt>nil</tt>'s maximality. There + are also some changes in other low level theorems, such as + <tt>head-insert</tt>. There should be little or no impact on user + theorems, unless you were reasoning "from first principles", e.g., + for "fast" functions defined using <tt>cons</tt> and so forth.</p> + + <p><em>Computed hints are now automatically managed.</em> + Previously, the macros <tt>enable/disable-set-reasoning</tt> were + used to turn on the computed hint for conducting pick-a-point + proofs. These macros have been removed and are no longer necessary, + and pick-a-point proofs are automatically enabled. (To disable + them, disable the "tagging" theorem, + <tt>pick-a-point-subset-strategy</tt>, instead.) Thanks to Matt + Kaufmann for modifying ACL2 to permit this change.</p> + + <p><em><tt>Membership.lisp</tt> has been cleaned up.</em> The + support for computed hints have been separated out and put into its + own package, <tt>COMPUTED-HINTS</tt>. The encapsulate event which + the pick-a-point subset strategy was based on is now more general + and can be used with the new extensions in this release. The + pick-a-point method is now developed earlier in the membership.lisp + file, and is used in order to prove many of the theorems which used + to be based on induction arguments, e.g., <tt>subset-reflexive</tt>. + </p> + + <p><em>A new package, <tt>INSTANCE</tt>, has been added to support + the new extensions.</em> Users should not need to use this package + directly.</p> + + <p><em>New extension: constructive quantification.</em> This + extension (in <tt>quantify.lisp</tt>) completely replaces typed sets + with a more general and powerful theory of constructive + quantification. Given a k-ary (k > 1) predicate <tt>P</tt>, you can + now quickly introduce a theory of quantification for that predicate + over sets and lists.</p> + + <p><em>New extension: mappings.</em> Building off the base provided + by constructive quantification, mappings allow you to discuss the + images of sets under some arbitrary k-ary function, F, where (k > 1). + As with constructive quantification, an elaborate rewriting strategy + is also introduced for reasoning about mappings. Mappings are also + implemented more efficiently (via MBE) than the naive implementation + using repeated insertion.</p> + + <p><em>Mergesort is easier to reason about.</em> <tt>Mergesort</tt> + now has a new logical definition via MBE, so that you can reason + about it as if it were a simple, recursive insert sort. Of course, + it still acts as an efficient mergesort under the hood. Thanks to + Serita Nelesen for pointing out the deficiencies with the previous + approach. I've also done away with the use of <tt>member-equal</tt>, + and instead a new <tt>in-list</tt> function has been added which + returns a boolean instead of part of the list.</p> + + <p><em>Cardinality reasoning has been improved.</em> This is + particularly true with regards to the cardinalities of + intersections. Added theorems <tt>cardinality-zero-empty</tt>, + <tt>intersect-cardinality-non-subset</tt>, + <tt>intersect-cardinality-subset-2</tt>, and + <tt>intersect-cardinality-non-subset-2</tt>. Also changed + <tt>intersect-cardinality-subset</tt> to also be a :rewrite rule in + addition to being :linear. Thanks to Robert Krug and Hanbing Liu + for their input in these changes.</p> + + <p><em>Subset reasoning has been improved.</em> Added the theorem + <tt>subset-tail</tt> at Hanbing Liu's suggestion, which is useful + for induction-style proofs of subset. Also, the theorems + <tt>difference-preserves-subset</tt> and <tt>subset-delete</tt>, + have been added at Omar El-Domeiri's suggestion. Finally, + <tt>subset-insert</tt> has been added, and parallels + <tt>subset-delete</tt>.</p> + + +<h4>Version 0.81, March 23, 2004</h4> + +<p>This is a minor release to merge the library with ACL2.</p> + + <p><em>Matt Kaufmann has integreated the library with ACL2.</em> The + library will now be part of the standard books released with ACL2. + The build system has been modified to work nicely with ACL2's + makefiles, changed the computed hints functions to be program mode + in order to fix some problems with the new, more stringent guard + checking in ACL2 2.8. He has also updated the README to be more + accurate about what is built, and cleaned up the stray parentheses + in membership.lisp. Thanks, Matt!</p> + + +<h4>Version 0.8, March 18, 2004</h4> + +<p>This is a significant release, involving significant cleanup work +and a few new theorems.</p> + + <p><em>The build system has been significantly improved.</em> A file + <tt>package.lisp</tt> has been added, and now contains the defpkg + event for the set theory books, so you can now simply "ld" this file + to get the set theory package. The <tt>.acl2</tt> have been changed + so that they do not contain include-book events, and + <tt>sets.lisp</tt> now includes the other books locally and then + redefines events from those books. This approach makes loading + <tt>sets.lisp</tt> faster, allows us to export events in a better + order, and hides all of the local proofs. These changes have all + been made at the suggestion of Eric Smith. Thanks! + </p> + + <p><em>A mergesort has been added.</em> This allows you to quickly + create a set from an unordered list which may contain duplicates, + and its performance seems quite good.</p> + + <p><em>Optional set order reasoning is now available.</em> The file + <tt>set-order.lisp</tt> has been added and can be optionally + included to help with reasoning about the set order. Of course, + this should only be done if you are arguing from "first principles" + that your functions create sets, and should otherwise generally be + avoided.</p> + + <p><em>Double containment is now a rewrite rule.</em> A new theorem, + double-containment, has been added in order to explicitly rewrite + equalities between sets into mutual subset statements. The computed + hints which previously performed double containment proofs have been + removed. + + <p><em>Computed hints can now be easily disabled.</em> The macro + <tt>disable-set-reasoning</tt> has been added, and can be used to + turn off the pick-a-point proofs that enable-set-reasoning turns + on.</p> + + <p><em>Some new theorems help fill out the rewriting strategy.</em> + In particular, the theorems <tt>difference-insert-X/Y</tt> and + <tt>difference-delete-X/Y</tt> were added.</p> + + +<h4>Version 0.7, Feb 19, 2004</h4> + +<p>This is a minor release, mainly introducing a new extension.</p> + + <p><em>A new induction scheme is now used for insert.</em> This + induction scheme rephrases insert's operation in terms of membership + rather than the set order, allowing inductive proofs over the + definition of insert to avoid introducing the set order into + proofs.</p> + + <p><em>New extension: typed sets.</em> This extension allows you to + introduce a theory about sets which contain elements of a fixed + type, e.g., <tt>integerp</tt>.</p> + + + +<h4>Version 0.6, Feb 1, 2004</h4> + +<p>This is the first publically available version of the set theory +library.</p> + +</body> +</html>
\ No newline at end of file diff --git a/books/workshops/2004/davis/support/README b/books/workshops/2004/davis/support/README new file mode 100644 index 0000000..bdff10c --- /dev/null +++ b/books/workshops/2004/davis/support/README @@ -0,0 +1,48 @@ +_____________________________________________________________________ + + Fully Ordered Finite Sets for ACL2 + Copyright (C) 2003, 2004 Kookamara LLC + + Version 0.90 - README +_____________________________________________________________________ + + + About + + This is a finite set theory library for ACL2. + + ACL2 Home Page: + - http://www.cs.utexas.edu/users/moore/acl2/ + + Ordered Sets Home Page: + - http://www.cs.utexas.edu/users/jared/osets/ + + The home page includes documentation and information on the + latest and upcoming versions, and you shoudl check to make + sure you have a recent copy. + + + Build Instructions + + You must have ACL2 2.9 installed to build this library. + + 1. Edit the makefile. + + - Change "include [...]/Makefile-generic" to point to the + file Makefile-generic in your acl2-sources/books + directory. + + - Change "ACL2 = [...]/saved_acl2" to point to your ACL2 + executable. + + + 2. Run "make" to build the library. + + - Check to make sure that the following files were created: + sets.cert, quantify.cert, set-order.cert, and map.cert. + If there was a problem, please send a report to + jared@cs.utexas.edu. + + + + All usage instructions are on the web page. diff --git a/books/workshops/2004/davis/support/cert.acl2 b/books/workshops/2004/davis/support/cert.acl2 new file mode 100644 index 0000000..6070e24 --- /dev/null +++ b/books/workshops/2004/davis/support/cert.acl2 @@ -0,0 +1,3 @@ +(value :q) +(lp) +(ld "package.lsp") diff --git a/books/workshops/2004/davis/support/computed-hints.lisp b/books/workshops/2004/davis/support/computed-hints.lisp new file mode 100644 index 0000000..2d43500 --- /dev/null +++ b/books/workshops/2004/davis/support/computed-hints.lisp @@ -0,0 +1,436 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; computed-hints.lisp +; +; We provide support for the development of "pick a point" style +; proofs through computed hints. + +(in-package "COMPUTED-HINTS") + +;;; Introduction +;;; +;;; Suppose we have some predicate, P, of any number of arguments. A +;;; natural operation is to extend this predicate to every element of +;;; a list, set, or other collection. In other words, we would like +;;; to know if every element in the set, list, tree, or whatever has +;;; the property when applied to arguments. +;;; +;;; For example, we might have the predicate: +;;; +;;; (defun integer-lessp (a b) +;;; (and (integerp a) +;;; (< a b))) +;;; +;;; We could now extend this concept to an entire list, to ask if +;;; every element in the list was an integer that is less than b. The +;;; function might be written as: +;;; +;;; (defun list-integer-lessp (a-list b) +;;; (declare (xargs :guard (true-listp a-list))) +;;; (or (endp a-list) +;;; (and (integer-lessp (car a-list) b) +;;; (list-integer-lessp (cdr a-list) b)))) +;;; +;;; Similarly, we might want to map the function across sets or other +;;; types of collections. +;;; +;;; Take an abstract mathematical view for a moment. Given some +;;; predicate P, what we would really like to do is be able to express +;;; the idea that given some collection x, every element of x +;;; satisfies P. In other words, we want to define: +;;; +;;; (collection-P x [args]) = forall a in x, (P x [args]) +;;; +;;; And indeed, it would be nice to be working with this very abstract +;;; mathematical definition, for which we will not need to make +;;; inductive arguments. Unfortunately, because all variables in +;;; ACL2's rewrite rules are implicitly universally quantified, we +;;; cannot express the above as a rewrite rule. +;;; +;;; However, through the use of constrained function symbols and +;;; functional instantiation, we can effectively accomplish the above +;;; reduction when it suits our purposes. And, the process can be +;;; automated through the use of computed hints. Overall, this is not +;;; as nice as working with a pure rewrite rule, and in fact has some +;;; unfortunate limitations. However, it does turn out to be very +;;; broadly applicable and invaluable for reasoning about set +;;; theoretic concepts, where concepts such as "subset" are really +;;; nothing more than the extension of the predicate "in" across a +;;; set. +;;; +;;; Moreover, the reduction that we set out to achieve will reduce +;;; (collection-P x [args]) to the following implication: +;;; +;;; (implies (in a x) +;;; (P a [args])) +;;; +;;; I call this a "pick a point" reduction, because it is similar to +;;; and takes its inspiration from the well known set theoretic +;;; technique of picking an arbitrary element (or point) in one set, +;;; then showing it is also a member of another set. + + + +;;; Preliminaries +;;; +;;; We will make minor use of the rewriting system developed in +;;; instance.lisp. We also enter program mode, because we are not +;;; interested in reasoning about these functions. + +(include-book "instance") +(program) + + +;;; Tagging +;;; +;;; Suppose that we have (collection-P x a0 a1 ... an) to a simpler +;;; argument. We begin by defining a synonym for collection-P, e.g., +;;; +;;; (defun collection-P-tag (x a0 a1 ... an) +;;; (collection-P x a0 a1 ... an)) +;;; +;;; Now we instruct the theorem prover to rewrite instances of +;;; conclusion into conclusion-tag, as long as we are not backchaining +;;; and as long as conclusion occurs as the goal. For example, +;;; +;;; (defthm tagging-theorem +;;; (implies +;;; (and (syntaxp (rewriting-goal-lit mfc state)) +;;; (syntaxp (rewriting-conc-lit `(collection-P ,x ,a0 ... ,an) +;;; mfc state))) +;;; (equal (collection-P x a0 ... an) +;;; (collection-P-tag x a0 ... an)))) +;;; +;;; This theorem is trivial to prove, since collection-P-tag is merely +;;; a synonym for collection-P. After the theorem is proven, +;;; collection-P-tag should be disabled. + +(defun rewriting-goal-lit (mfc state) + (declare (xargs :stobjs state) + (ignore state)) + (null (mfc-ancestors mfc))) + +(defun rewriting-conc-lit (term mfc state) + (declare (xargs :stobjs state) + (ignore state)) + (let ((clause (mfc-clause mfc))) + (member-equal term (last clause)))) + + + + +;;; Computing a Hint +;;; +;;; Now, what we are going to do next is create a computed hint that +;;; will look for instances of a trigger, and if it sees one, we will +;;; try to provide a functional instantiation hint. This takes some +;;; work. Our computed hint function is called as ACL2 is working to +;;; simplify terms, and it is allowed to examine the current clause. +;;; The current clause will be a a disjunction of literals. For +;;; example, +;;; +;;; (a ^ b ^ ...) => P is (~a v ~b v ... v P) +;;; (a v b v ...) => P is subgoal1: (~a v P), sg2: (~b v P), ... +;;; +;;; Our first step is to see if our computed hint should even be +;;; applied to this clause. We only allow the hint to be applied if +;;; the current clause is stable under simplification, i.e., if other +;;; attempts to prove it have failed. At that point, we check the +;;; clause to see if our trigger occurs as a term within it. If so, +;;; the tagging theorem has applied and thinks we should try to use +;;; our computed hint! +;;; +;;; We check for the existence of our trigger using the following +;;; function, (harvest-trigger clause trigger-fn), which extracts all +;;; the terms from clause whose function symbol is trigger-fn, and +;;; returns them as a list. +;;; +;;; Now, our intention is to functionally instantiate the theorem in +;;; question. To do this, we need to provide values for the +;;; hypotheses and arguments a0 ... an. +;;; +;;; In order to recover the hypotheses, we first remove from the +;;; clause all of our trigger terms. We then negate each of the +;;; remaining literals as they occur in the clause. And, if there are +;;; more than one of them, we are going to AND their negations +;;; together. This is done by the functions others-to-negated-list, +;;; and others-to-hyps. +;;; +;;; For example, if we originally had the conjecture (a ^ b ^ ...) => +;;; P Then this became the clause: (~a v ~b v ... v P), which is +;;; represented by the list ((not a) (not b) ... P). Suppose that P +;;; was our trigger term. We remove P from the clause, yielding ((not +;;; a) (not b) ...), and then we negate all of these literals, +;;; creating the list (a b ...). We now and these together, creating +;;; the the term (and a b ...), which was our original hypotheses! + +(defun harvest-trigger (clause trigger-fn) + (if (endp clause) + nil + (if (eq (caar clause) trigger-fn) + (cons (car clause) (harvest-trigger (cdr clause) trigger-fn)) + (harvest-trigger (cdr clause) trigger-fn)))) + +(defun others-to-negated-list (others) + (if (endp others) + nil + (if (equal (caar others) 'not) ; don't create ugly double not's + (cons (second (car others)) + (others-to-negated-list (cdr others))) + (cons (list 'not (car others)) + (others-to-negated-list (cdr others)))))) + +(defun others-to-hyps (others) + (if (endp others) + t + (let ((negated (others-to-negated-list others))) + (if (endp (cdr negated)) ; don't wrap single literals in and's + (car negated) + (cons 'and (others-to-negated-list others)))))) + + + +;;; Absolute Restrictions: +;;; +;;; Collection predicate must have a first argument which is the +;;; collection to traverse!! +;;; +;;; Need to be able to create hint for predicate as well. + + + +;;; Building Hints +;;; +;;; Our ultimate goal now is to be able to create functional +;;; instantiation hints for each trigger which was found. In other +;;; words, we now have a set of triggers which look like the following: +;;; +;;; ((collection-P-tag col1 [extra-args1]) +;;; (collection-P-tag col2 [extra-args2]) +;;; ...) +;;; +;;; We want to instantiate generic theorems of the form: +;;; +;;; (defthm generic-theorem +;;; (implies (hyps) +;;; (collection-P-tag (collection) [extra-args]))) +;;; +;;; Where we have the following generic constraint: +;;; +;;; (implies (hyps) +;;; (implies (in a (collection)) +;;; (predicate a))) +;;; +;;; So, the functional instantiation hints we want to create will look +;;; like the following: +;;; +;;; (:functional-instance generic-theorem +;;; (hyps (lambda () [substitution for hyps])) +;;; (collection (lambda () [substitution for collection])) +;;; (predicate (lambda (x) [substitution for predicate])) +;;; (collection-P (lambda (x) [substitution for collection-P]))) +;;; +;;; Lets consider how we can build these substitutions for some +;;; trigger = (collection-P-tag col1 [extra-args1]). Some of this +;;; is easy: +;;; +;;; The substitution for hyps is actually built using the process +;;; described above, e.g., they are extracted from the clause and +;;; eventually restored to normal using others-to-hyps, so I will +;;; not spend any time on them. +;;; +;;; The collection is simply (second trigger), since we require that +;;; the collection predicate has the collection as its first +;;; argument. +;;; +;;; The substitution for collection-P is also fairly easy. Since +;;; we require that the collection function's first argument is +;;; the collection under examination, we simply need to write +;;; (lambda (?x) (actual-collection-P ?x [extra-args])), where the +;;; extra arguments are taken from the trigger we are looking at. +;;; +;;; This leaves us with predicate. The substitution for predicate +;;; is difficult, because we want to support very flexible +;;; predicates involving many arguments and various weird terms. +;;; To do this, we will allow the user to provide a rewrite rule +;;; that says how to handle the predicate. +;;; +;;; In other words, given the trigger (trigger-term col a0 a1 a2 +;;; ... an) we will create the following "base predicate" to +;;; rewrite: +;;; +;;; (predicate ?x a0 a1 a2 ... an) +;;; +;;; Where "predicate" is literally the name of the generic +;;; predicate. The user can then provide a substitution such +;;; as: +;;; +;;; (predicate ?x ?y) -> (not (integer-lessp ?x ?y)) +;;; +;;; And this will transform the above into the desired result. + + +(defun build-hint (trigger ; list, the actual trigger to use + generic-theorem ; symbol, the name of generic-theorem + generic-hyps ; symbol, the name of (hyps) + generic-collection ; symbol, the name of (collection) + generic-predicate ; symbol, the name of predicate + generic-collection-P ; symbol, the name of collection-P + collection-P-sub ; symbol, name of actual collection-P + hyps-sub ; the computed substitution for hyps + predicate-rewrite) ; rewrite rule for predicate + (let* ((base-pred (cons generic-predicate (cons '?x (cddr trigger)))) + (pred-sub (instance-rewrite base-pred predicate-rewrite))) + `(:functional-instance + ,generic-theorem + (,generic-hyps + (lambda () ,hyps-sub)) + (,generic-collection + (lambda () ,(second trigger))) + (,generic-collection-P + (lambda (?x) ,(cons collection-P-sub (cons '?x (cddr trigger))))) + (,generic-predicate + (lambda (?x) ,pred-sub))))) + +(defun build-hints (triggers + generic-theorem + generic-hyps + generic-collection + generic-predicate + generic-collection-P + collection-P-sub + hyps-sub + predicate-rewrite) + (if (endp triggers) + nil + (cons (build-hint (car triggers) + generic-theorem + generic-hyps + generic-collection + generic-predicate + generic-collection-P + collection-P-sub + hyps-sub + predicate-rewrite) + (build-hints (cdr triggers) + generic-theorem + generic-hyps + generic-collection + generic-predicate + generic-collection-P + collection-P-sub + hyps-sub + predicate-rewrite)))) + + +(defconst *message* + "~|~%We suspect this conjecture should be proven by functional ~ + instantiation of ~x0. This suspicion is caused by ~x2, so ~ + if this is not what you want to do, then you should disable ~ + ~x2. Accordingly, we suggest the following hint: ~ + ~%~%~x1~%") + + + +;;; Of course, some of those hints can be computed. Here we write a function +;;; to actually provide these hints and install the computed hint function. + +(defun automate-instantiation-fn (new-hint-name + generic-theorem + generic-hyps + generic-collection + generic-predicate + generic-collection-P + collection-P-sub + predicate-rewrite + trigger-symbol + tagging-theorem) + `(encapsulate () + + (defun ,new-hint-name (id clause world stable) + (declare (xargs :mode :program) + (ignore world)) + (if (not stable) + nil + (let ((triggers (harvest-trigger clause ,trigger-symbol))) + (if (not triggers) + nil + (let* ((others (set-difference-equal clause triggers)) + (hyps (others-to-hyps others)) + (phrase (string-for-tilde-@-clause-id-phrase id)) + (fi-hints (build-hints triggers + ,generic-theorem + ,generic-hyps + ,generic-collection + ,generic-predicate + ,generic-collection-P + ,collection-P-sub + hyps + ,predicate-rewrite)) + (hints (list :use fi-hints + :expand triggers))) + (prog2$ (cw *message* + ,generic-theorem + (list phrase hints) + ,tagging-theorem) + hints)))))) + + (add-default-hints! + '((,new-hint-name id clause world stable-under-simplificationp))) + + )) + + + + +(defmacro automate-instantiation (&key new-hint-name + generic-theorem + generic-hyps + generic-collection + generic-predicate + generic-collection-predicate + actual-collection-predicate + predicate-rewrite + actual-trigger + tagging-theorem) + (automate-instantiation-fn new-hint-name + (list 'quote generic-theorem) + (list 'quote generic-hyps) + (list 'quote generic-collection) + (list 'quote generic-predicate) + (list 'quote generic-collection-predicate) + (list 'quote actual-collection-predicate) + (list 'quote predicate-rewrite) + (list 'quote actual-trigger) + (list 'quote tagging-theorem))) + diff --git a/books/workshops/2004/davis/support/fast.lisp b/books/workshops/2004/davis/support/fast.lisp new file mode 100644 index 0000000..fa26330 --- /dev/null +++ b/books/workshops/2004/davis/support/fast.lisp @@ -0,0 +1,430 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; 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 "SET") +(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. + +(defun fast-union (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 (tail X) (tail Y)))) + ((<< (head X) (head Y)) + (cons (head X) (fast-union (tail X) Y))) + (t (cons (head Y) (fast-union X (tail Y)))))) + + +(encapsulate () + + (local (defthmd fast-union-head-weak + (implies (and (setp X) + (setp Y) + (setp (fast-union X Y)) + (not (equal (head (fast-union X Y)) (head X)))) + (equal (head (fast-union X Y)) (head Y))) + :hints(("Goal" + :in-theory (enable primitive-order-theory) + :use (:instance fast-union (X X) (Y Y)))))) + + (defthm fast-union-set + (implies (and (setp X) (setp Y)) + (setp (fast-union X Y))) + :hints(("Goal" + :in-theory (enable primitive-order-theory)) + ("Subgoal *1/9" + :use (:instance fast-union-head-weak + (X X) + (Y (tail Y)))) + ("Subgoal *1/7" + :use (:instance fast-union-head-weak + (X (tail X)) + (Y Y))) + ("Subgoal *1/5" + :use (:instance fast-union-head-weak + (X (tail X)) + (Y (tail Y)))))) + + + (local (defthm fast-union-head-strong + (implies (and (setp X) (setp Y)) + (equal (head (fast-union 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 (tail X) (tail Y)))))))) + + + (defthm fast-union-membership + (implies (and (setp X) (setp Y)) + (equal (in a (fast-union 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 X (tail Y))))) + ("Subgoal *1/4" + :use ((:instance cons-head + (a (head X)) + (X (fast-union (tail X) Y))) + (:instance cons-to-insert-nonempty + (a (head X)) + (X (fast-union (tail X) Y))) + (:instance in-insert + (a a) + (b (head X)) + (X (fast-union (tail X) Y))))) + ("Subgoal *1/3" + :use (:instance cons-head + (a (head X)) + (X (fast-union (tail X) (tail 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. + +(defun fast-intersect (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 (tail X) (tail Y)))) + ((<< (head X) (head Y)) + (fast-intersect (tail X) Y)) + (t (fast-intersect X (tail Y))))) + + +(encapsulate () + + (defthm fast-intersect-empty + (implies (empty X) + (equal (fast-intersect 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 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 X Y))) + (<< (head X) (head Y))) + (not (empty (tail X)))))) + + (local (defthmd fast-intersect-head + (implies (and (not (empty X)) + (not (empty Y)) + (equal (head X) (head Y)) + (not (empty (fast-intersect X Y)))) + (equal (head (fast-intersect X Y)) + (head X))) + :hints(("Goal" :in-theory (disable cons-set))))) + + (local (defthm fast-intersect-order-weak + (implies (and (setp X) + (setp Y) + (not (empty X)) + (not (empty Y)) + (not (empty (fast-intersect X Y))) + (<< a (head X)) + (<< a (head Y))) + (<< a (head (fast-intersect X Y)))) + :hints(("Goal" :in-theory (enable primitive-order-theory)) + ("Subgoal *1/6" :use (:instance fast-intersect-head)) + ("Subgoal *1/5" :use (:instance fast-intersect-head)) + ("Subgoal *1/4" :use (:instance fast-intersect-head)) + ("Subgoal *1/3" :use (:instance fast-intersect-head))))) + + (local (defthm fast-intersect-nonempty-weak + (implies (not (empty (fast-intersect 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 (tail x) (tail y))) + (setp x) + (setp y)) + (setp (fast-intersect x y))) + :hints(("Goal" :in-theory (e/d (primitive-order-theory) + (cons-set + fast-intersect-nonempty-weak + fast-intersect-order-weak)) + :use ((:instance fast-intersect-nonempty-weak + (x (tail x)) + (y (tail y))) + (:instance fast-intersect-order-weak + (a (head X)) + (X (tail X)) + (Y (tail Y)))))))) + + (defthm fast-intersect-set + (implies (and (setp X) (setp Y)) + (setp (fast-intersect X Y))) + :hints(("Goal" :in-theory (enable primitive-order-theory)) + ("Subgoal *1/5" :use (:instance lemma-3)))) + + (defthm fast-intersect-membership + (implies (and (setp X) (setp Y)) + (equal (in a (fast-intersect 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-order-weak + (a (head X)) + (X (tail X)) + (Y (tail 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. + +(defun fast-difference (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 (tail X) (tail Y))) + ((<< (head X) (head Y)) + (cons (head X) (fast-difference (tail X) Y))) + (t (fast-difference X (tail Y))))) + + + + +(encapsulate () + + (local (defthm lemma + (implies (and (not (empty X)) + (not (empty Y)) + (not (empty (fast-difference X Y))) + (not (equal (head X) (head Y))) + (<< (head X) (head Y))) + (equal (head (fast-difference X Y)) + (head X))) + :hints(("Goal" + :in-theory (disable cons-set) + :use (:instance cons-head + (a (head X)) + (X (fast-difference (tail X) Y))))))) + + (local (defthm lemma-2 + (implies (and (not (empty X)) + (not (empty Y)) + (not (empty (fast-difference X Y))) + (equal (head X) (head Y))) + (not (empty (tail X)))))) + + (local (defthm fast-difference-order-weak + (implies (and (not (empty X)) + (not (empty (fast-difference X Y))) + (<< a (head X))) + (<< a (head (fast-difference 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-set + (implies (and (setp X) (setp Y)) + (setp (fast-difference X Y))) + :hints(("Goal" :in-theory (enable primitive-order-theory)) + ("Subgoal *1/7" :use (:instance fast-difference-order-weak + (a (head X)) + (X (tail X)) + (Y Y))))) + + (defthm fast-difference-membership + (implies (and (setp X) (setp Y)) + (equal (in a (fast-difference 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-order-weak + (a (head X)) + (X (tail X)) + (Y Y))))) + + (defthm fast-difference-empty + (implies (empty X) + (equal (fast-difference X Y) (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)) + diff --git a/books/workshops/2004/davis/support/instance.lisp b/books/workshops/2004/davis/support/instance.lisp new file mode 100644 index 0000000..cd6d922 --- /dev/null +++ b/books/workshops/2004/davis/support/instance.lisp @@ -0,0 +1,675 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; instance.lisp +; +; This is a system for dynamically instantiating ACL2 "theories" (which are +; represented as constants) to create new, concrete "theories". + +(in-package "INSTANCE") + + +; Everything in this file is in program mode. We do not intend to +; reason about these functions -- instead, we intend to use these +; functions to create new functions, which the user will reason +; about. + +(program) + + +; Introduction +; +; +; The following work has been motivated by my work with quantification +; over sets. When I started on this file, I had roughly 2000 lines of +; complicted macros in order to be able to instantiate generic and +; concrete theories for this work, and it was just becoming +; unmanageable. My hope was that rewriting the definitions and +; theorems into concrete forms would provide a more concise way of +; instantiating the theory, and make it easier to keep everything +; consistent. +; +; Originally, I wanted to extract the definitions for generic +; functions from ACL2's state (well, actually from the current world). +; But, to do so becomes very complicated, because of the restrictions +; on macros that they cannot take state as a parameter. So, the best +; that I could ever accomplish that way would be to display a list of +; events, which a user could copy into a file. But, that is wholly +; unsatisfying, because it would mean that the resulting theories +; could never be "automagically" updated when new theorems are added +; to the generic theory. +; +; So, instead of doing things that way, I now simply store events in +; constants. These constants can then be rewritten to create new but +; related theories. +; +; A first step towards this is to introduce a simple rewriter. +; Originally I had based my rewriter on the built in one-way-unify +; function in ACL2, but it operates only on pseudo-terms, and +; pseudo-terms cannot contain atoms other than symbols. This gave me +; serious trouble when trying to rewrite theorems involving constants, +; e.g., to say that something was an integerp and greater than zero. +; So, instead of using one-way-unify, I introduce a simple unification +; algorithm which has been adapted from Warren Hunt's work. + +; The system treats all symbols beginning with a ? as variables, and +; all other atoms as literals. + +(defun instance-variablep (x) + (and (symbolp x) + (equal (car (explode-atom x 10)) #\?))) + + + +; We return two values: a boolean flag which indicates if we are +; successful in finding a match, and a list of substitutions of the +; form (variable . value). This is all be fairly standard stuff. +; +; For example: +; +; (instance-unify-term '(predicate ?x) '(predicate (car a)) nil) +; ==> +; (t ((?x . (car a)))) + +(mutual-recursion + + (defun instance-unify-term (pattern term sublist) + (if (atom pattern) + (if (instance-variablep pattern) + (let ((value (assoc pattern sublist))) + (if (consp value) + (if (equal term (cdr value)) + (mv t sublist) + (mv nil nil)) + (mv t (acons pattern term sublist)))) + (if (equal term pattern) + (mv t sublist) + (mv nil nil))) + (if (or (atom term) + (not (eq (car term) (car pattern)))) + (mv nil nil) + (if (or (eq (car term) 'quote) + (eq (car pattern) 'quote)) + (if (equal term pattern) + (mv t sublist) + (mv nil nil)) + (instance-unify-list (cdr pattern) (cdr term) sublist))))) + + (defun instance-unify-list (pattern-list term-list sublist) + (if (or (atom term-list) + (atom pattern-list)) + (if (and (atom term-list) + (atom pattern-list)) + (mv t sublist) + (mv nil nil)) + (mv-let (successp new-sublist) + (instance-unify-term (car pattern-list) + (car term-list) + sublist) + (if successp + (instance-unify-list (cdr pattern-list) + (cdr term-list) + new-sublist) + (mv nil nil))))) +) + + +; After a list of substitutions has been generated, we typically want +; to apply them to a term. We recur over the list of substitutions, +; simply calling subst to do our work throughout a term. +; +; For example: +; +; (instance-substitute '((?x . (car a))) '(not (predicate ?x))) +; ==> +; (not (predicate (car a))) + +(defun instance-substitute (sublist term) + (if (endp sublist) + term + (let* ((old (car (car sublist))) + (new (cdr (car sublist))) + (result (subst new old term))) + (instance-substitute (cdr sublist) result)))) + + + +; We now introduce our actual rewriter. We take three arguments: pat +; is the pattern to look for throughout the term, e.g., (predicate +; ?x), repl is the replacement to use, e.g., (not (predicate ?x)), and +; term is the term to match the pattern against in order to get the +; substitutions. +; +; For Example: +; +; (instance-rewrite1 '(predicate ?x) +; '(not (predicate ?x)) +; '(if (predicate (car x)) t nil)) +; => +; (if (not (predicate (car x))) t nil) + +(mutual-recursion + + (defun instance-rewrite1 (pat repl term) + (mv-let (successful sublist) + (instance-unify-term pat term nil) + (if successful + (instance-substitute sublist repl) + (if (atom term) + term + (cons (instance-rewrite1 pat repl (car term)) + (instance-rewrite-lst1 pat repl (cdr term))))))) + + (defun instance-rewrite-lst1 (pat repl lst) + (if (endp lst) + nil + (cons (instance-rewrite1 pat repl (car lst)) + (instance-rewrite-lst1 pat repl (cdr lst))))) +) + + + +; Finally, given that we can apply a rewrite a term with a single +; replacement, we go ahead and extend this notion to multiple +; replacements. In other words, we walk through a list of +; substitutions, sequentially rewriting the term using each +; substitution. + +(defun instance-rewrite (term subs) + (if (endp subs) + term + (let ((first-sub (car subs))) + (instance-rewrite (instance-rewrite1 (first first-sub) + (second first-sub) + term) + (cdr subs))))) + + + + +; Instantiating Defuns +; +; +; Theories consist mainly of definitions and theorems. Given generic +; theorems, we will want to rewrite them so that they perform +; different functions. For example, a generic "all" function might +; need to be rewritten so that its calls to (predicate x) are replaced +; with calls to (not (predicate x)) for all x. +; +; To begin, we instantiate the function's declarations (e.g., comment +; strings, xargs, ignores, and so forth). We simply duplicate comment +; strings, but for declare forms we allow rewriting to occur. + +(defun instance-decls (decls subs) + (if (endp decls) + nil + (if (pseudo-termp (car decls)) + (cons (instance-rewrite (car decls) subs) + (instance-decls (cdr decls) subs)) + (cons (car decls) + (instance-decls (cdr decls) subs))))) + + +; For the defun itself, we retain the same defun symbol (e.g., defun +; or defund), but we change the name and args of the function by first +; creating the list '(oldname oldarg1 oldarg2 ...) then applying our +; substitutions to the new function. +; +; As a trivial example, +; (instance-defun '(defun f (x) (+ x 1)) '(((f x) (g x)))) +; => +; (defun g (x) (+ x 1)) + +(defun instance-defun (defun subs) + (let* ((defun-symbol (first defun)) + (defun-name (second defun)) + (defun-args (third defun)) + (defun-decls (butlast (cdddr defun) 1)) + (defun-body (car (last defun))) + (name/args (cons defun-name defun-args)) + (new-body (instance-rewrite defun-body subs)) + (new-name/args (instance-rewrite name/args subs)) + (new-decls (instance-decls defun-decls subs)) + (new-name (car new-name/args)) + (new-args (cdr new-name/args))) + `(,defun-symbol + ,new-name ,new-args + ,@new-decls + ,new-body))) + +; We also provide a convenience function that allows you to instance +; a list of defuns. + +(defun instance-defuns (defun-list subs) + (if (endp defun-list) + nil + (cons (instance-defun (car defun-list) subs) + (instance-defuns (cdr defun-list) subs)))) + + + +; Renaming theorems + +(defun defthm-names (event-list) + (if (endp event-list) + nil + (let* ((first-event (car event-list)) + (event-type (first first-event))) + (cond ((or (eq event-type 'defthm) + (eq event-type 'defthmd)) + (cons (second first-event) + (defthm-names (cdr event-list)))) + ((eq event-type 'encapsulate) + (append (defthm-names (cddr first-event)) + (defthm-names (cdr event-list)))) + (t (defthm-names (cdr event-list))))))) + +(defun create-new-names (name-list suffix) + (if (endp name-list) + nil + (acons (car name-list) + (intern-in-package-of-symbol (string-append (symbol-name (car name-list)) + (symbol-name suffix)) + suffix) + (create-new-names (cdr name-list) suffix)))) + +(defun rename-defthms (event-list suffix) + (sublis (create-new-names (defthm-names event-list) suffix) + event-list)) + + + +; Instantiating Theorems +; +; +; To instantiate defthms, we will want to be able to provide +; functional instantiations of the generic theory. This is much +; more complicated than instancing definitions, and involves: +; +; a) determining what functional substitutions to make +; b) determining the theory in which to conduct the proofs +; c) handling rule classes and other optional components +; d) generating the actual defthm event +; +; My idea is essentially that if a substitution list can be used for +; functionally instantiating theorems, then it can also be used for +; creating the new theorem. +; +; (a) Determining what functional substitutions to make. +; +; I pass in a list of substitutions of the following form. +; +; (((predicate ?x) (not (in ?x y))) +; ((all ?x) (all-not-in ?x y)) +; ((exists ?x) (exists-not-in ?x y))) +; +; From this list we can generate the functional instantiation hints. +; So, for example, we simply convert ((predicate ?x) (not (in ?x y))) +; into the substitution: +; +; (predicate (lambda (?x) (not (in ?x y)))) +; +; This is easy to do with the following functions: + +(defun sub-to-lambda (sub) + (let ((term (first sub)) + (repl (second sub))) + (let ((function-symbol (car term)) + (lambda-args (cdr term))) + `(,function-symbol (lambda ,lambda-args ,repl))))) + +(defun subs-to-lambdas (subs) + (if (endp subs) + nil + (cons (sub-to-lambda (car subs)) + (subs-to-lambdas (cdr subs))))) + + +; (b) Determining the theory in which to conduct the proofs. +; +; When we prove the functional instantiation constraints, ideally we +; should work in an environment where the only definitions that are +; enabled are the definitions used in the functional instantiation +; hints. +; +; Well, the definitions we need are (almost) simply all of the +; function symbols in the right-hand side of the substitution list. +; In other words, for the above substitutions, I would want to have +; the definitions of not, in, all-not-in, and exists-not-in available. +; +; Now, the problem with this approach is, what if those symbols don't +; have definitions? This can occur if, for example, we are using a +; constrained function in the substitution list. This is actually +; useful, e.g., for substituting (predicate ?x) -> (not (predicate +; ?x)). +; +; My solution is a stupid hack. We simply pass in the names of the +; generic functions for which we do not want to generate definitions +; along with the substitutinos. +; +; To begin, the following function will extract all function symbols +; that occur within a term. + +(mutual-recursion + + (defun term-functions (term) + (if (atom term) + nil + (cons (car term) + (term-list-functions (cdr term))))) + + (defun term-list-functions (list) + (if (endp list) + nil + (append (term-functions (car list)) + (term-list-functions (cdr list))))) +) + +; Next, I wrote the following function, which walks over the +; substitution list and extracts the function symbols from each right +; hand side, using term-functions. The net result is the list of all +; functions that were used in replacements. + +(defun subs-repl-functions (subs) + (if (endp subs) + nil + (let* ((sub1 (car subs)) + (repl (second sub1))) + (append (term-functions repl) + (subs-repl-functions (cdr subs)))))) + +; Given the above, we could then convert the list of function symbols +; into a list of (:definition f)'s with the following function. + +(defun function-list-to-definitions (funcs) + (if (endp funcs) + nil + (cons `(:definition ,(car funcs)) + (function-list-to-definitions (cdr funcs))))) + +; And finally, here is a function that does "all of the work", calling +; function-list-to-definitions for all of the functions found in the +; substitution list, minus all of the generic functions that we don't +; want to generate :definition hints for. + +(defun subs-to-defs (subs generics) + (let* ((all-fns (subs-repl-functions subs)) + (real-fns (set-difference-eq all-fns generics))) + (function-list-to-definitions real-fns))) + + +; (c) Handling rule classes and other optional components. +; +; We are interested in several parts of a defthm. In addition to the +; conjecture itself, we need to consider the rule-classes used by the +; theorem, and the other optional attributes such as the :hints, :doc, +; :otf-flg, etc. We parse these attributes into a five-tuple of pairs +; of the form (present . value), where present is a boolean that says +; whether or not the flag has been seen, value is its value, and the +; order of the elements is rule-classes, instructions, hints, otf-flg, +; and finally doc. We parse these options with the following code: + +(defconst *default-parse-values* + '((nil . nil) (nil . nil) (nil . nil) (nil . nil) (nil . nil))) + +(defun parse-defthm-option (option return-value) + (cond ((equal (first option) :rule-classes) + (update-nth 0 (list t (second option)) return-value)) + ((equal (first option) :instructions) + (update-nth 1 (list t (second option)) return-value)) + ((equal (first option) :hints) + (update-nth 2 (list t (second option)) return-value)) + ((equal (first option) :otf-flg) + (update-nth 3 (list t (second option)) return-value)) + ((equal (first option) :doc) + (update-nth 4 (list t (second option)) return-value)) + (t (er hard "Unknown flag in defthm options ~x0." (first option))))) + +(defun parse-defthm-options (options return-value) + (if (endp options) + return-value + (parse-defthm-options (cddr options) + (parse-defthm-option options return-value)))) + + +; (d) Generating the actual defthm event. +; +; When we are ready to instance a defthm event, we combine the above +; work with a few new things. First of all, we need the original +; theorem event, a new name to use, the substitutions to use, and the +; list of generic function symbols in use so that we do not create +; (:definition f) entries for them. +; +; We begin by making our substitutions in the body of the theorem. We +; then parse the optional components of the defthm, but we only are +; interested in the rule-classes. (Hints, instructions, and otf-flg +; will not be needed, because we will be proving this via functional +; instantiation. Doc we ignore for no good reason.) We construct a +; new theorem that has our new name and body, replicating the rule +; classes if necessary. We also provide a functional instantiation +; hint of the generic theorem's name, along with a list of lambda +; substitutions to make. + +(defun instance-defthm (event new-name subs generics extra-defs) + (let* ((defthm-symbol (first event)) + (defthm-name (second event)) + (defthm-body (third event)) + (new-body (instance-rewrite defthm-body subs)) + (options (parse-defthm-options (cdddr event) + *default-parse-values*)) + (rc-opt (first options))) + `(,defthm-symbol ,new-name + ,new-body + :hints(("Goal" + :use (:functional-instance ,defthm-name + ,@(subs-to-lambdas subs)) + :in-theory (union-theories (theory 'minimal-theory) + (union-theories ',extra-defs + ',(subs-to-defs subs generics))))) + ,@(if (car rc-opt) `(:rule-classes ,(cdr rc-opt)) nil)))) + + + +; Instantiating Encapsulates +; +; +; There are two reasons that I typically use encapsulation. The first +; is as a purely structural/organizational purpose, where I am trying +; to prove some theorem is true, but I need some lemmas to do so. In +; this case I use an (encapsulate nil ...) and wrap my lemmas in local +; forms. The other reason is to actually go ahead and introduce +; constrained functions. +; +; Two strategies will be necessary for handling these situations. In +; particular, if we are in an encapsulate which has no constrained +; function symbols, we will want to skip all local events and only add +; the non-local events (using functional instantiation to create the +; theorems). On the other hand, for the case when we are introducing +; constrained functions, we will want to introduce new constrained +; functions based on the encapsulate. +; +; So, encapsulates are handled separately based on whether or not any +; functions are constrained. +; +; Within an (encapsulate nil ...), local events will be skipped and +; defthm events will be proven using the functional instantiation of +; their generic counterparts. +; +; Within an (encapsulate (...) ...), local events will not be skipped +; but will instead be reintroduced with new names. Further, defthm +; events will be copied using new names and will not be proven using +; functional instantiation. +; +; The only "extra" thing we really need for handling encapsulates is a +; system to make the substitutions within the signatures. We do that +; here by simple rewriting. Note that we do not allow the number of +; return values to change. I don't really think of this as a major +; limitation, since almost always my constrained functions return a +; single value. If you have an example of where this would be useful, +; it would be interesting to see it. + +(defun instance-signature (signature subs) + (let ((name (first signature)) + (rest (rest signature))) + (cons (instance-rewrite subs name) rest))) + +(defun instance-signatures (signatures subs) + (if (endp signatures) + nil + (cons (instance-signature (car signatures) subs) + (instance-signatures (cdr signatures) subs)))) + +; Because encapsulates can contain many events within them, it is +; natural to make them mutually recursive with the main event list +; handler, which we are now ready to introduce. + + + + + +; Instantiating Entire Theories +; +; +; We are now ready to introduce the functions which will walk through +; a theory and call the appropriate instancing functions on each of +; the forms we encounter. To support encapsulation, our functions +; here are all mutually recursive. +; +; The arguments that we pass around are the following: +; +; - The event or event list to instantiate +; +; - The global list of substitutions used to derive the instance +; +; - A suffix which will be appended to generate new names +; +; - A list of generic functions which have no definitions +; +; - A mode, which is either 'constrained to indicate that the +; nearest encapsulate event has constrained functions, or is nil +; to indicate that the nearest encapsulate is merely a structural +; wrapper for local lemmas. +; +; Finally, we overload our behavior based on suffix, so that if no +; suffix is given, we simply replicate the generic theory instead +; of instantiating a concrete instance of it. + + +(mutual-recursion + + (defun instance-event (event subs suffix generics mode extra-defs) + (if (null suffix) + event + (cond ((or (eq (car event) 'defun) + (eq (car event) 'defund)) + (instance-defun event subs)) + ((or (eq (car event) 'defthm) + (eq (car event) 'defthmd)) + (let* ((name (second event)) + (new-name (intern-in-package-of-symbol + (string-upcase + (concatenate 'string + (symbol-name name) + (symbol-name suffix))) + suffix))) + (instance-defthm event new-name subs generics extra-defs))) + ((equal (car event) 'local) + (if (eq mode 'constrained) + (instance-event (second event) subs suffix generics mode extra-defs) + nil)) + ((equal (car event) 'encapsulate) + (instance-encapsulate event subs suffix generics mode extra-defs)) + (t (er hard "Don't know how to handle ~x0" (car event)))))) + + (defun instance-event-list (events subs suffix generics mode extra-defs) + (if (endp events) + nil + (let ((first (instance-event (car events) subs suffix generics mode extra-defs)) + (rest (instance-event-list (cdr events) subs suffix generics mode extra-defs))) + (if first + (cons first rest) + rest)))) + + (defun instance-encapsulate (event subs suffix generics mode extra-defs) + (declare (ignore mode)) + (let* ((signatures (second event)) + (new-sigs (if signatures + (instance-signatures subs signatures) + nil)) + (new-events (instance-event-list (cddr event) subs suffix generics + (if signatures + 'constrained + nil) + extra-defs))) + `(encapsulate ,new-sigs ,@new-events))) + +) + + +; To be able to actually introduce the events, we need to emit a macro that +; can be used to actually perform substitutions. + +(defmacro instance (theory) + (let ((macro-name (intern-in-package-of-symbol + (string-upcase (concatenate 'string + "instance-" (string theory))) + theory))) + `(defmacro ,macro-name (&key subs suffix generics extra-defs) + (list* 'encapsulate + nil + (instance-event-list ,theory subs suffix generics nil extra-defs))))) + + + + +; Some thoughts +; +; A fundamental issue seems to be that a function and its arguments +; are not always used in a consistent manner. For example, say we +; want to rewrite (all ?x) to (all-foo ?x y) and we want to rewrite +; (predicate ?x) to (not (foo ?x y)). How can we accurately say just +; what it is that we want to rewrite in each case? +; +; Right now our substitutions are based on +; ( (predicate ?x) (not (foo ?x y)) ) +; ( (all ?x) (all-foo ?x y) ) +; +; We can easily pick out and say "all" is replaced by "all-foo", +; but if we try to just use the car of the term as its symbol +; replacement, then "predicate" would be "not". +; +; OK, so we could do some kind of preprocessing step where we fill +; in argument guards. The "generics" list right now is a big huge +; hack that allows us to ignore the fact that :predicate doens't +; have a definition. Really the issue that this is trying to solve +; is to tell us how to build our :in-theory event. Right now the +; :in-theory event is just a hack that we don't really understand. diff --git a/books/workshops/2004/davis/support/map.lisp b/books/workshops/2004/davis/support/map.lisp new file mode 100644 index 0000000..c8e038e --- /dev/null +++ b/books/workshops/2004/davis/support/map.lisp @@ -0,0 +1,461 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; 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<function> +; map-list<function> +; +; 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. +; +; (SET::map-function (integerp x)) +; - (SET::map<integerp> '(1 2 3)) = (t) +; - (SET::map-list<integerp> '(1 a 2 b)) = (t nil t nil) +; +; (defun square (x) +; (declare (xargs :guard t)) +; (* (rfix x) (rfix x))) +; +; (SET::map-function (square x)) +; - (SET::map<square> '(1 2 3)) = (1 4 9) +; - (SET::map<square> '(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<f> 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: +; +; (SET::map-function (square x) +; :in-package-of defthm) +; +; And map<square> 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))) +; +; (SET::map-function (square-then-add input offset) +; :in-package-of defthm) +; +; (map<square-then-add> '(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<integerp> ?set)) ; set's name must be ?set +; :list-guard ((all-list<integerp> ?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 "SET") +(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<inversep> 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<not-inversep> X a)))) + + +; With this notion of membership in play, we can now use the +; properties of all<not-inversep> 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<inversep> 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<f> (mksym (app "map" wrap) in-package)) + (map-list<f> (mksym (app "map-list" wrap) in-package)) + (inversep (app "inversep" wrap)) + (ipw (app "<" (app inversep ">"))) + (not-ipw (app "<not-" (app inversep ">"))) + (inversep<f> (mksym inversep in-package)) + + (all<inversep<f>> (mksym (app "all" ipw) in-package)) + (exists<inversep<f>> (mksym (app "exists" ipw) in-package)) + (find<inversep<f>> (mksym (app "find" ipw) in-package)) + (filter<inversep<f>> (mksym (app "filter" ipw) in-package)) + (all-list<inversep<f>> (mksym (app "all-list" ipw) in-package)) + (exists-list<inversep<f>> (mksym (app "exists-list" ipw) in-package)) + (find-list<inversep<f>> (mksym (app "find-list" ipw) in-package)) + (filter-list<inversep<f>> (mksym (app "filter-list" ipw) in-package)) + + (all<not-inversep<f>> (mksym (app "all" not-ipw) in-package)) + (exists<not-inversep<f>> (mksym (app "exists" not-ipw) in-package)) + (find<not-inversep<f>> (mksym (app "find" not-ipw) in-package)) + (filter<not-inversep<f>> (mksym (app "filter" not-ipw) in-package)) + (all-list<not-inversep<f>> (mksym (app "all-list" not-ipw) in-package)) + (exists-list<not-inversep<f>> (mksym (app "exists-list" not-ipw) in-package)) + (find-list<not-inversep<f>> (mksym (app "find-list" not-ipw) in-package)) + (filter-list<not-inversep<f>> (mksym (app "filter-list" not-ipw) in-package)) + + + (subs `(((transform ?x) (,name ?x ,@extra-args)) + ((map ?x) (,map<f> ?x ,@extra-args)) + ((map-list ?x) (,map-list<f> ?x ,@extra-args)) + ((inversep ?a ?b) (,inversep<f> ?a ?b ,@extra-args)) + + ((all<inversep> ?a ?b) (,all<inversep<f>> ?a ?b ,@extra-args)) + ((exists<inversep> ?a ?b) (,exists<inversep<f>> ?a ?b ,@extra-args)) + ((find<inversep> ?a ?b) (,find<inversep<f>> ?a ?b ,@extra-args)) + ((filter<inversep> ?a ?b) (,filter<inversep<f>> ?a ?b ,@extra-args)) + + ((all-list<inversep> ?a ?b) (,all-list<inversep<f>> ?a ?b ,@extra-args)) + ((exists-list<inversep> ?a ?b) (,exists-list<inversep<f>> ?a ?b ,@extra-args)) + ((find-list<inversep> ?a ?b) (,find-list<inversep<f>> ?a ?b ,@extra-args)) + ((filter-list<inversep> ?a ?b) (,filter-list<inversep<f>> ?a ?b ,@extra-args)) + + ((all<not-inversep> ?a ?b) (,all<not-inversep<f>> ?a ?b ,@extra-args)) + ((exists<not-inversep> ?a ?b) (,exists<not-inversep<f>> ?a ?b ,@extra-args)) + ((find<not-inversep> ?a ?b) (,find<not-inversep<f>> ?a ?b ,@extra-args)) + ((filter<not-inversep> ?a ?b) (,filter<not-inversep<f>> ?a ?b ,@extra-args)) + + ((all-list<not-inversep> ?a ?b) (,all-list<not-inversep<f>> ?a ?b ,@extra-args)) + ((exists-list<not-inversep> ?a ?b) (,exists-list<not-inversep<f>> ?a ?b ,@extra-args)) + ((find-list<not-inversep> ?a ?b) (,find-list<not-inversep<f>> ?a ?b ,@extra-args)) + ((filter-list<not-inversep> ?a ?b) (,filter-list<not-inversep<f>> ?a ?b ,@extra-args)) + )) + + (theory<f> (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<f>-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<f> 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<f>) + + (deftheory ,theory<f> + (union-theories + (theory ',(mksym (app "theory" ipw) in-package)) + '(,map<f> ,map-list<f> ,inversep<f> + ,@theory<f>-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<inversep>) + `(,@(INSTANCE::defthm-names *map-theorems*) + map + map-list + inversep))) + +(in-theory (disable generic-map-theory)) diff --git a/books/workshops/2004/davis/support/membership.lisp b/books/workshops/2004/davis/support/membership.lisp new file mode 100644 index 0000000..cac57c5 --- /dev/null +++ b/books/workshops/2004/davis/support/membership.lisp @@ -0,0 +1,647 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; +; membership.lisp +; +; We are now getting into more interesting territory. The primitive set +; functions nicely contain the potential messes that we would have to face if +; we were implementing sets just using the primitive list functions. However, +; they are still plagued with order. +; +; The end user of the set library should not have to care that the elements of +; the set are ordered or not. (Well, with the exception that if they are +; trying to make a fast version of a function, they might decide to exploit +; that order.) +; +; Set reasoning should be done in terms of membership. In traditional +; mathematics, subsets are defined through quantification over membership, as +; is set equailty, and so forth. But right now, the best we can do is induct +; over insert, which is somewhat messy. +; +; This file introduces the notions of set membership and subset. We also go +; into an abstract argument which will form the basis for quantification. The +; goal is to transform the insertion induction proofs into more traditional +; pick-a-point and double containment proofs. +; +; At the end of this file, we will disable all of the theorems that pertain to +; the order of elements, providing an entirely membership-based reasoning +; environment for the outer level. + +(in-package "SET") +(include-book "primitives") +(include-book "computed-hints") +(set-verify-guards-eagerness 2) + + + +;;; Set Membership. +;;; +;;; We could go ahead and write another version of in, which could use +;;; the total order to stop early if it ever encountered an element +;;; too big. I.e., looking for 1 in the list '(2 3 4), it could say +;;; that since 1 << 2, we are done. +;;; +;;; Should we do so? Really the only question is whether or not it +;;; would be faster. Certainly we can contrive situations in which it +;;; would be better, i.e. (in 1 '(2 3 4 .... 100000)), where we would +;;; save 100,000 calls to in. But we can also contrive situations +;;; that it would be slower, for example (in 100001 '(1 2 3 4 +;;; ... 100000)), where we would incur the extra cost of 100,000 calls +;;; to <<. +;;; +;;; I have arbitrarily decided not to implement short-circuiting. My +;;; reasoning is that (1) it is not clear which would be faster, (2) +;;; it is not clear what "typical" usage behavior of in would be, so +;;; even if we wanted to benchmark the two solutions, we could +;;; probably not come up with a good benchmarking suite, (3) both +;;; solutions are O(n) anyway so I don't think there's much to be +;;; gained here, and (4) the current method is arguably "no less +;;; efficient" than an unordered implementation. + +(defun in (a X) + (declare (xargs :guard (setp X))) + (and (not (empty X)) + (or (equal a (head X)) + (in a (tail X))))) + +(defthm in-type + (or (equal (in a X) t) + (equal (in a X) nil)) + :rule-classes :type-prescription) + +(encapsulate () + + (local (defthm lemma + (implies (> (acl2-count x) (acl2-count y)) + (not (in x y))))) + + (defthm not-in-self + (not (in x x))) + +) + +(defthm in-sfix-cancel + (equal (in a (sfix X)) (in a X))) + +(defthm never-in-empty + (implies (empty X) (not (in a X)))) + +(defthm in-set + (implies (in a X) (setp X))) + +(defthm in-tail + (implies (in a (tail X)) (in a X))) + +(defthm in-tail-or-head + (implies (and (in a X) + (not (in a (tail X)))) + (equal (head X) a))) + + +;;; We now begin to move away from set order. + +(encapsulate () + + (local (defthm lemma + (implies (and (not (empty X)) + (not (equal a (head X))) + (not (<< a (head (tail X)))) + (<< a (head X))) + (not (in a X))) + :hints(("Goal" + :in-theory (enable primitive-order-theory) + :cases ((empty (tail X))))))) + + (defthm head-minimal + (implies (<< a (head X)) + (not (in a X))) + :hints(("Goal" + :in-theory (enable primitive-order-theory)))) + + (defthm head-minimal-2 + (implies (in a X) + (not (<< a (head X))))) + +) + +(encapsulate () + + (local (defthm lemma + (implies (empty (tail X)) + (not (in (head X) (tail X)))))) + + (local (defthm lemma-2 + (implies (not (empty (tail X))) + (not (in (head X) (tail X)))) + :hints(("Goal" :in-theory (enable primitive-order-theory))))) + + ;; This is an interesting theorem, which gives us a concept of + ;; uniqueness without using the set order to state it! + + (defthm head-unique + (not (in (head X) (tail X))) + :hints(("Goal" + :use ((:instance lemma) + (:instance lemma-2))))) +) + + +(defthm insert-identity + (implies (in a X) + (equal (insert a X) X)) + :hints(("Goal" :in-theory (enable insert-induction-case)))) + + +(defthm in-insert + (equal (in a (insert b X)) + (or (in a X) + (equal a b))) + :hints(("Goal" :in-theory (enable primitive-order-theory) + :induct (insert b X)))) + + + + +;;; The behavior of insert is, of course, determined by the set order. +;;; Yet, we often need to induct upon insert's definition to prove +;;; theorems. So, here we introduce a new induction scheme which +;;; hides the set order, yet still allows us to induct on insert very +;;; nicely. We then disable the induction scheme that insert normally +;;; uses, and set up an induction hint so that weak-insert-induction +;;; will automatically be used instead. + +(defthm weak-insert-induction-helper-1 + (implies (and (not (in a X)) + (not (equal (head (insert a X)) a))) + (equal (head (insert a X)) (head X))) + :hints(("Goal" :in-theory (enable primitive-order-theory)))) + +(defthm weak-insert-induction-helper-2 + (implies (and (not (in a X)) + (not (equal (head (insert a X)) a))) + (equal (tail (insert a X)) (insert a (tail X)))) + :hints(("Goal" :in-theory (enable primitive-order-theory)))) + +(defthm weak-insert-induction-helper-3 + (implies (and (not (in a X)) + (equal (head (insert a X)) a)) + (equal (tail (insert a X)) (sfix X))) + :hints(("Goal" :in-theory (enable primitive-order-theory)))) + +(defun weak-insert-induction (a X) + (declare (xargs :guard (setp X))) + (cond ((empty X) nil) + ((in a X) nil) + ((equal (head (insert a X)) a) nil) + (t (list (weak-insert-induction a (tail X)))))) + +(in-theory (disable (:induction insert))) + +(defthm use-weak-insert-induction t + :rule-classes ((:induction + :pattern (insert a X) + :scheme (weak-insert-induction a X)))) + + + + + +;;; Subset Testing. +;;; +;;; Now we introduce subset. This becomes complicated because we want +;;; to use MBE to make it fast. The fast-subset function is a tail +;;; re- cursive, linear pass through both lists. Subset, by +;;; comparison, is a nice to reason about definition and much simpler, +;;; but would require quadratic time if we didn't use MBE here. + +(defun fast-subset (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (cond ((empty X) t) + ((empty Y) nil) + ((<< (head X) (head Y)) nil) + ((equal (head X) (head Y)) (fast-subset (tail X) (tail Y))) + (t (fast-subset X (tail Y))))) + +(defun subset (X Y) + (declare (xargs :guard (and (setp X) (setp Y)) + :verify-guards nil)) + (mbe :logic (if (empty X) + t + (and (in (head X) Y) + (subset (tail X) Y))) + :exec (fast-subset X Y))) + +(defthm subset-type + (or (equal (subset X Y) t) + (equal (subset X Y) nil)) + :rule-classes :type-prescription) + +(encapsulate () + + (local (defthmd lemma + (implies (not (in (head Y) X)) + (equal (subset X Y) (subset X (tail Y)))))) + + (local (defthm case-1 + (implies (and (not (empty X)) + (not (empty Y)) + (not (<< (head X) (head Y))) + (not (equal (head X) (head Y))) + (implies (and (setp X) (setp (tail Y))) + (equal (fast-subset X (tail Y)) + (subset X (tail Y))))) + (implies (and (setp X) (setp Y)) + (equal (fast-subset X Y) + (subset X Y)))) + :hints(("Goal" :in-theory (enable primitive-order-theory) + :use (:instance lemma))))) + + (local (defthm case-2 + (implies (and (not (empty x)) + (not (empty y)) + (not (<< (head x) (head y))) + (equal (head x) (head y)) + (implies (and (setp (tail x)) (setp (tail y))) + (equal (fast-subset (tail x) (tail y)) + (subset (tail x) (tail y))))) + (implies (and (setp x) (setp y)) + (equal (fast-subset x y) + (subset x y)))) + :hints(("Goal" :in-theory (enable primitive-order-theory) + :use (:instance lemma (X (tail X))))))) + + (local (defthm fast-subset-equivalence + (implies (and (setp X) (setp Y)) + (equal (fast-subset X Y) (subset X Y))) + :hints(("Goal" :in-theory (enable primitive-order-theory) + :induct (fast-subset X Y))))) + + (verify-guards subset) + +) + + + + +;;; Quantification over Sets. +;;; +;;; Up until version 0.81, we used an explicit argument to reduce subset +;;; proofs to pick-a-point style membership arguments. Starting in 0.9, +;;; we generalize this argument to arbitrary predicates instead. +;;; +;;; I'll begin with some background on what we historically wanted to +;;; do. The "ultimate goal" was to use pick-a-point reasoning to +;;; prove subset relationships. In traditional mathematics, subset is +;;; defined using quantification over members, e.g., as follows: +;;; +;;; (subset X Y) iff "forall a : (in a X) implies (in a Y)" +;;; +;;; Traditionally, one would prove the membership part of this +;;; statement, and use it to conclude whether or not (subset X Y) is +;;; true. But, in ACL2, we cannot write a theorem of the following +;;; form, because all variables are implicitly universally quantified. +;;; +;;; [ "forall a : (in a ...) implies (in a ___)" ] +;;; => +;;; (subset ... ___) +;;; +;;; However, we can take the contrapositive of this theorem, which +;;; looks like the following: +;;; +;;; ~(subset ... ___) => "exists a : (in a ...) ^ ~(in a ___) +;;; +;;; And we can prove this, by using a new function to search for an +;;; element which satisfies the existential predicate. +;;; +;;; Once we prove the above, we still need to be able to "reduce" a +;;; proof of (subset X Y) to a proof of (in a X) => (in a Y). While +;;; we can't do this with a direct rewrite rule, we can sort of fake +;;; it using functional instantiation. In other words, we set up an +;;; encapsulated event with (in a X) => (in a Y) as its constraint, +;;; then we can use this constraint to prove that (subset X Y). By +;;; functionally instantiating the resulting theorem, we can reduce +;;; the subset problem to a membership problem. +;;; +;;; All of this was an explicit argument until version 0.9. But, now +;;; the process is generalized. First notice that subset is really +;;; nothing more than "forall a, (in a x) => (in a Y)." If you let (P +;;; x) = (in a Y), then this is "forall a, (in a x) => (P a)". This +;;; is a more general concept which can capture not only subset, but +;;; also many other ideas by simply changing the meaning of (P x). +;;; For example, if P = integerp, then we can test if every element in +;;; the set is an integer, and so forth. So, starting in v0.9, we use +;;; this more general form of encapsulate instead of the more specific +;;; version used in previous versions. +;;; +;;; We begin by introducing a completely arbitrary predicate. Based +;;; on this generic predicate we will introduce a new function, all, +;;; which checks to see if every member in a set satisfies a +;;; predicate. We also introduce find-not, which can be used to find +;;; us a witness for proving all-by-membership. Finally, we set up an +;;; encapsulate which allows us to assume that if some hypotheses are +;;; true, then any member of some set satisfies the predicate, and use +;;; this constraint to prove that if those same hypotheses are +;;; satisfied, then all is true for the same set. + +(encapsulate + (((predicate *) => *)) + (local (defun predicate (x) x))) + +(defun all (set-for-all-reduction) + (declare (xargs :guard (setp set-for-all-reduction))) + (if (empty set-for-all-reduction) + t + (and (predicate (head set-for-all-reduction)) + (all (tail set-for-all-reduction))))) + +(defun find-not (X) + (declare (xargs :guard (setp X))) + (cond ((empty X) nil) + ((not (predicate (head X))) (head X)) + (t (find-not (tail X))))) + + + +(encapsulate + (((all-hyps) => *) + ((all-set) => *)) + + (local (defun all-hyps () nil)) + (local (defun all-set () nil)) + + (defthmd membership-constraint + (implies (all-hyps) + (implies (in arbitrary-element (all-set)) + (predicate arbitrary-element)))) +) + +(encapsulate () + + (local (defthm lemma-find-not-is-a-witness + (implies (not (all x)) + (and (in (find-not x) x) + (not (predicate (find-not x))))))) + + (defthmd all-by-membership + (implies (all-hyps) + (all (all-set))) + :hints(("Goal" + :use (:instance membership-constraint + (arbitrary-element (find-not (all-set))))))) +) + + +;;; The theorem all-by-membership is massively important. It is the basis +;;; for reducing subset arguments to membership arguments. It also has a +;;; sufficiently general character that we can reuse it to make similar +;;; reductions for problems other than subset. +;;; +;;; However, for the time being, it's important that we actually do apply +;;; this theorem to the subset function, which is a particularly useful +;;; way of reasoning about sets. Two important questions are: how can we +;;; apply the theorem, and when should we apply it? +;;; +;;; To support these notions, a framework is introduced in the file +;;; computed-hints.lisp. Basically, we introduce a "trigger" function +;;; which is nothing more than an alias for subset. We then use the +;;; "tagging theorem" pick-a-point-subset-strategy in order to rewrite +;;; subsets into subset-triggers. This theorem is constrained so that +;;; it will only rewrite conclusions and it will not apply while +;;; backchaining, via syntaxp hypotheses. This process is described +;;; in more detail in computed-hints.lisp. + +(defun subset-trigger (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (subset X Y)) + +(defthm pick-a-point-subset-strategy + (implies (and (syntaxp (rewriting-goal-lit mfc state)) + (syntaxp (rewriting-conc-lit `(subset ,X ,Y) mfc state))) + (equal (subset X Y) + (subset-trigger X Y)))) + +(in-theory (disable subset-trigger)) + + + +(COMPUTED-HINTS::automate-instantiation + :new-hint-name pick-a-point-subset-hint + :generic-theorem all-by-membership + :generic-predicate predicate + :generic-hyps all-hyps + :generic-collection all-set + :generic-collection-predicate all + :actual-collection-predicate subset + :actual-trigger subset-trigger + :predicate-rewrite (((predicate ?x ?y) (in ?x ?y))) + :tagging-theorem pick-a-point-subset-strategy +) + + + + + +;;; We now show the basic properties of subset. The first theorems +;;; are mundane but then we get more interesting, showing that subset +;;; is reflexive and transitive. The goal here is to build up +;;; sufficient theorems to do pick-a-point proofs, which come next. + +(defthm subset-sfix-cancel-X + (equal (subset (sfix X) Y) + (subset X Y))) + +(defthm subset-sfix-cancel-Y + (equal (subset X (sfix Y)) + (subset X Y))) + +(defthm empty-subset + (implies (empty X) + (subset X Y))) + +(defthm empty-subset-2 + (implies (empty Y) + (equal (subset X Y) (empty X)))) + +(defthm subset-in + (implies (and (subset X Y) + (in a X)) + (in a Y))) + +(defthm subset-in-2 + (implies (and (subset X Y) + (not (in a Y))) + (not (in a X)))) + +(defthm subset-insert-X + (equal (subset (insert a X) Y) + (and (subset X Y) + (in a Y))) + :hints(("Goal" :induct (insert a X)))) + +(defthm subset-reflexive + (subset X X)) + +(defthm subset-transitive + (implies (and (subset X Y) + (subset Y Z)) + (subset X Z))) + +(defthm subset-membership-tail + (implies (and (subset X Y) + (in a (tail X))) + (in a (tail Y))) + :hints(("Goal" :in-theory (enable primitive-order-theory)))) + +(defthm subset-membership-tail-2 + (implies (and (subset X Y) + (not (in a (tail Y)))) + (not (in a (tail X)))) + :hints(("Goal" :in-theory (disable subset-membership-tail) + :use (:instance subset-membership-tail)))) + +(defthm subset-insert + (subset X (insert a X))) + +(defthm subset-tail + (subset (tail X) X) + :rule-classes ((:rewrite) + (:forward-chaining :trigger-terms ((tail x))))) + + + + + + +;;; Proofs of equality by double containment are also very common. So, +;;; to support these, we want to show that double containment is the +;;; same as equality. +;;; +;;; The general argument is the following: +;;; +;;; Suppose that we have two sets which are subsets of one another, +;;; i.e. (subset X Y) and (subset Y X) are true. First, we will show +;;; that (head X) = (head Y). Next we will show that (in a (tail X)) +;;; implies that (in a (tail Y)). This fact is then used for a sub- +;;; set by membership argument to show that (tail X) = (tail Y). +;;; Now, (head X) = (head Y) and (tail X) = (tail Y) can be used +;;; together to show that X = Y (see primitives.lisp, head-tail-same) +;;; so we are done. + +(encapsulate () + + ;; Here are the details. First we show that the heads are the same: + + (local (defthmd double-containment-lemma-head + (implies (and (subset X Y) + (subset Y X)) + (equal (head X) (head Y))) + :hints(("Goal" :in-theory (enable primitive-order-theory))))) + + + ;; Next we show that (tail X) is a subset of (tail Y), using a subset + ;; by membership argument: + + (local (defthmd in-tail-expand + (equal (in a (tail X)) + (and (in a X) + (not (equal a (head X))))))) + + (local (defthmd double-containment-lemma-in-tail + (implies (and (subset X Y) + (subset Y X)) + (implies (in a (tail X)) ; could be "equal" instead, + (in a (tail Y)))) ; but that makes loops. + :hints(("Goal" + :in-theory (enable primitive-order-theory) + :use ((:instance in-tail-expand (a a) (X X)) + (:instance in-tail-expand (a a) (X Y))))))) + + (local (defthmd double-containment-lemma-tail + (implies (and (subset X Y) + (subset Y X)) + (subset (tail X) (tail Y))) + :hints(("Goal" :in-theory (enable double-containment-lemma-in-tail))))) + + ;; Finally, we are ready to show that double containment is equality. + ;; To do this, we need to induct in such a way that we consider the + ;; tails of X and Y. Then, we will use our fact that about the tails + ;; being subsets of one another in the inductive case. + + (local (defun double-tail-induction (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (if (or (empty X) (empty Y)) + (list X Y) + (double-tail-induction (tail X) (tail Y))))) + + (local (defthm double-containment-is-equality-lemma + (IMPLIES (AND (NOT (OR (EMPTY X) (EMPTY Y))) + (IMPLIES (AND (SUBSET (TAIL X) (TAIL Y)) + (SUBSET (TAIL Y) (TAIL X))) + (EQUAL (EQUAL (TAIL X) (TAIL Y)) T)) + (SETP X) + (SETP Y) + (SUBSET X Y) + (SUBSET Y X)) + (EQUAL (EQUAL X Y) T)) + :hints(("Goal" + :use ((:instance double-containment-lemma-tail + (X X) (Y Y)) + (:instance double-containment-lemma-tail + (X Y) (Y X)) + (:instance double-containment-lemma-head + (X X) (Y Y))))))) + + (local (defthmd double-containment-is-equality + (implies (and (setp X) + (setp Y) + (subset X Y) + (subset Y X)) + (equal (equal X Y) t)) + :hints(("Goal" :induct (double-tail-induction X Y))))) + + (defthm double-containment + (implies (and (setp X) + (setp Y)) + (equal (equal X Y) + (and (subset X Y) + (subset Y X)))) + :hints(("Goal" :use (:instance double-containment-is-equality)))) + +) + + +;;; We are now done with the membership level. We disable all of the +;;; order based reasoning that we introduced here. + +(in-theory (disable head-minimal + head-minimal-2)) diff --git a/books/workshops/2004/davis/support/outer.lisp b/books/workshops/2004/davis/support/outer.lisp new file mode 100644 index 0000000..b0a8885 --- /dev/null +++ b/books/workshops/2004/davis/support/outer.lisp @@ -0,0 +1,531 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; 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 introduced 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 "SET") +(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))) + +(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))) + +(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))) + +(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 (len 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)))) diff --git a/books/workshops/2004/davis/support/package.lsp b/books/workshops/2004/davis/support/package.lsp new file mode 100644 index 0000000..fcf4c01 --- /dev/null +++ b/books/workshops/2004/davis/support/package.lsp @@ -0,0 +1,66 @@ +#| + + Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> + + + + package.lisp + + Defpackage events for the set theory library. + +|# + + +(defpkg "INSTANCE" + (union-eq '() + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*))) + + +(defpkg "COMPUTED-HINTS" + (union-eq '(mfc-ancestors + mfc-clause + string-for-tilde-@-clause-id-phrase + INSTANCE::instance-rewrite) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*))) + + +(defpkg "SET" + (set-difference-equal (union-eq '(lexorder + COMPUTED-HINTS::rewriting-goal-lit + COMPUTED-HINTS::rewriting-conc-lit) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(union delete find map))) + diff --git a/books/workshops/2004/davis/support/primitives.lisp b/books/workshops/2004/davis/support/primitives.lisp new file mode 100644 index 0000000..eb5ac38 --- /dev/null +++ b/books/workshops/2004/davis/support/primitives.lisp @@ -0,0 +1,450 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; primitives.lisp +; +; Consider implementing a set theory library in ACL2. Lists are a natural +; choice for an underlying representation. And, naturally, we are drawn to +; define our functions in terms of the primitive list functions (car, cdr, +; endp, cons). +; +; These functions are ill-suited for use in our set theory books because of the +; non-set convention. This convention states that non-sets should be treated +; as the empty set. But the primitive list functions do not support this idea. +; For example: +; +; (car '(1 1 1)) = 1, but (car nil) = nil +; (cdr '(1 1 1)) = (1 1), but (cdr nil) = nil +; (cons 1 '(1 1 1)) = (1 1 1 1), but (cons 1 nil) = (1) +; (endp '(1 1 1)) = nil, but (endp nil) = t +; +; These are "problems" in the sense that, when reasoning about sets, the +; primitive list functions do not respect the non-set convention. These +; functions do not fit our problem well, and will introduce all manner of cases +; into our proofs that we should not have to consider. +; +; Having recognized this as a problem, here is what we are going to do. +; Instead of using the list primitives to manipulate sets, we will use new +; primitives which are very similar, but which respect the non-set convention. +; These primitives get the following names: +; +; (head X) - the first element of a set, nil for non/empty sets. +; (tail X) - all but the first element, nil for non/empty sets. +; (insert a X) - ordered insert of a into the set X +; (empty X) - recognizer for non/empty sets. +; +; This file introduces these functions, and shows several theorems about them. +; The purpose of all of this is to, at the end of this file, disable the +; definitions for these functions, and thereby keep the primitive list +; functions (car, cdr, ...) confined where they cannot cause case splits. +; +; Before we can introduce the list primitives, we need to be able to define a +; set. Our sets will be ordered under a total order, <<. Note that this order +; is encapsulated: we locally use the same order as the standard +; "misc/total-order" book, which was put together by Matt Kaufmann, Pete +; Manolios, and Rob Sumners. However, we will only use this locally and will +; allow other orders to be used, in order to be a more flexible library. + +(in-package "SET") +(set-verify-guards-eagerness 2) + + + +;;; First we introduce the total order, <<. and prove that it is a +;;; total order (irreflexivity, transitivity, asymmetricity, trichot- +;;; omy). + +(defun << (a b) + (declare (xargs :guard t)) + (and (lexorder a b) + (not (equal a b)))) + +(defthm <<-type + (or (equal (<< a b) t) + (equal (<< a b) nil)) + :rule-classes :type-prescription) + +(defthm <<-irreflexive + (not (<< a a))) + +(defthm <<-transitive + (implies (and (<< a b) (<< b c)) + (<< a c))) + +(defthm <<-asymmetric + (implies (<< a b) + (not (<< b a)))) + +(defthm <<-trichotomy + (implies (and (not (<< b a)) + (not (equal a b))) + (<< a b))) + +(in-theory (disable <<)) + + + + +;;; Now we can define sets. Sets are those lists whose elements are +;;; fully ordered under the relation above. Note that this implicitly +;;; means that sets contain no duplicate elements. Testing for sets +;;; will inherently be somewhat slow since we have to check that the +;;; elements are in order. However, its complexity is still only lin- +;;; ear with the size of X. + +(defun setp (X) + (declare (xargs :guard t)) + (if (atom X) + (null X) + (or (null (cdr X)) + (and (consp (cdr X)) + (<< (car X) (cadr X)) + (setp (cdr X)))))) + +(defthm setp-type + (or (equal (setp X) t) + (equal (setp X) nil)) + :rule-classes :type-prescription) + +(defthm sets-are-true-lists + (implies (setp X) + (true-listp X))) + + + + +;;; At this point, we simply introduce the remainder of the primitive +;;; functions. These definitions should hold few surprises. The MBE +;;; macro is used in all of these functions except for insert, to +;;; avoid potentially slow calls to setp. + +(defun empty (X) + (declare (xargs :guard (setp X))) + (mbe :logic (or (null X) + (not (setp X))) + :exec (null X))) + +(defthm empty-type + (or (equal (empty X) t) + (equal (empty X) nil)) + :rule-classes :type-prescription) + +(defun sfix (X) + (declare (xargs :guard (setp X))) + (mbe :logic (if (empty X) nil X) + :exec X)) + +(defun head (X) + (declare (xargs :guard (and (setp X) + (not (empty X))))) + (mbe :logic (car (sfix X)) + :exec (car X))) + +(defun tail (X) + (declare (xargs :guard (and (setp X) + (not (empty X))))) + (mbe :logic (cdr (sfix X)) + :exec (cdr X))) + +(defun insert (a X) + (declare (xargs :guard (setp X))) + (cond ((empty X) (list a)) + ((equal (head X) a) X) + ((<< a (head X)) (cons a X)) + (t (cons (head X) (insert a (tail X)))))) + + + + +;;; Our goal is to "hide" the list primitives (car, cdr, ...) within +;;; head, tail, etc. This means that an end-user's functions will end +;;; up recurring over tail. It is therefore important to show that +;;; tail actually decreases some measure, so that they can prove their +;;; functions terminate. Naturally, we show that acl2-count decreases +;;; with tail. We also show that acl2-count decreases with head, in +;;; case this fact is needed. + +(defthm tail-count + (implies (not (empty X)) + (< (acl2-count (tail X)) (acl2-count X))) + :rule-classes :linear) + +(defthm head-count + (implies (not (empty X)) + (< (acl2-count (head X)) (acl2-count X))) + :rule-classes :linear) + + + + +;;; Concluding that objects are sets is important for satisfying guard +;;; conjectures, and also for proofs of equality via a double contain- +;;; ment approach. Here are some nice theorems to help with this: + +(defthm sfix-produces-set + (setp (sfix X))) + +(defthm tail-produces-set + (setp (tail X))) + +(defthm insert-produces-set + (setp (insert a X))) + +(defthm nonempty-means-set + (implies (not (empty X)) + (setp X))) + + + +;;; Does every set have a unique representation? Yes and no. It is +;;; true in the sense that, if (setp X) holds, then there is no Y such +;;; that (in a X) <=> (in a Y) except for Y = X. But what about when +;;; (setp X) does not hold? Well, technically X is no longer a set, +;;; but our functions treat X as if it were empty. We would like to +;;; be able to reason about this case. +;;; +;;; Well, although we cannot say (empty X) ^ (empty Y) => X = Y, we +;;; can state several similarly spirited theorems. For example, we +;;; can say that the heads, tails, sfix's, and results of inserting +;;; elements into X and Y are always the same. Here are several the- +;;; orems to this effect: + +(defthm empty-set-unique + (implies (and (setp X) + (setp Y) + (empty X) + (empty Y)) + (equal (equal X Y) t))) + +(defthm head-empty-same + (implies (and (empty X) + (empty Y)) + (equal (equal (head X) (head Y)) t))) + +(defthm tail-empty-same + (implies (and (empty X) + (empty Y)) + (equal (equal (tail X) (tail Y)) t))) + +(defthm insert-empty-same + (implies (and (empty X) + (empty Y)) + (equal (equal (insert a X) (insert a Y)) t))) + +(defthm sfix-empty-same + (implies (and (empty X) + (empty Y)) + (equal (equal (sfix X) (sfix Y)) t))) + +(defthm head-tail-same + (implies (and (not (empty X)) + (not (empty Y)) + (equal (head X) (head Y)) + (equal (tail X) (tail Y))) + (equal (equal X Y) t))) + + + +;;; While the above theorems show a sort of equivalence between empty +;;; sets, it is also important to know what operations preserve and +;;; destroy emptiness. + +(defthm insert-never-empty + (not (empty (insert a X)))) + +(defthm tail-preserves-empty + (implies (empty X) + (empty (tail X)))) + + + + +;;; While it did take quite a few theorems to have enough information +;;; about empty, the sfix function is more simple. Sfix is the ident- +;;; ity function on sets, and maps all non-sets to nil. We can show +;;; that all of the other primitives treat have a sort of equivalence +;;; under sfix, and quickly eliminate it when we see it: + +(defthm sfix-set-identity + (implies (setp X) + (equal (sfix X) X))) + +(defthm empty-sfix-cancel + (equal (empty (sfix X)) (empty X))) + +(defthm head-sfix-cancel + (equal (head (sfix X)) (head X))) + +(defthm tail-sfix-cancel + (equal (tail (sfix X)) (tail X))) + +(defthm insert-sfix-cancel + (equal (insert a (sfix X)) (insert a X))) + + + + +;;; Now it is time to reason about insert. These theorems are about +;;; as most complicated that we get. +;;; +;;; Historic Note: We used to require that nil was "greater than" +;;; everything else in our order. This had the advantage that the +;;; following theorems could have a combined case for (empty X) and +;;; (<< a (head X)). Starting in Version 0.9, we remove this res- +;;; triction in order to be more flexible about our order. + +(defthm head-insert + (equal (head (insert a X)) + (cond ((empty X) a) + ((<< a (head X)) a) + (t (head X))))) + +(defthm tail-insert + (equal (tail (insert a X)) + (cond ((empty X) (sfix X)) + ((<< a (head X)) (sfix X)) + ((equal a (head X)) (tail X)) + (t (insert a (tail X)))))) + +(defthm insert-insert + (equal (insert a (insert b X)) + (insert b (insert a X))) + :rule-classes ((:rewrite :loop-stopper ((a b))))) + +(defthm repeated-insert + (equal (insert a (insert a X)) + (insert a X))) + +(defthm insert-head + (implies (not (empty X)) + (equal (insert (head X) X) X))) + +(defthm insert-head-tail + (implies (not (empty X)) + (equal (insert (head X) (tail X)) X))) + + + +;;; We also need to be able to reason about insertions into empty +;;; sets. Do not move these theorems above head-insert and +;;; tail-insert, or they will be subsumed and proofs in +;;; membership.lisp will fail. + +(defthm head-insert-empty + (implies (empty X) + (equal (head (insert a X)) a))) + +(defthm tail-insert-empty + (implies (empty X) + (empty (tail (insert a X))))) + + + + +;;; Insert can be reasoned about in terms of induction, but its induc- +;;; tive case contains a call to "cons", and we cannot let that escape +;;; into the wild. Instead, we write a theorem to rephrase this cons +;;; into an insert. WARNING: This can cause loops. It is disabled by +;;; default for this reason. + +(defthmd insert-induction-case + (implies (and (not (empty X)) + (not (equal a (head X))) + (not (<< a (head X)))) + (equal (insert a X) + (insert (head X) (insert a (tail X)))))) + + + + +;;; The last thing we really need to do is reason about element order. +;;; The following theorems are crucial for proofs in the membership +;;; level, which must stricly use induction and arguments about the +;;; set elements' order for proofs. Since we are disabling all of +;;; the functions at the end of this book, these are the only facts +;;; which membership.lisp will be able to use. + +(defthm head-tail-order + (implies (not (empty (tail X))) + (<< (head X) (head (tail X))))) + +(defthm head-tail-order-contrapositive + (implies (not (<< (head X) (head (tail X)))) + (empty (tail X)))) + +(defthm head-not-head-tail + (implies (not (empty (tail X))) + (not (equal (head X) (head (tail X)))))) + + + + +;;; Finally, this is an obscure looking theorem, which is only used to +;;; prove (not (in X X)) in membership.lisp. TODO: Make sure it gets +;;; disabled afterwards. This is a really odd theorem to just leave +;;; lying around enabled. + +(defthm head-not-whole + (implies (not (empty X)) + (not (equal (head X) X)))) + + +;;; And that concludes the theorems we need about the primitive set +;;; functions. Now we are interested in setting up theories and in +;;; disabling most of the potentially bad issues that might arise. +;;; +;;; You should never need to use primitive-theory unless you are using +;;; non-set functions, e.g. cons, to build sets. +;;; +;;; The primitive order theory is intended to be disabled for typical +;;; reasoning, but is needed for some theorems in the membership level. + +(deftheory primitives-theory + '(setp + empty + head + tail + sfix + (:definition insert))) + +(deftheory primitive-order-theory + '(<<-irreflexive + <<-transitive + <<-asymmetric + <<-trichotomy + head-insert + tail-insert + head-tail-order + head-tail-order-contrapositive)) + +(in-theory (disable primitives-theory + primitive-order-theory)) diff --git a/books/workshops/2004/davis/support/quantify.lisp b/books/workshops/2004/davis/support/quantify.lisp new file mode 100644 index 0000000..a50671e --- /dev/null +++ b/books/workshops/2004/davis/support/quantify.lisp @@ -0,0 +1,970 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; +; quantify.lisp +; +; This is an optional extension of the sets library, and is not included by +; default when you run (include-book "sets"). +; +; +; Constructive Quantification over Sets and Lists. +; +; We create the macro, quantify-predicate, which introduces the following +; functions for any arbitrary predicate. +; +; all<predicate> all<not-predicate> +; exists<predicate> exists<not-predicate> +; find<predicate> find<not-predicate> +; filter<predicate> filter<not-predicate> +; +; all-list<predicate> all-list<not-predicate> +; exists-list<predicate> exists-list<not-predicate> +; find-list<predicate> find-list<not-predicate> +; filter-list<predicate> filter-list<not-predicate> +; +; In addition to introducing these functions, an entire rewriting strategy is +; introduced for reasoning about these functions with respect to sets and +; lists. +; +; Introductory Examples. +; +; Here are some of the most simple examples. All of these predicates have only +; a single argument, and their guard is "t". +; +; (SET::quantify-predicate (integerp x)) +; (SET::quantify-predicate (symbolp x)) +; (SET::quantify-predicate (rationalp x)) +; (SET::quantify-predicate (natp x)) +; +; Notice that you cannot use macros here. For example, the following is an +; error: (quantify-predicate (real/rationalp x)). Once you have done the +; above, you can now run these functions, e.g., +; +; (SET::all<integerp> '(1 2 3)) = t +; (SET::all<not-integerp> '(a b c)) = t +; (SET::find<symbolp> '(1 2 3 a b c)) = a +; +; Controlling Packages. +; +; As you can see, all of these functions are introduced in the SETS package by +; default. If you'd like them to be in a different place instead, you can +; specify the :in-package-of argument and provide a symbol from some other +; package. For example, since defthm is in the ACL2 package, we might write: +; +; (SET::quantify-predicate (eqlablep x) +; :in-package-of defthm) +; +; And then the functions all<integerp>, all<not-integerp>, and so forth will be +; in the ACL2 package instead of the LISTS package. +; +; +; Multi-Argument Predicates. +; +; You can also quantify over predicates with many arguments. As an example, we +; introduce the function lessp as follows: +; +; (defun lessp (a b) +; (declare (xargs :guard t)) +; (< (rfix a) (rfix b))) +; +; (quantify-predicate (lessp a b)) +; +; We could now ask, is every element in a set less than some maximum value? +; For example: +; +; (all<lessp> '(1 2 3) 6) = t +; (all<lessp> '(1 2 3) 2) = nil +; +; +; +; Supporting Guards. +; +; If efficiency is important, our predicate may have guards and we may want to +; put guards on the introduced functions. For example, we might write +; fast-lessp below: +; +; (defun fast-lessp (a b) +; (declare (xargs :guard (and (rationalp a) +; (rationalp b)))) +; (< a b)) +; +; Now we need to supply an extra :guard argument so that the guards of +; all<fast-lessp>, exists<fast-lessp>, and so forth can be verified. +; +; When writing this guard, the list which all-list<fast-lessp> and so forth are +; iterating over will be called ?list, and the set that all<fast-lessp> and so +; forth are iterating over will be called ?set. The other arguments will all +; be named with whatever names you gave them when you called +; quantify-predicate. For example, below we name fast-lessp's second argument +; "max", so it will be named "max" in our guards as well. +; +; Here's an example: +; +; (in-package "ACL2") +; +; (SET::quantify-predicate (rationalp x) +; :in-package-of defthm) +; +; (SET::quantify-predicate (fast-lessp x max) +; :set-guard ((all<rationalp> ?set)) +; :list-guard ((all-list<rationalp> ?list)) +; :arg-guard ((rationalp max)) +; :in-package-of defthm) +; +; +; Disabling the theory. +; +; Calling quantify-predicate will result in a lot of theorems being introduced. +; You can disable all of these theorems by using the deftheory event +; theory<predicate>. For example, +; +; (in-theory (disable theory<integerp>)) +; (in-theory (disable theory<fast-lessp>)) +; +; And so forth. + + +(in-package "SET") +(include-book "sets") +(set-verify-guards-eagerness 2) + + + +; We introduce our theory as a constant so that we can derive +; new instances of it for concrete predicates + +(defconst *positive-functions* '( + +;; We introduce "list versions" of the functions so that we can reason +;; through mergesorts. + + (defun all-list (list-for-all-reduction) + (declare (xargs :guard (true-listp list-for-all-reduction))) + (if (endp list-for-all-reduction) + t + (and (predicate (car list-for-all-reduction)) + (all-list (cdr list-for-all-reduction))))) + + (defun exists-list (x) + (declare (xargs :guard (true-listp x))) + (cond ((endp x) nil) + ((predicate (car x)) t) + (t (exists-list (cdr x))))) + + (defun find-list (x) + (declare (xargs :guard (true-listp x))) + (cond ((endp x) nil) + ((predicate (car x)) (car x)) + (t (find-list (cdr x))))) + + (defun filter-list (x) + (declare (xargs :guard (true-listp x))) + (cond ((endp x) nil) + ((predicate (car x)) + (cons (car x) (filter-list (cdr x)))) + (t (filter-list (cdr x))))) + + +;; We also introduce "set versions" of the functions, so that we can +;; reason about sets. + + (defun all (set-for-all-reduction) + (declare (xargs :guard (setp set-for-all-reduction))) + (if (empty set-for-all-reduction) + t + (and (predicate (head set-for-all-reduction)) + (all (tail set-for-all-reduction))))) + + (defun exists (X) + (declare (xargs :guard (setp X))) + (cond ((empty X) nil) + ((predicate (head X)) t) + (t (exists (tail X))))) + + (defun find (X) + (declare (xargs :guard (setp X))) + (cond ((empty X) nil) + ((predicate (head X)) (head X)) + (t (find (tail X))))) + + (defun filter (X) + (declare (xargs :guard (setp X))) + (declare (xargs :verify-guards nil)) + (cond ((empty X) (sfix X)) + ((predicate (head X)) + (insert (head X) (filter (tail X)))) + (t (filter (tail X))))) + + )) + +; We then create "negative" versions of the above functions by +; performing a set of substitutions on the constants. + +(defconst *negative-functions* + (INSTANCE::instance-defuns *positive-functions* + '(((predicate ?x) (not (predicate ?x))) + ((all ?x) (all<not> ?x)) + ((exists ?x) (exists<not> ?x)) + ((find ?x) (find<not> ?x)) + ((filter ?x) (filter<not> ?x)) + ((all-list ?x) (all-list<not> ?x)) + ((exists-list ?x) (exists-list<not> ?x)) + ((find-list ?x) (find-list<not> ?x)) + ((filter-list ?x) (filter-list<not> ?x))))) + + +; And then we smash together the positive and negative functions to +; create a single function list which can be instantiated later. + +(defconst *functions* + (append *positive-functions* *negative-functions*)) + + +; Now we create the instance-*functions* macro which will allow us +; to actually derive an instance of all of the functions + +(INSTANCE::instance *functions*) + + +; And we call the macro with no arguments, to introduce a verbatim +; copy of the theory. In other words, we introduce the generic +; theory itself here. + +(instance-*functions*) + + +(defconst *positive-theorems* '( + +; List Theory Reasoning +; +; We begin with several theorems about the "list versions" of the +; above functions. + + (defthm all-list-type + (or (equal (all-list x) t) + (equal (all-list x) nil)) + :rule-classes :type-prescription) + + (defthm all-list-cdr + (implies (all-list x) + (all-list (cdr x)))) + + (defthm all-list-endp + (implies (endp x) + (all-list x))) + + (defthm all-list-in + (implies (and (all-list x) + (in-list a x)) + (predicate a))) + + (defthm all-list-in-2 + (implies (and (all-list x) + (not (predicate a))) + (not (in-list a x)))) + + (defthm all-list-cons + (equal (all-list (cons a x)) + (and (predicate a) + (all-list x)))) + + (defthm all-list-append + (equal (all-list (append x y)) + (and (all-list x) + (all-list y)))) + + (defthm all-list-nth + (implies (and (all-list x) + (<= 0 n) + (< n (len x))) + (predicate (nth n x)))) + + (encapsulate nil + + (local (defthm lemma1 + (implies (and (all-list acc) + (all-list x)) + (all-list (revappend x acc))))) + + (local (defthm lemma2 + (implies (not (all-list acc)) + (not (all-list (revappend x acc)))))) + + (local (defthm lemma3 + (implies (and (all-list acc) + (not (all-list x))) + (not (all-list (revappend x acc)))))) + + (defthm all-list-revappend + (equal (all-list (revappend x acc)) + (and (all-list x) + (all-list acc)))) + ) + + (defthm all-list-reverse + (equal (all-list (reverse x)) + (all-list x))) + + (defthm exists-list-elimination + (equal (exists-list x) + (not (all-list<not> x)))) + + (defthm filter-list-true-list + (true-listp (filter-list x)) + :rule-classes :type-prescription) + + (defthm filter-list-membership + (equal (in-list a (filter-list x)) + (and (predicate a) + (in-list a x)))) + + (defthm filter-list-all-list + (all-list (filter-list x))) + + + + + + +; Set Theory Reasoning +; +; Of course, really we are more interested in reasoning about sets +; than lists. We write several theorems about our set functions. + + (defthm all-type + (or (equal (all X) t) + (equal (all X) nil)) + :rule-classes :type-prescription) + + (defthm all-sfix + (equal (all (sfix X)) + (all X))) + + ;; TODO: extend to forward chaining. + + (defthm all-tail + (implies (all X) + (all (tail X)))) + + (defthm all-empty + (implies (empty X) + (all X))) + + (defthm all-in + (implies (and (all X) + (in a X)) + (predicate a))) + + (defthm all-in-2 + (implies (and (all X) + (not (predicate a))) + (not (in a X)))) + + (defthm all-insert + (equal (all (insert a X)) + (and (predicate a) + (all X))) + :hints(("Goal" :induct (insert a X)))) + + (defthm all-delete + (implies (all X) + (all (delete a X)))) + + (defthm all-delete-2 + (implies (predicate a) + (equal (all (delete a X)) + (all X)))) + + (defthm all-union + (equal (all (union X Y)) + (and (all X) + (all Y)))) + + (defthm all-intersect-X + (implies (all X) + (all (intersect X Y)))) + + (defthm all-intersect-Y + (implies (all X) + (all (intersect Y X)))) + + (defthm all-difference + (implies (all X) + (all (difference X Y)))) + + (defthm all-difference-2 + (implies (all Y) + (equal (all (difference X Y)) + (all X)))) + + + (defthm exists-elimination + (equal (exists X) + (not (all<not> X)))) + + + (defthm find-sfix + (equal (find (sfix X)) + (find X))) + + (defthm find-witness + (implies (not (all X)) + (and (in (find<not> X) X) + (not (predicate (find<not> X))))) + :rule-classes :forward-chaining) + + + (defthm filter-set + (setp (filter X))) + + (defthm filter-sfix + (equal (filter (sfix X)) + (filter X))) + + (defthm filter-in + (equal (in a (filter X)) + (and (predicate a) + (in a X))) + :hints(("Goal" :induct (filter X)))) + + (defthm filter-subset + (subset (filter X) X)) + + (defthm filter-all + (all (filter X))) + + (defthm filter-all-2 + (implies (all X) + (equal (filter X) (sfix X))) + :hints(("Goal" :in-theory (disable double-containment)))) + + + + +; In order to reason past a mergesort, we need to provide some +; theorems that tie together our list and set theories. We begin +; this here. + + (defthm all-mergesort + (equal (all (mergesort X)) + (all-list X))) + + (defthm all-list-applied-to-set + (implies (setp X) + (equal (all-list X) + (all X))) + :hints(("Goal" :in-theory (enable setp empty sfix head tail)))) + +)) + + + +; Notice that the positive functions and the negative functions are +; symmetric. We now invert the above theorem to create the +; corresponding theorems for the negative functions. + +(defconst *negative-theorems* + (INSTANCE::instance-rewrite *positive-theorems* + + ;; we first replace calls to "positive" functions with calls to + ;; temporary symbols, which simply acts as placeholders. + + '(((predicate ?x) (predicate-temp ?x)) + ((all ?x) (all-temp ?x)) + ((exists ?x) (exists-temp ?x)) + ((find ?x) (find-temp ?x)) + ((filter ?x) (filter-temp ?x)) + ((all-list ?x) (all-list-temp ?x)) + ((exists-list ?x) (exists-list-temp ?x)) + ((find-list ?x) (find-list-temp ?x)) + ((filter-list ?x) (filter-list-temp ?x)) + + ;; now we replace calls to "negative" functions with calls to + ;; positive functions. + + ((not (predicate ?x)) (predicate ?x)) + ((all<not> ?x) (all ?x)) + ((exists<not> ?x) (exists ?x)) + ((find<not> ?x) (find ?x)) + ((filter<not> ?x) (filter ?x)) + ((all-list<not> ?x) (all-list ?x)) + ((exists-list<not> ?x) (exists-list ?x)) + ((find-list<not> ?x) (find-list ?x)) + ((filter-list<not> ?x) (filter-list ?x)) + + ;; and finally we replace our temporary placeholder symbols with + ;; calls to the actual negative functions. + + ((predicate-temp ?x) (not (predicate ?x))) + ((all-temp ?x) (all<not> ?x)) + ((exists-temp ?x) (exists<not> ?x)) + ((find-temp ?x) (find<not> ?x)) + ((filter-temp ?x) (filter<not> ?x)) + ((all-list-temp ?x) (all-list<not> ?x)) + ((exists-list-temp ?x) (exists-list<not> ?x)) + ((find-list-temp ?x) (find-list<not> ?x)) + ((filter-list-temp ?x) (filter-list<not> ?x)) +))) + + +; We now smash together the positive and negative theorems to form a +; single, complete theory. Note that we have to rename all of the +; defthms in *negative-theorems* so that their names will not collide +; with the theorems in *theorems*. + +(defconst *theorems* + (append *positive-theorems* + (INSTANCE::rename-defthms *negative-theorems* '-not))) + + +; As with the functions, we create a new macro which will allow us to +; derive new instances of our theorems. + +(INSTANCE::instance *theorems*) + + +; And as before, we call the resulting macro with no arguments, which +; gives us a verbatim copy of the positive and negative theorems. + +(instance-*theorems*) + + + + + + + +; We already have an all-by-membership theorem set up for sets. But, +; we would like to have a corresponding theorem to use with lists. We +; create that here. + +(encapsulate + (((all-list-hyps) => *) + ((all-list-list) => *)) + + (local (defun all-list-hyps () nil)) + (local (defun all-list-list () nil)) + + (defthmd list-membership-constraint + (implies (all-list-hyps) + (implies (in-list arbitrary-element (all-list-list)) + (predicate arbitrary-element)))) +) + +(encapsulate () + + (local (defthm witness-lemma + (implies (not (all-list x)) + (and (in-list (find-list<not> x) x) + (not (predicate (find-list<not> x))))))) + + (defthmd all-list-by-membership + (implies (all-list-hyps) + (all-list (all-list-list))) + :hints(("Goal" + :use (:instance list-membership-constraint + (arbitrary-element (find-list<not> (all-list-list))))))) +) + + + +(defconst *final-theorems* '( + + (defthm cardinality-filter + (equal (cardinality X) + (+ (cardinality (filter X)) + (cardinality (filter<not> X)))) + :rule-classes :linear) + + (defthm all-subset + (implies (and (all Y) + (subset X Y)) + (all X)) + :hints(("Goal" + :use (:functional-instance all-by-membership + (all-hyps (lambda () (and (all Y) + (subset X Y)))) + (all-set (lambda () X)))))) + + (defthm all-subset-not + (implies (and (all<not> Y) + (subset X Y)) + (all<not> X)) + :hints(("Goal" + :use (:functional-instance all-by-membership + (all-hyps (lambda () (and (all<not> Y) + (subset X Y)))) + (all-set (lambda () X)) + (predicate (lambda (x) (not (predicate x)))) + (all (lambda (x) (all<not> x))))))) + +)) + +(INSTANCE::instance *final-theorems*) +(instance-*final-theorems*) + +(verify-guards filter) +(verify-guards filter<not>) + + + + +; ------------------------------------------------------------------- +; +; Instancing Concrete Theories +; +; ------------------------------------------------------------------- + +; Each concrete theory we instantiate will require the introduction of +; 16 new functions and a wealth of theorems. We don't want to +; overburden the user with having to instantiate all of these and give +; them names, so we adopt a naming convention where the predicate's +; name is used to generate the names of the new functions. Of course, +; we still have to generate the new names. + +(defun mksym (name sym) + (declare (xargs :mode :program)) + (intern-in-package-of-symbol (string-upcase name) sym)) + +(defun app (x y) + (declare (xargs :mode :program)) + (string-append x y)) + +(defun ?ify (args) + (declare (xargs :mode :program)) + (if (endp args) + nil + (cons (mksym (app "?" (symbol-name (car args))) + (car args)) + (?ify (cdr args))))) + +(defun standardize-to-package (symbol-name replacement term) + (declare (xargs :mode :program)) + (if (atom term) + (if (and (symbolp term) + (equal (symbol-name term) symbol-name)) + replacement + term) + (cons (standardize-to-package symbol-name replacement (car term)) + (standardize-to-package symbol-name replacement (cdr term))))) + + +(defun quantify-simple-predicate (predicate in-package + set-guard list-guard arg-guard) + (declare (xargs :guard (symbolp in-package) + :mode :program)) + (let* ((name (car predicate)) + (args (cons '?x (cddr predicate))) + (wrap (app "<" (app (symbol-name name) ">"))) + (not-wrap (app "<" (app "not-" (app (symbol-name name) ">")))) + + ;; First we build up all the symbols that we will use. + + (all<p> (mksym (app "all" wrap) in-package)) + (exists<p> (mksym (app "exists" wrap) in-package)) + (find<p> (mksym (app "find" wrap) in-package)) + (filter<p> (mksym (app "filter" wrap) in-package)) + (all<not-p> (mksym (app "all" not-wrap) in-package)) + (exists<not-p> (mksym (app "exists" not-wrap) in-package)) + (find<not-p> (mksym (app "find" not-wrap) in-package)) + (filter<not-p> (mksym (app "filter" not-wrap) in-package)) + (all-list<p> (mksym (app "all-list" wrap) in-package)) + (exists-list<p> (mksym (app "exists-list" wrap) in-package)) + (find-list<p> (mksym (app "find-list" wrap) in-package)) + (filter-list<p> (mksym (app "filter-list" wrap) in-package)) + (all-list<not-p> (mksym (app "all-list" not-wrap) in-package)) + (exists-list<not-p> (mksym (app "exists-list" not-wrap) in-package)) + (find-list<not-p> (mksym (app "find-list" not-wrap) in-package)) + (filter-list<not-p> (mksym (app "filter-list" not-wrap) in-package)) + + ;; And we create a substitution list, to instantiate the + ;; generic theory/functions with their new, concrete values. + + (subs `(((predicate ?x) (,name ,@args)) + ((all ?x) (,all<p> ,@args)) + ((exists ?x) (,exists<p> ,@args)) + ((find ?x) (,find<p> ,@args)) + ((filter ?x) (,filter<p> ,@args)) + ((all<not> ?x) (,all<not-p> ,@args)) + ((exists<not> ?x) (,exists<not-p> ,@args)) + ((find<not> ?x) (,find<not-p> ,@args)) + ((filter<not> ?x) (,filter<not-p> ,@args)) + ((all-list ?x) (,all-list<p> ,@args)) + ((exists-list ?x) (,exists-list<p> ,@args)) + ((find-list ?x) (,find-list<p> ,@args)) + ((filter-list ?x) (,filter-list<p> ,@args)) + ((all-list<not> ?x) (,all-list<not-p> ,@args)) + ((exists-list<not> ?x) (,exists-list<not-p> ,@args)) + ((find-list<not> ?x) (,find-list<not-p> ,@args)) + ((filter-list<not> ?x) (,filter-list<not-p> ,@args)))) + + ;; We use this hack to support alternate guards. We + ;; basically use our rewriter to inject the extra guards into + ;; the function's existing guards. + + (fn-subs + (list* `((declare (xargs :guard (true-listp ?list))) + (declare (xargs :guard (and (true-listp ?list) + ,@list-guard + ,@arg-guard)))) + `((declare (xargs :guard (setp ?set))) + (declare (xargs :guard (and (setp ?set) + ,@set-guard + ,@arg-guard)))) + subs)) + + + ;; And we make some symbols for use in automating the all-by-membership + ;; strategy with computed hints. + + (all-trigger<p> (mksym (app "all-trigger" wrap) in-package)) + (all-trigger<not-p> (mksym (app "all-trigger" not-wrap) in-package)) + (all-strategy<p> (mksym (app "all-strategy" wrap) in-package)) + (all-strategy<not-p> (mksym (app "all-strategy" not-wrap) in-package)) + (all-list-trigger<p> (mksym (app "all-list-trigger" wrap) in-package)) + (all-list-trigger<not-p> (mksym (app "all-list-trigger" not-wrap) in-package)) + (all-list-strategy<p> (mksym (app "all-list-strategy" wrap) in-package)) + (all-list-strategy<not-p> (mksym (app "all-list-strategy" not-wrap) in-package)) + + ;; We finally make a deftheory event with the following name, which + ;; holds all of these theorems: + + (theory<p> (mksym (app "theory" wrap) in-package)) + (suffix (mksym wrap in-package)) + (thm-names (append (INSTANCE::defthm-names *theorems*) + (INSTANCE::defthm-names *final-theorems*))) + (thm-name-map (INSTANCE::create-new-names thm-names suffix)) + (theory<p>-defthms (sublis thm-name-map thm-names)) + + ) + + `(encapsulate () + + ;; It's now quite easy to instantiate all of our functions. + + (instance-*functions* + :subs ,fn-subs + :suffix ,name) + + ;; And similarly we can instantiate all of the theorems. + + (instance-*theorems* + :subs ,subs + :suffix ,(mksym wrap in-package)) + ;:extra-defs (empty)) + + + ;; Automating the computed hints is a pain in the ass. We + ;; first need triggers as aliases for all<p>, all<not-p>, etc. + + (defund ,all-trigger<p> (,@args) + (declare (xargs :verify-guards nil)) + (,all<p> ,@args)) + + (defund ,all-trigger<not-p> (,@args) + (declare (xargs :verify-guards nil)) + (,all<not-p> ,@args)) + + (defund ,all-list-trigger<p> (,@args) + (declare (xargs :verify-guards nil)) + (,all-list<p> ,@args)) + + (defund ,all-list-trigger<not-p> (,@args) + (declare (xargs :verify-guards nil)) + (,all-list<not-p> ,@args)) + + + ;; Now we need "tagging theorems" that instruct the rewriter + ;; to tag the appropriate terms. + + (defthm ,all-strategy<p> + (implies (and (syntaxp (rewriting-goal-lit mfc state)) + (syntaxp (rewriting-conc-lit (list ',all<p> ,@args) + mfc state))) + (equal (,all<p> ,@args) + (,all-trigger<p> ,@args))) + :hints(("Goal" + :in-theory (union-theories + (theory 'minimal-theory) + '((:definition ,all-trigger<p>)))))) + + (defthm ,all-strategy<not-p> + (implies (and (syntaxp (rewriting-goal-lit mfc state)) + (syntaxp (rewriting-conc-lit (list ',all<not-p> ,@args) + mfc state))) + (equal (,all<not-p> ,@args) + (,all-trigger<not-p> ,@args))) + :hints(("Goal" + :in-theory (union-theories + (theory 'minimal-theory) + '((:definition ,all-trigger<not-p>)))))) + + (defthm ,all-list-strategy<p> + (implies (and (syntaxp (rewriting-goal-lit mfc state)) + (syntaxp (rewriting-conc-lit (list ',all-list<p> ,@args) + mfc state))) + (equal (,all-list<p> ,@args) + (,all-list-trigger<p> ,@args))) + :hints(("Goal" + :in-theory (union-theories + (theory 'minimal-theory) + '((:definition ,all-list-trigger<p>)))))) + + (defthm ,all-list-strategy<not-p> + (implies (and (syntaxp (rewriting-goal-lit mfc state)) + (syntaxp (rewriting-conc-lit (list ',all-list<not-p> ,@args) + mfc state))) + (equal (,all-list<not-p> ,@args) + (,all-list-trigger<not-p> ,@args))) + :hints(("Goal" + :in-theory (union-theories + (theory 'minimal-theory) + '((:definition ,all-list-trigger<not-p>)))))) + + + ;; And then we call upon our computed hints routines to generate a + ;; computed hint for us to use, and add it to the default hints. + + (COMPUTED-HINTS::automate-instantiation + :new-hint-name ,(mksym (app "all-by-membership-hint" wrap) in-package) + :generic-theorem all-by-membership + :generic-predicate predicate + :generic-hyps all-hyps + :generic-collection all-set + :generic-collection-predicate all + :actual-collection-predicate ,all<p> + :actual-trigger ,all-trigger<p> + :predicate-rewrite (((predicate ,@(?ify args)) + (,name ,@(?ify args)))) + :tagging-theorem ,all-strategy<p> + ) + + (COMPUTED-HINTS::automate-instantiation + :new-hint-name ,(mksym (app "all-by-membership-hint" not-wrap) in-package) + :generic-theorem all-by-membership + :generic-predicate predicate + :generic-hyps all-hyps + :generic-collection all-set + :generic-collection-predicate all + :actual-collection-predicate ,all<not-p> + :actual-trigger ,all-trigger<not-p> + :predicate-rewrite (((predicate ,@(?ify args)) + (not (,name ,@(?ify args))))) + :tagging-theorem ,all-strategy<not-p> + ) + + (COMPUTED-HINTS::automate-instantiation + :new-hint-name ,(mksym (app "all-list-by-membership-hint" wrap) in-package) + :generic-theorem all-list-by-membership + :generic-predicate predicate + :generic-hyps all-list-hyps + :generic-collection all-list-list + :generic-collection-predicate all-list + :actual-collection-predicate ,all-list<p> + :actual-trigger ,all-list-trigger<p> + :predicate-rewrite (((predicate ,@(?ify args)) + (,name ,@(?ify args)))) + :tagging-theorem ,all-list-strategy<p> + ) + + (COMPUTED-HINTS::automate-instantiation + :new-hint-name ,(mksym (app "all-list-by-membership-hint" not-wrap) in-package) + :generic-theorem all-list-by-membership + :generic-predicate predicate + :generic-hyps all-list-hyps + :generic-collection all-list-list + :generic-collection-predicate all-list + :actual-collection-predicate ,all-list<not-p> + :actual-trigger ,all-list-trigger<not-p> + :predicate-rewrite (((predicate ,@(?ify args)) + (not (,name ,@(?ify args))))) + :tagging-theorem ,all-list-strategy<not-p> + ) + + + (instance-*final-theorems* + :subs ,subs + :suffix ,(mksym wrap in-package)) + ;:extra-defs (empty)) + + + (verify-guards ,filter<p>) + (verify-guards ,filter<not-p>) + + ;; In the end, we want to create a deftheory event so that you can + ;; easily turn off the reasoning about these functions when you + ;; don't need it. We do that with the following event: + + (deftheory ,theory<p> '(,@theory<p>-defthms + ,all<p> ,all-list<p> + ,exists<p> ,exists-list<p> + ,find<p> ,find-list<p> + ,filter<p> ,filter-list<p> + ,all<not-p> ,all-list<not-p> + ,exists<not-p> ,exists-list<not-p> + ,find<not-p> ,find-list<not-p> + ,filter<not-p> ,filter-list<not-p> + ,all-trigger<p> ,all-list-trigger<p> + ,all-trigger<not-p> ,all-list-trigger<not-p> + ,all-strategy<p> ,all-list-strategy<p> + ,all-strategy<not-p> ,all-list-strategy<not-p> + )) + ))) + + +(defmacro quantify-predicate (predicate + &key in-package-of + set-guard list-guard arg-guard) + (quantify-simple-predicate predicate + (if in-package-of in-package-of 'in) + (standardize-to-package "?SET" '?set set-guard) + (standardize-to-package "?LIST" '?list list-guard) + arg-guard)) + + + +; We don't want to keep all these generic theorems around, because +; many of them are rewrite rules with targets that are actual +; functions. For example, if a rule concludes with (in a X), we don't +; want to start backchaining on it if its hypothese include generic +; rules. + +(deftheory generic-quantification-theory + `(,@(INSTANCE::defthm-names *theorems*) + ,@(INSTANCE::defthm-names *final-theorems*) + all exists find filter + all-list exists-list find-list filter-list + all<not> exists<not> find<not> filter<not> + all-list<not> exists-list<not> find-list<not> filter-list<not>)) + +(in-theory (disable generic-quantification-theory)) diff --git a/books/workshops/2004/davis/support/set-order.lisp b/books/workshops/2004/davis/support/set-order.lisp new file mode 100644 index 0000000..aecb922 --- /dev/null +++ b/books/workshops/2004/davis/support/set-order.lisp @@ -0,0 +1,175 @@ +; Fully Ordered Finite Sets, Version 0.81 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; set-order.lisp +; +; This is a top level file which you should use if you intend to +; reason about the set order. Normally you should not do this, +; but you might need it if you want to argue "from first principles" +; that list operations create sets, i.e. for efficiency reasons. +; +; Note that merely including this file will do nothing for you. +; You need to also enable the relavent theories: +; +; primitive-reasoning +; basic definitions of the primitive functions. useful if you +; have a very low level proof about the stucture of sets or +; something. doesn't pertain to the order itself. +; +; order-reasoning +; properties of the order itself, and its relation to the set +; primitives. most of the membership level is based on this. +; +; cons-reasoning +; properties relating cons to sets through the set order. +; this might be useful if you are introducing new "fast" +; functions, based on cons rather than insert to construct +; sets. it is not easy to reason with. + +(in-package "SET") +(set-verify-guards-eagerness 2) + +(local (include-book "primitives")) +(local (include-book "membership")) +(local (include-book "fast")) +(include-book "sets") + + +; ------------------------------------------------------------------- +; primitive-reasoning + +(deftheory primitive-reasoning + '(setp + empty + head + tail + sfix + insert)) + + + +; ------------------------------------------------------------------- +; order-reasoning + +(defthmd <<-type + (or (equal (<< a b) t) + (equal (<< a b) nil)) + :rule-classes :type-prescription) + +(defthmd <<-irreflexive + (not (<< a a))) + +(defthmd <<-transitive + (implies (and (<< a b) (<< b c)) + (<< a c))) + +(defthmd <<-asymmetric + (implies (<< a b) + (not (<< b a)))) + +(defthmd <<-trichotomy + (implies (and (not (<< b a)) + (not (equal a b))) + (<< a b))) + +(defthmd head-insert + (equal (head (insert a X)) + (cond ((empty X) a) + ((<< a (head X)) a) + (t (head X))))) + +(defthmd tail-insert + (equal (tail (insert a X)) + (cond ((empty X) (sfix X)) + ((<< a (head X)) (sfix X)) + ((equal a (head X)) (tail X)) + (t (insert a (tail X)))))) + +(defthmd head-tail-order + (implies (not (empty (tail X))) + (<< (head X) (head (tail X))))) + +(defthmd head-tail-order-contrapositive + (implies (not (<< (head X) (head (tail X)))) + (empty (tail X)))) + +(deftheory order-reasoning + '(<<-type + <<-irreflexive + <<-transitive + <<-asymmetric + <<-trichotomy + (:induction insert) + head-insert + tail-insert + head-tail-order + head-tail-order-contrapositive)) + + + + +; ------------------------------------------------------------------- +; cons-reasoning + +(defthmd cons-set + (equal (setp (cons a X)) + (and (setp X) + (or (<< a (head X)) + (empty X))))) + +(defthmd cons-head + (implies (setp (cons a X)) + (equal (head (cons a X)) a))) + +(defthmd cons-to-insert-empty + (implies (and (setp X) + (empty X)) + (equal (cons a X) (insert a X)))) + +(defthmd cons-to-insert-nonempty + (implies (and (setp X) + (<< a (head X))) + (equal (cons a X) (insert a X)))) + +(defthmd cons-in + (implies (and (setp (cons a X)) + (setp X)) + (equal (in b (cons a X)) + (or (equal a b) + (in b X))))) + +(deftheory cons-reasoning + '(cons-set + cons-head + cons-to-insert-empty + cons-to-insert-nonempty + cons-in)) diff --git a/books/workshops/2004/davis/support/sets.lisp b/books/workshops/2004/davis/support/sets.lisp new file mode 100644 index 0000000..a94f052 --- /dev/null +++ b/books/workshops/2004/davis/support/sets.lisp @@ -0,0 +1,884 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; +; sets.lisp +; +; This is the top level file, which you should include to use the ordered set +; theory library. + +(in-package "SET") +(set-verify-guards-eagerness 2) + + +; We need some program-mode definitions which are used in order to +; automate the pick-a-point strategies. + +(include-book "computed-hints") + + +; The definitions in this file are redundant from the local include +; books. This approach has several advantages. +; +; - it gives a better event order than simply including the books +; one by one +; +; - this file is also faster to include than all of the local books +; below, and allows the "ugliness" of auxilliary lemmas to be +; hidden away +; +; - it makes clear that these theorems are public, and entirely +; prevents the use of "internal" lemmas and theorems. + +(local (include-book "primitives")) +(local (include-book "membership")) +(local (include-book "fast")) +(local (include-book "outer")) +(local (include-book "sort")) + + +; We begin with the definitions of the set theory functions and a +; few trivial type prescriptions. + +(defund << (a b) + (declare (xargs :guard t)) + (and (lexorder a b) + (not (equal a b)))) + +(defund setp (X) + (declare (xargs :guard t)) + (if (atom X) + (null X) + (or (null (cdr X)) + (and (consp (cdr X)) + (<< (car X) (cadr X)) + (setp (cdr X)))))) + +(defthm setp-type + (or (equal (setp X) t) + (equal (setp X) nil)) + :rule-classes :type-prescription) + +(defund empty (X) + (declare (xargs :guard (setp X))) + (mbe :logic (or (null X) + (not (setp X))) + :exec (null X))) + +(defthm empty-type + (or (equal (empty X) t) + (equal (empty X) nil)) + :rule-classes :type-prescription) + +(defund sfix (X) + (declare (xargs :guard (setp X))) + (mbe :logic (if (empty X) nil X) + :exec X)) + +(defund head (X) + (declare (xargs :guard (and (setp X) + (not (empty X))))) + (mbe :logic (car (sfix X)) + :exec (car X))) + +(defund tail (X) + (declare (xargs :guard (and (setp X) + (not (empty X))))) + (mbe :logic (cdr (sfix X)) + :exec (cdr X))) + +(defund insert (a X) + (declare (xargs :guard (setp X))) + (cond ((empty X) (list a)) + ((equal (head X) a) X) + ((<< a (head X)) (cons a X)) + (t (cons (head X) (insert a (tail X)))))) + +(defun in (a X) + (declare (xargs :guard (setp X))) + (and (not (empty X)) + (or (equal a (head X)) + (in a (tail X))))) + +(defthm in-type + (or (equal (in a X) t) + (equal (in a X) nil)) + :rule-classes :type-prescription) + +(defund fast-subset (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (cond ((empty X) t) + ((empty Y) nil) + ((<< (head X) (head Y)) nil) + ((equal (head X) (head Y)) (fast-subset (tail X) (tail Y))) + (t (fast-subset X (tail Y))))) + +(defund subset (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (mbe :logic (if (empty X) + t + (and (in (head X) Y) + (subset (tail X) Y))) + :exec (fast-subset X Y))) + +(defthm subset-type + (or (equal (subset X Y) t) + (equal (subset X Y) nil)) + :rule-classes :type-prescription) + +(defund fast-measure (X Y) + (+ (acl2-count X) (acl2-count Y))) + +(defund fast-union (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 (tail X) (tail Y)))) + ((<< (head X) (head Y)) + (cons (head X) (fast-union (tail X) Y))) + (t (cons (head Y) (fast-union X (tail Y)))))) + +(defund fast-intersect (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 (tail X) (tail Y)))) + ((<< (head X) (head Y)) + (fast-intersect (tail X) Y)) + (t (fast-intersect X (tail Y))))) + +(defund fast-difference (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 (tail X) (tail Y))) + ((<< (head X) (head Y)) + (cons (head X) (fast-difference (tail X) Y))) + (t (fast-difference X (tail Y))))) + +(defun delete (a X) + (declare (xargs :guard (setp X))) + (cond ((empty X) nil) + ((equal a (head X)) (tail X)) + (t (insert (head X) (delete a (tail X)))))) + +(defun union (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (mbe :logic (if (empty X) + (sfix Y) + (insert (head X) (union (tail X) Y))) + :exec (fast-union X Y))) + +(defun intersect (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (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))) + +(defun difference (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (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))) + +(defun cardinality (X) + (declare (xargs :guard (setp X))) + (mbe :logic (if (empty X) + 0 + (1+ (cardinality (tail X)))) + :exec (len X))) + +(defund split-list (x) + (declare (xargs :guard (true-listp x))) + (cond ((endp x) (mv nil nil)) + ((endp (cdr x)) (mv (list (car x)) nil)) + (t (mv-let (part1 part2) + (split-list (cddr x)) + (mv (cons (car x) part1) + (cons (cadr x) part2)))))) + +(defun in-list (a x) + (declare (xargs :guard (true-listp x))) + (if (endp x) + nil + (or (equal a (car x)) + (in-list a (cdr x))))) + +(defun mergesort-exec (x) + (declare (xargs :guard (true-listp x) + :measure (:? x))) + (cond ((endp x) nil) + ((endp (cdr x)) (insert (car x) nil)) + (t (mv-let (part1 part2) + (split-list x) + (union (mergesort-exec part1) (mergesort-exec part2)))))) + +(defun mergesort (x) + (declare (xargs :guard (true-listp x))) + (mbe :logic (if (endp x) + nil + (insert (car x) + (mergesort (cdr x)))) + :exec (mergesort-exec x))) + + + +; "High Powered" Strategies +; +; We put these at the beginning of the file so that they are tried +; as a last resort when simple methods have failed. + +(encapsulate + (((predicate *) => *)) + (local (defun predicate (x) x))) + +(defun all (set-for-all-reduction) + (declare (xargs :guard (setp set-for-all-reduction))) + (if (empty set-for-all-reduction) + t + (and (predicate (head set-for-all-reduction)) + (all (tail set-for-all-reduction))))) + +(encapsulate + (((all-hyps) => *) + ((all-set) => *)) + + (local (defun all-hyps () nil)) + (local (defun all-set () nil)) + + (defthmd membership-constraint + (implies (all-hyps) + (implies (in arbitrary-element (all-set)) + (predicate arbitrary-element)))) +) + +(defthmd all-by-membership + (implies (all-hyps) + (all (all-set)))) + +(defund subset-trigger (X Y) + (declare (xargs :guard (and (setp X) (setp Y)))) + (subset X Y)) + +(defthm pick-a-point-subset-strategy + (implies (and (syntaxp (rewriting-goal-lit mfc state)) + (syntaxp (rewriting-conc-lit `(subset ,X ,Y) mfc state))) + (equal (subset X Y) + (subset-trigger X Y)))) + +(COMPUTED-HINTS::automate-instantiation + :new-hint-name pick-a-point-subset-hint + :generic-theorem all-by-membership + :generic-predicate predicate + :generic-hyps all-hyps + :generic-collection all-set + :generic-collection-predicate all + :actual-collection-predicate subset + :actual-trigger subset-trigger + :predicate-rewrite (((predicate ?x ?y) (in ?x ?y))) + :tagging-theorem pick-a-point-subset-strategy +) + +(defthm double-containment + (implies (and (setp X) + (setp Y)) + (equal (equal X Y) + (and (subset X Y) + (subset Y X))))) + + + +; ------------------------------------------------------------------- +; Primitives Level Theorems + +(defthm sets-are-true-lists + (implies (setp X) + (true-listp X))) + +(defthm tail-count + (implies (not (empty X)) + (< (acl2-count (tail X)) (acl2-count X))) + :rule-classes :linear) + +(defthm head-count + (implies (not (empty X)) + (< (acl2-count (head X)) (acl2-count X))) + :rule-classes :linear) + +(defthm insert-insert + (equal (insert a (insert b X)) + (insert b (insert a X))) + :rule-classes ((:rewrite :loop-stopper ((a b))))) + +(defthm sfix-produces-set + (setp (sfix X))) + +(defthm tail-produces-set + (setp (tail X))) + +(defthm insert-produces-set + (setp (insert a X))) + +(defthm insert-never-empty + (not (empty (insert a X)))) + +(defthm tail-preserves-empty + (implies (empty X) + (empty (tail X)))) + +(defthm nonempty-means-set + (implies (not (empty X)) (setp X))) + +(defthm sfix-set-identity + (implies (setp X) (equal (sfix X) X))) + +(defthm empty-sfix-cancel + (equal (empty (sfix X)) (empty X))) + +(defthm head-sfix-cancel + (equal (head (sfix X)) (head X))) + +(defthm tail-sfix-cancel + (equal (tail (sfix X)) (tail X))) + +(defthm insert-head-tail + (implies (not (empty X)) + (equal (insert (head X) (tail X)) X))) + +(defthm repeated-insert + (equal (insert a (insert a X)) + (insert a X))) + +(defthm insert-sfix-cancel + (equal (insert a (sfix X)) (insert a X))) + +(defthm head-insert-empty + (implies (empty X) + (equal (head (insert a X)) a))) + +(defthm tail-insert-empty + (implies (empty X) + (empty (tail (insert a X))))) + + + + +; ------------------------------------------------------------------- +; Membership Level Theorems + +(defthm not-in-self + (not (in x x))) + +(defthm in-sfix-cancel + (equal (in a (sfix X)) (in a X))) + +(defthm never-in-empty + (implies (empty X) (not (in a X)))) + +(defthm in-set + (implies (in a X) (setp X))) + +(defthm in-tail + (implies (in a (tail X)) (in a X))) + +(defthm in-tail-or-head + (implies (and (in a X) (not (in a (tail X)))) + (equal (head X) a))) + +(defthm head-unique + (not (in (head X) (tail X)))) + +(defthm insert-identity + (implies (in a X) (equal (insert a X) X))) + +(defthm in-insert + (equal (in a (insert b X)) + (or (in a X) + (equal a b)))) + +(defthm subset-transitive + (implies (and (subset X Y) (subset Y Z)) + (subset X Z))) + +(defthm subset-insert-X + (equal (subset (insert a X) Y) + (and (subset X Y) + (in a Y)))) + +(defthm subset-sfix-cancel-X + (equal (subset (sfix X) Y) (subset X Y))) + +(defthm subset-sfix-cancel-Y + (equal (subset X (sfix Y)) (subset X Y))) + +(defthm subset-in + (implies (and (subset X Y) (in a X)) + (in a Y))) + +(defthm subset-in-2 + (implies (and (subset X Y) (not (in a Y))) + (not (in a X)))) + +(defthm empty-subset + (implies (empty X) (subset X Y))) + +(defthm empty-subset-2 + (implies (empty Y) + (equal (subset X Y) (empty X)))) + +(defthm subset-reflexive + (subset X X)) + +(defthm subset-insert + (subset X (insert a X))) + +(defthm subset-tail + (subset (tail X) X) + :rule-classes ((:rewrite) + (:forward-chaining :trigger-terms ((tail x))))) + + + +; ------------------------------------------------------------------- +; Weakly Inducting over Insertions + +(defthm weak-insert-induction-helper-1 + (implies (and (not (in a X)) + (not (equal (head (insert a X)) a))) + (equal (head (insert a X)) (head X)))) + +(defthm weak-insert-induction-helper-2 + (implies (and (not (in a X)) + (not (equal (head (insert a X)) a))) + (equal (tail (insert a X)) (insert a (tail X))))) + +(defthm weak-insert-induction-helper-3 + (implies (and (not (in a X)) + (equal (head (insert a X)) a)) + (equal (tail (insert a X)) (sfix X)))) + +(defun weak-insert-induction (a X) + (declare (xargs :guard (setp X))) + (cond ((empty X) nil) + ((in a X) nil) + ((equal (head (insert a X)) a) nil) + (t (list (weak-insert-induction a (tail X)))))) + +(defthm use-weak-insert-induction t + :rule-classes ((:induction + :pattern (insert a X) + :scheme (weak-insert-induction a X)))) + + + + +; ------------------------------------------------------------------- +; Outer Level Theorems + +(defthm delete-delete + (equal (delete a (delete b X)) + (delete b (delete a X))) + :rule-classes ((:rewrite :loop-stopper ((a b))))) + +(defthm delete-set + (setp (delete a X))) + +(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 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)) + + + +(defthm union-symmetric + (equal (union X Y) (union Y X)) + :rule-classes ((:rewrite :loop-stopper ((X Y))))) + +(defthm union-commutative + (equal (union X (union Y Z)) + (union Y (union X Z))) + :rule-classes ((:rewrite :loop-stopper ((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-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)))) + +(defthm union-subset-X + (subset X (union X Y))) + +(defthm union-subset-Y + (subset Y (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-outer-cancel + (equal (union X (union X Z)) + (union X Z))) + + + +(defthm intersect-symmetric + (equal (intersect X Y) (intersect Y X)) + :rule-classes ((:rewrite :loop-stopper ((X 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-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)))) + +(defthm intersect-in + (equal (in a (intersect X Y)) + (and (in a Y) (in a X)))) + +(defthm intersect-subset-X + (subset (intersect X Y) X)) + +(defthm intersect-subset-Y + (subset (intersect X Y) Y)) + +(defthm intersect-self + (equal (intersect X X) (sfix X))) + +(defthm intersect-associative + (equal (intersect (intersect X Y) Z) + (intersect X (intersect Y Z)))) + +(defthmd 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))) + + + +(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)))) + +(defthm difference-in + (equal (in a (difference X Y)) + (and (in a X) + (not (in a Y))))) + +(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)))) + + +(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))) + +(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)))) + +(defthm subset-cardinality + (implies (subset X Y) + (<= (cardinality X) (cardinality 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))) + +(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) + +(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)))) + + + +; ------------------------------------------------------------------- +; Mergesort Theorems + +(defthm in-list-cons + (equal (in-list a (cons b x)) + (or (equal a b) + (in-list a x)))) + +(defthm in-list-append + (equal (in-list a (append x y)) + (or (in-list a x) + (in-list a y)))) + +(defthm in-list-revappend + (equal (in-list a (revappend x y)) + (or (in-list a x) + (in-list a y)))) + +(defthm in-list-reverse + (equal (in-list a (reverse x)) + (in-list a x))) + +(defthm in-list-on-set + (implies (setp X) + (equal (in-list a X) + (in a X)))) + +(defthm mergesort-set + (setp (mergesort x))) + +(defthm in-mergesort + (equal (in a (mergesort x)) + (in-list a x))) + +(defthm mergesort-set-identity + (implies (setp X) + (equal (mergesort X) X))) + + diff --git a/books/workshops/2004/davis/support/sort.lisp b/books/workshops/2004/davis/support/sort.lisp new file mode 100644 index 0000000..fd537d5 --- /dev/null +++ b/books/workshops/2004/davis/support/sort.lisp @@ -0,0 +1,221 @@ +; Fully Ordered Finite Sets, Version 0.9 +; Copyright (C) 2003, 2004 Kookamara LLC +; +; Contact: +; +; Kookamara LLC +; 11410 Windermere Meadows +; Austin, TX 78759, USA +; http://www.kookamara.com/ +; +; License: (An MIT/X11-style license) +; +; Permission is hereby granted, free of charge, to any person obtaining a +; copy of this software and associated documentation files (the "Software"), +; to deal in the Software without restriction, including without limitation +; the rights to use, copy, modify, merge, publish, distribute, sublicense, +; and/or sell copies of the Software, and to permit persons to whom the +; Software is furnished to do so, subject to the following conditions: +; +; The above copyright notice and this permission notice shall be included in +; all copies or substantial portions of the Software. +; +; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER +; DEALINGS IN THE SOFTWARE. +; +; Original author: Jared Davis <jared@kookamara.com> +; +; sort.lisp +; +; We implement a mergesort which can convert lists into sets more efficiencly +; than repeated insertion. Logically, (mergesort x) is exactly the same as +; repeated insertion, so it is fairly easy to reason about. But, under the +; hood, mergesort is implemented fairly efficiently using MBE. +; +; The sort we implement is probably not "blisteringly fast". Most of the +; literature on the subject suggests using a bubblesort when we get down to +; some threshold, say 40 elements. I'm not going to bother with any of that. +; If you find that the mergesort's perfor- mance is inadequate, which is +; unlikely, you can work on making it faster. +; +; There are a few points of interest. If you look at the actual sort code +; (mergesort-exec), you will see that it is actually using the set library's +; own union function to perform the union. This is pretty slick because union +; is linear complexity, and yet is easy to reason about since we have already +; got a lot of theory in place about it. +; +; In any case, our strategy for proving the equality of this merge- sort with a +; simple insert-sort is the exact same trick we use everywhere else in the sets +; library. We begin by showing that both produce sets, and then show that +; membership in either is true exactly when an element is member-equal in the +; original list. + +(in-package "SET") +(include-book "outer") +(set-verify-guards-eagerness 2) + + + +; A List Membership Function +; +; The current member-equal function has weird semantics, returning a +; list rather than a boolean value. We provide a convenient +; alternative which always returns t or nil instead. +; +; We don't try to develop a complete theory for this function here, +; but we will provide several useful utility theorems for relating in +; with the common list functions such as cons, append, and reverse. +; In the future we might want to expand this section to include more +; theorems. + +(defun in-list (a x) + (declare (xargs :guard (true-listp x))) + (if (endp x) + nil + (or (equal a (car x)) + (in-list a (cdr x))))) + +(defthm in-list-cons + (equal (in-list a (cons b x)) + (or (equal a b) + (in-list a x)))) + +(defthm in-list-append + (equal (in-list a (append x y)) + (or (in-list a x) + (in-list a y)))) + +(encapsulate nil + + (local (defthm lemma + (implies (in-list a acc) + (in-list a (revappend x acc))))) + + (defthm in-list-revappend + (equal (in-list a (revappend x y)) + (or (in-list a x) + (in-list a y)))) +) + +(defthm in-list-reverse + (equal (in-list a (reverse x)) + (in-list a x))) + +(defthm in-list-on-set + (implies (setp X) + (equal (in-list a X) + (in a X))) + :hints(("Goal" :in-theory (enable sfix head tail empty setp)))) + +; We now introduce a naive function to split a list into two. + +(defun split-list (x) + (declare (xargs :guard (true-listp x))) + (cond ((endp x) (mv nil nil)) + ((endp (cdr x)) (mv (list (car x)) nil)) + (t (mv-let (part1 part2) + (split-list (cddr x)) + (mv (cons (car x) part1) + (cons (cadr x) part2)))))) + +(local (defthm split-list-membership + (equal (in-list a x) + (or (in-list a (mv-nth 0 (split-list x))) + (in-list a (mv-nth 1 (split-list x))))))) + +(local (defthm split-list-part1-truelist + (true-listp (mv-nth 0 (split-list x))) + :rule-classes :type-prescription)) + +(local (defthm split-list-part2-truelist + (true-listp (mv-nth 1 (split-list x))) + :rule-classes :type-prescription)) + +(local (defthm split-list-length-part1 + (implies (consp (cdr x)) + (equal (len (mv-nth 0 (split-list x))) + (+ 1 (len (mv-nth 0 (split-list (cddr x))))))))) + +(local (defthm split-list-length-part2 + (implies (consp (cdr x)) + (equal (len (mv-nth 1 (split-list x))) + (+ 1 (len (mv-nth 1 (split-list (cddr x))))))))) + +(local (defthm split-list-length-less-part1 + (implies (consp (cdr x)) + (< (len (mv-nth 0 (split-list x))) + (len x))))) + +(local (defthm split-list-length-less-part2 + (implies (consp (cdr x)) + (< (len (mv-nth 1 (split-list x))) + (len x))))) + +(local (in-theory (disable split-list-length-part1 + split-list-length-part2))) + +(defun mergesort-exec (x) + (declare (xargs + :guard (true-listp x) + :measure (len x) + :hints(("Goal" :use ((:instance split-list-length-less-part1) + (:instance split-list-length-less-part2)))) + :verify-guards nil)) + (cond ((endp x) nil) + ((endp (cdr x)) (insert (car x) nil)) + (t (mv-let (part1 part2) + (split-list x) + (union (mergesort-exec part1) (mergesort-exec part2)))))) + +(local (defthm mergesort-exec-set + (setp (mergesort-exec x)))) + +(local (in-theory (disable split-list-membership))) + +(local (defthm mergesort-membership-2 + (implies (in-list a x) + (in a (mergesort-exec x))) + :hints(("Subgoal *1/3" :use (:instance split-list-membership))))) + +(local (defthm mergesort-membership-1 + (implies (in a (mergesort-exec x)) + (in-list a x)) + :hints(("Subgoal *1/6" :use (:instance split-list-membership)) + ("Subgoal *1/5" :use (:instance split-list-membership)) + ("Subgoal *1/4" :use (:instance split-list-membership))))) + +(local (defthm mergesort-membership + (iff (in a (mergesort-exec x)) + (in-list a x)))) + +(verify-guards mergesort-exec + :hints(("Goal" :in-theory (disable mv-nth)))) + + +(defun mergesort (x) + (declare (xargs :guard (true-listp x) + :verify-guards nil)) + (mbe :logic (if (endp x) + nil + (insert (car x) + (mergesort (cdr x)))) + :exec (mergesort-exec x))) + +(defthm mergesort-set + (setp (mergesort x))) + +(defthm in-mergesort + (equal (in a (mergesort x)) + (in-list a x))) + +(verify-guards mergesort) + +(defthm mergesort-set-identity + (implies (setp X) + (equal (mergesort X) X)) + :hints(("Goal" :in-theory (enable setp sfix head tail empty)))) diff --git a/books/workshops/2004/davis/workshop-osets-slides.pdf.gz b/books/workshops/2004/davis/workshop-osets-slides.pdf.gz Binary files differnew file mode 100644 index 0000000..3d2a415 --- /dev/null +++ b/books/workshops/2004/davis/workshop-osets-slides.pdf.gz |