; 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 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: J Strother Moore
; email: Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 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")
(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))
(e0-ord-< (acl2-count (cdr x)) (acl2-count x)))
(implies (not (ur-elementp x))
(e0-ord-< (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))
(e0-ord-< (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 acl2::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 acl2::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 acl2::x-equiv)
(y y))
(:instance canonicalize-fix
(x x))
(:instance canonicalize-fix
(x acl2::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 acl2::y-equiv))
(:instance canonicalize-fix
(x y))
(:instance canonicalize-fix
(x acl2::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 acl2::x-equiv)
(y y))
(:instance canonicalize-fix
(x x))
(:instance canonicalize-fix
(x acl2::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 acl2::y-equiv))
(:instance canonicalize-fix
(x y))
(:instance canonicalize-fix
(x acl2::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 acl2::x-equiv))
(:instance canonicalize-fix
(x x))
(:instance canonicalize-fix
(x acl2::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 acl2::x-equiv)
(y y))
(:instance canonicalize-fix
(x x))
(:instance canonicalize-fix
(x acl2::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 acl2::y-equiv))
(:instance canonicalize-fix
(x y))
(:instance canonicalize-fix
(x acl2::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 acl2::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 acl2::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 acl2::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 acl2::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 acl2::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::delete1-eq x vars))
(e (genname 'e vars1))
(a (genname x vars1))
(x-equiv (acl2::packn (list x "-EQUIV")))) ;;; ACL2 package
`(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::delete1-eq x vars))
(a1 (genname1 x 1 vars1))
(a2 (genname1 x 2 (cons a1 vars1)))
(x-equiv (acl2::packn (list x "-EQUIV"))))
`(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 "/projects/acl2/v2-5/books/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))))
(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)))
(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))))
; 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)
(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 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))
|#
(defthm nil-not-scons
(and (not (= nil (scons e sr)))
(not (= (scons e sr) nil)))
:hints (("Goal" :in-theory (enable =))))
(defthm subsetp-diff-scons
(iff (subsetp (diff a (brace e)) (scons e b))
(subsetp (diff a (brace e)) b)))
(defthm subsetp-union-backchain
(implies (and (subsetp a c)
(subsetp b c))
(subsetp (union a b) c)))
(defthm diff-brace-no-op
(iff (= (diff sr (scons e nil)) sr)
(if (ur-elementp sr)
(equal sr nil)
(not (mem e sr)))))
(defthm diff-brace-nil
(iff (= (diff sr (scons e nil)) nil)
(or (ur-elementp sr)
(= sr (scons e nil)))))
(defthm subsetp-diff-brace
(iff (subsetp (diff a (brace e)) b)
(subsetp a (scons e b))))