diff options
author | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
---|---|---|
committer | Camm Maguire <camm@debian.org> | 2017-05-08 12:58:52 -0400 |
commit | 092176848cbfd27b96c323cc30c54dff4c4a6872 (patch) | |
tree | 91b91b4db76805fd2a09de0745b22080a9ebd335 /books/workshops/2002/manolios-kaufmann/support |
Import acl2_7.4dfsg.orig.tar.gz
[dgit import orig acl2_7.4dfsg.orig.tar.gz]
Diffstat (limited to 'books/workshops/2002/manolios-kaufmann/support')
27 files changed, 8760 insertions, 0 deletions
diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp new file mode 100644 index 0000000..bca7312 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-original.lsp @@ -0,0 +1,27 @@ +(lp) +(in-package "ACL2") + +(certify-book "total-ordering-original" 0) +:u + +(defpkg "S" + (set-difference-equal + (union-eq '(PACK + ORDINARYP + << + <<-IRREFLEXIVITY + <<-TRICHOTOMY + <<-MUTUAL-EXCLUSION + <<-TRANSITIVITY + FAST-<<-TRICHOTOMY + FAST-<<-MUTUAL-EXCLUSION + FAST-<<-TRANSITIVITY + FAST-<<-RULES + SLOW-<<-RULES + <<-RULES) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(union intersection subsetp add-to-set functionp = apply))) + +(certify-book "set-theory-original" 1) +:u :u diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp new file mode 100644 index 0000000..41a77ce --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord-original.lsp @@ -0,0 +1,5 @@ +(lp) +(in-package "ACL2") + +(certify-book "total-ordering-original" 0) +:u diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp new file mode 100644 index 0000000..8386126 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify-total-ord.lsp @@ -0,0 +1,5 @@ +(lp) +(in-package "ACL2") + +(certify-book "total-ordering" 0) +:u diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp new file mode 100644 index 0000000..4d65db8 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/certify.lsp @@ -0,0 +1,27 @@ +(lp) +(in-package "ACL2") + +(certify-book "total-ordering" 0) +:u + +(defpkg "S" + (set-difference-equal + (union-eq '(PACK + ORDINARYP + << + <<-IRREFLEXIVITY + <<-TRICHOTOMY + <<-MUTUAL-EXCLUSION + <<-TRANSITIVITY + FAST-<<-TRICHOTOMY + FAST-<<-MUTUAL-EXCLUSION + FAST-<<-TRANSITIVITY + FAST-<<-RULES + SLOW-<<-RULES + <<-RULES) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(union intersection subsetp add-to-set functionp = apply))) + +(certify-book "set-theory" 1) +:u :u diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2 b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2 new file mode 100644 index 0000000..b44f97f --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.acl2 @@ -0,0 +1,24 @@ +(value :q) + +(LP) + +(defpkg "S" + (set-difference-equal + (union-eq '(PACK + ORDINARYP + << + <<-IRREFLEXIVITY + <<-TRICHOTOMY + <<-MUTUAL-EXCLUSION + <<-TRANSITIVITY + FAST-<<-TRICHOTOMY + FAST-<<-MUTUAL-EXCLUSION + FAST-<<-TRANSITIVITY + FAST-<<-RULES + SLOW-<<-RULES + <<-RULES) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(union intersection subsetp add-to-set functionp = apply))) + +(certify-book "set-theory-original" ? t) diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp new file mode 100644 index 0000000..b710d78 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory-original.lisp @@ -0,0 +1,3318 @@ +; Finite Set Theory for ACL2 +; Copyright (C) 2000 University of Texas at Austin + +; This program is free software; you can redistribute it and/or modify it under +; the terms of Version 2 of the GNU General Public License as published by the +; Free Software Foundation. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: J Strother Moore +; email: Moore@cs.utexas.edu +; Department of Computer Science +; University of Texas at Austin +; Austin, TX 78701 U.S.A. + +; The original kernel of this book was created with support from +; Compaq Systems Research Center, Palo Alto, CA. A report documenting +; the main ideas in this book is available from the ACL2 home page. +; Visit the link "Papers about ACL2 and its Applications" and then +; visit "Finite Set Theory". + +(in-package "S") + +(include-book "total-ordering-original") + +(defun standard-atom (x) + (or (acl2-numberp x) + (characterp x) + (stringp x) + (symbolp x))) + +(defthm standard-atom-type + (iff (standard-atom x) + (or (acl2-numberp x) + (characterp x) + (stringp x) + (symbolp x))) + :rule-classes :compound-recognizer) + +(in-theory (disable standard-atom)) + +(defun ur-elementp (x) + (or (atom x) + (eq (car x) :UR-CONS))) + +; (defthm consp-ur-element +; (implies (not (ur-elementp x)) +; (consp x)) +; :rule-classes :compound-recognizer) + +(defthm set-recursion + (and (implies (not (ur-elementp x)) + (o< (acl2-count (cdr x)) (acl2-count x))) + (implies (not (ur-elementp x)) + (o< (acl2-count (car x)) (acl2-count x)))) + :rule-classes :built-in-clause) + +; (in-theory (disable ur-elementp)) + +; Example objects are +; 3 numbers +; #\A characters +; "Abc" strings +; ABC symbols +; (:UR-CONS (a b c)) lists +; (1 2 1 3 (:UR-CONS (a b c))) sets + +; Some Comments on :UR-CONS + +; It is simplest never to write the symbol :UR-CONS in your sets +; unless you mean to mark consp ur-elements. The symbol :UR-CONS if +; encountered in unexpected places produces counter-intuitive results. + +; For example, (1 2 :UR-CONS) might be thought of as {1 2 :UR-CONS} +; but in fact is {1 2}. The reason is that it is parsed as (1 2 +; . (:UR-CONS)). The enumeration of the elements of a set is +; terminated by the first ur-element cdr. So just as (1 2 . 3) is {1 +; 2}, so is (1 2 . (:UR-CONS ...)). Any attempt to include :UR-CONS +; as an element of an explicit set constant terminates the enumeration +; of the set elements and so fails to include :UR-CONS as an element. + +; Is it possible to use scons to add :UR-CONS to a list? You might +; expect (scons :UR-CONS '(1 2)) to be {:UR-CONS 1 2}. But it is in +; fact {CONS 1 2}. If you ever succeed in using :UR-CONS as an +; ur-element it is treated as though it were a non-canonical +; representation of the symbol ACL2::CONS. + +; These considerations make it simplest to avoid using :UR-CONS except +; in the syntax of sets. + +(defun set-insert (e s) + +; NIL is the only ur-elementp upon which set-insert is ever called, in +; the process of canonicalizing. But I prove theorems about +; set-insert and to make them simpler to state, I have it treat all +; ur-elements s as the empty set. Also, both e and s are assumed to +; be canonical. + + (cond ((ur-elementp s) (cons e nil)) + ((equal e (car s)) s) + ((<< e (car s)) + (cons (car s) + (set-insert e (cdr s)))) + (t (cons e s)))) + +; Observe that if we encounter a non-standard atom we map it to a +; character. Suppose we mapped it, instead, to a symbol, e.g., +; :NON-STANDARD-ATOM. Then = would not be a congruence for SYMBOLP. +; For example, let x be a non-standard atom. Then (= x +; :NON-STANDARD-ATOM). But (SYMBOLP x) is nil while (SYMBOLP +; :NON-STANDARD-ATOM) is t. The moral of this story that if we +; canonicalize non-standard atoms to objects of type type then type +; will not admit = as a congruence. We figure that characters are the +; least used primitive type. + +(defun o-fix (x) + (cond ((atom x) + (cond ((standard-atom x) x) + (t (code-char 255)))) + (t (cons (o-fix (car x)) + (o-fix (cdr x)))))) + +(defthm ordinaryp-o-fix + (and (ordinaryp (o-fix x)) + (implies (ordinaryp x) (equal (o-fix x) x)))) + +(defun ur-fix (x) + +; This converts an arbitrary Lisp object into an ordinary ur-element +; without changing the type. We do not want to change the type so +; that set equality refines IFF and is a congruence relation for the +; arithmetic primitives in ACL2. We discuss the conversions below. + + (cond ((atom x) + (cond ((eq x :UR-CONS) 'ACL2::UR-CONS) + (t (o-fix x)))) + ((eq (car x) :UR-CONS) + (cond ((or (atom (cdr x)) + (atom (cadr x))) + '(:UR-CONS (NIL))) + (t (list :UR-CONS (o-fix (cadr x)))))) + (t nil))) + +; Conversions: +; (1) Make sure the output is ordinary, by using o-fix. +; (2) If we encounter :UR-CONS where an ur-element is expected, we convert it +; the symbol ACL2::UR-CONS. This prevents the accidental formation of +; a :UR-CONS by set operations on data containing :UR-CONS. For example, +; (scons :UR-CONS '(a b c)) will produce the set {ACL2::UR-CONS a b c}, not +; the set {:UR-CONS a b c} and not the ``ur-element'' (:UR-CONS a b c). +; (3) If we encounter (:UR-CONS . xxx) where an ur-element is expected, we +; are sure to return something of the form (:UR-CONS (...)). An ur-element +; marked :UR-CONS means a cons of some sort, no matter what is inside. +; A rough model of the conversion rule is that if the :UR-CONS expression +; is ill-formed it denotes (:UR-CONS (NIL)). More accurately, there are +; three cases: +; (a) (:UR-CONS . atom) => (:UR-CONS (NIL)) +; (b) (:UR-CONS atom . anything) => (:UR-CONS (NIL)) +; (c) (:UR-CONS (...) . anything) => (:UR-CONS (...)) + +(defthm ordinaryp-ur-fix + (ordinaryp (ur-fix x))) + +; (in-theory (disable ur-fix)) + +(defun canonicalize (x) + (cond ((ur-elementp x) (ur-fix x)) + ((ur-elementp (cdr x)) + (list (canonicalize (car x)))) + (t (set-insert (canonicalize (car x)) + (canonicalize (cdr x)))))) + +(defthm ordinaryp-set-insert + (implies (and (ordinaryp e) + (ordinaryp x)) + (ordinaryp (set-insert e x)))) + +(defthm ordinaryp-canonicalize + (ordinaryp (canonicalize x))) + +(defun orderedp (x) + (cond ((ur-elementp x) t) + ((ur-elementp (cdr x)) t) + ((<< (cadr x) (car x)) + (orderedp (cdr x))) + (t nil))) + +(defun canonicalp (x) + (cond ((atom x) + (and (not (eq x :UR-CONS)) + (standard-atom x))) + ((eq (car x) :UR-CONS) + (and (consp (cdr x)) + (consp (cadr x)) + (ordinaryp (cadr x)) + (equal (cddr x) nil))) + ((ur-elementp (cdr x)) + (and (canonicalp (car x)) + (equal (cdr x) nil))) + (t (and (canonicalp (car x)) + (canonicalp (cdr x)) + (orderedp x))))) + +(defthm canonicalp-ordinaryp + (implies (canonicalp x) (ordinaryp x))) + +(defthm orderedp-set-insert + (implies (and (canonicalp e) + (canonicalp a)) + (orderedp (set-insert e a))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm canonicalp-set-insert + (implies (and (canonicalp e) + (canonicalp a)) + (canonicalp (set-insert e a))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm o-fix-ur-cons + (equal (equal (o-fix x) :UR-CONS) + (equal x :UR-CONS))) + +(defthm consp-o-fix + (equal (consp (o-fix x)) + (consp x))) + +(defthm canonicalp-ur-fix + (canonicalp (ur-fix X))) + +(defthm canonicalp-canonicalize + (canonicalp (canonicalize x))) + +(defthm canonicalize-canonicalp + (implies (canonicalp x) (equal (canonicalize x) x))) + +; So here is equality in our system. + +(defun = (x y) + (equal (canonicalize x) + (canonicalize y))) + +(defequiv =) + +; ---------------------------------------------------------------------------- +; The Set Constructor/Destructor Primitives + +; It is very convenient to pretend that sets are built as a new data +; type. So here are the basic functions. I will keep them enabled +; until I have proved the necessary facts about canonicalization, +; equality (=) and subsetp. Then I'll disable them. But I introduce +; them now so that mem and subsetp can be defined in terms of them. I +; have also collected together certain of their elementary properties. +; Most of these theorems are not used until after I have disabled +; these primitives. + +(defun sfix (a) + (if (ur-elementp a) + nil + a)) + +(defun scons (e a) + (if (equal e :UR-CONS) + (cons (canonicalize e) + (sfix a)) + (cons e (sfix a)))) + +; The macro below allows me to write (brace a b c) to mean {a, b, c}. + +(defmacro brace (&rest args) + (cond ((endp args) nil) + (t `(scons ,(car args) + (brace ,@(cdr args)))))) + +; Here are some timings of this entire library. These timings started +; when I began experimenting with three different flavors of scar and +; scdr. The flavors are shown below along with some Caerlaverock +; timings. I chose functionp1-set-insert as a representative expensive +; proof. + +; When these timings were done, there were 279 events and the last one +; was APPLY-RESTRICT. Since the book has probably changed since then, +; these timings are only relevant insofar as they reflect the relative +; effects of the various experiments. Even that claim is suspect: +; since doing these timings I have discovered that there can be a +; considerable difference (30%) between the time it takes in a fresh +; GCL and the time it takes to ``repeat'' the computation in a soiled +; GCL. Fresh GCL is faster. I did not record whether the times below +; were done in fresh system or not. + +; During the first three experiments, I had the <<-rules -- namely <<, +; transitivity, mutual-exclusion, and trichotomy -- disabled by +; default and turned them on during certain proofs. They were on +; during functionp1-set-insert, even though I eventually discovered +; they didn't have to be for the proof to go through. + +; functionp1-set-insert entire file + +(defun scar (a) +; (car a) ;;; 232 secs 1153 secs +; (if (equal (car a) :UR-CONS) nil (car a)) ;;; 404 secs 1212 secs + (if (ur-elementp a) nil (car a)) ;;; 308 secs 1239 secs + ) + +; I then learned that I did not have to have <<-rules enabled during +; the functionp1-set-insert proof or the analogous ones. So I took out +; those theory commands and got: + +; ;;; 2 secs 889 secs + +; Then I had the idea of coding up the ``fast << rules.'' Operating +; in the fast-<<-rules theory by default and occasionally either +; enabling << or switching over to the slow-<<-rules, I got the +; following times in a fresh GCL: + +; ;;; 2 secs 370 secs + + +(defun scdr (a) +; (sfix (cdr a)) +; (if (equal (car a) :UR-CONS) nil (sfix (cdr a))) + (if (ur-elementp a) nil (sfix (cdr a))) + ) + +(defcong = = (scons e a) 1 + :hints (("Goal" :in-theory (enable =)))) + +(defcong = = (scons e a) 2 + :hints (("Goal" :in-theory (enable =)))) + +(defthm scar-scons + (= (scar (scons e a)) e)) + +(defthm scdr-scons + (= (scdr (scons e a)) (sfix a))) + +(defthm ur-elementp-scar + (implies (ur-elementp x) (equal (scar x) nil))) + +(defthm ur-elementp-scdr + (implies (ur-elementp x) (equal (scdr x) nil))) + +(defun setp (x) + (or (equal x nil) + (not (ur-elementp x)))) + +(defthm setp-scdr + (setp (scdr a)) + :rule-classes (:type-prescription :generalize)) + +(defthm scons-scar-scdr + (implies (not (ur-elementp a)) + (= (scons (scar a) (scdr a)) a)) + :rule-classes :elim) + +(defthm acl2-count-scdr + (implies (not (ur-elementp a)) + (o< (acl2-count (scdr a)) + (acl2-count a))) + :rule-classes + ((:built-in-clause) + (:linear :corollary + (implies (not (ur-elementp a)) + (< (acl2-count (scdr a)) + (acl2-count a)))))) + +(defthm consp-set-insert + (consp (set-insert e a)) + :rule-classes :type-prescription) + +(defthm car-set-insert-not-equal-ur-cons + (implies (and (canonicalp e) + (canonicalp a)) + (not (equal (set-insert e a) (cons :UR-CONS x))))) + +(defcong = equal (ur-elementp x) 1) + +; Note: We will generally keep sfix enabled, so this rule will not be +; of much use. + +(defcong = = (sfix x) 1) + +(defthm not-ur-elementp-scons + (not (ur-elementp (scons e a)))) + +(defthm not-consp-implies-ur-elementp + (implies (not (consp e)) + (ur-elementp e))) + +(defthm scons-nil + (implies (and (syntaxp (not (equal a ''nil))) + (ur-elementp a)) + (= (scons e a) + (scons e nil)))) + +(defthm canonicalize-ur-cons + (not (equal (canonicalize x) :UR-CONS))) + +(defthm set-insert-set-insert + (implies (and (canonicalp e) + (canonicalp d) + (canonicalp a)) + (equal (set-insert e (set-insert d a)) + (set-insert d (set-insert e a)))) + :hints (("Goal" :induct (set-insert e a) + :in-theory (slow-<<-rules)))) + +; This rule lets us do a cross-fertilization without waiting for the +; prior elim. The version of this rule that rewrites (set-insert e xxx) +; to (set-insert d (set-insert e a)) has been known to cause infinite +; loops, even with a hand-picked :loop-stopper. + +(defthm set-insert-short-cut + (implies (and (equal xxx (set-insert d a)) + (canonicalp e) + (canonicalp d) + (canonicalp a)) + (equal (equal (set-insert e xxx) + (set-insert d (set-insert e a))) + t))) + +(defthm set-insert-dup + (implies (and (canonicalp e) + (canonicalp a)) + (equal (set-insert e (set-insert e a)) + (set-insert e a))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm scons-scons-2 + (= (scons e (scons d a)) + (scons d (scons e a)))) + +(defthm scons-scons-1 + (= (scons e (scons e a)) + (scons e a))) + +(defthm equal-singleton-set-insert + (implies (and (canonicalp e) + (canonicalp d) + (canonicalp a)) + (equal (equal (list e) (set-insert d a)) + (and (equal e d) + (or (equal (sfix a) nil) + (equal (list e) a))))) + :hints (("Goal" :induct (set-insert d a)))) + +(defthm car-set-insert + (implies (and (canonicalp e) + (canonicalp a)) + (equal (car (set-insert e a)) + (if (ur-elementp a) + e + (if (<< (car a) e) + e + (car a))))) + :hints (("Goal" + :induct (set-insert e a) + :in-theory (enable ur-elementp)))) + +(defthm =-singletons + (equal (= (scons e nil) (scons d a)) + (and (= e d) + (or (ur-elementp a) + (= (scons e nil) a)))) + :hints (("Goal" :in-theory (enable = scons ur-elementp))) + :rule-classes + ((:rewrite) + (:rewrite :corollary + (equal (= (scons d a) (scons e nil)) + (and (= e d) + (or (ur-elementp a) + (= (scons e nil) a)))) + +; Note: This hint is required here because we do not know that +; = is commutative (except by opening it up)! + + :hints (("Goal" :in-theory (enable =)))))) + +; Basic... +(defun <<-cons-1-hint (x y) + (if (consp x) + (list (<<-cons-1-hint (car x) (cdr x))) + y)) + +(defthm <<-cons-1 + (implies (and (ordinaryp x) + (ordinaryp y)) + (<< x (cons x y))) + :hints (("Goal" :induct (<<-cons-1-hint x y) + :in-theory (slow-<<-rules <<)))) + +(defthm not-=-x-set-insert-x + (implies (and (canonicalp e) + (canonicalp x)) + (not (equal e (set-insert e x)))) + :hints (("Goal" :in-theory (cons 'ur-elementp + (slow-<<-rules))))) + +(defthm not-=-x-scons-x + (not (= e (scons e x))) + :hints (("Goal" :in-theory (enable = scons ur-elementp))) + :rule-classes + ((:rewrite) + (:rewrite :corollary (not (= (scons e x) e))))) + +; ---------------------------------------------------------------------------- +; Set Membership and the Subset Relation + +(defun mem (e a) + (cond ((ur-elementp a) nil) + (t (or (= e (scar a)) + (mem e (scdr a)))))) + +(defun subsetp (a b) + (cond ((ur-elementp a) t) + (t (and (mem (scar a) b) + (subsetp (scdr a) b))))) + +; I now prove that = is a congruence for both arguments of mem. The +; proof for the first argument is easy because (mem e s) only uses +; (canonicalize e). [So, if (canonicalize e) is (canonicalize e') +; it is obvious that (mem e s) is (mem e' s).] + +; The proof for the second argument is harder and works this way. We +; will establish that (mem e (canonicalize s)) is the same as (mem e +; s). Suppose that is proved. Then suppose (= s s'). That is, +; (canonicalize s) is (canonicalize s'). We must show that (mem e s) +; is (mem e s'). Use the theorem to replace each by (mem e +; (canonicalize s)) and (mem e (canonicalize s')), then substitute. + +; Even though I don't need it, I will prove the following for regularity. + +(defthm mem-canonicalize-1 + (equal (mem (canonicalize e) a) + (mem e a))) + +; We need to little lemmas to do the second argument. + +; In the lemma below we must assume that the arguments to set-insert +; are canonical. That is because it really compares using EQUAL. +; When we use the lemma it will be on canonicalized arguments. + +(defthm mem-set-insert + (implies (and (canonicalp d) + (canonicalp a)) + (equal (mem e (set-insert d a)) + (or (= e d) + (mem e a)))) + :hints (("Goal" + :induct (set-insert d a)))) + +; Here is the second lemma. + +(defthm mem-canonicalize-2 + (equal (mem e (canonicalize a)) + (mem e a))) + +(defcong = equal (mem e a) 1) + +(defcong = equal (mem e a) 2 + :hints (("Goal" :in-theory (disable mem-canonicalize-2) + :use ((:instance mem-canonicalize-2 + (e e) + (a a)) + (:instance mem-canonicalize-2 + (e e) + (a a-equiv)))))) + + +; Now I repeat it for subsetp. The first argument of subsetp is the +; harder, because we are recursing down it. The second argument is +; easy and follows from what we already know about mem. + +(defthm subsetp-set-insert-1 + (implies (and (canonicalp e) + (canonicalp a)) + (equal (subsetp (set-insert e a) b) + (and (mem e b) + (subsetp a b)))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm subsetp-canonicalize-1 + (equal (subsetp (canonicalize a) b) + (subsetp a b)) + :hints (("Goal" :induct (subsetp a b)))) + +(defcong = equal (subsetp a b) 1 + :hints (("Goal" + :in-theory (disable subsetp-canonicalize-1) + :use ((:instance subsetp-canonicalize-1 + (a a) + (b b)) + (:instance subsetp-canonicalize-1 + (a a-equiv) + (b b)))))) + +(defcong = equal (subsetp a b) 2 + :hints (("Goal" :in-theory (disable =)))) + +; For regularity: + +(defthm subsetp-canonicalize-2 + (equal (subsetp a (canonicalize b)) + (subsetp a b))) + +; Next, I will prove the key facts about subsetp. + +(defthm subsetp-cons + (implies (and (not (equal e :UR-CONS)) + (subsetp a b)) + (subsetp a (cons e b)))) + +(defthm subsetp-x-x + (subsetp x x)) + +(in-theory (disable =)) + +(defthm mem-subsetp + (implies (and (mem e a) + (subsetp a b)) + (mem e b))) + +(defthm transitivity-of-subsetp + (implies (and (subsetp a b) + (subsetp b c)) + (subsetp a c))) + +; ---------------------------------------------------------------------------- +; The Canonicality Theorem + +; Finally, I want to establish the key fact about equality and subset, +; namely, that two sets are = iff they are subsets of eachother. + +; If (= a b), then it is obvious that (subsetp a b) and vice versa, +; given the congruence rules above. + +; Suppose therefore that (subsetp a b) and (subsetp b a). We +; prove (= a b). The proof relies on the fact that << is a total +; ordering. + +; Proof. Let ca and cb be (canonicalize a) and (canonicalize b). +; Observe that they are both ordinary. By the subsetp-canonicalize-i +; lemmas we know that (subsetp ca cb) and (subsetp cb ca). We will +; prove that (subsetp ca cb) implies (not (<< cb ca)). Thus, +; ca equals cb. Q.E.D. + +(defthm =-is-equal + (implies (and (canonicalp x) + (canonicalp y)) + (equal (= x y) + (equal x y))) + :hints (("Goal" :in-theory (enable =)))) + +; I do not want to further encumber << with another rule. But this +; is an important fact and I will :use it. + +(defthm mem-<< + (implies (and (canonicalp e) + (canonicalp a) + (mem e a)) + (<< e a)) + :rule-classes nil + :hints (("Goal" :in-theory (slow-<<-rules <<)))) + +(defthm not-mem-e-e + (not (mem e e)) + :hints (("Goal" + :use (:instance MEM-<< + (e (canonicalize e)) + (a (canonicalize e)))))) + +; This rule seems overly expensive so I keep it disabled most of the time. + +(defthm mem-container + (implies (mem e a) + (not (mem a e))) + :hints (("Goal" + :use ((:instance mem-<< + (e (canonicalize e)) + (a (canonicalize a))) + (:instance mem-<< + (a (canonicalize e)) + (e (canonicalize a))))))) + +(in-theory (disable mem-container)) + +(defthm mem-implies-not-<<-car + (implies (and (canonicalp e) + (canonicalp a) + (mem e a)) + (not (<< (car a) e))) + :hints (("Goal" :in-theory (slow-<<-rules <<)))) + +(defthm <<-cons + (implies (and (canonicalp e) + (canonicalp a) + (mem e a)) + (equal (<< a (cons e z)) + (if (equal (car a) e) + (<< (cdr a) z) + nil))) + :hints (("Goal" :in-theory (enable <<) ; (fast-<<-rules <<) + ))) + +(defthm subsetp-cons-reversed + (implies (and (subsetp a (cons e b)) + (not (equal e :UR-CONS)) + (not (mem e a))) + (subsetp a b))) + +(defthm yucko + (implies (and (canonicalp a) + (canonicalp b) + (subsetp a b) + (mem (car b) a)) + (equal (car a) (car b))) + :rule-classes nil + :hints (("Goal" + :use ((:instance <<-trichotomy + (acl2::x (car a)) + (acl2::y (car b))))))) + +(defthm subsetp-<< + (implies (and (setp a) + (setp b) + (canonicalp a) + (canonicalp b) + (subsetp a b)) + (not (<< b a))) + :rule-classes nil + :hints (("Goal" :induct (<< b a)) + ("Subgoal *1/24.3" + :use (:instance yucko + (a (cdr a)) + (b b))) + ("Subgoal *1/22'''" :in-theory (enable <<) ; (fast-<<-rules <<) + ))) + +(defthm setp-canonicalize + (implies (setp x) + (setp (canonicalize x)))) + +; The Canonalicality Theorem: +(defthm =-iff-subsetps + (implies (and (setp a) + (setp b)) + (iff (= a b) + (and (subsetp a b) + (subsetp b a)))) + :rule-classes nil + :hints + (("Goal" + :in-theory (union-theories '(=) + (disable subsetp-canonicalize-1 + subsetp-canonicalize-2 + canonicalize + setp + transitivity-of-subsetp)) + + :use ((:instance subsetp-canonicalize-1 + (a a) + (b b)) + (:instance subsetp-canonicalize-2 + (a (canonicalize a)) + (b b)) + (:instance subsetp-canonicalize-1 + (a b) + (b a)) + (:instance subsetp-canonicalize-2 + (a (canonicalize b)) + (b a)) + (:instance subsetp-<< + (a (canonicalize a)) + (b (canonicalize b))) + (:instance subsetp-<< + (a (canonicalize b)) + (b (canonicalize a))))))) + +; Now we disable those of the above rules that we don't think are +; worth their cost. + +(in-theory (disable =-is-equal + mem-implies-not-<<-car + <<-cons)) + +;---------------------------------------------------------------------------- +; = Refines iff and is a Congruence for Many ACL2 Functions + +(defthm standard-atom-set-insert + (not (standard-atom (set-insert e a)))) + +(defthm standard-atom-canonicalize + (equal (standard-atom (canonicalize x)) + (atom x))) + +(defcong = equal (canonicalize x) 1 + :hints (("Goal" :in-theory (enable =)))) + +(defthm canonicalize-= + (= (canonicalize x) x) + :hints (("Goal" :in-theory (enable =)))) + +(defthm canonicalize-non-nil + (iff (canonicalize x) x) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defrefinement = iff + :hints (("Goal" :in-theory (enable =)))) + +(defthm canonicalize-fix + (equal (canonicalize (fix x)) + (fix (canonicalize x))) + :rule-classes nil + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm <-fixes + (equal (< x y) (< (fix x) (fix y))) + :rule-classes nil) + +(defcong = equal (< x y) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance <-fixes + (x x) + (y y)) + (:instance <-fixes + (x x-equiv) + (y y)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + +(defcong = equal (< x y) 2 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance <-fixes + (x x) + (y y)) + (:instance <-fixes + (x x) + (y y-equiv)) + (:instance canonicalize-fix + (x y)) + (:instance canonicalize-fix + (x y-equiv)))))) + +(defthm +-fixes + (equal (+ x y) (+ (fix x) (fix y))) + :rule-classes nil) + +(defcong = equal (+ x y) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance +-fixes + (x x) + (y y)) + (:instance +-fixes + (x x-equiv) + (y y)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + +(defcong = equal (+ x y) 2 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance +-fixes + (x x) + (y y)) + (:instance +-fixes + (x x) + (y y-equiv)) + (:instance canonicalize-fix + (x y)) + (:instance canonicalize-fix + (x y-equiv)))))) + +(defthm --fixes + (equal (- x) (- (fix x))) + :rule-classes nil) + +(defcong = equal (- x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance --fixes + (x x)) + (:instance --fixes + (x x-equiv)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + + +(defthm *-fixes + (equal (* x y) (* (fix x) (fix y))) + :rule-classes nil) + +(defcong = equal (* x y) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance *-fixes + (x x) + (y y)) + (:instance *-fixes + (x x-equiv) + (y y)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + +(defcong = equal (* x y) 2 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance *-fixes + (x x) + (y y)) + (:instance *-fixes + (x x) + (y y-equiv)) + (:instance canonicalize-fix + (x y)) + (:instance canonicalize-fix + (x y-equiv)))))) + +(defthm integerp-canonicalize + (equal (integerp (canonicalize x)) + (integerp x))) + +(defthm rationalp-canonicalize + (equal (rationalp (canonicalize x)) + (rationalp x))) + +(defthm symbolp-canonicalize + (equal (symbolp (canonicalize x)) + (symbolp x)) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm stringp-canonicalize + (equal (stringp (canonicalize x)) + (stringp x))) + +(defthm characterp-canonicalize + (equal (characterp (canonicalize x)) + (or (characterp x) + (and (atom x) + (not (standard-atom x))))) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm consp-canonicalize + (equal (consp (canonicalize x)) + (consp x)) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defcong = equal (integerp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(integerp-canonicalize)) + :use ((:instance integerp-canonicalize + (x x)) + (:instance integerp-canonicalize + (x x-equiv)))))) + +(defcong = equal (rationalp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(rationalp-canonicalize)) + :use ((:instance rationalp-canonicalize + (x x)) + (:instance rationalp-canonicalize + (x x-equiv)))))) + +(defcong = equal (symbolp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(symbolp-canonicalize)) + :use ((:instance symbolp-canonicalize + (x x)) + (:instance symbolp-canonicalize + (x x-equiv)))))) + +(defcong = equal (stringp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(stringp-canonicalize)) + :use ((:instance stringp-canonicalize + (x x)) + (:instance stringp-canonicalize + (x x-equiv)))))) + +(defcong = equal (consp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(consp-canonicalize)) + :use ((:instance consp-canonicalize + (x x)) + (:instance consp-canonicalize + (x x-equiv)))))) + + +; We do not get (defcong = equal (characterp x) 1) because we +; canonicalize non-standard atoms to (code-char 255). + +; ---------------------------------------------------------------------------- +; Codified Theorem Proving Strategies + +; The following all turn into the corresponding defthms: +; (defx name term) +; (defx name term :hints ... :rule-classes ...) + +; But if you write +; (defx ...a... :strategy xxx ...b...) +; it macro expands to +; (xxx ...a... ...b...) + +; Thus, if you want to codify a new theorem proving strategy xxx, you can +; defmacro xxx and then write (defx ... :strategy xxx ...). + +; The main point of this is to let me write defx events and introduce +; new strategies as I go. Also, I can name my strategies without +; including ``def'' in front of them and still search for ``(def...'' +; when looking for things. + +(defun packn-in-pkg (lst pkg-witness) + (declare (xargs :mode :program)) + (acl2::intern-in-package-of-symbol (coerce (acl2::packn1 lst) 'string) + pkg-witness)) + +(defmacro defx (&rest args) + (let ((temp (member :strategy args))) + +; We allow the strategy to be a keyword, in which case we convert it +; to the corresponding symbol in this package. If the strategy is not +; a keyword, it is used as supplied. + + (cond + (temp + `(,(if (keywordp (cadr temp)) + (packn-in-pkg (list (symbol-name (cadr temp))) 'defx) + (cadr temp)) + ,@(butlast args (length temp)) + ,@(cddr temp))) + (t `(defthm ,@args))))) + +; ---------------------------------------------------------------------------- +; Proving Congruences + +; There are two common ways to prove congruence rules in this theory. + +; (1) The :canonicalize strategy: prove that (fn (canonicalize x)) is +; (fn x). This is generally used if fn returns an ur-element (as +; opposed to a set). + +; (2) The :subsetp stragegy: prove that (subsetp a1 a2) implies +; (subsetp (fn a1) (fn a2)). This is generally used if fn returns a +; set. + +(defun genname1 (name n avoid) + (declare (xargs :mode :program)) + (let ((new-name (packn-in-pkg (list name n) name))) + (cond ((acl2::member-equal new-name avoid) + (genname1 name (+ 1 n) avoid)) + (t new-name)))) + +(defun genname (name avoid) + (declare (xargs :mode :program)) + (cond ((acl2::member-equal name avoid) + (genname1 name 1 avoid)) + (t name))) + +(defun put-nth (e n lst) + (cond ((zp n) (cons e (cdr lst))) + (t (cons (car lst) (put-nth e (- n 1) (cdr lst)))))) + +; And here is the macro + +(defmacro congruence (expr n &key method) + (cond + ((eq method :canonicalize) + (let* ((fn (car expr)) + (vars (cdr expr)) + (x (nth (- n 1) vars)) + (name1 + (packn-in-pkg (list fn "-SET-INSERT") fn)) + (name2 + (packn-in-pkg (list fn "-CANONICALIZE") fn)) + (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4 + (e (genname 'e vars1)) + (a (genname x vars1)) + (x-equiv (packn-in-pkg (list x "-EQUIV") x))) + `(encapsulate + nil + (local (in-theory (enable scons scar scdr ur-elementp))) + + (defthm ,name1 + (implies (and (canonicalp ,e) + (canonicalp ,a)) + (equal (,fn ,@(put-nth `(set-insert ,e ,a) + (- n 1) + vars)) + (,fn ,@(put-nth `(cons ,e ,a) + (- n 1) + vars)))) + :hints (("Goal" + :induct (set-insert ,e ,a) + +; Note that the following in-theory is commented out! I learned that +; if you enable = during these proofs it is generally slower. So I +; don't. +; :in-theory (enable =) + + + ))) + + (defthm ,name2 + (equal (,fn ,@(put-nth `(canonicalize ,x) + (- n 1) + vars)) + (,fn ,@vars))) + + (defcong = equal ,expr ,n + :hints + (("Goal" + :in-theory (disable ,name2) + :use ((:instance ,name2 (,x ,x)) + (:instance ,name2 + (,x ,x-equiv))))))))) + ((eq method :subsetp) + (let* ((fn (car expr)) + (vars (cdr expr)) + (x (nth (- n 1) vars)) + (name1 + (packn-in-pkg (list "SUBSETP-" fn "-" fn) fn)) + (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4 + (a1 (genname1 x 1 vars1)) + (a2 (genname1 x 2 (cons a1 vars1))) + (x-equiv (packn-in-pkg (list x "-EQUIV") x))) + `(encapsulate + nil + (defthm ,name1 + (implies (subsetp ,a1 ,a2) + (subsetp (,fn ,@(put-nth a1 (- n 1) vars)) + (,fn ,@(put-nth a2 (- n 1) vars))))) + + (defcong = = ,expr ,n + :hints (("Goal" + :use (:instance =-iff-subsetps + (a ,expr) + (b (,fn ,@(put-nth x-equiv + (- n 1) + vars)))))))))) + ((eq method nil) + `(defcong = = ,expr ,n)) + (t `(acl2::er acl2::soft 'congruence + "The :method ~x0 is unknown." + ',method)))) + +; ---------------------------------------------------------------------------- +; The User Level Theory + +(in-theory (disable scons scar scdr ur-elementp)) + +; ---------------------------------------------------------------------------- +; Set Union + +(defun union (a b) + (if (ur-elementp a) + (sfix b) + (scons (scar a) + (union (scdr a) b)))) + +; My next goal is to prove both + +; (defcong = = (union a b) 1) +; (defcong = = (union a b) 2) + +; The first of these is problematic but the second is easy. +; Generally, if the congruence rule is in a slot that is held fixed in +; the recursion (as in the second case above), the proof is an easy +; induction, using congruence rules for the subfunctions. But if the +; congruence rule is in a controller slot, you generally need lemmas. + +(defthm mem-union + (equal (mem e (union a b)) + (or (mem e a) + (mem e b)))) + +(defthm subsetp-scons + (implies (subsetp a b) + (subsetp a (scons e b)))) + +(defthm subsetp-union-1 + (subsetp a (union a b))) + +(defthm subsetp-union-2 + (subsetp a (union b a))) + +(defthm subsetp-union + (implies (subsetp a1 a2) + (subsetp (union a1 b) + (union a2 b)))) +(defthm setp-union + (setp (union a b))) + +(defx :strategy :congruence (union a b) 1 :method :subsetp) + +(defx :strategy :congruence (union a b) 2) + +(defthm union-right-id + (implies (ur-elementp b) + (= (union a b) (sfix a)))) + +(defthm union-scons + (= (union a (scons e b)) + (scons e (union a b)))) + +(defthm commutativity-of-union + (= (union a b) (union b a))) + +(defthm ur-elementp-union + (equal (ur-elementp (union a b)) + (and (ur-elementp a) + (ur-elementp b)))) + +(defthm associativity-of-union + (= (union (union a b) c) + (union a (union b c)))) + + +; ---------------------------------------------------------------------------- +; Set Intersection + +(defun intersection (a b) + (if (ur-elementp a) + nil + (if (mem (scar a) b) + (scons (scar a) + (intersection (scdr a) b)) + (intersection (scdr a) b)))) + +(defthm mem-intersection + (equal (mem e (intersection a b)) + (and (mem e a) + (mem e b)))) + +(defthm subsetp-intersection-1 + (subsetp (intersection a b) a)) + +(defthm subsetp-intersection-2 + (subsetp (intersection b a) a)) + +(defthm subsetp-intersection + (implies (subsetp a1 a2) + (subsetp (intersection a1 b) + (intersection a2 b)))) + +(defthm setp-intersection + (setp (intersection a b))) + +(defx :strategy :congruence (intersection a b) 1 :method :subsetp) +(defx :strategy :congruence (intersection a b) 2) + +(defthm intersection-right-id + (implies (ur-elementp b) + (= (intersection a b) nil))) + +(defthm scons-id + (implies (mem e a) + (= (scons e a) a))) + +(defthm intersection-scons + (= (intersection a (scons e b)) + (if (mem e a) + (scons e (intersection a b)) + (intersection a b)))) + +(defthm commutativity-of-intersection + (= (intersection a b) (intersection b a))) + +(defthm associativity-of-intersection + (= (intersection (intersection a b) c) + (intersection a (intersection b c)))) + +; ---------------------------------------------------------------------------- +; Arithmetic + +(include-book "../../../../../arithmetic/top-with-meta") + +(defun cardinality (a) + (if (ur-elementp a) + 0 + (if (mem (scar a) (scdr a)) + (cardinality (scdr a)) + (+ 1 (cardinality (scdr a)))))) + +(defx :strategy :congruence (cardinality a) 1 :method :canonicalize) + +(defthm cardinality-union-2 + (<= (cardinality b) (cardinality (union a b))) + :rule-classes :linear) + +; Observe that we proved the easy case first, by induction on b, +; and then we prove the other case by commutativity. + +(defthm cardinality-union-1 + (<= (cardinality b) (cardinality (union b a))) + :rule-classes :linear) + +(defthm cardinality-union-3 + (<= (cardinality (union a b)) + (+ (cardinality a) + (cardinality b))) + :rule-classes :linear) + +(defthm cardinality-0 + (equal (equal (cardinality a) 0) + (ur-elementp a))) + +(defthm cardinality-non-0 + (implies (mem e x) + (< 0 (cardinality x))) + :rule-classes :linear) + +(defthm cardinality-intersection-1 + (<= (cardinality (intersection a b)) (cardinality a)) + :rule-classes :linear) + +(defthm cardinality-intersection-2 + (<= (cardinality (intersection b a)) (cardinality a)) + :rule-classes :linear) + +(defthm cardinality-scons + (equal (cardinality (scons e a)) + (if (mem e a) + (cardinality a) + (+ 1 (cardinality a))))) + +(defthm cardinality-disjoint-union + (implies (not (intersection a b)) + (= (cardinality (union a b)) + (+ (cardinality a) + (cardinality b))))) + + +; ---------------------------------------------------------------------------- +; Choose + +(defun choose (a) + (car (sfix (canonicalize a)))) + +(defx :strategy :congruence (choose a) 1) + +(defthm ur-elementp-canonicalize + (equal (ur-elementp (canonicalize x)) + (ur-elementp x)) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm mem-choose-lemma + (equal (mem (car (canonicalize a)) a) + (not (ur-elementp a))) + :hints (("Goal" + :in-theory (enable scar scdr ur-elementp)))) + +(defthm mem-choose + (equal (mem (choose a) a) + (not (ur-elementp a)))) + +; One might think that the following follows from the previous +; theorems about choose. But that is not correct. For example, +; (choose {1 2 3}) might be 2 but (choose {2 3}) might be 3. This +; property is due to the fact that choose is really the biggest +; element of the set. + +(defthm car-canonicalize-ur-cons + (equal (equal (car (canonicalize a)) :UR-CONS) + (and (consp a) + (equal (car a) :UR-CONS))) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm choose-scons + (implies (not (= (choose (scons e a)) e)) + (= (choose (scons e a)) (choose a))) + :hints (("Goal" + :in-theory + (enable = scons ur-elementp)))) + +(defthm choose-singleton + (= (choose (scons e nil)) e) + :hints (("Goal" :in-theory (enable = scons ur-elementp)))) + +(in-theory (disable choose)) + +(defthm elim-choose-singleton + (implies (equal (cardinality x) 1) + (= (scons (choose x) nil) x))) + +(defthm mem-singleton + (implies (and (equal (cardinality x) 1) + (mem e x)) + (= (scons e nil) x)) + :rule-classes nil + :hints (("Goal" :in-theory (disable elim-choose-singleton) + :use elim-choose-singleton))) + +(defthm choose-ur-elementp + (implies (ur-elementp x) + (= (choose x) nil)) + :hints (("Goal" :in-theory (enable choose ur-elementp sfix)))) + + +; ---------------------------------------------------------------------------- +; Set Difference + +(defun diff (a b) + (cond ((ur-elementp a) + nil) + ((mem (scar a) b) + (diff (scdr a) b)) + (t (scons (scar a) + (diff (scdr a) b))))) + +(defthm mem-diff + (equal (mem e (diff a b)) + (and (mem e a) + (not (mem e b))))) + +(defthm subsetp-diff-1 + (subsetp (diff a b) a)) + +(defthm subsetp-diff + (implies (subsetp a1 a2) + (subsetp (diff a1 b) + (diff a2 b)))) + +(defthm setp-diff + (setp (diff a b))) + +(defx :strategy :congruence (diff a b) 1 :method :subsetp) +(defx :strategy :congruence (diff a b) 2) + +(defthm diff-right-id + (implies (ur-elementp b) + (= (diff a b) (sfix a)))) + +(defthm cardinality-diff-singleton + (equal (cardinality (diff y (scons x nil))) + (if (mem x y) + (- (cardinality y) 1) + (cardinality y)))) + +(defthm cardinality-diff + (<= (cardinality (diff a b)) (cardinality a)) + :rule-classes :linear) + +(defthm diff-nil + (implies (subsetp x y) + (= (diff x y) nil))) + +(defthm diff-scons + (implies (not (mem e s)) + (= (diff s (scons e y)) (diff s y)))) + +(encapsulate nil + (local + (defthm scons-x-diff-x + (implies (mem x s) + (= (scons x (diff s (scons x nil))) s)) + :hints (("Subgoal *1/3'5'" + :cases ((mem sr sr0)))))) + + (defthm scons-diff-scons + (= (scons e (diff a (scons e nil))) + (scons e a)) + :hints (("Goal" :cases ((mem e a)))))) + +(defthm elim-choose-doubleton + (implies (equal (cardinality x) 2) + (= (scons (choose x) + (scons (choose (diff x (scons (choose x) nil))) + nil)) + x))) + +(defthm subsetp-diff-1-corrollary + (implies (subsetp a b) + (subsetp (diff a c) b))) + +(defthm subsetp-not-subsetp-trick + (implies (and (subsetp a b) + (not (subsetp a (scdr b)))) + (mem (scar b) a))) + +(defthm intersection-diff-2 + (= (intersection a (diff b c)) + (diff (intersection a b) c))) + +(defthm intersection-diff-1 + (= (intersection (diff b c) a) + (diff (intersection a b) c))) + +; There are others, but I am not going to prove them now. + +; ---------------------------------------------------------------------------- +; Ordered Pairs as Sets + +; It is possible to provide ordered pairs as ur-elements. For example +; we could define (pair x y) to be (list :UR-CONS (cons x y)). But here +; we develop the classical treatment of ordered pairs. + +(defun pair (x y) + (brace x (brace x y))) + +; Observe that a pair necessarily has cardinality 2. But the larger +; element need not have cardinality 2. For example, (pair x x) is +; {x {x}}. + +; We must be able to determine whether a set of cardinality 2 is a +; pair. Call the two elements x and y. Then either (mem x y) or (mem +; y x). Furthermore, the larger must be of cardinality 2 or less. To +; code this up, we have to have a way of finding ``the two elements'' +; of a set, a, of cardinality 2, when a is not necessarily in +; canonical form. E.g., (1 (1 2)) is a pair but so is (1 1 (2 1) (1 +; 2)). At first, I wanted to avoid canonicalizing the set, for +; efficiency reasons. + +; Here was my first attempt to extract ``the other'' element of a +; set of cardinality 2. + +; (defun find-other (e s) +; ; Find the first element of s that is not e. +; (cond ((ur-elementp s) nil) +; ((= e (scar s)) (find-other e (scdr s))) +; (t (scar s)))) + +; Unfortunately, this function does not admit = as a congruence in +; the second argument. For example (find-other 1 '(1 2 3)) and +; (find-other 1 '(1 3 2)) return different things, even though their +; arguments are =. (It would admit it if we limited s to sets of +; cardinality 2, but we can't.) + +; So I have decided simply use the classical approach in terms of +; choose. If the first element of a pair is a number, this is not too +; expensive. + +(defun pairp (a) + (if (equal (cardinality a) 2) + (let* ((x (choose a)) + (y (choose (diff a (brace x))))) + (or (and (mem x y) + (<= (cardinality y) 2)) + (and (mem y x) + (<= (cardinality x) 2)))) + nil)) + +(defun hd (a) + (cond ((pairp a) + (let* ((x (choose a)) + (y (choose (diff a (brace x))))) + (if (mem x y) + x + y))) + (t nil))) + +(defun tl (a) + (cond ((pairp a) + (let* ((x (choose a)) + (y (choose (diff a (brace x))))) + (if (mem x y) + (if (equal (cardinality y) 1) + x + (choose (diff y (brace x)))) + (if (equal (cardinality x) 1) + y + (choose (diff x (brace y))))))) + (t nil))) + +(defthm setp-pair + (setp (pair x y))) + +(defcong = = (pair a b) 1) +(defcong = = (pair a b) 2) +(defcong = equal (pairp a) 1) +(defcong = = (hd a) 1) +(defcong = = (tl a) 1) + +(in-theory (enable mem-container)) + +(defthm hd-pair + (= (hd (pair x y)) x)) + +(defthm tl-pair + (= (tl (pair x y)) y)) + +(defthm pairp-pair + (pairp (pair x y)) + :rule-classes (:type-prescription :generalize)) + +(defthm pairp-implies-setp + (implies (pairp x) (setp x))) + +(encapsulate + nil + +; Our goal here is to prove + +; (implies (pairp a) +; (= (pair (hd a) (tl a)) a)) + +; We have to give the proof pretty explicitly. It exploits the fact +; that we know how to represent singleton and doubleton sets in terms +; of choose. Since we have to use these lemmas explicitly, we disable +; them. + + (local (in-theory (disable elim-choose-doubleton + elim-choose-singleton))) + +; To make the proof easier to understand, we give names to certain +; expressions. In the definitions of pair, hd and tl, we use two +; local variables, + +; (let* ((x (choose a)) +; (y (choose (diff a (brace x))))) +; ...) + +; Here we define functions corresponding to their values. + + (local (defun x (a) (choose a))) + (local (defun y (a) (choose (diff a (brace (x a)))))) + +; Given that a is known to be a pairp, there are four cases, depending +; on which of x and y is an element of the other and whether the +; cardinality of the bigger is 1 or 2. We will prove the main goal +; for each of the four cases. + + (local + (defthm case-1 + (implies (and (mem (x a) (y a)) + (equal (cardinality (y a)) 2) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ( + +; Proof of Case 1: + +; (i) Represent A as a doubleton in terms of choose. + + (:instance elim-choose-doubleton (x A)) + +; (ii) Represent y as a doubleton. + + (:instance elim-choose-doubleton (x (y a))) + +; (iii) When x is removed from y, the result is a singleton, which can +; be represented with choose. + + (:instance elim-choose-singleton + (x (diff (y a) (scons (x a) nil)))) + +; (iv) If x is a member of a singleton set, the set is {x}. + + (:instance mem-singleton + (e (x a)) + (x (diff (y a) (scons (x a) nil))))))))) + + (local + (defthm case-2 + (implies (and (mem (x a) (y a)) + (equal (cardinality (y a)) 1) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ( + +; Proof of Case 2: + +; (i) Represent A as a doubleton in terms of choose. + + (:instance elim-choose-doubleton (x A)) + +; (ii) Represent y as a singleton. + + (:instance elim-choose-singleton (x (y a))) + +; (iii) If x is a member of singleton set, the set is {x}. + + (:instance mem-singleton + (e (x a)) + (x (y a)))))))) + +; Cases 3 and 4 are symmetric with Cases 1 and 2, interchanging the +; roles of x and y. + + (local + (defthm case-3 + (implies (and (mem (y a) (x a)) + (equal (cardinality (x a)) 2) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ((:instance elim-choose-doubleton (x A)) + (:instance elim-choose-doubleton (x (x a))) + (:instance elim-choose-singleton + (x (diff (x a) (scons (y a) nil)))) + (:instance mem-singleton + (e (y a)) + (x (diff (x a) (scons (y a) nil))))))))) + + (local + (defthm case-4 + (implies (and (mem (y a) (x a)) + (equal (cardinality (x a)) 1) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ((:instance elim-choose-doubleton (x A)) + (:instance elim-choose-singleton (x (x a))) + (:instance mem-singleton + (e (y a)) + (x (x a)))))))) + + (defthm pair-hd-tl + (implies (pairp A) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" :in-theory (disable pair hd tl) + :cases ((and (mem (x a) (y a)) ;;; Case 1 + (equal (cardinality (y a)) 2)) + (and (mem (x a) (y a)) ;;; Case 2 + (equal (cardinality (y a)) 1)) + (and (mem (y a) (x a)) ;;; Case 3 + (equal (cardinality (x a)) 2)) + (and (mem (y a) (x a)) ;;; Case 4 + (equal (cardinality (x a)) 1))))) + :rule-classes (:rewrite :elim))) + +(in-theory (disable mem-container)) + +(in-theory (disable pairp pair hd tl)) + +(defthm equal-booleans + (implies (and (acl2::booleanp p) + (acl2::booleanp q)) + (equal (equal p q) + (iff p q)))) + +(defthm equal-pair + (equal (= (pair x1 y1) + (pair x2 y2)) + (and (= x1 x2) + (= y1 y2))) + :hints + (("Goal" :in-theory (disable hd-pair tl-pair) + :use ((:instance hd-pair (x x1) (y y1)) + (:instance hd-pair (x x2) (y y2)) + (:instance tl-pair (x x1) (y y1)) + (:instance tl-pair (x x2) (y y2)))))) + +(in-theory (disable equal-booleans)) + +(defthm equal-pair-generalized + (equal (= (pair x1 x2) y) + (and (pairp y) + (= x1 (hd y)) + (= x2 (tl y))))) + +(in-theory (disable equal-pair-generalized)) + + + +; ---------------------------------------------------------------------------- +; Functions as Sets + +; The following is an example of set comprehension. In particular, it +; is + +; { x in s | (and (pairp x) (= e (hd x)))} + +(defun subset-such-that1 (s e) + (cond ((ur-elementp s) nil) + ((and (pairp (scar s)) + (= e (hd (scar s)))) + (scons (scar s) (subset-such-that1 (scdr s) e))) + (t (subset-such-that1 (scdr s) e)))) + +; When such a function is defined we should immediately prove the +; obvious three relationships: + +(defthm setp-subset-such-that1 + (setp (subset-such-that1 a e))) + +(defthm mem-subset-such-that1 + (iff (mem pair (subset-such-that1 a x)) + (and (pairp pair) + (mem pair a) + (= (hd pair) x))) + :hints (("Goal" :do-not '(generalize)))) + +(defthm subsetp-subset-such-that1 + (subsetp (subset-such-that1 a x) a)) + +; The congruence rules are easy. + +(defx :strategy :congruence (subset-such-that1 a e) 1 :method :subsetp) +(defx :strategy :congruence (subset-such-that1 a e) 2) + +(defthm mem-subset-such-that1-corrollary + (implies (and (subsetp a (subset-such-that1 f x)) + (mem e a)) + (and (pairp e) + (= (hd e) x)))) + +; Now we define apply: + +(defun apply (s e) + (tl (choose (subset-such-that1 s e)))) + +(defcong = = (apply s e) 1) +(defcong = = (apply s e) 2) + +(defun except (s e v) + (scons (pair e v) + (diff s (subset-such-that1 s e)))) + +(defcong = = (except s e v) 1) +(defcong = = (except s e v) 2) +(defcong = = (except s e v) 3) + +(defthm diff-scons-1 + (implies (acl2::syntaxp (not (equal b ''nil))) + (= (diff a (scons e b)) + (diff (diff a b) (brace e))))) + +(defthm ur-elementp-diff + (iff (ur-elementp (diff a b)) + (subsetp a b))) + +(defthm subset-such-that1-diff-subset-such-that-1 + (= (subset-such-that1 (diff f (subset-such-that1 f x)) y) + (if (= x y) + nil + (subset-such-that1 f y)))) + +(encapsulate + nil + (local + (defthm lemma2 + (implies (and (subsetp f (subset-such-that1 g x)) + (not (= x y))) + (= (subset-such-that1 f y) + nil)))) + + (defthm apply-except + (= (apply (except f x v) y) + (if (= x y) + v + (apply f y))))) + +(defthm mem-except + (equal (mem e (except f x v)) + (if (pairp e) + (if (= (hd e) x) + (= (tl e) v) + (mem e f)) + (mem e f)))) + +(defthm subsetp-except + (iff (subsetp (except f x v) g) + (and (mem (pair x v) g) + (subsetp (diff f (subset-such-that1 f x)) + g)))) + +(defthm ur-elementp-except + (not (ur-elementp (except f x v)))) + +(in-theory (disable apply except)) + +(defmacro func* (&rest args) + (cond ((endp args) nil) + ((endp (cdr args)) (car args)) + (t `(except (func* ,@(cdr args)) + ,(car (car args)) + ,(cadr (car args)))))) + +(defmacro func (&rest args) + `(func* ,@args nil)) + + +; ---------------------------------------------------------------------------- +; Sets of ordered pairs. + +; This is really just a simple map over a checking a predicate. I +; need to automate this sort of thing but I will do it by hand right +; now. + +(defun pairsp (a) + (cond ((ur-elementp a) t) + (t (and (pairp (scar a)) + (pairsp (scdr a)))))) + +(defx :strategy :congruence (pairsp a) 1 :method :canonicalize) + +(defthm pairsp-union + (equal (pairsp (union a b)) + (and (pairsp a) + (pairsp b)))) + +(defthm pairsp-diff + (implies (pairsp a) + (pairsp (diff a b)))) + +; This one is more useful when dealing with sets created by EXCEPT. + +(defthm pairsp-diff-subset-such-that1 + (equal (pairsp (diff a (subset-such-that1 b x))) + (pairsp a))) + +(defthm pairsp-scons + (equal (pairsp (scons e a)) + (and (pairp e) + (pairsp a)))) + +(defthm mem-pairsp + (implies (and (mem e f) + (pairsp f)) + (pairp e))) + +(defthm pairsp-subset-such-that1 + (implies (pairsp f) + (pairsp (subset-such-that1 f x)))) + +(defthm nil-not-mem-pairsp + (implies (pairsp f) + (not (mem nil f)))) + +; ---------------------------------------------------------------------------- +; Recognizing Functions + +; The basic idea is to define the predicate that recognizes when a set +; is both pairsp and has unique hds. We've got the first part. The +; second part is called functionp1. + +; Here is my first functionp1. It does not insure that every element +; of f is a pair. Thus, + +; (functionp1 (brace (pair 1 2)) (brace (pair 1 2) 3)) = t + +; Second, it is fragile in the sense that if a is not a subset of f, it +; fails, e.g., + +; (functionp1 (brace (pair 1 2)) (brace (pair 3 4))) = nil + +; This is not a problem at the top level, where a is f. But in stating +; theorems about functionp1 it would be convenient to allow arbitrary a +; with sensible results. + +; (defun functionp1 (a f) +; (cond ((ur-elementp a) t) +; (t (and (pairp (scar a)) +; (equal (cardinality (subset-such-that1 f (hd (scar a)))) 1) +; (functionp1 (scdr a) f))))) + +; So here is my second: + +(defun functionp1 (a f) + (cond ((ur-elementp a) t) + (t (and (<= (cardinality (subset-such-that1 f (hd (scar a)))) 1) + (functionp1 (scdr a) f))))) + +(defx :strategy :congruence (functionp1 a f) 1 :method :canonicalize) +(defcong = equal (functionp1 a f) 2) + + +; Is 8 a function? I say no. The reason I say no, is that I want it +; to be the case that two functions are equal iff apply gives the same +; answers on both. But if I defined a function as (and (pairsp f) +; (functionp1 f f)) then 8 is a functionp, because every element of 8 +; is a pair and their hds are unique. + +(defun functionp (f) + (if (ur-elementp f) + (= f nil) + (and (pairsp f) + (functionp1 f f)))) + +(defcong = equal (functionp f) 1) + +; My next goal is to prove that functionp is preserved by EXCEPT. +; I need some lemmas about functionp1 + +(defthm cardinality-subset-such-that1 + (<= (cardinality (subset-such-that1 f x)) + (cardinality f)) + :rule-classes :linear) + +(defun simultaneously (a b) + (declare (xargs :measure (cardinality a))) + (cond ((ur-elementp a) b) + (t (simultaneously (diff a (brace (scar a))) + (diff b (brace (scar a))))))) + +(defthm cardinality-subsetp + (implies (subsetp a b) + (<= (cardinality a) + (cardinality b))) + :hints (("Goal" :induct (simultaneously a b))) + :rule-classes :linear) + + + +; The next two theorems are not used until later, but they seem +; natural to have around. + +(defthm functionp1-subsetp-2 + (implies (and (functionp1 a g) + (subsetp f g)) + (functionp1 a f)) + :hints + (("Subgoal *1/4'" + :in-theory (disable cardinality-subsetp) + :use (:instance cardinality-subsetp + (a (SUBSET-SUCH-THAT1 F (HD (SCAR A)))) + (b (SUBSET-SUCH-THAT1 G (HD (SCAR A)))))))) + +(defthm functionp1-diff + (implies (functionp1 a f) + (functionp1 a (diff f b))) + :hints (("Goal" :in-theory (disable subsetp-diff-1) + :use (:instance subsetp-diff-1 + (a f) + (b b))))) + +; Consider the goal (implies (functionp f) (functionp f')), where f' +; is (except f x v). Ignoring the pairsp part, this opens into + +; (implies (functionp1 f f) (functionp1 f' f')) + +; We have to break both duplications. Each requires a lemma. Then +; we put the two lemmas together to get something like: + +; (implies (functionp1 b f) (functionp1 a f')) + +; where (subsetp a b). + +; Here is one of the two ``breakers.'' + +(defthm functionp1-subsetp-1 + (implies (and (subsetp a b) + (functionp1 b f)) + (functionp1 a f)) + :hints (("Goal" :do-not '(generalize)))) + +(encapsulate + nil + +; This is the other ``breaker''. The scons below is f', i.e., the +; expansion of (except f x v). + + (local + (defthm functionp1-except-lemma + (implies (functionp1 a f) + (functionp1 a (scons (pair x v) + (diff f (subset-such-that1 f x))))))) + +; Now we put the two breakers together to get the main lemma about +; functionp1 and except. + + (defthm functionp1-except + (implies (and (functionp1 b f) + (subsetp a b)) + (functionp1 a (scons (pair x v) + (diff f (subset-such-that1 f x))))))) + +(defthm functionp-except + (implies (functionp f) + (functionp (except f x v))) + :hints (("Goal" :in-theory (enable except)))) + +(defthm functionp-implies-pairsp + (implies (functionp f) + (pairsp f))) + +(in-theory (disable functionp)) + +;---------------------------------------------------------------------------- +; Domain and Range + +(defun domain (f) + (cond ((ur-elementp f) nil) + (t (scons (hd (scar f)) + (domain (scdr f)))))) + +(defun range (f) + (cond ((ur-elementp f) nil) + (t (scons (tl (scar f)) (range (scdr f)))))) + +(defthm mem-implies-mem-domain + (implies (mem e f) + (mem (hd e) (domain f)))) + +(defthm ur-elementp-domain + (equal (ur-elementp (domain f)) + (ur-elementp f))) + +(defx :strategy :congruence (domain f) 1 :method :subsetp) + +(defthm mem-implies-mem-range + (implies (mem e f) + (mem (tl e) (range f)))) + +(defthm ur-elementp-range + (equal (ur-elementp (range f)) + (ur-elementp f))) + +(defx :strategy :congruence (range f) 1 :method :subsetp) + +(defthm domain-scons + (= (domain (scons e f)) + (scons (hd e) (domain f)))) + +(defthm domain-diff-subset-such-that1 + (implies (pairsp f) + (= (domain (diff f (subset-such-that1 f x))) + (diff (domain f) (brace x))))) + +(defthm domain-except + (implies (pairsp f) + (= (domain (except f x v)) + (scons x (domain f)))) + :hints (("Goal" :in-theory (enable except)))) + +; The range of (except f x v) is harder to characterize. If f is +; not a function, then (except f x v) might be. The range of f +; might include many things that are removed by the except. + +(defthm range-scons + (= (range (scons e f)) + (scons (tl e) (range f)))) + +(defthm subsetp-range-except + (subsetp (range (except f x v)) + (scons v (range f))) + :hints (("Goal" :in-theory (enable except)))) + +; We have these two, even though the union is not necessarily a +; function. + +(defthm domain-union + (= (domain (union f g)) + (union (domain f) (domain g)))) + +(defthm range-union + (= (range (union f g)) + (union (range f) (range g)))) + +(defthm cardinality-domain + (<= (cardinality (domain f)) (cardinality f)) + :rule-classes :linear) + +(defthm cardinality-range + (<= (cardinality (range f)) (cardinality f)) + :rule-classes :linear) + +(defthm ur-element-subset-such-that1 + (implies (pairsp f) + (equal (ur-elementp (subset-such-that1 f x)) + (not (mem x (domain f)))))) + +(defthm cardinality-<=-0 + (equal (< 0 (cardinality a)) + (not (ur-elementp a)))) + +(defthm cardinality-domain-functionp + (implies (functionp f) + (equal (cardinality (domain f)) + (cardinality f))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm subset-such-that1-empty + (implies (not (mem e (domain b))) + (= (subset-such-that1 b e) + nil))) + +; Is the (pairsp b) hypothesis below necessary? Yes. Here is a counterexample +; of the formula without the hypothesis. + +#|(let ((b (brace 123)) + (a (brace (pair nil 33))) + (pair (pair nil 2))) + (equal (functionp1 a (scons pair b)) + (if (and (pairp pair) + (mem (hd pair) (domain a))) + (and (functionp1 a b) + (or (mem pair b) + (not (mem (hd pair) (domain b))))) + (functionp1 a b))))|# + +(defthm functionp1-scons + (implies (pairsp b) + (equal (functionp1 a (scons pair b)) + (if (and (pairp pair) + (mem (hd pair) (domain a))) + (and (functionp1 a b) + (or (mem pair b) + (not (mem (hd pair) (domain b))))) + (functionp1 a b))))) + +(defthm cardinality-<=-1-cases + (iff (< 1 (cardinality x)) + (not (or (ur-elementp x) + (equal (cardinality x) 1))))) + +(defthm functionp-scons-lemma + (implies (and (functionp1 a b) + (subsetp a b) + (pairsp b) + (mem e a)) + (equal (cardinality (subset-such-that1 b (hd e))) + 1))) + +; Note that the following theorem is essentially a recursive +; alternative definition of functionp. + +(defthm functionp-scons + (equal (functionp (scons e a)) + (if (ur-elementp a) + (pairp e) + (and (functionp a) + (pairp e) + (or (mem e a) + (not (mem (hd e) (domain a))))))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm functionp-union + (implies (and (functionp a) + (functionp b) + (not (intersection (domain a) (domain b)))) + (functionp (union a b)))) + +(defthm disjoint-domains-implies-disjoint + (implies (not (intersection (domain a) (domain b))) + (not (intersection a b))) + :rule-classes nil) + +(defthm cardinality-except + (implies (functionp f) + (= (cardinality (except f x v)) + (if (mem x (domain f)) + (cardinality f) + (+ 1 (cardinality f))))) + :hints (("Goal" + :use ((:instance cardinality-domain-functionp (f (except f x v))) + (:instance cardinality-domain-functionp (f f))) + :in-theory (disable cardinality-domain-functionp)))) + +(defthm apply-outside-domain + (implies (not (mem e (domain f))) + (= (apply f e) nil)) + :hints (("Goal" :in-theory (enable apply)))) + +;---------------------------------------------------------------------------- +; Restrictions + +; I can think of three slightly different ways to define the restriction +; of a function f to some domain s. + +; (1) Iterate over s and make a function of the defined values. This +; always produces a function. However, if f is not a function, the +; function it produces is sort of unpredictable because it uses apply, +; so the restricted function chooses the largest pairs. + +(defun restrict (f s) + (cond ((ur-elementp s) nil) + ((mem (scar s) (domain f)) + (except (restrict f (scdr s)) + (scar s) + (apply f (scar s)))) + (t (restrict f (scdr s))))) + +; (2) Iterate over f and make a function of the values of elements of +; s. This always produces a function. But if f is not a function, +; the restricted function is unpredictable because it chooses the +; first pair presented for each domain element. I reject this +; definition because it does not do the ``normal'' things with a +; function. The normal things you do with a function are enquire +; about its domain and apply it. Looking at its internal structure is +; an invitation to low-level work. + +; (defun restrict2 (f s) +; (cond ((ur-elementp f) nil) +; ((and (pairp (scar f)) +; (mem (hd (scar f)) s)) +; (except (restrict2 (scdr f) s) +; (hd (scar f)) +; (tl (scar f)))) +; (t (restrict2 (scdr f) s)))) + +; (3) Iterate over f and collect everything whose hd is in s. The +; result may not be a function, but it is if f is. This has the +; appeal of being really simple, but, again, uses f in an abnormal +; way. + +; (defun restrict3 (f s) +; (cond ((ur-elementp f) nil) +; ((mem (hd (scar f)) s) +; (scons (scar f) (restrict3 (scdr f) s))) +; (t (restrict3 (scdr f) s)))) + +(defx :strategy :congruence (restrict f s) 1) + +; Next we prove that the second argument of restrict admits = as a +; congruence relation. For some reason it took me a while to +; realize that if you are going to prove that something is a +; subset of (restrict f s) you must be able to answer the question +; ``when is e a member of (restrict f s)?'' I was seeing this question +; come up and generalized it to ``when is e a member of a function?'' +; Answering that was harder than answering it for (restrict f s), +; which is always a function but which is built in a way that makes +; it easier to answer the question. Here is how you do it. + +; The system can prove mem-restrict, below, without further help. It +; generates three inductively proved subgoals. These are not worth +; turning into rules because mem-restrict, once proved, is better than +; each of them. + +(defthm mem-restrict + (equal (mem e (restrict f s)) + (and (pairp e) + (mem (hd e) (domain f)) + (= (tl e) (apply f (hd e))) + (mem (hd e) s))) + :hints (("Goal" :do-not '(generalize)))) + +; At first I wrote (= (restrict f s) nil) instead of the inner equal. +; But I really need the stronger equal because in the defcong= proof +; below the question of whether (restrict f s) is a set comes up. To +; be a set it must be either not an ur-element or nil. This means +; that we end up testing (restrict f s) against nil in a propositional +; setting, not a set theory setting. Since = does not refine iff +; (because '(:UR-CONS NIL) is canonicalized to NIL), knowing that +; (restrict f s) is not = nil does not help us. + +(defthm ur-elementp-restrict + (equal (ur-elementp (restrict f s)) + (equal (restrict f s) nil))) + +(defx :strategy :congruence (restrict f s) 2 :method :subsetp) + +(defthm functionp-restrict + (functionp (restrict f s))) + +; My next main goal is the fundamental fact characterizing the elements +; of a function. + +; Perhaps disable this when we're done? + + +(defthm pigeon-hole-1 + (implies (and (mem e a) + (mem d a) + (equal (cardinality a) 1)) + (= e d)) + :rule-classes nil) + +; The next three theorems are trivial consequences of other lemmas +; given the fact that (choose a) is an element of a. I really ought +; to provide macros that capture these kind of theorems. The idea in +; all of them is that if every element of a has some property then +; (choose a) has that property if a is non-empty. + +(defthm hd-choose-subset-such-that1 + (= (hd (choose (subset-such-that1 f x))) + (if (ur-elementp (subset-such-that1 f x)) + nil + x)) + :hints (("Goal" + :in-theory (disable mem-choose) + :use ((:instance mem-choose + (a (subset-such-that1 f x))))))) + +(defthm pairp-choose-subset-such-that1 + (implies (pairsp f) + (equal (pairp (choose (subset-such-that1 f x))) + (and (not (ur-elementp f)) + (mem x (domain f))))) + :hints (("Goal" + :in-theory (cons 'equal-booleans + (disable mem-choose)) + :use ((:instance mem-choose + (a (subset-such-that1 f x))))))) + +(defthm mem-choose-subset-such-that1 + (implies (pairsp f) + (equal (mem (choose (subset-such-that1 f x)) f) + (and (not (ur-elementp f)) + (mem x (domain f))))) + :hints (("Goal" + :in-theory (cons 'equal-booleans + (disable mem-choose)) + :use ((:instance mem-choose + (a (subset-such-that1 f x))))))) + +; This is a pretty obscure fact, I think. If x is a pair in f and +; there is only one pair in f with its hd, then choose chooses x. + +(defthm mem-x-implies-not-ur-elementp-subset-such-that1 + (implies (and (mem x f) + (pairp x)) + (not (ur-elementp (subset-such-that1 f (hd x)))))) + +(defthm choose-subset-such-that1 + (implies (and (<= (cardinality (subset-such-that1 f (hd x))) 1) + (mem x f) + (pairp x) + (pairsp f)) + (= (choose (subset-such-that1 f (hd x))) + x)) + :hints (("Goal" + :use (:instance pigeon-hole-1 + (e x) + (d (choose (subset-such-that1 f (hd x)))) + (a (subset-such-that1 f (hd x))))))) + +(defthm functionp-implies-mem-1 + (implies (and (functionp1 a f) + (pairsp f) + (subsetp a f) + (mem hd (domain a))) + (mem (pair hd (tl (choose (subset-such-that1 f hd)))) + f))) + +(defthm functionp-implies-mem-2 + (implies (and (functionp1 a f) + (pairsp f) + (subsetp a f) + (mem (hd x) (domain a)) + (pairp x) + (mem x f)) + (= (choose (subset-such-that1 f (hd x))) + x))) + +; This is the fundamental fact about membership in a function. It +; loops if made into a rewrite rule. + +(defthm mem-functionp + (implies (functionp f) + (equal (mem e f) + (and (pairp e) + (mem (hd e) (domain f)) + (= (tl e) (apply f (hd e)))))) + :rule-classes nil + :hints (("Goal" + :in-theory (enable functionp apply equal-booleans)))) + +(defthm domain-restrict + (= (domain (restrict f s)) + (intersection s (domain f)))) + +(defthm apply-restrict + (implies (and (mem x (domain f)) + (mem x s)) + (= (apply (restrict f s) x) + (apply f x)))) + +(defthm except-scdr-scar-elim + (implies (and (functionp f) + (not (ur-elementp f))) + (= (except (scdr f) (hd (scar f)) (tl (scar f))) + f)) + :otf-flg t + :hints + (("Goal" + :in-theory (enable except functionp equal-pair-generalized) + :use ((:instance mem-functionp + (e (pair (hd (scar f)) (tl (scar f)))) + (f f)) + (:instance mem-singleton + (e (pair (hd (scar f)) (tl (scar f)))) + (x (subset-such-that1 (scdr f) (hd (scar f))))))))) + +(defthm functionp-nil + (implies (ur-elementp f) + (equal (functionp f) (= f nil))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm functionp-pairp + (implies (not (pairp x)) + (not (functionp (scons x y)))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm except-scdr-scar-elim-special-case + (implies (and (functionp f) + (not (ur-elementp f)) + (ur-elementp (scdr f))) + (= (except nil (hd (scar f)) (tl (scar f))) + f)) + :hints (("Goal" :in-theory (enable except)))) + +(defthm functionp-scdr + (implies (functionp f) + (functionp (scdr f))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm restrict-domain + (implies (and (functionp f) + (functionp g) + (subsetp f g)) + (= (restrict g (domain f)) f)) + :hints + (("Subgoal *1/4" + :use ((:instance mem-functionp (e (scar f)) (f g)))))) + +; The lemma above will rewrite (restrict a (domain a)) to a, provided +; (functionp a). But it is often the case that the domain expression +; will be rewritten to something else, e.g., an intersection. So +; we provide a bridge. + +(defthm restrict-domain-special-case + (implies (and (functionp f) + (= a (domain f))) + (= (restrict f a) f))) + +(defthm restrict-scons + (= (restrict f (scons e s)) + (if (mem e (domain f)) + (except (restrict f s) + e + (apply f e)) + (restrict f s)))) + +; ---------------------------------------------------------------------------- +; Strategies for Proving Functions and Sets Equivalent + +(encapsulate ((functional-equiv-fn1 () t) + (functional-equiv-fn2 () t)) + (local (defun functional-equiv-fn1 nil nil)) + (local (defun functional-equiv-fn2 nil nil)) + (defthm functional-equivalence-constraint-1 + (functionp (functional-equiv-fn1))) + (defthm functional-equivalence-constraint-2 + (functionp (functional-equiv-fn2))) + (defthm functional-equivalence-constraint-3 + (= (domain (functional-equiv-fn2)) + (domain (functional-equiv-fn1)))) + +; We use the unusual variable name fex (``functional equivalence x'') because +; any variable appearing in a constraint is prohibited from occurring in +; any theorem proved with functional-instantiation from this constraint. + + (defthm functional-equivalence-constraint-4 + (implies (mem fex (domain (functional-equiv-fn1))) + (= (apply (functional-equiv-fn1) fex) + (apply (functional-equiv-fn2) fex))))) + +(defun every-where-= (s f g) + (cond ((ur-elementp s) t) + (t (and (= (apply f (scar s)) + (apply g (scar s))) + (every-where-= (scdr s) f g))))) + +(defthm every-where-=-implies-=-restrict + (implies (and (functionp f) + (functionp g) + (subsetp s (domain f)) + (subsetp s (domain g)) + (every-where-= s f g)) + (= (restrict f s) + (restrict g s))) + :rule-classes nil) + +(encapsulate + nil + (local + (defthm every-where-=-functional-equiv-fn1-functional-equiv-fn2 + (implies (subsetp s (domain (functional-equiv-fn1))) + (every-where-= s (functional-equiv-fn1) (functional-equiv-fn2))))) + + (defthm functional-equivalence-theorem + (= (functional-equiv-fn1) (functional-equiv-fn2)) + :rule-classes nil + :hints (("Goal" + :use (:instance every-where-=-implies-=-restrict + (f (functional-equiv-fn1)) + (g (functional-equiv-fn2)) + (s (domain (functional-equiv-fn1)))))))) + +; The above encapsulation provides a nice way to prove two functions +; are equal. You can just instantiate the lemma above with any two +; functions that are known to have the same domain and that are +; apply-equal everywhere. + +(defmacro functional-equivalence (name term + &key + hints + (rule-classes 'nil rule-classesp) + (otf-flg 'nil otf-flgp)) + (let* ((xterm + (acl2::case-match + term + (('implies acl2::& ('= acl2::& acl2::&)) + term) + (('= acl2::& acl2::&) + `(implies t ,term)) + (t nil)))) + (cond + ((null xterm) + `(acl2::er acl2::soft 'functional-equivalence + "The functional-equivalence strategy requires a term of ~ + the form (= f g) or (implies h (= f g)). Your term, ~x0, ~ + is not of this form." + ',term)) + ((acl2::assoc-equal "Goal" hints) + `(acl2::er acl2::soft 'functional-equivalence + "The functional-equivalence strategy provides hints for ~ + \"Goal\". Your hints should be provided for some Subgoal.")) + (t + (let ((hyps (cadr xterm)) + (lhs (cadr (caddr xterm))) + (rhs (caddr (caddr xterm)))) + `(defthm ,name ,term + :hints + (("Goal" + :use ((:functional-instance + functional-equivalence-theorem + (functional-equiv-fn1 + (lambda () + ,(if (eq hyps t) + lhs + `(if ,hyps ,lhs nil)))) + (functional-equiv-fn2 + (lambda () + ,(if (eq hyps t) + rhs + `(if ,hyps ,rhs nil))))))) + ,@hints) + ,@(if rule-classesp + `(:rule-classes ,rule-classes) + nil) + ,@(if otf-flgp + `(:otf-flg ,otf-flg) + nil))))))) + +; While I'm at it, I'll provide a way to prove that two sets are equal. + +; Suppose you have two arbitrary sets with the property that if x is a +; member of one, then x is a member of the other. + +(encapsulate ((subsetp-strategy-set1 () t) + (subsetp-strategy-set2 () t)) + (local (defun subsetp-strategy-set1 () nil)) + (local (defun subsetp-strategy-set2 () nil)) + +; We use the unusual variable name ssx (``subsetp strategy x'') because whatever +; var we use in a constraint is off-limits to the user in any theorem proved +; via functional instantiation based on these constraints. + + (defthm subsetp-strategy-constraint + (implies (mem ssx (subsetp-strategy-set1)) + (mem ssx (subsetp-strategy-set2))))) + +; Then the first set is a subset of the second. + +(encapsulate + nil + (local + (defthm subsetp-strategy-lemma + (implies (subsetp a (subsetp-strategy-set1)) + (subsetp a (subsetp-strategy-set2))))) + + (defthm subsetp-strategy + (subsetp (subsetp-strategy-set1) + (subsetp-strategy-set2)) + :rule-classes nil)) + +; And here is a handy macro to use this strategy to prove the subsetp +; relation between two expressions under a hypothesis. + +; This macro allows us to write: +; (defx foo (subsetp ... ...) +; :strategy subset-relation +; :rule-classes ...) + +(defmacro subset-relation (name term + &key + hints + (rule-classes 'nil rule-classesp) + (otf-flg 'nil otf-flgp)) + (let* ((xterm + (acl2::case-match + term + (('implies acl2::& ('subsetp acl2::& acl2::&)) + term) + (('subsetp acl2::& acl2::&) + `(implies t ,term)) + (t nil)))) + (cond + ((null xterm) + `(acl2::er acl2::soft 'subset-relation + "The subset-relation strategy requires a term of ~ + the form (subsetp a b) or (implies h (subsetp a b)). Your term, ~x0, ~ + is not of this form." + ',term)) + ((acl2::assoc-equal "Goal" hints) + `(acl2::er acl2::soft 'subset-relation + "The subset-relation strategy provides hints for ~ + \"Goal\". Your hints should be provided for some Subgoal.")) + (t + (let ((hyps (cadr xterm)) + (lhs (cadr (caddr xterm))) + (rhs (caddr (caddr xterm)))) + `(defthm ,name ,term + :hints + (("Goal" + :use ((:functional-instance + subsetp-strategy + (subsetp-strategy-set1 + (lambda () + ,(if (eq hyps t) + lhs + `(if ,hyps ,lhs nil)))) + (subsetp-strategy-set2 + (lambda () + ,(if (eq hyps t) + rhs + `(if ,hyps ,rhs nil))))))) + ,@hints) + ,@(if rule-classesp + `(:rule-classes ,rule-classes) + nil) + ,@(if otf-flgp + `(:otf-flg ,otf-flg) + nil))))))) + +; Here is a way to set equality using two subsets. It requires +; proving (mem x a) <-> (mem x b). + +; We can thus write +; (defx foo (implies ... (= ... ...)) +; :strategy equivalence-relation +; :rule-classes ...) + +; Two proof obligations are generated, each a mem implying a mem. You +; can provide hints for them with :hints-1 and :hints-2. + +(defmacro set-equivalence (name term + &key hints + (rule-classes 'nil rule-classesp) + (otf-flg 'nil otf-flgp) + (hints-1 'nil hints-1p) + (otf-flg-1 'nil otf-flg-1p) + (hints-2 'nil hints-2p) + (otf-flg-2 'nil otf-flg-2p)) + (let* ((xterm + (acl2::case-match term + (('implies acl2::& ('= acl2::& acl2::&)) + term) + (('= acl2::& acl2::&) + `(implies t ,term)) + (t nil)))) + (cond + ((null xterm) + `(acl2::er acl2::soft 'set-equivalence + "~x0 is not of the form (= x y) or of the form ~ + (implies hyps (= x y))." + ',term)) + ((or (acl2::assoc-equal "Goal" hints) + (acl2::assoc-equal "Goal" hints-1) + (acl2::assoc-equal "Goal" hints-2)) + `(acl2::er acl2::soft 'set-equivalence + "The set-equivalence strategy provides hints for ~ + \"Goal\". Your hints should be provided for some Subgoal.")) + (t + (let ((hyps (cadr xterm)) + (lhs (cadr (caddr xterm))) + (rhs (caddr (caddr xterm))) + (name-1 (packn-in-pkg (list name "-1") name)) + (name-2 (packn-in-pkg (list name "-2") name))) + `(encapsulate + nil + (local + (defx ,name-1 + ,(if (eq hyps t) + `(subsetp ,lhs ,rhs) + `(implies ,hyps (subsetp ,lhs ,rhs))) + :strategy subset-relation + ,@(if hints-1p `(:hints ,hints-1) nil) + ,@(if otf-flg-1p `(:otf-flg ,otf-flg-1) nil) + :rule-classes nil)) + (local + (defx ,name-2 + ,(if (eq hyps t) + `(subsetp ,rhs ,lhs) + `(implies ,hyps (subsetp ,rhs ,lhs))) + :strategy subset-relation + ,@(if hints-2p `(:hints ,hints-2) nil) + ,@(if otf-flg-2p `(:otf-flg ,otf-flg-2) nil) + :rule-classes nil)) + (defthm ,name ,term + :hints + (("Goal" + :use ((:instance =-iff-subsetps + (a ,(if (eq hyps t) + lhs + `(if ,hyps ,lhs nil))) + (b ,(if (eq hyps t) + rhs + `(if ,hyps ,rhs nil)))) + (:instance ,name-1) + (:instance ,name-2)) + ,@hints)) + ,@(if rule-classesp + `(:rule-classes ,rule-classes) + nil) + ,@(if otf-flgp + `(:otf-flg ,otf-flg) + nil)))))))) + +; ---------------------------------------------------------------------------- +; An Example + +(defx union-diff-diff + (implies (and (subsetp a b) + (subsetp b c)) + (= (union (diff b a) + (diff c b)) + (diff c a))) + :strategy :set-equivalence) + +;---------------------------------------------------------------------------- +; Sequences + +; A sequence is a function whose domain is an initial subset of the +; natural numbers. + +(defun nats (n) + (if (zp n) + '(0) + (scons n (nats (- n 1))))) + +(defthm ur-elementp-nats + (not (ur-elementp (nats n)))) + +(defcong = = (nats n) 1 + :hints (("Goal" :in-theory (enable zp)))) + +(defthm mem-nats + (equal (mem e (nats n)) + (and (integerp e) + (<= 0 e) + (<= e (nfix n)))) + :hints (("Goal" :in-theory (enable =)))) + +(defun sequencep (s) + (and (functionp s) + (= (domain s) + (diff (nats (cardinality s)) '(0))))) + +(defthm functionp-sequencep + (implies (sequencep s) + (functionp s))) + +(defthm domain-sequencep + (implies (sequencep s) + (= (domain s) + (diff (nats (cardinality s)) '(0))))) + +(in-theory (disable sequencep)) + +(defun shift (i j f delta) + (declare (xargs :measure (nfix (- (+ 1 (acl2::ifix j)) (acl2::ifix i))))) + (cond ((and (integerp i) + (integerp j) + (<= i j)) + (except (shift (+ 1 i) j f delta) + (+ i delta) + (apply f i))) + (t nil))) + +(defcong = = (shift i j f delta) 1) +(defcong = = (shift i j f delta) 2) +(defcong = = (shift i j f delta) 3) +(defcong = = (shift i j f delta) 4) + +(defthm functionp-shift + (functionp (shift i j f delta))) + +; If f is a sequence, its domain is [1...n]. So (shift i j f delta) +; takes [i...j] to [i+delta ... j+delta]. This is + +(defthm mem-domain-shift + (implies (integerp delta) + (= (mem x (domain (shift i j f delta))) + (and (integerp i) + (integerp j) + (<= i j) + (integerp x) + (<= (+ i delta) x) + (<= x (+ j delta)))))) + +; We can express the domain of a shift of a sequence as a set of nats. + +(defx domain-shift + (implies (and (sequencep s) + (integerp delta) + (<= 0 delta)) + (= (domain (shift 1 (cardinality s) s delta)) + (diff (nats (+ delta (cardinality s))) + (nats delta)))) + :strategy :set-equivalence) + +(defun concat (r s) + (union r (shift 1 (cardinality s) s (cardinality r)))) + +(defcong = = (concat r s) 1) +(defcong = = (concat r s) 2) + +(defthm functionp-concat + (implies (and (sequencep r) + (sequencep s)) + (functionp (concat r s)))) + +(defthm subsetp-nats-0 + (subsetp '(0) (nats i))) + +(defthm =-0 + (equal (= i 0) + (equal i 0)) + :hints (("Goal" :in-theory (enable =)))) + +(defthm subsetp-nats-nats + (equal (subsetp (nats i) (nats j)) + (<= (nfix i) (nfix j)))) + +(defthm domain-concat + (implies (and (sequencep r) + (sequencep s)) + (= (domain (concat r s)) + (diff (nats (+ (cardinality r) (cardinality s))) + '(0))))) + +; I need the (integerp delta) hypothesis because cardinality raises +; the question of membership in the shifted domain and +; mem-domain-shift has an integerp hyp. + +(defthm cardinality-shift + (implies (integerp delta) + (= (cardinality (shift i j f delta)) + (if (and (integerp i) + (integerp j) + (<= i j)) + (+ 1 (- j i)) + 0)))) + +(defthm cardinality-concat + (implies (and (sequencep r) + (sequencep s)) + (= (cardinality (concat r s)) + (+ (cardinality r) (cardinality s)))) + :hints (("Goal" + :use (:instance disjoint-domains-implies-disjoint + (a r) + (b (shift 1 (cardinality s) s (cardinality r))))))) + +(defthm sequencep-concat + (implies (and (sequencep r) + (sequencep s)) + (sequencep (concat r s))) + :hints (("Goal" + :in-theory + (set-difference-theories (enable sequencep) + '(concat))))) + +; Here is a recursive alternative definition of apply. + +(defthm apply-scons + (implies (functionp (scons pair f)) + (= (apply (scons pair f) x) + (if (= (hd pair) x) + (tl pair) + (apply f x)))) + :hints (("Goal" :in-theory (enable apply)) + ("Subgoal 2.1'" + :in-theory (set-difference-theories (enable functionp) + '(functionp-scons-lemma)) + + :use ((:instance functionp-scons-lemma + (a f) + (b f) + (e (pair hd tl))) + (:instance mem-singleton + (x (subset-such-that1 f hd)) + (e (pair hd tl))))))) + +(defthm apply-disjoint-union + (implies (and (functionp a) + (functionp b) + (not (intersection (domain a) (domain b)))) + (= (apply (union a b) x) + (if (mem x (domain a)) + (apply a x) + (apply b x))))) + +; Suppose you have a function, f, (not necessarily a sequence) and you +; form another function, f', by shifting [i...j] of f up by delta. +; What is (apply f' x)? The domain of f' is [i+delta ... j+delta]. +; If x is in that domain, then (apply f' x) is (apply f (- x delta)). + +; To prove this we need the important fact: + +(defthm apply-shift + (= (apply (shift i j f delta) x) + (if (mem x (domain (shift i j f delta))) + (apply f (- x delta)) + nil))) + +(defthm apply-concat + (implies (and (sequencep r) + (sequencep s)) + (= (apply (concat r s) i) + (cond ((and (integerp i) + (< 0 i)) + (if (<= i (cardinality r)) + (apply r i) + (apply s (- i (cardinality r))))) + (t nil)))) + :hints (("Subgoal 11" + :in-theory (disable apply-outside-domain) + :use + ((:instance apply-outside-domain + (e (- i (cardinality r))) + (f s)))))) + +(in-theory (disable concat)) + +(defx associativity-of-concat + (implies (and (sequencep a) + (sequencep b) + (sequencep c)) + (= (concat (concat a b) c) + (concat a (concat b c)))) + :strategy :functional-equivalence) + +; Now I will define seq-hd and seq-tl to let me do recursion down +; sequences. + +(defun seq-hd (s) (apply s 1)) + +(defcong = = (seq-hd s) 1) + +(defun seq-tl (s) + (restrict (shift 1 (cardinality s) s -1) + (diff (nats (- (cardinality s) 1)) + (brace 0)))) + +(defcong = = (seq-tl s) 1) + +(defthm functionp-seq-tl + (functionp (seq-tl s))) + +(defthm cardinality-restrict + (= (cardinality (restrict f s)) + (cardinality (intersection (domain f) s)))) + + + +(defx domain-shift-generalized + (implies (and (integerp i) + (integerp j) + (<= i j) + (integerp delta) + (<= 0 (+ i delta))) + (= (domain (shift i j s delta)) + (if (= (+ delta i) 0) + (nats (+ delta j)) + (diff (nats (+ delta j)) + (nats (+ delta i -1)))))) + :strategy :set-equivalence) + +(defthm cardinality-positive + (implies (not (ur-elementp s)) + (< 0 (cardinality s))) + :rule-classes :linear) + +(defthm intersection-x-x + (= (intersection x x) (sfix x))) + +(defthm cardinality-diff-nats-0 + (implies (and (integerp i) + (<= 0 i)) + (= (cardinality (diff (nats i) '(0))) + i))) + +(defthm cardinality-seq-tl + (implies (not (ur-elementp s)) + (= (cardinality (seq-tl s)) + (- (cardinality s) 1)))) + +(defthm sequencep-seq-tl + (implies (not (ur-elementp s)) + (sequencep (seq-tl s))) + :hints (("Goal" :in-theory (enable sequencep)))) + +(defthm seq-tl-recursion + (implies (not (ur-elementp s)) + (< (cardinality (seq-tl s)) + (cardinality s))) + :rule-classes (:built-in-clause :linear)) + +(in-theory (disable seq-hd seq-tl)) + +; Next, I define defmap. Thus, + +; (defmap subset (a s b) :for x :in s :such-that (bd a x b)) +; and +; (defmap image (a s b) :for x :in s :map (bd a x b)) + +; will define subset and image recursively so that they return the +; sets described below + +; (subset a s b) = {x in s | (bd a x b)} +; and +; (image a s b) = {(bd a x b) | x in s} + +; In addition, I get a few useful theorems about these functions, including +; that = is a congruence for every argument. + +; It must be the case that congruence rules are already in place for +; (bd a x b). + +(defun defmap-congruences (vars call sloc i) + (cond + ((endp vars) nil) + (t (cons (if (equal sloc i) + `(defx :strategy :congruence ,call ,i :method :subsetp) + `(defx :strategy :congruence ,call ,i)) + (defmap-congruences (cdr vars) call sloc (+ 1 i)))))) + +(defmacro defmap (name vars + &key + (for 'nil forp) + (in 'nil inp) + (such-that 'nil such-thatp) + (map 'nil mapp)) + +; (defmap foo (s ...) :for x :in s :such-that px) +; or +; (defmap foo (s ...) :for x :in s :map px) + + (cond + ((not (and (symbolp name) + (acl2::symbol-listp vars) + forp + (symbolp for) + (not (acl2::member-equal for vars)) + inp + (symbolp in) + (acl2::member-equal in vars) + (or (and such-thatp (not mapp)) + (and (not such-thatp) mapp)))) + `(acl2::er acl2::soft 'defmap + "The proper form of a defmap command is~%~ + (defmap name vars :for x :in v :such-that body)~%~ + or~%~ + (defmap name vars :for x :in v :map body),~%~ + where name is a new function name, vars is a list of ~ + variables, x is a variable not in vars, ~ + v is a variable in vars, and body is a term.")) + (such-thatp + (let* ((x for) + (s in) + (sloc (- (length vars) (length (member s vars)))) + (body such-that) + (s1 (genname1 s 1 (cons x vars))) + (call `(,name ,@vars)) + (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars)))) + `(encapsulate + nil + (defun ,name (,@vars) + (if (ur-elementp ,s) + nil + (let ((,x (scar ,s))) + (if ,body + (scons (scar ,s) ,rcall) + ,rcall)))) + + (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap) + (setp ,call)) + + (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap) + (equal (ur-elementp ,call) + (equal ,call nil))) + + (defthm ,(packn-in-pkg (list "MEM-" name) 'defmap) + (equal (mem ,x ,call) + (and ,body ; we write it this way in case body + (mem ,x ,s))) ; is not Boolean! + :otf-flg t) + + (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap) + (subsetp ,call ,s)) + + ,@(defmap-congruences vars call (+ sloc 1) 1) + + (defthm ,(packn-in-pkg (list "MEM-" name "-CORROLLARY") 'defmap) + (implies (and (subsetp ,s1 ,call) + (mem ,x ,s1)) + ,body)) + + (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap) + (<= (cardinality ,call) + (cardinality ,s)) + :rule-classes :linear) + + (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap) + (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars)) + (union (,name ,@(put-nth s1 sloc vars)) + ,call))) + + (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap) + (= (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars)) + (intersection (,name ,@(put-nth s1 sloc vars)) + ,call))) + + ))) + (t ;;; :map + + (let* ((x for) + (s in) + (sloc (- (length vars) (length (member s vars)))) + (body map) + (fx (genname1 x 1 (cons x vars))) + (s1 (genname1 s 1 (cons fx (cons x vars)))) + (call `(,name ,@vars)) + (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars)))) + `(encapsulate + nil + (defun ,name (,@vars) + (if (ur-elementp ,s) + nil + (let ((,x (scar ,s))) + (scons ,body ,rcall)))) + + (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap) + (setp ,call)) + + (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap) + (equal (ur-elementp ,call) + (ur-elementp ,s))) + + (defthm ,(packn-in-pkg (list "WEAK-MEM-" name) 'defmap) + (implies (and (mem ,x ,s) + (= ,fx ,body)) + (mem ,fx ,call))) + + + (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap) + (implies (subsetp ,s1 ,s) + (subsetp (,name ,@(put-nth s1 sloc vars)) + ,call))) + + ,@(defmap-congruences vars call (+ sloc 1) 1) + + (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap) + (<= (cardinality ,call) + (cardinality ,s)) + :rule-classes :linear) + + (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap) + (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars)) + (union (,name ,@(put-nth s1 sloc vars)) + ,call))) + +; Once I thought that +; (image (intersection s1 s)) = (intersection (image s1) (image s)) +; But this is wrong. Consider +; s1 = {(0 . 1) (0 . 2)} +; s = {(1 . 1) (1 . 2)} +; let (body e) = (cdr e) (or (tl e) if the elements are pairps) +; Then the lhs is nil because the two sets are disjoint, but the +; rhs is {1 2}. + + (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap) + (subsetp (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars)) + (intersection (,name ,@(put-nth s1 sloc vars)) + ,call))) + + ))))) + +#| +; Here are examples of both styles of defmap: + +(defstub bd (a x b) t) +(acl2::skip-proofs + (progn (defcong = = (bd a x b) 1) + (defcong = = (bd a x b) 2) + (defcong = = (bd a x b) 3))) + +(defmap subset (a s b) :for x :in s :such-that (bd a x b)) +(defmap image (a s b) :for x :in s :map (bd a x b)) + +|# + diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl2 b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl2 new file mode 100644 index 0000000..cbe122f --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.acl2 @@ -0,0 +1,24 @@ +(value :q) + +(LP) + +(defpkg "S" + (set-difference-equal + (union-eq '(PACK + ORDINARYP + << + <<-IRREFLEXIVITY + <<-TRICHOTOMY + <<-MUTUAL-EXCLUSION + <<-TRANSITIVITY + FAST-<<-TRICHOTOMY + FAST-<<-MUTUAL-EXCLUSION + FAST-<<-TRANSITIVITY + FAST-<<-RULES + SLOW-<<-RULES + <<-RULES) + (union-eq *acl2-exports* + *common-lisp-symbols-from-main-lisp-package*)) + '(union intersection subsetp add-to-set functionp = apply))) + +(certify-book "set-theory" ? t) diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp new file mode 100644 index 0000000..6108bb5 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/set-theory.lisp @@ -0,0 +1,3232 @@ +; Finite Set Theory for ACL2 +; Copyright (C) 2001 Georgia Institute of Technology + +; This book is derived from the book "set-theory-original" by J Moore, +; which is included in this directory. The only difference between +; this version and J Moore's version is that I use the book +; "total-ordering" also in this directory instead of the orginal +; "total-ordering-original". This allows me to simplify some of the +; theorems and to also remove theorems. + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios +; email: manolios@cc.gatech.edu +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "S") + +(include-book "total-ordering") + +(defun ur-elementp (x) + (or (atom x) + (eq (car x) :UR-CONS))) + +; Example objects are +; 3 numbers +; #\A characters +; "Abc" strings +; ABC symbols +; (:UR-CONS (a b c)) lists +; (1 2 1 3 (:UR-CONS (a b c))) sets + +; Some Comments on :UR-CONS + +; It is simplest never to write the symbol :UR-CONS in your sets +; unless you mean to mark consp ur-elements. The symbol :UR-CONS if +; encountered in unexpected places produces counter-intuitive results. + +; For example, (1 2 :UR-CONS) might be thought of as {1 2 :UR-CONS} +; but in fact is {1 2}. The reason is that it is parsed as (1 2 +; . (:UR-CONS)). The enumeration of the elements of a set is +; terminated by the first ur-element cdr. So just as (1 2 . 3) is {1 +; 2}, so is (1 2 . (:UR-CONS ...)). Any attempt to include :UR-CONS +; as an element of an explicit set constant terminates the enumeration +; of the set elements and so fails to include :UR-CONS as an element. + +; Is it possible to use scons to add :UR-CONS to a list? You might +; expect (scons :UR-CONS '(1 2)) to be {:UR-CONS 1 2}. But it is in +; fact {CONS 1 2}. If you ever succeed in using :UR-CONS as an +; ur-element it is treated as though it were a non-canonical +; representation of the symbol ACL2::CONS. + +; These considerations make it simplest to avoid using :UR-CONS except +; in the syntax of sets. + +(defun set-insert (e s) + +; NIL is the only ur-elementp upon which set-insert is ever called, in +; the process of canonicalizing. But I prove theorems about +; set-insert and to make them simpler to state, I have it treat all +; ur-elements s as the empty set. Also, both e and s are assumed to +; be canonical. + + (cond ((ur-elementp s) (cons e nil)) + ((equal e (car s)) s) + ((<< e (car s)) + (cons (car s) + (set-insert e (cdr s)))) + (t (cons e s)))) + +(defun ur-fix (x) + +; This converts an arbitrary Lisp object into an ordinary ur-element +; without changing the type. We do not want to change the type so +; that set equality refines IFF and is a congruence relation for the +; arithmetic primitives in ACL2. We discuss the conversions below. + + (cond ((atom x) + (cond ((eq x :UR-CONS) 'ACL2::UR-CONS) + (t x))) + ((eq (car x) :UR-CONS) + (cond ((or (atom (cdr x)) + (atom (cadr x))) + '(:UR-CONS (NIL))) + (t (list :UR-CONS (cadr x))))) + (t nil))) + +; Conversions: +; (1) If we encounter :UR-CONS where an ur-element is expected, we convert it +; the symbol ACL2::UR-CONS. This prevents the accidental formation of +; a :UR-CONS by set operations on data containing :UR-CONS. For example, +; (scons :UR-CONS '(a b c)) will produce the set {ACL2::UR-CONS a b c}, not +; the set {:UR-CONS a b c} and not the ``ur-element'' (:UR-CONS a b c). +; (2) If we encounter (:UR-CONS . xxx) where an ur-element is expected, we +; are sure to return something of the form (:UR-CONS (...)). An ur-element +; marked :UR-CONS means a cons of some sort, no matter what is inside. +; A rough model of the conversion rule is that if the :UR-CONS expression +; is ill-formed it denotes (:UR-CONS (NIL)). More accurately, there are +; three cases: +; (a) (:UR-CONS . atom) => (:UR-CONS (NIL)) +; (b) (:UR-CONS atom . anything) => (:UR-CONS (NIL)) +; (c) (:UR-CONS (...) . anything) => (:UR-CONS (...)) + + +; (in-theory (disable ur-fix)) + +(defun canonicalize (x) + (cond ((ur-elementp x) (ur-fix x)) + ((ur-elementp (cdr x)) + (list (canonicalize (car x)))) + (t (set-insert (canonicalize (car x)) + (canonicalize (cdr x)))))) + + +(defun orderedp (x) + (cond ((ur-elementp x) t) + ((ur-elementp (cdr x)) t) + ((<< (cadr x) (car x)) + (orderedp (cdr x))) + (t nil))) + +(defun canonicalp (x) + (cond ((atom x) + (not (eq x :UR-CONS))) + ((eq (car x) :UR-CONS) + (and (consp (cdr x)) + (consp (cadr x)) + (equal (cddr x) nil))) + ((ur-elementp (cdr x)) + (and (canonicalp (car x)) + (equal (cdr x) nil))) + (t (and (canonicalp (car x)) + (canonicalp (cdr x)) + (orderedp x))))) + +(defthm orderedp-set-insert + (implies (and (canonicalp e) + (canonicalp a)) + (orderedp (set-insert e a))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm canonicalp-set-insert + (implies (and (canonicalp e) + (canonicalp a)) + (canonicalp (set-insert e a))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm canonicalp-ur-fix + (canonicalp (ur-fix X))) + +(defthm canonicalp-canonicalize + (canonicalp (canonicalize x))) + +(defthm canonicalize-canonicalp + (implies (canonicalp x) (equal (canonicalize x) x))) + +; So here is equality in our system. + +(defun = (x y) + (equal (canonicalize x) + (canonicalize y))) + +(defequiv =) + +; ---------------------------------------------------------------------------- +; The Set Constructor/Destructor Primitives + +; It is very convenient to pretend that sets are built as a new data +; type. So here are the basic functions. I will keep them enabled +; until I have proved the necessary facts about canonicalization, +; equality (=) and subsetp. Then I'll disable them. But I introduce +; them now so that mem and subsetp can be defined in terms of them. I +; have also collected together certain of their elementary properties. +; Most of these theorems are not used until after I have disabled +; these primitives. + +(defun sfix (a) + (if (ur-elementp a) + nil + a)) + +(defun scons (e a) + (if (equal e :UR-CONS) + (cons (canonicalize e) + (sfix a)) + (cons e (sfix a)))) + +; The macro below allows me to write (brace a b c) to mean {a, b, c}. + +(defmacro brace (&rest args) + (cond ((endp args) nil) + (t `(scons ,(car args) + (brace ,@(cdr args)))))) + +; Here are some timings of this entire library. These timings started +; when I began experimenting with three different flavors of scar and +; scdr. The flavors are shown below along with some Caerlaverock +; timings. I chose functionp1-set-insert as a representative expensive +; proof. + +; When these timings were done, there were 279 events and the last one +; was APPLY-RESTRICT. Since the book has probably changed since then, +; these timings are only relevant insofar as they reflect the relative +; effects of the various experiments. Even that claim is suspect: +; since doing these timings I have discovered that there can be a +; considerable difference (30%) between the time it takes in a fresh +; GCL and the time it takes to ``repeat'' the computation in a soiled +; GCL. Fresh GCL is faster. I did not record whether the times below +; were done in fresh system or not. + +; During the first three experiments, I had the <<-rules -- namely <<, +; transitivity, mutual-exclusion, and trichotomy -- disabled by +; default and turned them on during certain proofs. They were on +; during functionp1-set-insert, even though I eventually discovered +; they didn't have to be for the proof to go through. + +; functionp1-set-insert entire file + +(defun scar (a) +; (car a) ;;; 232 secs 1153 secs +; (if (equal (car a) :UR-CONS) nil (car a)) ;;; 404 secs 1212 secs + (if (ur-elementp a) nil (car a)) ;;; 308 secs 1239 secs + ) + +; I then learned that I did not have to have <<-rules enabled during +; the functionp1-set-insert proof or the analogous ones. So I took out +; those theory commands and got: + +; ;;; 2 secs 889 secs + +; Then I had the idea of coding up the ``fast << rules.'' Operating +; in the fast-<<-rules theory by default and occasionally either +; enabling << or switching over to the slow-<<-rules, I got the +; following times in a fresh GCL: + +; ;;; 2 secs 370 secs + + +(defun scdr (a) +; (sfix (cdr a)) +; (if (equal (car a) :UR-CONS) nil (sfix (cdr a))) + (if (ur-elementp a) nil (sfix (cdr a))) + ) + +(defcong = = (scons e a) 1 + :hints (("Goal" :in-theory (enable =)))) + +(defcong = = (scons e a) 2 + :hints (("Goal" :in-theory (enable =)))) + +(defthm scar-scons + (= (scar (scons e a)) e)) + +(defthm scdr-scons + (= (scdr (scons e a)) (sfix a))) + +(defthm ur-elementp-scar + (implies (ur-elementp x) (equal (scar x) nil))) + +(defthm ur-elementp-scdr + (implies (ur-elementp x) (equal (scdr x) nil))) + +(defun setp (x) + (or (equal x nil) + (not (ur-elementp x)))) + +(defthm setp-scdr + (setp (scdr a)) + :rule-classes (:type-prescription :generalize)) + +(defthm scons-scar-scdr + (implies (not (ur-elementp a)) + (= (scons (scar a) (scdr a)) a)) + :rule-classes :elim) + +(defthm acl2-count-scdr + (implies (not (ur-elementp a)) + (o< (acl2-count (scdr a)) + (acl2-count a))) + :rule-classes + ((:built-in-clause) + (:linear :corollary + (implies (not (ur-elementp a)) + (< (acl2-count (scdr a)) + (acl2-count a)))))) + +(defthm consp-set-insert + (consp (set-insert e a)) + :rule-classes :type-prescription) + +(defthm car-set-insert-not-equal-ur-cons + (implies (and (canonicalp e) + (canonicalp a)) + (not (equal (set-insert e a) (cons :UR-CONS x))))) + +(defcong = equal (ur-elementp x) 1) + +; Note: We will generally keep sfix enabled, so this rule will not be +; of much use. + +(defcong = = (sfix x) 1) + +(defthm not-ur-elementp-scons + (not (ur-elementp (scons e a)))) + +(defthm not-consp-implies-ur-elementp + (implies (not (consp e)) + (ur-elementp e))) + +(defthm scons-nil + (implies (and (syntaxp (not (equal a ''nil))) + (ur-elementp a)) + (= (scons e a) + (scons e nil)))) + +(defthm canonicalize-ur-cons + (not (equal (canonicalize x) :UR-CONS))) + +(defthm set-insert-set-insert + (implies (and (canonicalp e) + (canonicalp d) + (canonicalp a)) + (equal (set-insert e (set-insert d a)) + (set-insert d (set-insert e a)))) + :hints (("Goal" :induct (set-insert e a) + :in-theory (slow-<<-rules)))) + +; This rule lets us do a cross-fertilization without waiting for the +; prior elim. The version of this rule that rewrites (set-insert e xxx) +; to (set-insert d (set-insert e a)) has been known to cause infinite +; loops, even with a hand-picked :loop-stopper. + +(defthm set-insert-short-cut + (implies (and (equal xxx (set-insert d a)) + (canonicalp e) + (canonicalp d) + (canonicalp a)) + (equal (equal (set-insert e xxx) + (set-insert d (set-insert e a))) + t))) + +(defthm set-insert-dup + (implies (and (canonicalp e) + (canonicalp a)) + (equal (set-insert e (set-insert e a)) + (set-insert e a))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm scons-scons-2 + (= (scons e (scons d a)) + (scons d (scons e a)))) + +(defthm scons-scons-1 + (= (scons e (scons e a)) + (scons e a))) + +(defthm equal-singleton-set-insert + (implies (and (canonicalp e) + (canonicalp d) + (canonicalp a)) + (equal (equal (list e) (set-insert d a)) + (and (equal e d) + (or (equal (sfix a) nil) + (equal (list e) a))))) + :hints (("Goal" :induct (set-insert d a)))) + +(defthm car-set-insert + (implies (and (canonicalp e) + (canonicalp a)) + (equal (car (set-insert e a)) + (if (ur-elementp a) + e + (if (<< (car a) e) + e + (car a))))) + :hints (("Goal" + :induct (set-insert e a) + :in-theory (enable ur-elementp)))) + +(defthm =-singletons + (equal (= (scons e nil) (scons d a)) + (and (= e d) + (or (ur-elementp a) + (= (scons e nil) a)))) + :hints (("Goal" :in-theory (enable = scons ur-elementp))) + :rule-classes + ((:rewrite) + (:rewrite :corollary + (equal (= (scons d a) (scons e nil)) + (and (= e d) + (or (ur-elementp a) + (= (scons e nil) a)))) + +; Note: This hint is required here because we do not know that +; = is commutative (except by opening it up)! + + :hints (("Goal" :in-theory (enable =)))))) + +; Basic... +(defun <<-cons-1-hint (x y) + (if (consp x) + (list (<<-cons-1-hint (car x) (cdr x))) + y)) + +(defthm <<-cons-1 + (<< x (cons x y)) + :hints (("Goal" :induct (<<-cons-1-hint x y) + :in-theory (cons 'acl2::lexorder (slow-<<-rules <<))))) + +(defthm not-=-x-set-insert-x + (implies (and (canonicalp e) + (canonicalp x)) + (not (equal e (set-insert e x)))) + :hints (("Goal" :in-theory (cons 'ur-elementp + (slow-<<-rules))))) + +(defthm not-=-x-scons-x + (not (= e (scons e x))) + :hints (("Goal" :in-theory (enable = scons ur-elementp))) + :rule-classes + ((:rewrite) + (:rewrite :corollary (not (= (scons e x) e))))) + +; ---------------------------------------------------------------------------- +; Set Membership and the Subset Relation + +(defun mem (e a) + (cond ((ur-elementp a) nil) + (t (or (= e (scar a)) + (mem e (scdr a)))))) + +(defun subsetp (a b) + (cond ((ur-elementp a) t) + (t (and (mem (scar a) b) + (subsetp (scdr a) b))))) + +; I now prove that = is a congruence for both arguments of mem. The +; proof for the first argument is easy because (mem e s) only uses +; (canonicalize e). [So, if (canonicalize e) is (canonicalize e') +; it is obvious that (mem e s) is (mem e' s).] + +; The proof for the second argument is harder and works this way. We +; will establish that (mem e (canonicalize s)) is the same as (mem e +; s). Suppose that is proved. Then suppose (= s s'). That is, +; (canonicalize s) is (canonicalize s'). We must show that (mem e s) +; is (mem e s'). Use the theorem to replace each by (mem e +; (canonicalize s)) and (mem e (canonicalize s')), then substitute. + +; Even though I don't need it, I will prove the following for regularity. + +(defthm mem-canonicalize-1 + (equal (mem (canonicalize e) a) + (mem e a))) + +; We need to little lemmas to do the second argument. + +; In the lemma below we must assume that the arguments to set-insert +; are canonical. That is because it really compares using EQUAL. +; When we use the lemma it will be on canonicalized arguments. + +(defthm mem-set-insert + (implies (and (canonicalp d) + (canonicalp a)) + (equal (mem e (set-insert d a)) + (or (= e d) + (mem e a)))) + :hints (("Goal" + :induct (set-insert d a)))) + +; Here is the second lemma. + +(defthm mem-canonicalize-2 + (equal (mem e (canonicalize a)) + (mem e a))) + +(defcong = equal (mem e a) 1) + +(defcong = equal (mem e a) 2 + :hints (("Goal" :in-theory (disable mem-canonicalize-2) + :use ((:instance mem-canonicalize-2 + (e e) + (a a)) + (:instance mem-canonicalize-2 + (e e) + (a a-equiv)))))) + + +; Now I repeat it for subsetp. The first argument of subsetp is the +; harder, because we are recursing down it. The second argument is +; easy and follows from what we already know about mem. + +(defthm subsetp-set-insert-1 + (implies (and (canonicalp e) + (canonicalp a)) + (equal (subsetp (set-insert e a) b) + (and (mem e b) + (subsetp a b)))) + :hints (("Goal" :induct (set-insert e a)))) + +(defthm subsetp-canonicalize-1 + (equal (subsetp (canonicalize a) b) + (subsetp a b)) + :hints (("Goal" :induct (subsetp a b)))) + +(defcong = equal (subsetp a b) 1 + :hints (("Goal" + :in-theory (disable subsetp-canonicalize-1) + :use ((:instance subsetp-canonicalize-1 + (a a) + (b b)) + (:instance subsetp-canonicalize-1 + (a a-equiv) + (b b)))))) + +(defcong = equal (subsetp a b) 2 + :hints (("Goal" :in-theory (disable =)))) + +; For regularity: + +(defthm subsetp-canonicalize-2 + (equal (subsetp a (canonicalize b)) + (subsetp a b))) + +; Next, I will prove the key facts about subsetp. + +(defthm subsetp-cons + (implies (and (not (equal e :UR-CONS)) + (subsetp a b)) + (subsetp a (cons e b)))) + +(defthm subsetp-x-x + (subsetp x x)) + +(in-theory (disable =)) + +(defthm mem-subsetp + (implies (and (mem e a) + (subsetp a b)) + (mem e b))) + +(defthm transitivity-of-subsetp + (implies (and (subsetp a b) + (subsetp b c)) + (subsetp a c))) + +; ---------------------------------------------------------------------------- +; The Canonicality Theorem + +; Finally, I want to establish the key fact about equality and subset, +; namely, that two sets are = iff they are subsets of eachother. + +; If (= a b), then it is obvious that (subsetp a b) and vice versa, +; given the congruence rules above. + +; Suppose therefore that (subsetp a b) and (subsetp b a). We +; prove (= a b). The proof relies on the fact that << is a total +; ordering. + +; Proof. Let ca and cb be (canonicalize a) and (canonicalize b). +; Observe that they are both ordinary. By the subsetp-canonicalize-i +; lemmas we know that (subsetp ca cb) and (subsetp cb ca). We will +; prove that (subsetp ca cb) implies (not (<< cb ca)). Thus, +; ca equals cb. Q.E.D. + +(defthm =-is-equal + (implies (and (canonicalp x) + (canonicalp y)) + (equal (= x y) + (equal x y))) + :hints (("Goal" :in-theory (enable =)))) + +; I do not want to further encumber << with another rule. But this +; is an important fact and I will :use it. + +(defthm mem-<< + (implies (and (canonicalp e) + (canonicalp a) + (mem e a)) + (<< e a)) + :rule-classes nil + :hints (("Goal" :in-theory (slow-<<-rules <<)))) + +(defthm not-mem-e-e + (not (mem e e)) + :hints (("Goal" + :use (:instance MEM-<< + (e (canonicalize e)) + (a (canonicalize e)))))) + +; This rule seems overly expensive so I keep it disabled most of the time. + +(defthm mem-container + (implies (mem e a) + (not (mem a e))) + :hints (("Goal" + :use ((:instance mem-<< + (e (canonicalize e)) + (a (canonicalize a))) + (:instance mem-<< + (a (canonicalize e)) + (e (canonicalize a))))))) + +(in-theory (disable mem-container)) + +(defthm mem-implies-not-<<-car + (implies (and (canonicalp e) + (canonicalp a) + (mem e a)) + (not (<< (car a) e))) + :hints (("Goal" :in-theory (slow-<<-rules <<)))) + +(defthm <<-cons + (implies (and (canonicalp e) + (canonicalp a) + (mem e a)) + (equal (<< a (cons e z)) + (if (equal (car a) e) + (<< (cdr a) z) + nil))) + :hints (("Goal" :in-theory (enable <<) ; (fast-<<-rules <<) + ))) + +(defthm subsetp-cons-reversed + (implies (and (subsetp a (cons e b)) + (not (equal e :UR-CONS)) + (not (mem e a))) + (subsetp a b))) + +(defthm yucko + (implies (and (canonicalp a) + (canonicalp b) + (subsetp a b) + (mem (car b) a)) + (equal (car a) (car b))) + :rule-classes nil) + +(defthm subsetp-<< + (implies (and (setp a) + (setp b) + (canonicalp a) + (canonicalp b) + (subsetp a b)) + (not (<< b a))) + :rule-classes nil + :hints (("Goal" :induct (<< b a)) + ("Subgoal *1/5.3" + :use (:instance yucko + (a (cdr a)) + (b b))) + ("Subgoal *1/4''" :in-theory (enable <<) ; (fast-<<-rules <<) + ))) + +(defthm setp-canonicalize + (implies (setp x) + (setp (canonicalize x)))) + +; The Canonalicality Theorem: +(defthm =-iff-subsetps + (implies (and (setp a) + (setp b)) + (iff (= a b) + (and (subsetp a b) + (subsetp b a)))) + :rule-classes nil + :hints + (("Goal" + :in-theory (union-theories '(=) + (disable subsetp-canonicalize-1 + subsetp-canonicalize-2 + canonicalize + setp + transitivity-of-subsetp)) + + :use ((:instance subsetp-canonicalize-1 + (a a) + (b b)) + (:instance subsetp-canonicalize-2 + (a (canonicalize a)) + (b b)) + (:instance subsetp-canonicalize-1 + (a b) + (b a)) + (:instance subsetp-canonicalize-2 + (a (canonicalize b)) + (b a)) + (:instance subsetp-<< + (a (canonicalize a)) + (b (canonicalize b))) + (:instance subsetp-<< + (a (canonicalize b)) + (b (canonicalize a))))))) + +; Now we disable those of the above rules that we don't think are +; worth their cost. + +(in-theory (disable =-is-equal + mem-implies-not-<<-car + <<-cons)) + +;---------------------------------------------------------------------------- +; = Refines iff and is a Congruence for Many ACL2 Functions + + +(defcong = equal (canonicalize x) 1 + :hints (("Goal" :in-theory (enable =)))) + +(defthm canonicalize-= + (= (canonicalize x) x) + :hints (("Goal" :in-theory (enable =)))) + +(defthm canonicalize-non-nil + (iff (canonicalize x) x) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defrefinement = iff + :hints (("Goal" :in-theory (enable =)))) + +(defthm canonicalize-fix + (equal (canonicalize (fix x)) + (fix (canonicalize x))) + :rule-classes nil + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm <-fixes + (equal (< x y) (< (fix x) (fix y))) + :rule-classes nil) + +(defcong = equal (< x y) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance <-fixes + (x x) + (y y)) + (:instance <-fixes + (x x-equiv) + (y y)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + +(defcong = equal (< x y) 2 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance <-fixes + (x x) + (y y)) + (:instance <-fixes + (x x) + (y y-equiv)) + (:instance canonicalize-fix + (x y)) + (:instance canonicalize-fix + (x y-equiv)))))) + +(defthm +-fixes + (equal (+ x y) (+ (fix x) (fix y))) + :rule-classes nil) + +(defcong = equal (+ x y) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance +-fixes + (x x) + (y y)) + (:instance +-fixes + (x x-equiv) + (y y)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + +(defcong = equal (+ x y) 2 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance +-fixes + (x x) + (y y)) + (:instance +-fixes + (x x) + (y y-equiv)) + (:instance canonicalize-fix + (x y)) + (:instance canonicalize-fix + (x y-equiv)))))) + +(defthm --fixes + (equal (- x) (- (fix x))) + :rule-classes nil) + +(defcong = equal (- x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance --fixes + (x x)) + (:instance --fixes + (x x-equiv)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + + +(defthm *-fixes + (equal (* x y) (* (fix x) (fix y))) + :rule-classes nil) + +(defcong = equal (* x y) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance *-fixes + (x x) + (y y)) + (:instance *-fixes + (x x-equiv) + (y y)) + (:instance canonicalize-fix + (x x)) + (:instance canonicalize-fix + (x x-equiv)))))) + +(defcong = equal (* x y) 2 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) '(fix)) + :use ((:instance *-fixes + (x x) + (y y)) + (:instance *-fixes + (x x) + (y y-equiv)) + (:instance canonicalize-fix + (x y)) + (:instance canonicalize-fix + (x y-equiv)))))) + +(defthm integerp-canonicalize + (equal (integerp (canonicalize x)) + (integerp x))) + +(defthm rationalp-canonicalize + (equal (rationalp (canonicalize x)) + (rationalp x))) + +(defthm symbolp-canonicalize + (equal (symbolp (canonicalize x)) + (symbolp x))) + +(defthm stringp-canonicalize + (equal (stringp (canonicalize x)) + (stringp x))) + +(defthm characterp-canonicalize + (equal (characterp (canonicalize x)) + (characterp x))) + +(defthm consp-canonicalize + (equal (consp (canonicalize x)) + (consp x)) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defcong = equal (integerp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(integerp-canonicalize)) + :use ((:instance integerp-canonicalize + (x x)) + (:instance integerp-canonicalize + (x x-equiv)))))) + +(defcong = equal (rationalp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(rationalp-canonicalize)) + :use ((:instance rationalp-canonicalize + (x x)) + (:instance rationalp-canonicalize + (x x-equiv)))))) + +(defcong = equal (symbolp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(symbolp-canonicalize)) + :use ((:instance symbolp-canonicalize + (x x)) + (:instance symbolp-canonicalize + (x x-equiv)))))) + +(defcong = equal (stringp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(stringp-canonicalize)) + :use ((:instance stringp-canonicalize + (x x)) + (:instance stringp-canonicalize + (x x-equiv)))))) + +(defcong = equal (consp x) 1 + :hints (("Goal" + :in-theory (set-difference-theories (enable =) + '(consp-canonicalize)) + :use ((:instance consp-canonicalize + (x x)) + (:instance consp-canonicalize + (x x-equiv)))))) + + +; We do not get (defcong = equal (characterp x) 1) because we +; canonicalize non-standard atoms to (code-char 255). + +; ---------------------------------------------------------------------------- +; Codified Theorem Proving Strategies + +; The following all turn into the corresponding defthms: +; (defx name term) +; (defx name term :hints ... :rule-classes ...) + +; But if you write +; (defx ...a... :strategy xxx ...b...) +; it macro expands to +; (xxx ...a... ...b...) + +; Thus, if you want to codify a new theorem proving strategy xxx, you can +; defmacro xxx and then write (defx ... :strategy xxx ...). + +; The main point of this is to let me write defx events and introduce +; new strategies as I go. Also, I can name my strategies without +; including ``def'' in front of them and still search for ``(def...'' +; when looking for things. + +(defun packn-in-pkg (lst pkg-witness) + (declare (xargs :mode :program)) + (acl2::intern-in-package-of-symbol (coerce (acl2::packn1 lst) 'string) + pkg-witness)) + +(defmacro defx (&rest args) + (let ((temp (member :strategy args))) + +; We allow the strategy to be a keyword, in which case we convert it +; to the corresponding symbol in this package. If the strategy is not +; a keyword, it is used as supplied. + + (cond + (temp + `(,(if (keywordp (cadr temp)) + (packn-in-pkg (list (symbol-name (cadr temp))) 'defx) + (cadr temp)) + ,@(butlast args (length temp)) + ,@(cddr temp))) + (t `(defthm ,@args))))) + +; ---------------------------------------------------------------------------- +; Proving Congruences + +; There are two common ways to prove congruence rules in this theory. + +; (1) The :canonicalize strategy: prove that (fn (canonicalize x)) is +; (fn x). This is generally used if fn returns an ur-element (as +; opposed to a set). + +; (2) The :subsetp stragegy: prove that (subsetp a1 a2) implies +; (subsetp (fn a1) (fn a2)). This is generally used if fn returns a +; set. + +(defun genname1 (name n avoid) + (declare (xargs :mode :program)) + (let ((new-name (packn-in-pkg (list name n) name))) + (cond ((acl2::member-equal new-name avoid) + (genname1 name (+ 1 n) avoid)) + (t new-name)))) + +(defun genname (name avoid) + (declare (xargs :mode :program)) + (cond ((acl2::member-equal name avoid) + (genname1 name 1 avoid)) + (t name))) + +(defun put-nth (e n lst) + (cond ((zp n) (cons e (cdr lst))) + (t (cons (car lst) (put-nth e (- n 1) (cdr lst)))))) + +; And here is the macro + +(defmacro congruence (expr n &key method) + (cond + ((eq method :canonicalize) + (let* ((fn (car expr)) + (vars (cdr expr)) + (x (nth (- n 1) vars)) + (name1 + (packn-in-pkg (list fn "-SET-INSERT") fn)) + (name2 + (packn-in-pkg (list fn "-CANONICALIZE") fn)) + (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4 + (e (genname 'e vars1)) + (a (genname x vars1)) + (x-equiv (packn-in-pkg (list x "-EQUIV") x))) + `(encapsulate + nil + (local (in-theory (enable scons scar scdr ur-elementp))) + + (defthm ,name1 + (implies (and (canonicalp ,e) + (canonicalp ,a)) + (equal (,fn ,@(put-nth `(set-insert ,e ,a) + (- n 1) + vars)) + (,fn ,@(put-nth `(cons ,e ,a) + (- n 1) + vars)))) + :hints (("Goal" + :induct (set-insert ,e ,a) + +; Note that the following in-theory is commented out! I learned that +; if you enable = during these proofs it is generally slower. So I +; don't. +; :in-theory (enable =) + + + ))) + + (defthm ,name2 + (equal (,fn ,@(put-nth `(canonicalize ,x) + (- n 1) + vars)) + (,fn ,@vars))) + + (defcong = equal ,expr ,n + :hints + (("Goal" + :in-theory (disable ,name2) + :use ((:instance ,name2 (,x ,x)) + (:instance ,name2 + (,x ,x-equiv))))))))) + ((eq method :subsetp) + (let* ((fn (car expr)) + (vars (cdr expr)) + (x (nth (- n 1) vars)) + (name1 + (packn-in-pkg (list "SUBSETP-" fn "-" fn) fn)) + (vars1 (acl2::remove1-eq x vars)) ; Matt K. mod from delete1-eq, v2-9-4 + (a1 (genname1 x 1 vars1)) + (a2 (genname1 x 2 (cons a1 vars1))) + (x-equiv (packn-in-pkg (list x "-EQUIV") x))) + `(encapsulate + nil + (defthm ,name1 + (implies (subsetp ,a1 ,a2) + (subsetp (,fn ,@(put-nth a1 (- n 1) vars)) + (,fn ,@(put-nth a2 (- n 1) vars))))) + + (defcong = = ,expr ,n + :hints (("Goal" + :use (:instance =-iff-subsetps + (a ,expr) + (b (,fn ,@(put-nth x-equiv + (- n 1) + vars)))))))))) + ((eq method nil) + `(defcong = = ,expr ,n)) + (t `(acl2::er acl2::soft 'congruence + "The :method ~x0 is unknown." + ',method)))) + +; ---------------------------------------------------------------------------- +; The User Level Theory + +(in-theory (disable scons scar scdr ur-elementp)) + +; ---------------------------------------------------------------------------- +; Set Union + +(defun union (a b) + (if (ur-elementp a) + (sfix b) + (scons (scar a) + (union (scdr a) b)))) + +; My next goal is to prove both + +; (defcong = = (union a b) 1) +; (defcong = = (union a b) 2) + +; The first of these is problematic but the second is easy. +; Generally, if the congruence rule is in a slot that is held fixed in +; the recursion (as in the second case above), the proof is an easy +; induction, using congruence rules for the subfunctions. But if the +; congruence rule is in a controller slot, you generally need lemmas. + +(defthm mem-union + (equal (mem e (union a b)) + (or (mem e a) + (mem e b)))) + +(defthm subsetp-scons + (implies (subsetp a b) + (subsetp a (scons e b)))) + +(defthm subsetp-union-1 + (subsetp a (union a b))) + +(defthm subsetp-union-2 + (subsetp a (union b a))) + +(defthm subsetp-union + (implies (subsetp a1 a2) + (subsetp (union a1 b) + (union a2 b)))) +(defthm setp-union + (setp (union a b))) + +(defx :strategy :congruence (union a b) 1 :method :subsetp) + +(defx :strategy :congruence (union a b) 2) + +(defthm union-right-id + (implies (ur-elementp b) + (= (union a b) (sfix a)))) + +(defthm union-scons + (= (union a (scons e b)) + (scons e (union a b)))) + +(defthm commutativity-of-union + (= (union a b) (union b a))) + +(defthm ur-elementp-union + (equal (ur-elementp (union a b)) + (and (ur-elementp a) + (ur-elementp b)))) + +(defthm associativity-of-union + (= (union (union a b) c) + (union a (union b c)))) + + +; ---------------------------------------------------------------------------- +; Set Intersection + +(defun intersection (a b) + (if (ur-elementp a) + nil + (if (mem (scar a) b) + (scons (scar a) + (intersection (scdr a) b)) + (intersection (scdr a) b)))) + +(defthm mem-intersection + (equal (mem e (intersection a b)) + (and (mem e a) + (mem e b)))) + +(defthm subsetp-intersection-1 + (subsetp (intersection a b) a)) + +(defthm subsetp-intersection-2 + (subsetp (intersection b a) a)) + +(defthm subsetp-intersection + (implies (subsetp a1 a2) + (subsetp (intersection a1 b) + (intersection a2 b)))) + +(defthm setp-intersection + (setp (intersection a b))) + +(defx :strategy :congruence (intersection a b) 1 :method :subsetp) +(defx :strategy :congruence (intersection a b) 2) + +(defthm intersection-right-id + (implies (ur-elementp b) + (= (intersection a b) nil))) + +(defthm scons-id + (implies (mem e a) + (= (scons e a) a))) + +(defthm intersection-scons + (= (intersection a (scons e b)) + (if (mem e a) + (scons e (intersection a b)) + (intersection a b)))) + +(defthm commutativity-of-intersection + (= (intersection a b) (intersection b a))) + +(defthm associativity-of-intersection + (= (intersection (intersection a b) c) + (intersection a (intersection b c)))) + +; ---------------------------------------------------------------------------- +; Arithmetic + +(include-book "../../../../../arithmetic/top-with-meta") + + +(defun cardinality (a) + (if (ur-elementp a) + 0 + (if (mem (scar a) (scdr a)) + (cardinality (scdr a)) + (+ 1 (cardinality (scdr a)))))) + +(defx :strategy :congruence (cardinality a) 1 :method :canonicalize) + +(defthm cardinality-union-2 + (<= (cardinality b) (cardinality (union a b))) + :rule-classes :linear) + +; Observe that we proved the easy case first, by induction on b, +; and then we prove the other case by commutativity. + +(defthm cardinality-union-1 + (<= (cardinality b) (cardinality (union b a))) + :rule-classes :linear) + +(defthm cardinality-union-3 + (<= (cardinality (union a b)) + (+ (cardinality a) + (cardinality b))) + :rule-classes :linear) + +(defthm cardinality-0 + (equal (equal (cardinality a) 0) + (ur-elementp a))) + +(defthm cardinality-non-0 + (implies (mem e x) + (< 0 (cardinality x))) + :rule-classes :linear) + +(defthm cardinality-intersection-1 + (<= (cardinality (intersection a b)) (cardinality a)) + :rule-classes :linear) + +(defthm cardinality-intersection-2 + (<= (cardinality (intersection b a)) (cardinality a)) + :rule-classes :linear) + +(defthm cardinality-scons + (equal (cardinality (scons e a)) + (if (mem e a) + (cardinality a) + (+ 1 (cardinality a))))) + +(defthm cardinality-disjoint-union + (implies (not (intersection a b)) + (= (cardinality (union a b)) + (+ (cardinality a) + (cardinality b))))) + + +; ---------------------------------------------------------------------------- +; Choose + +(defun choose (a) + (car (sfix (canonicalize a)))) + +(defx :strategy :congruence (choose a) 1) + +(defthm ur-elementp-canonicalize + (equal (ur-elementp (canonicalize x)) + (ur-elementp x))) + +(defthm mem-choose-lemma + (equal (mem (car (canonicalize a)) a) + (not (ur-elementp a))) + :hints (("Goal" + :in-theory (enable scar scdr ur-elementp)))) + +(defthm mem-choose + (equal (mem (choose a) a) + (not (ur-elementp a)))) + +; One might think that the following follows from the previous +; theorems about choose. But that is not correct. For example, +; (choose {1 2 3}) might be 2 but (choose {2 3}) might be 3. This +; property is due to the fact that choose is really the biggest +; element of the set. + +(defthm car-canonicalize-ur-cons + (equal (equal (car (canonicalize a)) :UR-CONS) + (and (consp a) + (equal (car a) :UR-CONS))) + :hints (("Goal" :in-theory (enable ur-elementp)))) + +(defthm choose-scons + (implies (not (= (choose (scons e a)) e)) + (= (choose (scons e a)) (choose a))) + :hints (("Goal" + :in-theory + (enable = scons ur-elementp)))) + +(defthm choose-singleton + (= (choose (scons e nil)) e) + :hints (("Goal" :in-theory (enable = scons ur-elementp)))) + +(in-theory (disable choose)) + +(defthm elim-choose-singleton + (implies (equal (cardinality x) 1) + (= (scons (choose x) nil) x))) + +(defthm mem-singleton + (implies (and (equal (cardinality x) 1) + (mem e x)) + (= (scons e nil) x)) + :rule-classes nil + :hints (("Goal" :in-theory (disable elim-choose-singleton) + :use elim-choose-singleton))) + +(defthm choose-ur-elementp + (implies (ur-elementp x) + (= (choose x) nil)) + :hints (("Goal" :in-theory (enable choose ur-elementp sfix)))) + + +; ---------------------------------------------------------------------------- +; Set Difference + +(defun diff (a b) + (cond ((ur-elementp a) + nil) + ((mem (scar a) b) + (diff (scdr a) b)) + (t (scons (scar a) + (diff (scdr a) b))))) + +(defthm mem-diff + (equal (mem e (diff a b)) + (and (mem e a) + (not (mem e b))))) + +(defthm subsetp-diff-1 + (subsetp (diff a b) a)) + +(defthm subsetp-diff + (implies (subsetp a1 a2) + (subsetp (diff a1 b) + (diff a2 b)))) + +(defthm setp-diff + (setp (diff a b))) + +(defx :strategy :congruence (diff a b) 1 :method :subsetp) +(defx :strategy :congruence (diff a b) 2) + +(defthm diff-right-id + (implies (ur-elementp b) + (= (diff a b) (sfix a)))) + +(defthm cardinality-diff-singleton + (equal (cardinality (diff y (scons x nil))) + (if (mem x y) + (- (cardinality y) 1) + (cardinality y)))) + +(defthm cardinality-diff + (<= (cardinality (diff a b)) (cardinality a)) + :rule-classes :linear) + +(defthm diff-nil + (implies (subsetp x y) + (= (diff x y) nil))) + +(defthm diff-scons + (implies (not (mem e s)) + (= (diff s (scons e y)) (diff s y)))) + +(encapsulate nil + (local + (defthm scons-x-diff-x + (implies (mem x s) + (= (scons x (diff s (scons x nil))) s)) + :hints (("Subgoal *1/3'5'" + :cases ((mem sr sr0)))))) + + (defthm scons-diff-scons + (= (scons e (diff a (scons e nil))) + (scons e a)) + :hints (("Goal" :cases ((mem e a)))))) + +(defthm elim-choose-doubleton + (implies (equal (cardinality x) 2) + (= (scons (choose x) + (scons (choose (diff x (scons (choose x) nil))) + nil)) + x))) + +(defthm subsetp-diff-1-corrollary + (implies (subsetp a b) + (subsetp (diff a c) b))) + +(defthm subsetp-not-subsetp-trick + (implies (and (subsetp a b) + (not (subsetp a (scdr b)))) + (mem (scar b) a))) + +(defthm intersection-diff-2 + (= (intersection a (diff b c)) + (diff (intersection a b) c))) + +(defthm intersection-diff-1 + (= (intersection (diff b c) a) + (diff (intersection a b) c))) + +; There are others, but I am not going to prove them now. + +; ---------------------------------------------------------------------------- +; Ordered Pairs as Sets + +; It is possible to provide ordered pairs as ur-elements. For example +; we could define (pair x y) to be (list :UR-CONS (cons x y)). But here +; we develop the classical treatment of ordered pairs. + +(defun pair (x y) + (brace x (brace x y))) + +; Observe that a pair necessarily has cardinality 2. But the larger +; element need not have cardinality 2. For example, (pair x x) is +; {x {x}}. + +; We must be able to determine whether a set of cardinality 2 is a +; pair. Call the two elements x and y. Then either (mem x y) or (mem +; y x). Furthermore, the larger must be of cardinality 2 or less. To +; code this up, we have to have a way of finding ``the two elements'' +; of a set, a, of cardinality 2, when a is not necessarily in +; canonical form. E.g., (1 (1 2)) is a pair but so is (1 1 (2 1) (1 +; 2)). At first, I wanted to avoid canonicalizing the set, for +; efficiency reasons. + +; Here was my first attempt to extract ``the other'' element of a +; set of cardinality 2. + +; (defun find-other (e s) +; ; Find the first element of s that is not e. +; (cond ((ur-elementp s) nil) +; ((= e (scar s)) (find-other e (scdr s))) +; (t (scar s)))) + +; Unfortunately, this function does not admit = as a congruence in +; the second argument. For example (find-other 1 '(1 2 3)) and +; (find-other 1 '(1 3 2)) return different things, even though their +; arguments are =. (It would admit it if we limited s to sets of +; cardinality 2, but we can't.) + +; So I have decided simply use the classical approach in terms of +; choose. If the first element of a pair is a number, this is not too +; expensive. + +(defun pairp (a) + (if (equal (cardinality a) 2) + (let* ((x (choose a)) + (y (choose (diff a (brace x))))) + (or (and (mem x y) + (<= (cardinality y) 2)) + (and (mem y x) + (<= (cardinality x) 2)))) + nil)) + +(defun hd (a) + (cond ((pairp a) + (let* ((x (choose a)) + (y (choose (diff a (brace x))))) + (if (mem x y) + x + y))) + (t nil))) + +(defun tl (a) + (cond ((pairp a) + (let* ((x (choose a)) + (y (choose (diff a (brace x))))) + (if (mem x y) + (if (equal (cardinality y) 1) + x + (choose (diff y (brace x)))) + (if (equal (cardinality x) 1) + y + (choose (diff x (brace y))))))) + (t nil))) + +(defthm setp-pair + (setp (pair x y))) + +(defcong = = (pair a b) 1) +(defcong = = (pair a b) 2) +(defcong = equal (pairp a) 1) +(defcong = = (hd a) 1) +(defcong = = (tl a) 1) + +(in-theory (enable mem-container)) + +(defthm hd-pair + (= (hd (pair x y)) x)) + +(defthm tl-pair + (= (tl (pair x y)) y)) + +(defthm pairp-pair + (pairp (pair x y)) + :rule-classes (:type-prescription :generalize)) + +(defthm pairp-implies-setp + (implies (pairp x) (setp x))) + +(encapsulate + nil + +; Our goal here is to prove + +; (implies (pairp a) +; (= (pair (hd a) (tl a)) a)) + +; We have to give the proof pretty explicitly. It exploits the fact +; that we know how to represent singleton and doubleton sets in terms +; of choose. Since we have to use these lemmas explicitly, we disable +; them. + + (local (in-theory (disable elim-choose-doubleton + elim-choose-singleton))) + +; To make the proof easier to understand, we give names to certain +; expressions. In the definitions of pair, hd and tl, we use two +; local variables, + +; (let* ((x (choose a)) +; (y (choose (diff a (brace x))))) +; ...) + +; Here we define functions corresponding to their values. + + (local (defun x (a) (choose a))) + (local (defun y (a) (choose (diff a (brace (x a)))))) + +; Given that a is known to be a pairp, there are four cases, depending +; on which of x and y is an element of the other and whether the +; cardinality of the bigger is 1 or 2. We will prove the main goal +; for each of the four cases. + + (local + (defthm case-1 + (implies (and (mem (x a) (y a)) + (equal (cardinality (y a)) 2) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ( + +; Proof of Case 1: + +; (i) Represent A as a doubleton in terms of choose. + + (:instance elim-choose-doubleton (x A)) + +; (ii) Represent y as a doubleton. + + (:instance elim-choose-doubleton (x (y a))) + +; (iii) When x is removed from y, the result is a singleton, which can +; be represented with choose. + + (:instance elim-choose-singleton + (x (diff (y a) (scons (x a) nil)))) + +; (iv) If x is a member of a singleton set, the set is {x}. + + (:instance mem-singleton + (e (x a)) + (x (diff (y a) (scons (x a) nil))))))))) + + (local + (defthm case-2 + (implies (and (mem (x a) (y a)) + (equal (cardinality (y a)) 1) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ( + +; Proof of Case 2: + +; (i) Represent A as a doubleton in terms of choose. + + (:instance elim-choose-doubleton (x A)) + +; (ii) Represent y as a singleton. + + (:instance elim-choose-singleton (x (y a))) + +; (iii) If x is a member of singleton set, the set is {x}. + + (:instance mem-singleton + (e (x a)) + (x (y a)))))))) + +; Cases 3 and 4 are symmetric with Cases 1 and 2, interchanging the +; roles of x and y. + + (local + (defthm case-3 + (implies (and (mem (y a) (x a)) + (equal (cardinality (x a)) 2) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ((:instance elim-choose-doubleton (x A)) + (:instance elim-choose-doubleton (x (x a))) + (:instance elim-choose-singleton + (x (diff (x a) (scons (y a) nil)))) + (:instance mem-singleton + (e (y a)) + (x (diff (x a) (scons (y a) nil))))))))) + + (local + (defthm case-4 + (implies (and (mem (y a) (x a)) + (equal (cardinality (x a)) 1) + (pairp A)) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" + :use + ((:instance elim-choose-doubleton (x A)) + (:instance elim-choose-singleton (x (x a))) + (:instance mem-singleton + (e (y a)) + (x (x a)))))))) + + (defthm pair-hd-tl + (implies (pairp A) + (= (pair (hd A) (tl A)) A)) + :hints + (("Goal" :in-theory (disable pair hd tl) + :cases ((and (mem (x a) (y a)) ;;; Case 1 + (equal (cardinality (y a)) 2)) + (and (mem (x a) (y a)) ;;; Case 2 + (equal (cardinality (y a)) 1)) + (and (mem (y a) (x a)) ;;; Case 3 + (equal (cardinality (x a)) 2)) + (and (mem (y a) (x a)) ;;; Case 4 + (equal (cardinality (x a)) 1))))) + :rule-classes (:rewrite :elim))) + +(in-theory (disable mem-container)) + +(in-theory (disable pairp pair hd tl)) + +(defthm equal-booleans + (implies (and (acl2::booleanp p) + (acl2::booleanp q)) + (equal (equal p q) + (iff p q)))) + +(defthm equal-pair + (equal (= (pair x1 y1) + (pair x2 y2)) + (and (= x1 x2) + (= y1 y2))) + :hints + (("Goal" :in-theory (disable hd-pair tl-pair) + :use ((:instance hd-pair (x x1) (y y1)) + (:instance hd-pair (x x2) (y y2)) + (:instance tl-pair (x x1) (y y1)) + (:instance tl-pair (x x2) (y y2)))))) + +(in-theory (disable equal-booleans)) + +(defthm equal-pair-generalized + (equal (= (pair x1 x2) y) + (and (pairp y) + (= x1 (hd y)) + (= x2 (tl y))))) + +(in-theory (disable equal-pair-generalized)) + + + +; ---------------------------------------------------------------------------- +; Functions as Sets + +; The following is an example of set comprehension. In particular, it +; is + +; { x in s | (and (pairp x) (= e (hd x)))} + +(defun subset-such-that1 (s e) + (cond ((ur-elementp s) nil) + ((and (pairp (scar s)) + (= e (hd (scar s)))) + (scons (scar s) (subset-such-that1 (scdr s) e))) + (t (subset-such-that1 (scdr s) e)))) + +; When such a function is defined we should immediately prove the +; obvious three relationships: + +(defthm setp-subset-such-that1 + (setp (subset-such-that1 a e))) + +(defthm mem-subset-such-that1 + (iff (mem pair (subset-such-that1 a x)) + (and (pairp pair) + (mem pair a) + (= (hd pair) x))) + :hints (("Goal" :do-not '(generalize)))) + +(defthm subsetp-subset-such-that1 + (subsetp (subset-such-that1 a x) a)) + +; The congruence rules are easy. + +(defx :strategy :congruence (subset-such-that1 a e) 1 :method :subsetp) +(defx :strategy :congruence (subset-such-that1 a e) 2) + +(defthm mem-subset-such-that1-corrollary + (implies (and (subsetp a (subset-such-that1 f x)) + (mem e a)) + (and (pairp e) + (= (hd e) x)))) + +; Now we define apply: + +(defun apply (s e) + (tl (choose (subset-such-that1 s e)))) + +(defcong = = (apply s e) 1) +(defcong = = (apply s e) 2) + +(defun except (s e v) + (scons (pair e v) + (diff s (subset-such-that1 s e)))) + +(defcong = = (except s e v) 1) +(defcong = = (except s e v) 2) +(defcong = = (except s e v) 3) + +(defthm diff-scons-1 + (implies (acl2::syntaxp (not (equal b ''nil))) + (= (diff a (scons e b)) + (diff (diff a b) (brace e))))) + +(defthm ur-elementp-diff + (iff (ur-elementp (diff a b)) + (subsetp a b))) + +(defthm subset-such-that1-diff-subset-such-that-1 + (= (subset-such-that1 (diff f (subset-such-that1 f x)) y) + (if (= x y) + nil + (subset-such-that1 f y)))) + +(encapsulate + nil + (local + (defthm lemma2 + (implies (and (subsetp f (subset-such-that1 g x)) + (not (= x y))) + (= (subset-such-that1 f y) + nil)))) + + (defthm apply-except + (= (apply (except f x v) y) + (if (= x y) + v + (apply f y))))) + +(defthm mem-except + (equal (mem e (except f x v)) + (if (pairp e) + (if (= (hd e) x) + (= (tl e) v) + (mem e f)) + (mem e f)))) + +(defthm subsetp-except + (iff (subsetp (except f x v) g) + (and (mem (pair x v) g) + (subsetp (diff f (subset-such-that1 f x)) + g)))) + +(defthm ur-elementp-except + (not (ur-elementp (except f x v)))) + +(in-theory (disable apply except)) + +(defmacro func* (&rest args) + (cond ((endp args) nil) + ((endp (cdr args)) (car args)) + (t `(except (func* ,@(cdr args)) + ,(car (car args)) + ,(cadr (car args)))))) + +(defmacro func (&rest args) + `(func* ,@args nil)) + + +; ---------------------------------------------------------------------------- +; Sets of ordered pairs. + +; This is really just a simple map over a checking a predicate. I +; need to automate this sort of thing but I will do it by hand right +; now. + +(defun pairsp (a) + (cond ((ur-elementp a) t) + (t (and (pairp (scar a)) + (pairsp (scdr a)))))) + +(defx :strategy :congruence (pairsp a) 1 :method :canonicalize) + +(defthm pairsp-union + (equal (pairsp (union a b)) + (and (pairsp a) + (pairsp b)))) + +(defthm pairsp-diff + (implies (pairsp a) + (pairsp (diff a b)))) + +; This one is more useful when dealing with sets created by EXCEPT. + +(defthm pairsp-diff-subset-such-that1 + (equal (pairsp (diff a (subset-such-that1 b x))) + (pairsp a))) + +(defthm pairsp-scons + (equal (pairsp (scons e a)) + (and (pairp e) + (pairsp a)))) + +(defthm mem-pairsp + (implies (and (mem e f) + (pairsp f)) + (pairp e))) + +(defthm pairsp-subset-such-that1 + (implies (pairsp f) + (pairsp (subset-such-that1 f x)))) + +(defthm nil-not-mem-pairsp + (implies (pairsp f) + (not (mem nil f)))) + +; ---------------------------------------------------------------------------- +; Recognizing Functions + +; The basic idea is to define the predicate that recognizes when a set +; is both pairsp and has unique hds. We've got the first part. The +; second part is called functionp1. + +; Here is my first functionp1. It does not insure that every element +; of f is a pair. Thus, + +; (functionp1 (brace (pair 1 2)) (brace (pair 1 2) 3)) = t + +; Second, it is fragile in the sense that if a is not a subset of f, it +; fails, e.g., + +; (functionp1 (brace (pair 1 2)) (brace (pair 3 4))) = nil + +; This is not a problem at the top level, where a is f. But in stating +; theorems about functionp1 it would be convenient to allow arbitrary a +; with sensible results. + +; (defun functionp1 (a f) +; (cond ((ur-elementp a) t) +; (t (and (pairp (scar a)) +; (equal (cardinality (subset-such-that1 f (hd (scar a)))) 1) +; (functionp1 (scdr a) f))))) + +; So here is my second: + +(defun functionp1 (a f) + (cond ((ur-elementp a) t) + (t (and (<= (cardinality (subset-such-that1 f (hd (scar a)))) 1) + (functionp1 (scdr a) f))))) + +(defx :strategy :congruence (functionp1 a f) 1 :method :canonicalize) +(defcong = equal (functionp1 a f) 2) + + +; Is 8 a function? I say no. The reason I say no, is that I want it +; to be the case that two functions are equal iff apply gives the same +; answers on both. But if I defined a function as (and (pairsp f) +; (functionp1 f f)) then 8 is a functionp, because every element of 8 +; is a pair and their hds are unique. + +(defun functionp (f) + (if (ur-elementp f) + (= f nil) + (and (pairsp f) + (functionp1 f f)))) + +(defcong = equal (functionp f) 1) + +; My next goal is to prove that functionp is preserved by EXCEPT. +; I need some lemmas about functionp1 + +(defthm cardinality-subset-such-that1 + (<= (cardinality (subset-such-that1 f x)) + (cardinality f)) + :rule-classes :linear) + +(defun simultaneously (a b) + (declare (xargs :measure (cardinality a))) + (cond ((ur-elementp a) b) + (t (simultaneously (diff a (brace (scar a))) + (diff b (brace (scar a))))))) + +(defthm cardinality-subsetp + (implies (subsetp a b) + (<= (cardinality a) + (cardinality b))) + :hints (("Goal" :induct (simultaneously a b))) + :rule-classes :linear) + + + +; The next two theorems are not used until later, but they seem +; natural to have around. + +(defthm functionp1-subsetp-2 + (implies (and (functionp1 a g) + (subsetp f g)) + (functionp1 a f)) + :hints + (("Subgoal *1/4'" + :in-theory (disable cardinality-subsetp) + :use (:instance cardinality-subsetp + (a (SUBSET-SUCH-THAT1 F (HD (SCAR A)))) + (b (SUBSET-SUCH-THAT1 G (HD (SCAR A)))))))) + +(defthm functionp1-diff + (implies (functionp1 a f) + (functionp1 a (diff f b))) + :hints (("Goal" :in-theory (disable subsetp-diff-1) + :use (:instance subsetp-diff-1 + (a f) + (b b))))) + +; Consider the goal (implies (functionp f) (functionp f')), where f' +; is (except f x v). Ignoring the pairsp part, this opens into + +; (implies (functionp1 f f) (functionp1 f' f')) + +; We have to break both duplications. Each requires a lemma. Then +; we put the two lemmas together to get something like: + +; (implies (functionp1 b f) (functionp1 a f')) + +; where (subsetp a b). + +; Here is one of the two ``breakers.'' + +(defthm functionp1-subsetp-1 + (implies (and (subsetp a b) + (functionp1 b f)) + (functionp1 a f)) + :hints (("Goal" :do-not '(generalize)))) + +(encapsulate + nil + +; This is the other ``breaker''. The scons below is f', i.e., the +; expansion of (except f x v). + + (local + (defthm functionp1-except-lemma + (implies (functionp1 a f) + (functionp1 a (scons (pair x v) + (diff f (subset-such-that1 f x))))))) + +; Now we put the two breakers together to get the main lemma about +; functionp1 and except. + + (defthm functionp1-except + (implies (and (functionp1 b f) + (subsetp a b)) + (functionp1 a (scons (pair x v) + (diff f (subset-such-that1 f x))))))) + +(defthm functionp-except + (implies (functionp f) + (functionp (except f x v))) + :hints (("Goal" :in-theory (enable except)))) + +(defthm functionp-implies-pairsp + (implies (functionp f) + (pairsp f))) + +(in-theory (disable functionp)) + +;---------------------------------------------------------------------------- +; Domain and Range + +(defun domain (f) + (cond ((ur-elementp f) nil) + (t (scons (hd (scar f)) + (domain (scdr f)))))) + +(defun range (f) + (cond ((ur-elementp f) nil) + (t (scons (tl (scar f)) (range (scdr f)))))) + +(defthm mem-implies-mem-domain + (implies (mem e f) + (mem (hd e) (domain f)))) + +(defthm ur-elementp-domain + (equal (ur-elementp (domain f)) + (ur-elementp f))) + +(defx :strategy :congruence (domain f) 1 :method :subsetp) + +(defthm mem-implies-mem-range + (implies (mem e f) + (mem (tl e) (range f)))) + +(defthm ur-elementp-range + (equal (ur-elementp (range f)) + (ur-elementp f))) + +(defx :strategy :congruence (range f) 1 :method :subsetp) + +(defthm domain-scons + (= (domain (scons e f)) + (scons (hd e) (domain f)))) + +(defthm domain-diff-subset-such-that1 + (implies (pairsp f) + (= (domain (diff f (subset-such-that1 f x))) + (diff (domain f) (brace x))))) + +(defthm domain-except + (implies (pairsp f) + (= (domain (except f x v)) + (scons x (domain f)))) + :hints (("Goal" :in-theory (enable except)))) + +; The range of (except f x v) is harder to characterize. If f is +; not a function, then (except f x v) might be. The range of f +; might include many things that are removed by the except. + +(defthm range-scons + (= (range (scons e f)) + (scons (tl e) (range f)))) + +(defthm subsetp-range-except + (subsetp (range (except f x v)) + (scons v (range f))) + :hints (("Goal" :in-theory (enable except)))) + +; We have these two, even though the union is not necessarily a +; function. + +(defthm domain-union + (= (domain (union f g)) + (union (domain f) (domain g)))) + +(defthm range-union + (= (range (union f g)) + (union (range f) (range g)))) + +(defthm cardinality-domain + (<= (cardinality (domain f)) (cardinality f)) + :rule-classes :linear) + +(defthm cardinality-range + (<= (cardinality (range f)) (cardinality f)) + :rule-classes :linear) + +(defthm ur-element-subset-such-that1 + (implies (pairsp f) + (equal (ur-elementp (subset-such-that1 f x)) + (not (mem x (domain f)))))) + +(defthm cardinality-<=-0 + (equal (< 0 (cardinality a)) + (not (ur-elementp a)))) + +(defthm cardinality-domain-functionp + (implies (functionp f) + (equal (cardinality (domain f)) + (cardinality f))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm subset-such-that1-empty + (implies (not (mem e (domain b))) + (= (subset-such-that1 b e) + nil))) + +; Is the (pairsp b) hypothesis below necessary? Yes. Here is a counterexample +; of the formula without the hypothesis. + +#|(let ((b (brace 123)) + (a (brace (pair nil 33))) + (pair (pair nil 2))) + (equal (functionp1 a (scons pair b)) + (if (and (pairp pair) + (mem (hd pair) (domain a))) + (and (functionp1 a b) + (or (mem pair b) + (not (mem (hd pair) (domain b))))) + (functionp1 a b))))|# + +(defthm functionp1-scons + (implies (pairsp b) + (equal (functionp1 a (scons pair b)) + (if (and (pairp pair) + (mem (hd pair) (domain a))) + (and (functionp1 a b) + (or (mem pair b) + (not (mem (hd pair) (domain b))))) + (functionp1 a b))))) + +(defthm cardinality-<=-1-cases + (iff (< 1 (cardinality x)) + (not (or (ur-elementp x) + (equal (cardinality x) 1))))) + +(defthm functionp-scons-lemma + (implies (and (functionp1 a b) + (subsetp a b) + (pairsp b) + (mem e a)) + (equal (cardinality (subset-such-that1 b (hd e))) + 1))) + +; Note that the following theorem is essentially a recursive +; alternative definition of functionp. + +(defthm functionp-scons + (equal (functionp (scons e a)) + (if (ur-elementp a) + (pairp e) + (and (functionp a) + (pairp e) + (or (mem e a) + (not (mem (hd e) (domain a))))))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm functionp-union + (implies (and (functionp a) + (functionp b) + (not (intersection (domain a) (domain b)))) + (functionp (union a b)))) + +(defthm disjoint-domains-implies-disjoint + (implies (not (intersection (domain a) (domain b))) + (not (intersection a b))) + :rule-classes nil) + +(defthm cardinality-except + (implies (functionp f) + (= (cardinality (except f x v)) + (if (mem x (domain f)) + (cardinality f) + (+ 1 (cardinality f))))) + :hints (("Goal" + :use ((:instance cardinality-domain-functionp (f (except f x v))) + (:instance cardinality-domain-functionp (f f))) + :in-theory (disable cardinality-domain-functionp)))) + +(defthm apply-outside-domain + (implies (not (mem e (domain f))) + (= (apply f e) nil)) + :hints (("Goal" :in-theory (enable apply)))) + +;---------------------------------------------------------------------------- +; Restrictions + +; I can think of three slightly different ways to define the restriction +; of a function f to some domain s. + +; (1) Iterate over s and make a function of the defined values. This +; always produces a function. However, if f is not a function, the +; function it produces is sort of unpredictable because it uses apply, +; so the restricted function chooses the largest pairs. + +(defun restrict (f s) + (cond ((ur-elementp s) nil) + ((mem (scar s) (domain f)) + (except (restrict f (scdr s)) + (scar s) + (apply f (scar s)))) + (t (restrict f (scdr s))))) + +; (2) Iterate over f and make a function of the values of elements of +; s. This always produces a function. But if f is not a function, +; the restricted function is unpredictable because it chooses the +; first pair presented for each domain element. I reject this +; definition because it does not do the ``normal'' things with a +; function. The normal things you do with a function are enquire +; about its domain and apply it. Looking at its internal structure is +; an invitation to low-level work. + +; (defun restrict2 (f s) +; (cond ((ur-elementp f) nil) +; ((and (pairp (scar f)) +; (mem (hd (scar f)) s)) +; (except (restrict2 (scdr f) s) +; (hd (scar f)) +; (tl (scar f)))) +; (t (restrict2 (scdr f) s)))) + +; (3) Iterate over f and collect everything whose hd is in s. The +; result may not be a function, but it is if f is. This has the +; appeal of being really simple, but, again, uses f in an abnormal +; way. + +; (defun restrict3 (f s) +; (cond ((ur-elementp f) nil) +; ((mem (hd (scar f)) s) +; (scons (scar f) (restrict3 (scdr f) s))) +; (t (restrict3 (scdr f) s)))) + +(defx :strategy :congruence (restrict f s) 1) + +; Next we prove that the second argument of restrict admits = as a +; congruence relation. For some reason it took me a while to +; realize that if you are going to prove that something is a +; subset of (restrict f s) you must be able to answer the question +; ``when is e a member of (restrict f s)?'' I was seeing this question +; come up and generalized it to ``when is e a member of a function?'' +; Answering that was harder than answering it for (restrict f s), +; which is always a function but which is built in a way that makes +; it easier to answer the question. Here is how you do it. + +; The system can prove mem-restrict, below, without further help. It +; generates three inductively proved subgoals. These are not worth +; turning into rules because mem-restrict, once proved, is better than +; each of them. + +(defthm mem-restrict + (equal (mem e (restrict f s)) + (and (pairp e) + (mem (hd e) (domain f)) + (= (tl e) (apply f (hd e))) + (mem (hd e) s))) + :hints (("Goal" :do-not '(generalize)))) + +; At first I wrote (= (restrict f s) nil) instead of the inner equal. +; But I really need the stronger equal because in the defcong= proof +; below the question of whether (restrict f s) is a set comes up. To +; be a set it must be either not an ur-element or nil. This means +; that we end up testing (restrict f s) against nil in a propositional +; setting, not a set theory setting. Since = does not refine iff +; (because '(:UR-CONS NIL) is canonicalized to NIL), knowing that +; (restrict f s) is not = nil does not help us. + +(defthm ur-elementp-restrict + (equal (ur-elementp (restrict f s)) + (equal (restrict f s) nil))) + +(defx :strategy :congruence (restrict f s) 2 :method :subsetp) + +(defthm functionp-restrict + (functionp (restrict f s))) + +; My next main goal is the fundamental fact characterizing the elements +; of a function. + +; Perhaps disable this when we're done? + + +(defthm pigeon-hole-1 + (implies (and (mem e a) + (mem d a) + (equal (cardinality a) 1)) + (= e d)) + :rule-classes nil) + +; The next three theorems are trivial consequences of other lemmas +; given the fact that (choose a) is an element of a. I really ought +; to provide macros that capture these kind of theorems. The idea in +; all of them is that if every element of a has some property then +; (choose a) has that property if a is non-empty. + +(defthm hd-choose-subset-such-that1 + (= (hd (choose (subset-such-that1 f x))) + (if (ur-elementp (subset-such-that1 f x)) + nil + x)) + :hints (("Goal" + :in-theory (disable mem-choose) + :use ((:instance mem-choose + (a (subset-such-that1 f x))))))) + +(defthm pairp-choose-subset-such-that1 + (implies (pairsp f) + (equal (pairp (choose (subset-such-that1 f x))) + (and (not (ur-elementp f)) + (mem x (domain f))))) + :hints (("Goal" + :in-theory (cons 'equal-booleans + (disable mem-choose)) + :use ((:instance mem-choose + (a (subset-such-that1 f x))))))) + +(defthm mem-choose-subset-such-that1 + (implies (pairsp f) + (equal (mem (choose (subset-such-that1 f x)) f) + (and (not (ur-elementp f)) + (mem x (domain f))))) + :hints (("Goal" + :in-theory (cons 'equal-booleans + (disable mem-choose)) + :use ((:instance mem-choose + (a (subset-such-that1 f x))))))) + +; This is a pretty obscure fact, I think. If x is a pair in f and +; there is only one pair in f with its hd, then choose chooses x. + +(defthm mem-x-implies-not-ur-elementp-subset-such-that1 + (implies (and (mem x f) + (pairp x)) + (not (ur-elementp (subset-such-that1 f (hd x)))))) + +(defthm choose-subset-such-that1 + (implies (and (<= (cardinality (subset-such-that1 f (hd x))) 1) + (mem x f) + (pairp x) + (pairsp f)) + (= (choose (subset-such-that1 f (hd x))) + x)) + :hints (("Goal" + :use (:instance pigeon-hole-1 + (e x) + (d (choose (subset-such-that1 f (hd x)))) + (a (subset-such-that1 f (hd x))))))) + +(defthm functionp-implies-mem-1 + (implies (and (functionp1 a f) + (pairsp f) + (subsetp a f) + (mem hd (domain a))) + (mem (pair hd (tl (choose (subset-such-that1 f hd)))) + f))) + +(defthm functionp-implies-mem-2 + (implies (and (functionp1 a f) + (pairsp f) + (subsetp a f) + (mem (hd x) (domain a)) + (pairp x) + (mem x f)) + (= (choose (subset-such-that1 f (hd x))) + x))) + +; This is the fundamental fact about membership in a function. It +; loops if made into a rewrite rule. + +(defthm mem-functionp + (implies (functionp f) + (equal (mem e f) + (and (pairp e) + (mem (hd e) (domain f)) + (= (tl e) (apply f (hd e)))))) + :rule-classes nil + :hints (("Goal" + :in-theory (enable functionp apply equal-booleans)))) + +(defthm domain-restrict + (= (domain (restrict f s)) + (intersection s (domain f)))) + +(defthm apply-restrict + (implies (and (mem x (domain f)) + (mem x s)) + (= (apply (restrict f s) x) + (apply f x)))) + +(defthm except-scdr-scar-elim + (implies (and (functionp f) + (not (ur-elementp f))) + (= (except (scdr f) (hd (scar f)) (tl (scar f))) + f)) + :otf-flg t + :hints + (("Goal" + :in-theory (enable except functionp equal-pair-generalized) + :use ((:instance mem-functionp + (e (pair (hd (scar f)) (tl (scar f)))) + (f f)) + (:instance mem-singleton + (e (pair (hd (scar f)) (tl (scar f)))) + (x (subset-such-that1 (scdr f) (hd (scar f))))))))) + +(defthm functionp-nil + (implies (ur-elementp f) + (equal (functionp f) (= f nil))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm functionp-pairp + (implies (not (pairp x)) + (not (functionp (scons x y)))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm except-scdr-scar-elim-special-case + (implies (and (functionp f) + (not (ur-elementp f)) + (ur-elementp (scdr f))) + (= (except nil (hd (scar f)) (tl (scar f))) + f)) + :hints (("Goal" :in-theory (enable except)))) + +(defthm functionp-scdr + (implies (functionp f) + (functionp (scdr f))) + :hints (("Goal" :in-theory (enable functionp)))) + +(defthm restrict-domain + (implies (and (functionp f) + (functionp g) + (subsetp f g)) + (= (restrict g (domain f)) f)) + :hints + (("Subgoal *1/4" + :use ((:instance mem-functionp (e (scar f)) (f g)))))) + +; The lemma above will rewrite (restrict a (domain a)) to a, provided +; (functionp a). But it is often the case that the domain expression +; will be rewritten to something else, e.g., an intersection. So +; we provide a bridge. + +(defthm restrict-domain-special-case + (implies (and (functionp f) + (= a (domain f))) + (= (restrict f a) f))) + +(defthm restrict-scons + (= (restrict f (scons e s)) + (if (mem e (domain f)) + (except (restrict f s) + e + (apply f e)) + (restrict f s)))) + +; ---------------------------------------------------------------------------- +; Strategies for Proving Functions and Sets Equivalent + +(encapsulate ((functional-equiv-fn1 () t) + (functional-equiv-fn2 () t)) + (local (defun functional-equiv-fn1 nil nil)) + (local (defun functional-equiv-fn2 nil nil)) + (defthm functional-equivalence-constraint-1 + (functionp (functional-equiv-fn1))) + (defthm functional-equivalence-constraint-2 + (functionp (functional-equiv-fn2))) + (defthm functional-equivalence-constraint-3 + (= (domain (functional-equiv-fn2)) + (domain (functional-equiv-fn1)))) + +; We use the unusual variable name fex (``functional equivalence x'') because +; any variable appearing in a constraint is prohibited from occurring in +; any theorem proved with functional-instantiation from this constraint. + + (defthm functional-equivalence-constraint-4 + (implies (mem fex (domain (functional-equiv-fn1))) + (= (apply (functional-equiv-fn1) fex) + (apply (functional-equiv-fn2) fex))))) + +(defun every-where-= (s f g) + (cond ((ur-elementp s) t) + (t (and (= (apply f (scar s)) + (apply g (scar s))) + (every-where-= (scdr s) f g))))) + +(defthm every-where-=-implies-=-restrict + (implies (and (functionp f) + (functionp g) + (subsetp s (domain f)) + (subsetp s (domain g)) + (every-where-= s f g)) + (= (restrict f s) + (restrict g s))) + :rule-classes nil) + +(encapsulate + nil + (local + (defthm every-where-=-functional-equiv-fn1-functional-equiv-fn2 + (implies (subsetp s (domain (functional-equiv-fn1))) + (every-where-= s (functional-equiv-fn1) (functional-equiv-fn2))))) + + (defthm functional-equivalence-theorem + (= (functional-equiv-fn1) (functional-equiv-fn2)) + :rule-classes nil + :hints (("Goal" + :use (:instance every-where-=-implies-=-restrict + (f (functional-equiv-fn1)) + (g (functional-equiv-fn2)) + (s (domain (functional-equiv-fn1)))))))) + +; The above encapsulation provides a nice way to prove two functions +; are equal. You can just instantiate the lemma above with any two +; functions that are known to have the same domain and that are +; apply-equal everywhere. + +(defmacro functional-equivalence (name term + &key + hints + (rule-classes 'nil rule-classesp) + (otf-flg 'nil otf-flgp)) + (let* ((xterm + (acl2::case-match + term + (('implies acl2::& ('= acl2::& acl2::&)) + term) + (('= acl2::& acl2::&) + `(implies t ,term)) + (t nil)))) + (cond + ((null xterm) + `(acl2::er acl2::soft 'functional-equivalence + "The functional-equivalence strategy requires a term of ~ + the form (= f g) or (implies h (= f g)). Your term, ~x0, ~ + is not of this form." + ',term)) + ((acl2::assoc-equal "Goal" hints) + `(acl2::er acl2::soft 'functional-equivalence + "The functional-equivalence strategy provides hints for ~ + \"Goal\". Your hints should be provided for some Subgoal.")) + (t + (let ((hyps (cadr xterm)) + (lhs (cadr (caddr xterm))) + (rhs (caddr (caddr xterm)))) + `(defthm ,name ,term + :hints + (("Goal" + :use ((:functional-instance + functional-equivalence-theorem + (functional-equiv-fn1 + (lambda () + ,(if (eq hyps t) + lhs + `(if ,hyps ,lhs nil)))) + (functional-equiv-fn2 + (lambda () + ,(if (eq hyps t) + rhs + `(if ,hyps ,rhs nil))))))) + ,@hints) + ,@(if rule-classesp + `(:rule-classes ,rule-classes) + nil) + ,@(if otf-flgp + `(:otf-flg ,otf-flg) + nil))))))) + +; While I'm at it, I'll provide a way to prove that two sets are equal. + +; Suppose you have two arbitrary sets with the property that if x is a +; member of one, then x is a member of the other. + +(encapsulate ((subsetp-strategy-set1 () t) + (subsetp-strategy-set2 () t)) + (local (defun subsetp-strategy-set1 () nil)) + (local (defun subsetp-strategy-set2 () nil)) + +; We use the unusual variable name ssx (``subsetp strategy x'') because whatever +; var we use in a constraint is off-limits to the user in any theorem proved +; via functional instantiation based on these constraints. + + (defthm subsetp-strategy-constraint + (implies (mem ssx (subsetp-strategy-set1)) + (mem ssx (subsetp-strategy-set2))))) + +; Then the first set is a subset of the second. + +(encapsulate + nil + (local + (defthm subsetp-strategy-lemma + (implies (subsetp a (subsetp-strategy-set1)) + (subsetp a (subsetp-strategy-set2))))) + + (defthm subsetp-strategy + (subsetp (subsetp-strategy-set1) + (subsetp-strategy-set2)) + :rule-classes nil)) + +; And here is a handy macro to use this strategy to prove the subsetp +; relation between two expressions under a hypothesis. + +; This macro allows us to write: +; (defx foo (subsetp ... ...) +; :strategy subset-relation +; :rule-classes ...) + +(defmacro subset-relation (name term + &key + hints + (rule-classes 'nil rule-classesp) + (otf-flg 'nil otf-flgp)) + (let* ((xterm + (acl2::case-match + term + (('implies acl2::& ('subsetp acl2::& acl2::&)) + term) + (('subsetp acl2::& acl2::&) + `(implies t ,term)) + (t nil)))) + (cond + ((null xterm) + `(acl2::er acl2::soft 'subset-relation + "The subset-relation strategy requires a term of ~ + the form (subsetp a b) or (implies h (subsetp a b)). Your term, ~x0, ~ + is not of this form." + ',term)) + ((acl2::assoc-equal "Goal" hints) + `(acl2::er acl2::soft 'subset-relation + "The subset-relation strategy provides hints for ~ + \"Goal\". Your hints should be provided for some Subgoal.")) + (t + (let ((hyps (cadr xterm)) + (lhs (cadr (caddr xterm))) + (rhs (caddr (caddr xterm)))) + `(defthm ,name ,term + :hints + (("Goal" + :use ((:functional-instance + subsetp-strategy + (subsetp-strategy-set1 + (lambda () + ,(if (eq hyps t) + lhs + `(if ,hyps ,lhs nil)))) + (subsetp-strategy-set2 + (lambda () + ,(if (eq hyps t) + rhs + `(if ,hyps ,rhs nil))))))) + ,@hints) + ,@(if rule-classesp + `(:rule-classes ,rule-classes) + nil) + ,@(if otf-flgp + `(:otf-flg ,otf-flg) + nil))))))) + +; Here is a way to set equality using two subsets. It requires +; proving (mem x a) <-> (mem x b). + +; We can thus write +; (defx foo (implies ... (= ... ...)) +; :strategy equivalence-relation +; :rule-classes ...) + +; Two proof obligations are generated, each a mem implying a mem. You +; can provide hints for them with :hints-1 and :hints-2. + +(defmacro set-equivalence (name term + &key hints + (rule-classes 'nil rule-classesp) + (otf-flg 'nil otf-flgp) + (hints-1 'nil hints-1p) + (otf-flg-1 'nil otf-flg-1p) + (hints-2 'nil hints-2p) + (otf-flg-2 'nil otf-flg-2p)) + (let* ((xterm + (acl2::case-match term + (('implies acl2::& ('= acl2::& acl2::&)) + term) + (('= acl2::& acl2::&) + `(implies t ,term)) + (t nil)))) + (cond + ((null xterm) + `(acl2::er acl2::soft 'set-equivalence + "~x0 is not of the form (= x y) or of the form ~ + (implies hyps (= x y))." + ',term)) + ((or (acl2::assoc-equal "Goal" hints) + (acl2::assoc-equal "Goal" hints-1) + (acl2::assoc-equal "Goal" hints-2)) + `(acl2::er acl2::soft 'set-equivalence + "The set-equivalence strategy provides hints for ~ + \"Goal\". Your hints should be provided for some Subgoal.")) + (t + (let ((hyps (cadr xterm)) + (lhs (cadr (caddr xterm))) + (rhs (caddr (caddr xterm))) + (name-1 (packn-in-pkg (list name "-1") name)) + (name-2 (packn-in-pkg (list name "-2") name))) + `(encapsulate + nil + (local + (defx ,name-1 + ,(if (eq hyps t) + `(subsetp ,lhs ,rhs) + `(implies ,hyps (subsetp ,lhs ,rhs))) + :strategy subset-relation + ,@(if hints-1p `(:hints ,hints-1) nil) + ,@(if otf-flg-1p `(:otf-flg ,otf-flg-1) nil) + :rule-classes nil)) + (local + (defx ,name-2 + ,(if (eq hyps t) + `(subsetp ,rhs ,lhs) + `(implies ,hyps (subsetp ,rhs ,lhs))) + :strategy subset-relation + ,@(if hints-2p `(:hints ,hints-2) nil) + ,@(if otf-flg-2p `(:otf-flg ,otf-flg-2) nil) + :rule-classes nil)) + (defthm ,name ,term + :hints + (("Goal" + :use ((:instance =-iff-subsetps + (a ,(if (eq hyps t) + lhs + `(if ,hyps ,lhs nil))) + (b ,(if (eq hyps t) + rhs + `(if ,hyps ,rhs nil)))) + (:instance ,name-1) + (:instance ,name-2)) + ,@hints)) + ,@(if rule-classesp + `(:rule-classes ,rule-classes) + nil) + ,@(if otf-flgp + `(:otf-flg ,otf-flg) + nil)))))))) + +; ---------------------------------------------------------------------------- +; An Example + +(defx union-diff-diff + (implies (and (subsetp a b) + (subsetp b c)) + (= (union (diff b a) + (diff c b)) + (diff c a))) + :strategy :set-equivalence) + +;---------------------------------------------------------------------------- +; Sequences + +; A sequence is a function whose domain is an initial subset of the +; natural numbers. + +(defun nats (n) + (if (zp n) + '(0) + (scons n (nats (- n 1))))) + +(defthm ur-elementp-nats + (not (ur-elementp (nats n)))) + +(defcong = = (nats n) 1 + :hints (("Goal" :in-theory (enable zp)))) + +(defthm mem-nats + (equal (mem e (nats n)) + (and (integerp e) + (<= 0 e) + (<= e (nfix n)))) + :hints (("Goal" :in-theory (enable =)))) + +(defun sequencep (s) + (and (functionp s) + (= (domain s) + (diff (nats (cardinality s)) '(0))))) + +(defthm functionp-sequencep + (implies (sequencep s) + (functionp s))) + +(defthm domain-sequencep + (implies (sequencep s) + (= (domain s) + (diff (nats (cardinality s)) '(0))))) + +(in-theory (disable sequencep)) + +(defun shift (i j f delta) + (declare (xargs :measure (nfix (- (+ 1 (acl2::ifix j)) (acl2::ifix i))))) + (cond ((and (integerp i) + (integerp j) + (<= i j)) + (except (shift (+ 1 i) j f delta) + (+ i delta) + (apply f i))) + (t nil))) + +(defcong = = (shift i j f delta) 1) +(defcong = = (shift i j f delta) 2) +(defcong = = (shift i j f delta) 3) +(defcong = = (shift i j f delta) 4) + +(defthm functionp-shift + (functionp (shift i j f delta))) + +; If f is a sequence, its domain is [1...n]. So (shift i j f delta) +; takes [i...j] to [i+delta ... j+delta]. This is + +(defthm mem-domain-shift + (implies (integerp delta) + (= (mem x (domain (shift i j f delta))) + (and (integerp i) + (integerp j) + (<= i j) + (integerp x) + (<= (+ i delta) x) + (<= x (+ j delta)))))) + +; We can express the domain of a shift of a sequence as a set of nats. + +(defx domain-shift + (implies (and (sequencep s) + (integerp delta) + (<= 0 delta)) + (= (domain (shift 1 (cardinality s) s delta)) + (diff (nats (+ delta (cardinality s))) + (nats delta)))) + :strategy :set-equivalence) + +(defun concat (r s) + (union r (shift 1 (cardinality s) s (cardinality r)))) + +(defcong = = (concat r s) 1) +(defcong = = (concat r s) 2) + +(defthm functionp-concat + (implies (and (sequencep r) + (sequencep s)) + (functionp (concat r s)))) + +(defthm subsetp-nats-0 + (subsetp '(0) (nats i))) + +(defthm =-0 + (equal (= i 0) + (equal i 0)) + :hints (("Goal" :in-theory (enable =)))) + +(defthm subsetp-nats-nats + (equal (subsetp (nats i) (nats j)) + (<= (nfix i) (nfix j)))) + +(defthm domain-concat + (implies (and (sequencep r) + (sequencep s)) + (= (domain (concat r s)) + (diff (nats (+ (cardinality r) (cardinality s))) + '(0))))) + +; I need the (integerp delta) hypothesis because cardinality raises +; the question of membership in the shifted domain and +; mem-domain-shift has an integerp hyp. + +(defthm cardinality-shift + (implies (integerp delta) + (= (cardinality (shift i j f delta)) + (if (and (integerp i) + (integerp j) + (<= i j)) + (+ 1 (- j i)) + 0)))) + +(defthm cardinality-concat + (implies (and (sequencep r) + (sequencep s)) + (= (cardinality (concat r s)) + (+ (cardinality r) (cardinality s)))) + :hints (("Goal" + :use (:instance disjoint-domains-implies-disjoint + (a r) + (b (shift 1 (cardinality s) s (cardinality r))))))) + +(defthm sequencep-concat + (implies (and (sequencep r) + (sequencep s)) + (sequencep (concat r s))) + :hints (("Goal" + :in-theory + (set-difference-theories (enable sequencep) + '(concat))))) + +; Here is a recursive alternative definition of apply. + +(defthm apply-scons + (implies (functionp (scons pair f)) + (= (apply (scons pair f) x) + (if (= (hd pair) x) + (tl pair) + (apply f x)))) + :hints (("Goal" :in-theory (enable apply)) + ("Subgoal 2.1'" + :in-theory (set-difference-theories (enable functionp) + '(functionp-scons-lemma)) + + :use ((:instance functionp-scons-lemma + (a f) + (b f) + (e (pair hd tl))) + (:instance mem-singleton + (x (subset-such-that1 f hd)) + (e (pair hd tl))))))) + +(defthm apply-disjoint-union + (implies (and (functionp a) + (functionp b) + (not (intersection (domain a) (domain b)))) + (= (apply (union a b) x) + (if (mem x (domain a)) + (apply a x) + (apply b x))))) + +; Suppose you have a function, f, (not necessarily a sequence) and you +; form another function, f', by shifting [i...j] of f up by delta. +; What is (apply f' x)? The domain of f' is [i+delta ... j+delta]. +; If x is in that domain, then (apply f' x) is (apply f (- x delta)). + +; To prove this we need the important fact: + +(defthm apply-shift + (= (apply (shift i j f delta) x) + (if (mem x (domain (shift i j f delta))) + (apply f (- x delta)) + nil))) + +(defthm apply-concat + (implies (and (sequencep r) + (sequencep s)) + (= (apply (concat r s) i) + (cond ((and (integerp i) + (< 0 i)) + (if (<= i (cardinality r)) + (apply r i) + (apply s (- i (cardinality r))))) + (t nil)))) + :hints (("Subgoal 11" + :in-theory (disable apply-outside-domain) + :use + ((:instance apply-outside-domain + (e (- i (cardinality r))) + (f s)))))) + +(in-theory (disable concat)) + +(defx associativity-of-concat + (implies (and (sequencep a) + (sequencep b) + (sequencep c)) + (= (concat (concat a b) c) + (concat a (concat b c)))) + :strategy :functional-equivalence) + +; Now I will define seq-hd and seq-tl to let me do recursion down +; sequences. + +(defun seq-hd (s) (apply s 1)) + +(defcong = = (seq-hd s) 1) + +(defun seq-tl (s) + (restrict (shift 1 (cardinality s) s -1) + (diff (nats (- (cardinality s) 1)) + (brace 0)))) + +(defcong = = (seq-tl s) 1) + +(defthm functionp-seq-tl + (functionp (seq-tl s))) + +(defthm cardinality-restrict + (= (cardinality (restrict f s)) + (cardinality (intersection (domain f) s)))) + + + +(defx domain-shift-generalized + (implies (and (integerp i) + (integerp j) + (<= i j) + (integerp delta) + (<= 0 (+ i delta))) + (= (domain (shift i j s delta)) + (if (= (+ delta i) 0) + (nats (+ delta j)) + (diff (nats (+ delta j)) + (nats (+ delta i -1)))))) + :strategy :set-equivalence) + +(defthm cardinality-positive + (implies (not (ur-elementp s)) + (< 0 (cardinality s))) + :rule-classes :linear) + +(defthm intersection-x-x + (= (intersection x x) (sfix x))) + +(defthm cardinality-diff-nats-0 + (implies (and (integerp i) + (<= 0 i)) + (= (cardinality (diff (nats i) '(0))) + i))) + +(defthm cardinality-seq-tl + (implies (not (ur-elementp s)) + (= (cardinality (seq-tl s)) + (- (cardinality s) 1)))) + +(defthm sequencep-seq-tl + (implies (not (ur-elementp s)) + (sequencep (seq-tl s))) + :hints (("Goal" :in-theory (enable sequencep)))) + +(defthm seq-tl-recursion + (implies (not (ur-elementp s)) + (< (cardinality (seq-tl s)) + (cardinality s))) + :rule-classes (:built-in-clause :linear)) + +(in-theory (disable seq-hd seq-tl)) + +; Next, I define defmap. Thus, + +; (defmap subset (a s b) :for x :in s :such-that (bd a x b)) +; and +; (defmap image (a s b) :for x :in s :map (bd a x b)) + +; will define subset and image recursively so that they return the +; sets described below + +; (subset a s b) = {x in s | (bd a x b)} +; and +; (image a s b) = {(bd a x b) | x in s} + +; In addition, I get a few useful theorems about these functions, including +; that = is a congruence for every argument. + +; It must be the case that congruence rules are already in place for +; (bd a x b). + +(defun defmap-congruences (vars call sloc i) + (cond + ((endp vars) nil) + (t (cons (if (equal sloc i) + `(defx :strategy :congruence ,call ,i :method :subsetp) + `(defx :strategy :congruence ,call ,i)) + (defmap-congruences (cdr vars) call sloc (+ 1 i)))))) + +(defmacro defmap (name vars + &key + (for 'nil forp) + (in 'nil inp) + (such-that 'nil such-thatp) + (map 'nil mapp)) + +; (defmap foo (s ...) :for x :in s :such-that px) +; or +; (defmap foo (s ...) :for x :in s :map px) + + (cond + ((not (and (symbolp name) + (acl2::symbol-listp vars) + forp + (symbolp for) + (not (acl2::member-equal for vars)) + inp + (symbolp in) + (acl2::member-equal in vars) + (or (and such-thatp (not mapp)) + (and (not such-thatp) mapp)))) + `(acl2::er acl2::soft 'defmap + "The proper form of a defmap command is~%~ + (defmap name vars :for x :in v :such-that body)~%~ + or~%~ + (defmap name vars :for x :in v :map body),~%~ + where name is a new function name, vars is a list of ~ + variables, x is a variable not in vars, ~ + v is a variable in vars, and body is a term.")) + (such-thatp + (let* ((x for) + (s in) + (sloc (- (length vars) (length (member s vars)))) + (body such-that) + (s1 (genname1 s 1 (cons x vars))) + (call `(,name ,@vars)) + (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars)))) + `(encapsulate + nil + (defun ,name (,@vars) + (if (ur-elementp ,s) + nil + (let ((,x (scar ,s))) + (if ,body + (scons (scar ,s) ,rcall) + ,rcall)))) + + (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap) + (setp ,call)) + + (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap) + (equal (ur-elementp ,call) + (equal ,call nil))) + + (defthm ,(packn-in-pkg (list "MEM-" name) 'defmap) + (equal (mem ,x ,call) + (and ,body ; we write it this way in case body + (mem ,x ,s))) ; is not Boolean! + :otf-flg t) + + (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap) + (subsetp ,call ,s)) + + ,@(defmap-congruences vars call (+ sloc 1) 1) + + (defthm ,(packn-in-pkg (list "MEM-" name "-CORROLLARY") 'defmap) + (implies (and (subsetp ,s1 ,call) + (mem ,x ,s1)) + ,body)) + + (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap) + (<= (cardinality ,call) + (cardinality ,s)) + :rule-classes :linear) + + (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap) + (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars)) + (union (,name ,@(put-nth s1 sloc vars)) + ,call))) + + (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap) + (= (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars)) + (intersection (,name ,@(put-nth s1 sloc vars)) + ,call))) + + ))) + (t ;;; :map + + (let* ((x for) + (s in) + (sloc (- (length vars) (length (member s vars)))) + (body map) + (fx (genname1 x 1 (cons x vars))) + (s1 (genname1 s 1 (cons fx (cons x vars)))) + (call `(,name ,@vars)) + (rcall `(,name ,@(put-nth `(scdr ,s) sloc vars)))) + `(encapsulate + nil + (defun ,name (,@vars) + (if (ur-elementp ,s) + nil + (let ((,x (scar ,s))) + (scons ,body ,rcall)))) + + (defthm ,(packn-in-pkg (list "SETP-" name) 'defmap) + (setp ,call)) + + (defthm ,(packn-in-pkg (list "UR-ELEMENTP-" name) 'defmap) + (equal (ur-elementp ,call) + (ur-elementp ,s))) + + (defthm ,(packn-in-pkg (list "WEAK-MEM-" name) 'defmap) + (implies (and (mem ,x ,s) + (= ,fx ,body)) + (mem ,fx ,call))) + + + (defthm ,(packn-in-pkg (list "SUBSETP-" name) 'defmap) + (implies (subsetp ,s1 ,s) + (subsetp (,name ,@(put-nth s1 sloc vars)) + ,call))) + + ,@(defmap-congruences vars call (+ sloc 1) 1) + + (defthm ,(packn-in-pkg (list "CARDINALITY-" name) 'defmap) + (<= (cardinality ,call) + (cardinality ,s)) + :rule-classes :linear) + + (defthm ,(packn-in-pkg (list "UNION-" name) 'defmap) + (= (,name ,@(put-nth `(union ,s1 ,s) sloc vars)) + (union (,name ,@(put-nth s1 sloc vars)) + ,call))) + +; Once I thought that +; (image (intersection s1 s)) = (intersection (image s1) (image s)) +; But this is wrong. Consider +; s1 = {(0 . 1) (0 . 2)} +; s = {(1 . 1) (1 . 2)} +; let (body e) = (cdr e) (or (tl e) if the elements are pairps) +; Then the lhs is nil because the two sets are disjoint, but the +; rhs is {1 2}. + + (defthm ,(packn-in-pkg (list "INTERSECTION-" name) 'defmap) + (subsetp (,name ,@(put-nth `(intersection ,s1 ,s) sloc vars)) + (intersection (,name ,@(put-nth s1 sloc vars)) + ,call))) + + ))))) + +#| +; Here are examples of both styles of defmap: + +(defstub bd (a x b) t) +(acl2::skip-proofs + (progn (defcong = = (bd a x b) 1) + (defcong = = (bd a x b) 2) + (defcong = = (bd a x b) 3))) + +(defmap subset (a s b) :for x :in s :such-that (bd a x b)) +(defmap image (a s b) :for x :in s :map (bd a x b)) + +|# + diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp new file mode 100644 index 0000000..de78bee --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering-original.lisp @@ -0,0 +1,267 @@ +; Finite Set Theory for ACL2 +; Copyright (C) 2000 University of Texas at Austin + +; This program is free software; you can redistribute it and/or modify it under +; the terms of Version 2 of the GNU General Public License as published by the +; Free Software Foundation. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: J Strother Moore +; email: Moore@cs.utexas.edu +; Department of Computer Science +; University of Texas at Austin +; Austin, TX 78701 U.S.A. + +; The original kernel of this book was created with support from +; Compaq Systems Research Center, Palo Alto, CA. + +(in-package "ACL2") + +; We define a total ordering on ordinary ACL2 objects composed of +; numbers, characters, strings, symbols, and conses of these things. + +; We export +; (ordinaryp x) the notion of "ordinary objects" +; (<< x y) disabled the total ordering on such objects + +; <<-irreflexivity the four obvious theorems about +; <<-trichotomy disabled total orders +; <<-mutual-exclusion disabled +; <<-transitivity disabled + +; We provide ``fast'' versions of the slow rules, named + +; fast-<<-trichotomy enabled +; fast-<<-mutual-exclusion enabled +; fast-<<-transitivity enabled + +; We also provide two theory macros for fiddling with the status of +; these rules. + +; Options: +; :in-theory (fast-<<-rules) ; the default setting above +; :in-theory (fast-<<-rules <<) ; default plus << enabled +; :in-theory (slow-<<-rules) ; slow rules enabled but << disabled +; :in-theory (slow-<<-rules <<) ; slow rules and << enabled + +; These macros never enable BOTH the fast and slow rules. Sometimes +; you need << and sometimes you don't. The optional << always has the +; same effect whether you're using fast- or slow-<<-rules. Including +; the << arg ENABLES <<. + +(defun ordinaryp (x) + (cond ((atom x) + (or (acl2-numberp x) + (characterp x) + (stringp x) + (symbolp x))) + (t (and (consp x) + (ordinaryp (car x)) + (ordinaryp (cdr x)))))) + +; This is used only for admitting the ordering relation. + +(defun vcount (x) + (cond ((atom x) + (cond ((acl2-numberp x) 0) + ((characterp x) 0) + ((stringp x) (+ 1 (length x))) + ((symbolp x) + (cond ((equal x nil) 0) + (t (+ 3 + (length (symbol-package-name x)) + (length (symbol-name x)))))) + (t 0))) + (t (+ 1 (vcount (car x)) (vcount (cdr x)))))) + +(local + (defthm vcount-character-listp + (implies (character-listp x) + (equal (vcount x) (len x))))) + +; The temptation below is to order all symbols by comparing their +; symbol-package-names and their symbol-names, lexicographically. But +; how does NIL compare to things? Since NIL occurs in its +; symbol-package-name, such recursion would not terminate. So we put +; NIL before all other symbols. + +(defun << (x y) + (declare (xargs :measure (vcount x))) + (cond + ((atom x) + (cond ((atom y) + (cond ((acl2-numberp x) + (cond ((acl2-numberp y) (< x y)) + (t t))) + ((characterp x) + (cond ((acl2-numberp y) nil) + ((characterp y) (< (char-code x) (char-code y))) + (t t))) + ((stringp x) + (cond ((acl2-numberp y) nil) + ((characterp y) nil) + ((stringp y) + (<< (coerce x 'list) + (coerce y 'list))) + (t t))) + ((symbolp x) + (cond ((acl2-numberp y) nil) + ((characterp y) nil) + ((stringp y) nil) + ((symbolp y) + (cond ((equal x nil) + (cond ((equal y nil) nil) + (t t))) + ((equal y nil) nil) + (t + (or (<< (symbol-package-name x) + (symbol-package-name y)) + (and (equal (symbol-package-name x) + (symbol-package-name y)) + (<< (symbol-name x) + (symbol-name y))))))) + (t t))) + (t nil))) + (t t))) + ((atom y) nil) + (t (or (<< (car x) (car y)) + (and (equal (car x) (car y)) + (<< (cdr x) (cdr y))))))) + +; Now we prove that << is a total ordering on ACL2 objects. + +(defthm <<-irreflexivity + (not (<< x x))) + +(local + (defthm character-listp-implies-ordinaryp + (implies (character-listp x) + (ordinaryp x)))) + +; The next three were pulled straight out of axioms.lisp, where they +; were proved locally. + +(local + (defthm symbol-equality-rewrite + (implies (and (symbolp s1) + (symbolp s2) + (equal (symbol-name s1) + (symbol-name s2)) + (equal (symbol-package-name s1) + (symbol-package-name s2))) + (equal (equal s1 s2) t)) + :hints (("Goal" :use symbol-equality)))) + +(local + (defthm equal-coerce + (implies (and (stringp x) + (stringp y)) + (equal (equal (coerce x 'list) + (coerce y 'list)) + (equal x y))) + :hints (("Goal" :use + ((:instance coerce-inverse-2 (x x)) + (:instance coerce-inverse-2 (x y))) + :in-theory (disable coerce-inverse-2))))) + +(local + (defthm equal-char-code-rewrite + (implies (and (characterp x) + (characterp y)) + (implies (equal (char-code x) (char-code y)) + (equal (equal x y) t))) + :hints (("Goal" :use equal-char-code)))) + +(defthm <<-trichotomy + (implies (and (ordinaryp x) + (ordinaryp y)) + (or (<< x y) + (equal x y) + (<< y x))) + :rule-classes + ((:rewrite :corollary + (implies (and (ordinaryp x) + (ordinaryp y) + (not (<< x y)) + (not (equal x y))) + (<< y x))))) + +(defthm <<-mutual-exclusion + (implies (<< x y) + (and (not (equal x y)) + (not (<< y x)))) + :rule-classes + ((:rewrite :corollary + (implies (<< x y) + (and (not (equal x y)) + (not (<< y x))))))) + +(defthm <<-transitivity + (implies (and (<< x y) (<< y z)) (<< x z))) + +(defthm fast-<<-trichotomy + (and (implies (and (not (<< xxx y)) + (equal xxx x) + (ordinaryp x) + (ordinaryp y) + (not (equal x y))) + (<< y x)) + (implies (and (not (<< x yyy)) + (equal yyy y) + (ordinaryp x) + (ordinaryp y) + (not (equal x y))) + (<< y x)))) + +(defthm fast-<<-mutual-exclusion + (and (implies (and (<< xxx y) + (equal xxx x)) + (and (not (equal x y)) + (not (<< y x)))) + (implies (and (<< x yyy) + (equal yyy y)) + (and (not (equal x y)) + (not (<< y x)))))) + +(defthm fast-<<-transitivity + (implies (and (<< x y) + (<< yyy z) + (equal yyy x)) + (<< x z))) + +(defmacro fast-<<-rules (&optional <<) + +; If << is non-nil, then enable <<, else, don't. + + `(set-difference-theories (enable ,@(if << '((:DEFINITION <<)) nil) + fast-<<-trichotomy + fast-<<-mutual-exclusion + fast-<<-transitivity) + '(,@(if << nil '((:DEFINITION <<))) + <<-trichotomy + <<-mutual-exclusion + <<-transitivity))) + +(defmacro slow-<<-rules (&optional <<) + +; If << is non-nil, then enable <<, else, don't. + + `(set-difference-theories (enable ,@(if << '((:DEFINITION <<)) nil) + <<-trichotomy + <<-mutual-exclusion + <<-transitivity) + '(,@(if << nil '((:DEFINITION <<))) + fast-<<-trichotomy + fast-<<-mutual-exclusion + fast-<<-transitivity))) + +(in-theory (fast-<<-rules)) + diff --git a/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp new file mode 100644 index 0000000..0ff4c19 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/finite-set-theory/total-ordering.lisp @@ -0,0 +1,165 @@ +; Finite Set Theory for ACL2 + +; Copyright (C) 2001 Georgia Institute of Technology + +; This book is derived from the book "total-ordering-original" by J +; Moore, which is included in this directory. The difference between +; this version and J Moore's version is that I use the total order +; built into ACL2 (starting with version 2.6). This allows me to +; significantly simplify some of the theorems and to also remove +; theorems. + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios +; email: manolios@cc.gatech.edu +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") + +; We define an irreflexive total ordering on the ACL2 universe. + +; We export +; (<< x y) disabled the total ordering + +; <<-irreflexivity the four obvious theorems about +; <<-trichotomy disabled total orders +; <<-mutual-exclusion disabled +; <<-transitivity disabled + +; We provide ``fast'' versions of the slow rules, named + +; fast-<<-trichotomy enabled +; fast-<<-mutual-exclusion enabled +; fast-<<-transitivity enabled + +; We also provide two theory macros for fiddling with the status of +; these rules. + +; Options: +; :in-theory (fast-<<-rules) ; the default setting above +; :in-theory (fast-<<-rules <<) ; default plus << enabled +; :in-theory (slow-<<-rules) ; slow rules enabled but << disabled +; :in-theory (slow-<<-rules <<) ; slow rules and << enabled + +; These macros never enable BOTH the fast and slow rules. Sometimes +; you need << and sometimes you don't. The optional << always has the +; same effect whether you're using fast- or slow-<<-rules. Including +; the << arg ENABLES <<. + +(defun <<< (x y) + (declare (xargs :guard t)) + (and (not (equal x y)) + (lexorder x y))) + +(defun << (x y) + (declare (xargs :guard t)) + (cond ((eq x nil) + (not (eq y nil))) + ((atom x) + (cond ((eq y nil) nil) + (t (<<< x y)))) + ((atom y) nil) + ((equal (car x) (car y)) + (<< (cdr x) (cdr y))) + (t (<< (car x) (car y))))) + +(defthm <<-irreflexivity + (not (<< x x))) + +(local +(defthm lexorder-atom + (implies (and (atom x) + (consp y)) + (lexorder x y)) + :hints (("Goal" :in-theory (enable lexorder))))) + +(defthm <<-trichotomy + (or (<< x y) + (equal x y) + (<< y x)) + :rule-classes + ((:rewrite :corollary + (implies (and (not (<< x y)) + (not (equal x y))) + (<< y x))))) + +(defthm <<-mutual-exclusion + (implies (<< x y) + (and (not (equal x y)) + (not (<< y x))))) + +(defthm <<-transitivity + (implies (and (<< x y) + (<< y z)) + (<< x z))) + +(defthm fast-<<-trichotomy + (and (implies (and (not (<< xxx y)) + (equal xxx x) + (not (equal x y))) + (<< y x)) + (implies (and (not (<< x yyy)) + (equal yyy y) + (not (equal x y))) + (<< y x)))) + +(defthm fast-<<-mutual-exclusion + (and (implies (and (<< xxx y) + (equal xxx x)) + (and (not (equal x y)) + (not (<< y x)))) + (implies (and (<< x yyy) + (equal yyy y)) + (and (not (equal x y)) + (not (<< y x)))))) + +(defthm fast-<<-transitivity + (implies (and (<< x y) + (<< yyy z) + (equal yyy x)) + (<< x z))) + +(defmacro fast-<<-rules (&optional <<) + +; If << is non-nil, then enable <<, else, don't. + + `(set-difference-theories (enable ,@(if << '((:DEFINITION <<) (:definition acl2::alphorder)) nil) + fast-<<-trichotomy + fast-<<-mutual-exclusion + fast-<<-transitivity) + '(,@(if << nil '((:DEFINITION <<))) + <<-trichotomy + <<-mutual-exclusion + <<-transitivity))) + +(defmacro slow-<<-rules (&optional <<) + +; If << is non-nil, then enable <<, else, don't. + + `(set-difference-theories (enable ,@(if << '((:DEFINITION <<) (:definition acl2::alphorder)) nil) + <<-trichotomy + <<-mutual-exclusion + <<-transitivity) + '(,@(if << nil '((:DEFINITION <<))) + fast-<<-trichotomy + fast-<<-mutual-exclusion + fast-<<-transitivity))) + +(in-theory (fast-<<-rules)) diff --git a/books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp b/books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp new file mode 100644 index 0000000..755b6ca --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/records/certify-original.lsp @@ -0,0 +1,2 @@ +(certify-book "records-original") +:u diff --git a/books/workshops/2002/manolios-kaufmann/support/records/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/records/certify.lsp new file mode 100644 index 0000000..c836b99 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/records/certify.lsp @@ -0,0 +1,4 @@ +(certify-book "total-order") +:u +(certify-book "records") +:u diff --git a/books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp b/books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp new file mode 100644 index 0000000..99326d3 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/records/records-original.lisp @@ -0,0 +1,380 @@ +(in-package "ACL2") + +(defun fieldp (x) + (or (symbolp x) (integerp x))) + +(defthm fieldp-compound-recognizer + (iff (fieldp x) + (or (symbolp x) + (integerp x))) + :rule-classes :compound-recognizer) + +(defthm integerp-forward-chain-fieldp + (implies (integerp x) (fieldp x)) + :rule-classes :forward-chaining) + +(defthm symbolp-forward-chain-fieldp + (implies (symbolp x) (fieldp x)) + :rule-classes :forward-chaining) + +(in-theory (disable fieldp)) + +(defun field-< (x y) + (if (symbolp x) + (and (symbolp y) + (symbol-< x y)) + (or (symbolp y) + (< x y)))) + +(local +(defthm field-<-irreflexive + (not (field-< x x)))) + +(local +(defthm field-<-transitive + (implies (and (field-< x y) + (field-< y z)) + (field-< x z)))) + +(local +(defthm field-<-asymmetric + (implies (field-< x y) + (not (field-< y x))))) + +(local +(defthm field-<-trichotomy + (implies (and (fieldp x) (fieldp y) + (not (field-< y x))) + (iff (field-< x y) + (not (equal x y)))))) + +(in-theory (disable field-<)) + + + + +; Ordered field-alist with no nil cdrs: +(defun sap (x) + (if (atom x) + (null x) + (and (consp (car x)) + (fieldp (caar x)) + (cdar x) + (if (atom (cdr x)) + (null (cdr x)) + (and (sap (cdr x)) + ;; We unforunately probably ruin tail-recursion here, but at + ;; least we can verify the guards. + (field-< (caar x) (caadr x))))))) + +; Lookup structure: +(defun lsp (x) + (or (sap x) + (and (consp x) + (not (lsp (cdr x))) + (sap (car x)) + (car x)))) + +(defun g (a x) + (cond + ((sap x) + (cdr (assoc-equal a x))) + ((lsp x) + (cdr (assoc-equal a (car x)))) + (t + nil))) + +; Ordinary setting, used for non-nil values: +(defun s-aux (a v r) + (cond ((endp r) + (cons (cons a v) nil)) + ((equal a (caar r)) + (cons (cons a v) (cdr r))) + ((field-< a (caar r)) + (cons (cons a v) r)) + (t (cons (car r) (s-aux a v (cdr r)))))) + +(defun delete-key (key alist) + (cond + ((endp alist) + alist) + ((equal key (caar alist)) + (cdr alist)) + (t + (cons (car alist) + (delete-key key (cdr alist)))))) + +(defun s (a v x) + (cond + ((sap x) + (if (null v) + (delete-key a x) + (s-aux a v x))) + ((not (lsp x)) + (if v + ;; then make x into the cdr of the returned lookup structure + (cons (list (cons a v)) x) + ;; else x already is an appropriate result + x)) + ((null v) + (if (and (null (cdr (car x))) + (equal (caar (car x)) a)) + (cdr x) + (cons (delete-key a (car x)) + (cdr x)))) + (t + (cons (s-aux a v (car x)) + (cdr x))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Interaction properties for s and g; +;;; search for $$$ for main theorems. +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(local +(defthm not-field-<-x-x + (not (field-< x x)) + :hints (("Goal" :in-theory (enable field-<))))) + +(local +(defthm delete-key-no-op + (implies (and (sap alist) + (not (assoc-equal key alist))) + (equal (delete-key key alist) alist)))) + +(local +(defthm values-not-nil + (implies (sap alist) + ;; The order below ooks dangerous, but apparently the prover's + ;; heuristics save us. + (iff (assoc-equal key alist) + (cdr (assoc-equal key alist)))))) + +(local +(defthm key-order-lemma + (implies (and (fieldp a) + (sap alist) + (field-< a (caar alist))) + (not (cdr (assoc-equal a alist)))))) + +(local +(defthm s-aux-to-same + (implies (and (fieldp a) + (sap alist) + (cdr (assoc-equal a alist))) + (equal (s-aux a (cdr (assoc-equal a alist)) + alist) + alist)))) + +; $$$ A main theorem +(defthm s-same-g + (implies (force (fieldp a)) + (equal (s a (g a r) r) + r))) + +(local +(defthm value-s-aux + (implies (and (fieldp a) + (sap alist)) + (equal (cdr (assoc-equal a (s-aux a v alist))) + v)))) + +(local +(defthm s-aux-preserves-sap + (implies (and (sap x) + (fieldp a) + v) + (sap (s-aux a v x))))) + +(local +(defthm cdr-assoc-equal-delete-key + (implies (sap x) + (not (cdr (assoc-equal a (delete-key a x))))))) + +; G-diff-s should go here, but I forgot it on the first pass, so I'll put +; it at the end where more lemmas are available. + +(local +(defthm sap-delete-key + (implies (sap alist) + (sap (delete-key a alist))))) + +(local +(defthm sap-forward-to-fieldp-caar + (implies (sap alist) + (fieldp (caar alist))) + :rule-classes :forward-chaining)) + +; $$$ A main theorem +(defthm g-same-s + (implies (force (fieldp a)) + (equal (g a (s a v r)) + v))) + +(local +(defthm s-aux-s-aux-same + (implies (and (fieldp a) + (sap alist)) + (equal (s-aux a v (s-aux a w alist)) + (s-aux a v alist))))) + +(local +(defthm delete-key-s-aux-same + (implies (and (fieldp a) + (sap alist)) + (equal (delete-key a (s-aux a v alist)) + (delete-key a alist))))) + +(local +(defthm field-<-s-aux + (implies (and (sap alist) + (fieldp a) + (fieldp b) + (field-< b (caar alist)) + (not (field-< a b)) + (not (equal a b))) + (field-< b (caar (s-aux a v alist)))))) + +(local +(defthm value-nil-sufficiency + (implies (and (sap alist) + (fieldp a) + (field-< a (caar alist))) + (equal (cdr (assoc-equal a alist)) + nil)))) + +(local +(defthm caar-delete-key + (implies (sap alist) + (equal (caar (delete-key a alist)) + (if (eq a (caar alist)) + (caadr alist) + (caar alist)))))) + +(local +(defthm s-aux-delete-key + (implies (sap alist) + (equal (s-aux a x (delete-key a alist)) + (s-aux a x alist))))) + +(local +(defthm field-<-hack + (implies (and (field-< r6 r9) + (not (field-< r4 r9)) + (not (equal r6 r4)) + (fieldp r4) + (fieldp r6) + (fieldp r9)) + (field-< r6 r4)) + :hints (("Goal" :in-theory (disable field-<-trichotomy) + :use ((:instance field-<-trichotomy + (x r6) (y r4))))))) + +; $$$ A main theorem +(defthm s-same-s + (implies (force (fieldp a)) + (equal (s a y (s a x r)) + (s a y r)))) + +(local +(defthm s-aux-diff-s-aux + (implies (and (not (equal a b)) + (sap r) + x + y + (fieldp a) + (fieldp b)) + (equal (s-aux b y (s-aux a x r)) + (s-aux a x (s-aux b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s-aux)))) + ;; The earlier forward-chaining rule hurts here. + :hints (("Goal" :in-theory (disable sap-forward-to-fieldp-caar))))) + +(local +(defthm sap-s-aux + (implies (and (sap x) + (fieldp a) + v) + (sap (s-aux a v x))))) + +(local +(defthm consp-delete-key + (implies (sap alist) + (equal (consp (delete-key a alist)) + (or (consp (cdr alist)) + (and (consp alist) + (not (equal a (caar alist))))))))) + +(local +(defthm delete-key-delete-key + (implies (sap r) + (equal (delete-key b (delete-key a r)) + (delete-key a (delete-key b r)))) + :rule-classes ((:rewrite :loop-stopper ((b a delete-key)))))) + +(local +(defthm delete-key-s-aux + (implies (and (not (equal a b)) + (sap r) + x + (fieldp a) + (fieldp b)) + (equal (delete-key b (s-aux a x r)) + (s-aux a x (delete-key b r)))) + ;; The earlier forward-chaining rule hurts here. + :hints (("Goal" :in-theory (disable sap-forward-to-fieldp-caar))))) + +(local +(defthm delete-key-nil + (implies (not (delete-key a x)) + (not (delete-key a (delete-key b x)))))) + +; $$$ A main theorem +(defthm s-diff-s + (implies (and (force (fieldp a)) + (force (fieldp b)) + (not (equal a b))) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +(local +(defthm assoc-equal-s-aux-different + (implies (not (equal a b)) + (equal (assoc-equal a (s-aux b v alist)) + (assoc-equal a alist))))) + +(local +(defthm assoc-equal-delete-key-different + (implies (not (equal a b)) + (equal (assoc-equal a (delete-key b alist)) + (assoc-equal a alist))))) + +; $$$ A main theorem +(defthm g-diff-s + (implies (and (force (fieldp a)) + (force (fieldp b)) + (not (equal a b))) + (equal (g a (s b v r)) + (g a r)))) + + +;;;; some simple macros for defining sets and gets.. + +(in-theory (disable s g)) + +(defmacro <- (x a) `(g ,a ,x)) + +(defmacro -> (x a v) `(s ,a ,v ,x)) + +(defun update-macro (upds result) + (declare (xargs :guard (keyword-value-listp upds))) + (if (endp upds) result + (update-macro (cddr upds) + (list 's (car upds) (cadr upds) result)))) + +(defmacro update (old &rest updates) + (declare (xargs :guard (keyword-value-listp updates))) + (update-macro updates old)) diff --git a/books/workshops/2002/manolios-kaufmann/support/records/records.lisp b/books/workshops/2002/manolios-kaufmann/support/records/records.lisp new file mode 100644 index 0000000..e7e40a2 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/records/records.lisp @@ -0,0 +1,287 @@ +(in-package "ACL2") +(include-book "total-order") + +; Ordered field-alist with no nil cdrs: +(defun sap (x) + (if (atom x) + (null x) + (and (consp (car x)) + (cdar x) + (if (atom (cdr x)) + (null (cdr x)) + (and (sap (cdr x)) + ;; We unforunately probably ruin tail-recursion here, but at + ;; least we can verify the guards. + (<< (caar x) (caadr x))))))) + +; Lookup structure: +(defun lsp (x) + (or (sap x) + (and (consp x) + (not (lsp (cdr x))) + (sap (car x)) + (car x)))) + +(defun g (a x) + (cond + ((sap x) + (cdr (assoc-equal a x))) + ((lsp x) + (cdr (assoc-equal a (car x)))) + (t + nil))) + +; Ordinary setting, used for non-nil values: +(defun s-aux (a v r) + (cond ((endp r) + (cons (cons a v) nil)) + ((equal a (caar r)) + (cons (cons a v) (cdr r))) + ((<< a (caar r)) + (cons (cons a v) r)) + (t (cons (car r) (s-aux a v (cdr r)))))) + +(defun delete-key (key alist) + (cond + ((endp alist) + alist) + ((equal key (caar alist)) + (cdr alist)) + (t + (cons (car alist) + (delete-key key (cdr alist)))))) + +(defun s (a v x) + (cond + ((sap x) + (if (null v) + (delete-key a x) + (s-aux a v x))) + ((not (lsp x)) + (if v + ;; then make x into the cdr of the returned lookup structure + (cons (list (cons a v)) x) + ;; else x already is an appropriate result + x)) + ((null v) + (if (and (null (cdr (car x))) + (equal (caar (car x)) a)) + (cdr x) + (cons (delete-key a (car x)) + (cdr x)))) + (t + (cons (s-aux a v (car x)) + (cdr x))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Interaction properties for s and g; +;;; search for $$$ for main theorems. +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(local +(defthm delete-key-no-op + (implies (and (sap alist) + (not (assoc-equal key alist))) + (equal (delete-key key alist) alist)))) + +(local +(defthm values-not-nil + (implies (sap alist) + ;; The order below ooks dangerous, but apparently the prover's + ;; heuristics save us. + (iff (assoc-equal key alist) + (cdr (assoc-equal key alist)))))) + +(local +(defthm key-order-lemma + (implies (and (sap alist) + (<< a (caar alist))) + (not (cdr (assoc-equal a alist)))))) + +(local +(defthm s-aux-to-same + (implies (and (sap alist) + (cdr (assoc-equal a alist))) + (equal (s-aux a (cdr (assoc-equal a alist)) + alist) + alist)))) + +; $$$ A main theorem +(defthm s-same-g + (equal (s a (g a r) r) + r)) + +(local +(defthm value-s-aux + (implies (sap alist) + (equal (cdr (assoc-equal a (s-aux a v alist))) + v)))) + +(local +(defthm s-aux-preserves-sap + (implies (and (sap x) + v) + (sap (s-aux a v x))))) + +(local +(defthm cdr-assoc-equal-delete-key + (implies (sap x) + (not (cdr (assoc-equal a (delete-key a x))))))) + +; G-diff-s should go here, but I forgot it on the first pass, so I'll put +; it at the end where more lemmas are available. + +(local +(defthm sap-delete-key + (implies (sap alist) + (sap (delete-key a alist))))) + +; $$$ A main theorem +(defthm g-same-s + (equal (g a (s a v r)) + v)) + +(local +(defthm s-aux-s-aux-same + (implies (sap alist) + (equal (s-aux a v (s-aux a w alist)) + (s-aux a v alist))))) + +(local +(defthm delete-key-s-aux-same + (implies (sap alist) + (equal (delete-key a (s-aux a v alist)) + (delete-key a alist))))) + +(local +(defthm <<-s-aux + (implies (and (sap alist) + (<< b (caar alist)) + (not (<< a b)) + (not (equal a b))) + (<< b (caar (s-aux a v alist)))))) + +(local +(defthm value-nil-sufficiency + (implies (and (sap alist) + (<< a (caar alist))) + (equal (cdr (assoc-equal a alist)) + nil)))) + +(local +(defthm caar-delete-key + (implies (sap alist) + (equal (caar (delete-key a alist)) + (if (eq a (caar alist)) + (caadr alist) + (caar alist)))))) + +(local +(defthm s-aux-delete-key + (implies (sap alist) + (equal (s-aux a x (delete-key a alist)) + (s-aux a x alist))))) + +(local +(defthm <<-hack + (implies (and (<< r6 r9) + (not (<< r4 r9)) + (not (equal r6 r4))) + (<< r6 r4)) + :hints (("Goal" :in-theory (disable <<-trichotomy) + :use ((:instance <<-trichotomy + (x r6) (y r4))))))) + +; $$$ A main theorem +(defthm s-same-s + (equal (s a y (s a x r)) + (s a y r))) + +(local +(defthm s-aux-diff-s-aux + (implies (and (not (equal a b)) + (sap r) + x + y) + (equal (s-aux b y (s-aux a x r)) + (s-aux a x (s-aux b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s-aux)))))) + +(local +(defthm sap-s-aux + (implies (and (sap x) + v) + (sap (s-aux a v x))))) + +(local +(defthm consp-delete-key + (implies (sap alist) + (equal (consp (delete-key a alist)) + (or (consp (cdr alist)) + (and (consp alist) + (not (equal a (caar alist))))))))) + +(local +(defthm delete-key-delete-key + (implies (sap r) + (equal (delete-key b (delete-key a r)) + (delete-key a (delete-key b r)))) + :rule-classes ((:rewrite :loop-stopper ((b a delete-key)))))) + +(local +(defthm delete-key-s-aux + (implies (and (not (equal a b)) + (sap r) + x) + (equal (delete-key b (s-aux a x r)) + (s-aux a x (delete-key b r)))))) + +(local +(defthm delete-key-nil + (implies (not (delete-key a x)) + (not (delete-key a (delete-key b x)))))) + +; $$$ A main theorem +(defthm s-diff-s + (implies (not (equal a b)) + (equal (s b y (s a x r)) + (s a x (s b y r)))) + :rule-classes ((:rewrite :loop-stopper ((b a s))))) + +(local +(defthm assoc-equal-s-aux-different + (implies (not (equal a b)) + (equal (assoc-equal a (s-aux b v alist)) + (assoc-equal a alist))))) + +(local +(defthm assoc-equal-delete-key-different + (implies (not (equal a b)) + (equal (assoc-equal a (delete-key b alist)) + (assoc-equal a alist))))) + +; $$$ A main theorem +(defthm g-diff-s + (implies (not (equal a b)) + (equal (g a (s b v r)) + (g a r)))) + + +;;;; some simple macros for defining sets and gets.. + +(in-theory (disable s g)) + +(defmacro <- (x a) `(g ,a ,x)) + +(defmacro -> (x a v) `(s ,a ,v ,x)) + +(defun update-macro (upds result) + (declare (xargs :guard (keyword-value-listp upds))) + (if (endp upds) result + (update-macro (cddr upds) + (list 's (car upds) (cadr upds) result)))) + +(defmacro update (old &rest updates) + (declare (xargs :guard (keyword-value-listp updates))) + (update-macro updates old)) diff --git a/books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp b/books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp new file mode 100644 index 0000000..71ec212 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/records/total-order.lisp @@ -0,0 +1,28 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify it under +; the terms of Version 2 of the GNU General Public License as published by the +; Free Software Foundation. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") +(include-book "../../../../../misc/total-order") diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp new file mode 100644 index 0000000..72154de --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/sorting/certify.lsp @@ -0,0 +1,10 @@ +(certify-book "perm") +:u +(certify-book "total-order") +:u +(certify-book "perm-order") +:u +(certify-book "insertion-sort") +:u +(certify-book "quicksort") +:u diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp new file mode 100644 index 0000000..1ba5653 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/sorting/insertion-sort.lisp @@ -0,0 +1,104 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") + +(include-book "perm-order") + +(defun insert (a x) + (if (consp x) + (if (<<= a (car x)) + (cons a x) + (cons (car x) (insert a (cdr x)))) + (list a))) + +(defun isort (x) + (if (consp x) + (insert (car x) (isort (cdr x))) + nil)) + +(defthm ordered-insert + (implies (orderedp y) + (orderedp (insert x y)))) + +(defthm ordered-sort + (orderedp (isort x))) + +(defthm perm-insert + (perm (insert x y) (cons x y))) + +(defthm perm-sort + (perm (isort x) x)) + +(defthm insert-insert + (equal (insert x (insert y z)) + (insert y (insert x z))) + :rule-classes ((:rewrite :loop-stopper ((x y))))) + +(defthm insert-in + (equal (isort (insert x y)) + (isort (cons x y)))) + +(defthm insert-sort-remove + (implies (in x y) + (equal (insert x (isort (remove-el x y))) + (isort y)))) + +(defthm sort-canonical + (implies (and (perm x y) + ;; Added for mod to ACL2 v2-8 that does better matching for calls of + ;; equivalence relations against the current context, to avoid a rewriter + ;; loop in the proof of mail: + (syntaxp (not (term-order x y)))) + (equal (isort x) + (isort y)))) + +(defthm main + (equal (perm x y) + (equal (isort x) + (isort y))) + :hints (("goal" + :use ((:instance perm-sort (x y)) + (:instance perm-sort)) + :in-theory (disable perm-sort))) + :rule-classes nil) + +(defthm main2 + (implies (and (orderedp x) + (perm x y)) + (equal (isort y) + x)) + :rule-classes nil) + +(defthm main3 + (implies (and (orderedp x) + (orderedp y) + (perm x y)) + (equal x y)) + :hints (("goal" + :use ((:instance main2) (:instance main2 (x y))))) + :rule-classes nil) diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp new file mode 100644 index 0000000..3b586fc --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/sorting/perm-order.lisp @@ -0,0 +1,39 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") +(include-book "perm") +(include-book "total-order") + +(defun <<= (x y) + (lexorder x y)) + +(defun orderedp (x) + (cond ((atom x) (null x)) + (t (or (null (cdr x)) + (and (<<= (car x) (cadr x)) + (orderedp (cdr x))))))) diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp new file mode 100644 index 0000000..718b72f --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/sorting/perm.lisp @@ -0,0 +1,107 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") + +(defun in (a X) + (declare (xargs :guard t)) + (cond ((atom X) nil) + ((equal a (car X)) t) + (t (in a (cdr X))))) + +(defun remove-el (a x) + (declare (xargs :guard t)) + (cond ((atom x) nil) + ((equal a (car x)) (cdr x)) + (t (cons (car x) (remove-el a (cdr x)))))) + +(defun perm (x y) + (declare (xargs :guard t)) + (cond ((atom x) (atom y)) + (t (and (in (car x) y) + (perm (cdr x) (remove-el (car x) y)))))) + +(defthm perm-reflexive + (perm a a)) + +(defthm remove-el-swap + (equal (remove-el a (remove-el b x)) + (remove-el b (remove-el a x)))) + +(defthm remove-el-in + (implies (not (equal a b)) + (equal (in a (remove-el b y)) + (in a y)))) + +(local + (defthm perm-remove + (implies (perm x y) + (perm (remove-el a x) (remove-el a y))))) + +(defthm car-perm + (implies (and (consp x) + (not (in (car x) y))) + (not (perm y x)))) + +(defthm perm-symmetric + (implies (perm x y) + (perm y x)) + :hints (("Goal" + :induct (perm y x)) + ("Subgoal *1/2''" + :use ((:instance perm-remove (a (car y))))))) + +(defthm perm-in + (implies (and (perm x y) + (in a x)) + (in a y)) + :rule-classes ((:forward-chaining :trigger-terms ((in a x) (in a y))))) + +(defthm perm-transitive + (implies (and (perm x y) (perm y z)) + (perm x z))) + +(defequiv perm) + +(defthm perm-remove-el-app + (implies (in x y) + (equal (remove-el x (append y z)) + (append (remove-el x y) z)))) + +(defcong perm perm (append x y) 1) + +(defcong perm perm (append x y) 2) + +(defcong perm perm (cons x y) 2) + +(defcong perm perm (remove-el x y) 2) + +(defthm perm-app-cons + (perm (append x (cons y z)) + (cons y (append x z)))) + +(defcong perm equal (in x y) 2) diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp new file mode 100644 index 0000000..970593e --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/sorting/quicksort.lisp @@ -0,0 +1,107 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") + +(include-book "insertion-sort") + +(defun less (x lst) + (cond ((atom lst) nil) + ((<< (car lst) x) + (cons (car lst) (less x (cdr lst)))) + (t (less x (cdr lst))))) + +(defun notless (x lst) + (cond ((atom lst) nil) + ((not (<< (car lst) x)) + (cons (car lst) (notless x (cdr lst)))) + (t (notless x (cdr lst))))) + +(defun qsort (x) + (cond ((atom x) nil) + (t (append (qsort (less (car x) (cdr x))) + (list (car x)) + (qsort (notless (car x) (cdr x))))))) + +(defun lessp (x lst) + (cond ((atom lst) t) + (t (and (<< (car lst) x) + (lessp x (cdr lst)))))) + +(defun notlessp (x lst) + (cond ((atom lst) t) + (t (and (not (<< (car lst) x)) + (notlessp x (cdr lst)))))) + +(defthm perm-less-notless + (perm (append (less x y) (notless x y)) + y)) + +(defthm perm-qsort + (perm (qsort x) x)) + +(defthm lessp-less + (lessp x (less x lst))) + +(defthm notlessp-notless + (notlessp x (notless x lst))) + +(defcong perm equal (lessp x lst) 2) + +(defcong perm equal (notlessp x lst) 2) + +(defthm lessp-less-qsort + (lessp x (qsort (less x lst)))) + +(defthm notlessp-notless-qsort + (notlessp x (qsort (notless x lst)))) + +(defthm orderedp-lemma + (implies (and (orderedp x) + (orderedp y) + (lessp z x) + (notlessp z y)) + (orderedp (append x (cons z y)))) + :hints (("goal" :in-theory (enable <<)))) + +(defthm qsort-is-ordered + (orderedp (qsort x))) + +(defthm qsort-main + (equal (qsort x) + (isort x)) + :hints (("goal" :use (:instance main2 (x (qsort x)) (y x))))) + +#| +Or we can prove it as follows: + +(defthm qsort-main + (equal (qsort x) + (isort x)) + :hints (("goal" :use (:instance main3 (x (qsort x)) (y (isort x)))))) + +|#
\ No newline at end of file diff --git a/books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp b/books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp new file mode 100644 index 0000000..c5984f1 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/sorting/total-order.lisp @@ -0,0 +1,29 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +(in-package "ACL2") +(include-book "../../../../../misc/total-order") diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/README b/books/workshops/2002/manolios-kaufmann/support/total-order/README new file mode 100644 index 0000000..2901539 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/total-order/README @@ -0,0 +1,11 @@ +The books in this directory should be certified with ACL2 v2.5. They +are: + +1. total-order: this is the book described in section 2.1 of the + paper. + +2. total-order-easy-direction: this is the book refered to at the end + of section 2.1. + +3. soundness: this is the book refered to in section 2.2. + diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude b/books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude new file mode 100644 index 0000000..ee02a5e --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/total-order/cert_pl_exclude @@ -0,0 +1,10 @@ +cert_pl_exclude + +The presence of this file tells cert.pl not to try to build any of the books in +this directory. + +Quoting from workshops/2002/manolios-kaufmann/support/Makefile: + +# Note: total-order is deliberately not included in DIRS because its +# certification fails for ACL2 versions after 2.5. + diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp b/books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp new file mode 100644 index 0000000..7c7541c --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/total-order/certify.lsp @@ -0,0 +1,6 @@ +(certify-book "total-order") +:u +(certify-book "total-order-easy-direction") +:u +(certify-book "soundness") +:u diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp b/books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp new file mode 100644 index 0000000..f6646ab --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/total-order/soundness.lisp @@ -0,0 +1,205 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +; Certify with ACL2 version 2.5 + +(in-package "ACL2") + +(defun good-atom (x) + (and (atom x) + (or (acl2-numberp x) + (symbolp x) + (characterp x) + (stringp x)))) + +(defthm good-atom-compound-recognizer + (iff (good-atom x) + (and (atom x) + (or (acl2-numberp x) + (symbolp x) + (characterp x) + (stringp x)))) + :rule-classes :compound-recognizer) + +(in-theory (disable good-atom)) + +(defun good-atom-order (x y) + (cond ((rationalp x) + (if (rationalp y) + (<= x y) + t)) + ((rationalp y) nil) + ((complex-rationalp x) + (if (complex-rationalp y) + (or (< (realpart x) (realpart y)) + (and (= (realpart x) (realpart y)) + (<= (imagpart x) (imagpart y)))) + t)) + ((complex-rationalp y) + nil) + ((characterp x) + (if (characterp y) + (<= (char-code x) + (char-code y)) + t)) + ((characterp y) nil) + ((stringp x) + (if (stringp y) + (and (string<= x y) t) + t)) + ((stringp y) nil) + ((symbolp x) + (if (symbolp y) + (not (symbol-< y x)) + t)) + ((symbolp y) nil) + (t t))) + +(defmacro boolp (x) + `(or (equal ,x t) + (equal ,x nil))) + +(defthm boolp-good-atom-order + (boolp (good-atom-order x y)) + :rule-classes :type-prescription) + +(defthm good-atom-order-reflexive + (implies (atom x) + (good-atom-order x x))) + +(defthm equal-coerce + (implies (and (stringp x) + (stringp y)) + (equal (equal (coerce x 'list) + (coerce y 'list)) + (equal x y))) + :hints (("Goal" :use + ((:instance coerce-inverse-2 (x x)) + (:instance coerce-inverse-2 (x y))) + :in-theory (disable coerce-inverse-2)))) + +(defthm string<=-l-transitive-at-0 + (implies (and (not (string<-l y x 0)) + (not (string<-l z y 0)) + (character-listp x) + (character-listp y) + (character-listp z)) + (not (string<-l z x 0))) + :hints + (("Goal" :use (:instance string<-l-transitive + (i 0) (j 0) (k 0))))) + +(defthm good-atom-order-transitive + (implies (and (good-atom-order x y) + (good-atom-order y z) + (atom x) + (atom y) + (atom z)) + (good-atom-order x z)) + :hints (("Goal" + :in-theory (enable string< symbol-<)))) + +(defthm good-atom-order-anti-symmetric + (implies (and (good-atom x) + (good-atom-order x y) + (good-atom-order y x)) + (equal x y)) + :hints (("Goal" + :in-theory (union-theories + '(string< symbol-<) + (disable code-char-char-code-is-identity)) + :use ((:instance symbol-equality (s1 x) (s2 y)) + (:instance code-char-char-code-is-identity (c y)) + (:instance code-char-char-code-is-identity (c x))))) + :rule-classes + ((:forward-chaining :corollary + (implies (and (good-atom-order x y) + (good-atom x) + (not (consp x)) + (not (consp y))) + (iff (good-atom-order y x) + (equal x y))) + :hints (("Goal" :in-theory + (disable good-atom-order)))))) + +(defthm good-atom-order-total + (implies (and (atom x) + (atom y)) + (or (good-atom-order x y) + (good-atom-order y x))) + :hints (("Goal" + :in-theory (enable string< symbol-<))) + :rule-classes + ((:forward-chaining :corollary + (implies (and (not (good-atom-order x y)) + (not (consp x)) + (not (consp y))) + (good-atom-order y x))))) + +(in-theory (disable good-atom-order)) + +(defun good-object (x) + (if (consp x) + (and (good-object (car x)) + (good-object (cdr x))) + (good-atom x))) + +(defun good-object-order (x y) + (cond ((atom x) + (cond ((atom y) + (good-atom-order x y)) + (t t))) + ((atom y) nil) + ((equal (car x) (car y)) + (good-object-order (cdr x) (cdr y))) + (t (good-object-order (car x) (car y))))) + +(defthm boolp-good-object-order + (boolp (good-object-order x y)) + :rule-classes :type-prescription) + +(defthm good-object-order-reflexive + (good-object-order x x)) + +(defthm good-object-order-anti-symmetric + (implies (and (good-object-order x y) + (good-object-order y x) + (good-object x) + (good-object y)) + (equal x y)) + :rule-classes :forward-chaining) + +(defthm good-object-order-transitive + (implies (and (good-object x) + (good-object-order x y) + (good-object-order y z)) + (good-object-order x z))) + +(defthm good-object-order-total + (or (good-object-order x y) + (good-object-order y x)) + :rule-classes nil) diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp new file mode 100644 index 0000000..d46c9a1 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order-easy-direction.lisp @@ -0,0 +1,98 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +; Certify with ACL2 version 2.5 + +(in-package "ACL2") + +(defmacro boolp (x) + `(or (equal ,x t) + (equal ,x nil))) + +(defstub total-order (x y) t) + +(defun bad-atom (x) + (not (or (consp x) + (acl2-numberp x) + (symbolp x) + (characterp x) + (stringp x)))) + +(defaxiom boolp-total-order + (boolp (total-order x y)) + :rule-classes :type-prescription) + +(defaxiom total-order-anti-symmetric + (implies (and (total-order x y) + (total-order y x)) + (equal x y)) + :rule-classes :forward-chaining) + +(defaxiom total-order-transitive + (implies (and (total-order x y) + (total-order y z)) + (total-order x z))) + +(defaxiom total-order-total + (or (total-order x y) + (total-order y x)) + :rule-classes nil) + +(encapsulate + ((bad-atom<= (x y) t)) + (local (defun bad-atom<= (x y) + (total-order x y))) + + (defthm boolp-bad-atom<= + (boolp (bad-atom<= x y)) + :rule-classes :type-prescription) + + (defthm bad-atom<=-anti-symmetric + (implies (and (bad-atom x) + (bad-atom y) + (bad-atom<= x y) + (bad-atom<= y x)) + (equal x y)) + :hints (("goal" :use total-order-anti-symmetric)) + :rule-classes nil) + + (defthm bad-atom<=-transitive + (implies (and (bad-atom x) + (bad-atom y) + (bad-atom z) + (bad-atom<= x y) + (bad-atom<= y z)) + (bad-atom<= x z))) + + (defthm bad-atom<=-total + (implies (and (bad-atom x) + (bad-atom y)) + (or (bad-atom<= x y) + (bad-atom<= y x))) + :hints (("goal" :use total-order-total)) + :rule-classes nil)) + diff --git a/books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp new file mode 100644 index 0000000..a6a5d23 --- /dev/null +++ b/books/workshops/2002/manolios-kaufmann/support/total-order/total-order.lisp @@ -0,0 +1,239 @@ +; Copyright (C) 2001 Georgia Institute of Technology + +; This program is free software; you can redistribute it and/or modify +; it under the terms of the GNU General Public License as published by +; the Free Software Foundation; either version 2 of the License, or +; (at your option) any later version. + +; This program is distributed in the hope that it will be useful, +; but WITHOUT ANY WARRANTY; without even the implied warranty of +; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +; GNU General Public License for more details. + +; You should have received a copy of the GNU General Public License +; along with this program; if not, write to the Free Software +; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. + +; Written by: Panagiotis Manolios who can be reached as follows. + +; Email: manolios@cc.gatech.edu + +; Postal Mail: +; College of Computing +; CERCS Lab +; Georgia Institute of Technology +; 801 Atlantic Drive +; Atlanta, Georgia 30332-0280 U.S.A. + +; Certify with ACL2 version 2.5 + +(in-package "ACL2") + +(defun bad-atom (x) + (not (or (consp x) + (acl2-numberp x) + (symbolp x) + (characterp x) + (stringp x)))) + +(defstub bad-atom<= (* *) => *) + +(defmacro boolp (x) + `(or (equal ,x t) + (equal ,x nil))) + +(defaxiom boolp-bad-atom<= + (boolp (bad-atom<= x y)) + :rule-classes :type-prescription) + +(defaxiom bad-atom<=-anti-symmetric + (implies (and (bad-atom x) + (bad-atom y) + (bad-atom<= x y) + (bad-atom<= y x)) + (equal x y)) + :rule-classes nil) + +(defaxiom bad-atom<=-transitive + (implies (and (bad-atom<= x y) + (bad-atom<= y z) + (bad-atom x) + (bad-atom y) + (bad-atom z)) + (bad-atom<= x z))) + +(defaxiom bad-atom<=-total + (implies (and (bad-atom x) + (bad-atom y)) + (or (bad-atom<= x y) + (bad-atom<= y x))) + :rule-classes nil) + +(defun atom-order (x y) + (cond ((rationalp x) + (if (rationalp y) + (<= x y) + t)) + ((rationalp y) nil) + ((complex-rationalp x) + (if (complex-rationalp y) + (or (< (realpart x) (realpart y)) + (and (= (realpart x) (realpart y)) + (<= (imagpart x) (imagpart y)))) + t)) + ((complex-rationalp y) + nil) + ((characterp x) + (if (characterp y) + (<= (char-code x) + (char-code y)) + t)) + ((characterp y) nil) + ((stringp x) + (if (stringp y) + (and (string<= x y) t) + t)) + ((stringp y) nil) + ((symbolp x) + (if (symbolp y) + (not (symbol-< y x)) + t)) + ((symbolp y) nil) + (t (bad-atom<= x y)))) + +(local + (defthm bad-atom<=-reflexive + (implies (bad-atom x) + (bad-atom<= x x)) + :hints (("Goal" + :by (:instance bad-atom<=-total (y x)))))) + +(local + (defthm bad-atom<=-total-rewrite + (implies (and (not (bad-atom<= y x)) + (bad-atom x) + (bad-atom y)) + (bad-atom<= x y)) + :hints (("Goal" + :by (:instance bad-atom<=-total))) + :rule-classes :forward-chaining)) + +(local + (defthm equal-coerce + (implies (and (stringp x) + (stringp y)) + (equal (equal (coerce x 'list) + (coerce y 'list)) + (equal x y))) + :hints (("Goal" :use + ((:instance coerce-inverse-2 (x x)) + (:instance coerce-inverse-2 (x y))) + :in-theory (disable coerce-inverse-2))))) + +(local + (defthm boolp-atom-order + (boolp (atom-order x y)) + :rule-classes :type-prescription)) + +(local + (defthm atom-order-reflexive + (implies (atom x) + (atom-order x x)))) + +(local + (defthm string<=-l-transitive-at-0 + (implies (and (not (string<-l y x 0)) + (not (string<-l z y 0)) + (character-listp x) + (character-listp y) + (character-listp z)) + (not (string<-l z x 0))) + :hints + (("Goal" :use (:instance string<-l-transitive + (i 0) (j 0) (k 0)))))) + +(local + (defthm atom-order-transitive + (implies (and (atom-order x y) + (atom-order y z) + (atom x) + (atom y) + (atom z)) + (atom-order x z)) + :hints (("Goal" + :in-theory (enable string< symbol-<))))) + +(local + (defthm atom-order-anti-symmetric + (implies (and (atom x) + (atom y) + (atom-order x y) + (atom-order y x)) + (equal x y)) + :hints (("Goal" + :in-theory (union-theories + '(string< symbol-<) + (disable code-char-char-code-is-identity)) + :use ((:instance symbol-equality (s1 x) (s2 y)) + (:instance bad-atom<=-anti-symmetric) + (:instance code-char-char-code-is-identity (c y)) + (:instance code-char-char-code-is-identity (c x))))) + :rule-classes + ((:forward-chaining :corollary + (implies (and (atom-order x y) + (not (consp x)) + (not (consp y))) + (iff (atom-order y x) + (equal x y))) + :hints (("Goal" :in-theory + (disable atom-order))))))) + +(local + (defthm atom-order-total + (implies (and (atom x) + (atom y)) + (or (atom-order x y) + (atom-order y x))) + :hints (("Goal" :use (:instance bad-atom<=-total) + :in-theory (enable string< symbol-<))) + :rule-classes + ((:forward-chaining :corollary + (implies (and (not (atom-order x y)) + (not (consp x)) + (not (consp y))) + (atom-order y x)))))) + +(in-theory (disable atom-order)) + +(defun total-order (x y) + (cond ((atom x) + (cond ((atom y) + (atom-order x y)) + (t t))) + ((atom y) nil) + ((equal (car x) (car y)) + (total-order (cdr x) (cdr y))) + (t (total-order (car x) (car y))))) + +(defthm boolp-total-order + (boolp (total-order x y)) + :rule-classes :type-prescription) + +(defthm total-order-reflexive + (total-order x x)) + +(defthm total-order-anti-symmetric + (implies (and (total-order x y) + (total-order y x)) + (equal x y)) + :rule-classes :forward-chaining) + +(defthm total-order-transitive + (implies (and (total-order x y) + (total-order y z)) + (total-order x z))) + +(defthm total-order-total + (or (total-order x y) + (total-order y x)) + :rule-classes nil) |