#|
Fully Ordered Finite Sets, Version 0.91
Copyright (C) 2003-2006 by Jared Davis
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License as
published by the Free Software Foundation; either version 2 of
the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public Lic-
ense along with this program; if not, write to the Free Soft-
ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
02111-1307, USA.
computed-hints.lisp
We provide support for the development of "pick a point" style
proofs through computed hints.
|#
(in-package "COMPUTED-HINTS")
;;; Introduction
;;;
;;; Suppose we have some predicate, P, of any number of arguments. A
;;; natural operation is to extend this predicate to every element of
;;; a list, set, or other collection. In other words, we would like
;;; to know if every element in the set, list, tree, or whatever has
;;; the property when applied to arguments.
;;;
;;; For example, we might have the predicate:
;;;
;;; (defun integer-lessp (a b)
;;; (and (integerp a)
;;; (< a b)))
;;;
;;; We could now extend this concept to an entire list, to ask if
;;; every element in the list was an integer that is less than b. The
;;; function might be written as:
;;;
;;; (defun list-integer-lessp (a-list b)
;;; (declare (xargs :guard (true-listp a-list)))
;;; (or (endp a-list)
;;; (and (integer-lessp (car a-list) b)
;;; (list-integer-lessp (cdr a-list) b))))
;;;
;;; Similarly, we might want to map the function across sets or other
;;; types of collections.
;;;
;;; Take an abstract mathematical view for a moment. Given some
;;; predicate P, what we would really like to do is be able to express
;;; the idea that given some collection x, every element of x
;;; satisfies P. In other words, we want to define:
;;;
;;; (collection-P x [args]) = forall a in x, (P x [args])
;;;
;;; And indeed, it would be nice to be working with this very abstract
;;; mathematical definition, for which we will not need to make
;;; inductive arguments. Unfortunately, because all variables in
;;; ACL2's rewrite rules are implicitly universally quantified, we
;;; cannot express the above as a rewrite rule.
;;;
;;; However, through the use of constrained function symbols and
;;; functional instantiation, we can effectively accomplish the above
;;; reduction when it suits our purposes. And, the process can be
;;; automated through the use of computed hints. Overall, this is not
;;; as nice as working with a pure rewrite rule, and in fact has some
;;; unfortunate limitations. However, it does turn out to be very
;;; broadly applicable and invaluable for reasoning about set
;;; theoretic concepts, where concepts such as "subset" are really
;;; nothing more than the extension of the predicate "in" across a
;;; set.
;;;
;;; Moreover, the reduction that we set out to achieve will reduce
;;; (collection-P x [args]) to the following implication:
;;;
;;; (implies (in a x)
;;; (P a [args]))
;;;
;;; I call this a "pick a point" reduction, because it is similar to
;;; and takes its inspiration from the well known set theoretic
;;; technique of picking an arbitrary element (or point) in one set,
;;; then showing it is also a member of another set.
;;; Preliminaries
;;;
;;; We will make minor use of the rewriting system developed in
;;; instance.lisp. We also enter program mode, because we are not
;;; interested in reasoning about these functions.
(include-book "instance")
(program)
;;; Tagging
;;;
;;; Suppose that we have (collection-P x a0 a1 ... an) to a simpler
;;; argument. We begin by defining a synonym for collection-P, e.g.,
;;;
;;; (defun collection-P-tag (x a0 a1 ... an)
;;; (collection-P x a0 a1 ... an))
;;;
;;; Now we instruct the theorem prover to rewrite instances of
;;; conclusion into conclusion-tag, as long as we are not backchaining
;;; and as long as conclusion occurs as the goal. For example,
;;;
;;; (defthm tagging-theorem
;;; (implies
;;; (and (syntaxp (rewriting-goal-lit mfc state))
;;; (syntaxp (rewriting-conc-lit `(collection-P ,x ,a0 ... ,an)
;;; mfc state)))
;;; (equal (collection-P x a0 ... an)
;;; (collection-P-tag x a0 ... an))))
;;;
;;; This theorem is trivial to prove, since collection-P-tag is merely
;;; a synonym for collection-P. After the theorem is proven,
;;; collection-P-tag should be disabled.
(defun rewriting-goal-lit (mfc state)
(declare (xargs :stobjs state)
(ignore state))
(null (mfc-ancestors mfc)))
(defun rewriting-conc-lit (term mfc state)
(declare (xargs :stobjs state)
(ignore state))
(let ((clause (mfc-clause mfc)))
(member-equal term (last clause))))
;;; Computing a Hint
;;;
;;; Now, what we are going to do next is create a computed hint that
;;; will look for instances of a trigger, and if it sees one, we will
;;; try to provide a functional instantiation hint. This takes some
;;; work. Our computed hint function is called as ACL2 is working to
;;; simplify terms, and it is allowed to examine the current clause.
;;; The current clause will be a a disjunction of literals. For
;;; example,
;;;
;;; (a ^ b ^ ...) => P is (~a v ~b v ... v P)
;;; (a v b v ...) => P is subgoal1: (~a v P), sg2: (~b v P), ...
;;;
;;; Our first step is to see if our computed hint should even be
;;; applied to this clause. We only allow the hint to be applied if
;;; the current clause is stable under simplification, i.e., if other
;;; attempts to prove it have failed. At that point, we check the
;;; clause to see if our trigger occurs as a term within it. If so,
;;; the tagging theorem has applied and thinks we should try to use
;;; our computed hint!
;;;
;;; We check for the existence of our trigger using the following
;;; function, (harvest-trigger clause trigger-fn), which extracts all
;;; the terms from clause whose function symbol is trigger-fn, and
;;; returns them as a list.
;;;
;;; Now, our intention is to functionally instantiate the theorem in
;;; question. To do this, we need to provide values for the
;;; hypotheses and arguments a0 ... an.
;;;
;;; In order to recover the hypotheses, we first remove from the
;;; clause all of our trigger terms. We then negate each of the
;;; remaining literals as they occur in the clause. And, if there are
;;; more than one of them, we are going to AND their negations
;;; together. This is done by the functions others-to-negated-list,
;;; and others-to-hyps.
;;;
;;; For example, if we originally had the conjecture (a ^ b ^ ...) =>
;;; P Then this became the clause: (~a v ~b v ... v P), which is
;;; represented by the list ((not a) (not b) ... P). Suppose that P
;;; was our trigger term. We remove P from the clause, yielding ((not
;;; a) (not b) ...), and then we negate all of these literals,
;;; creating the list (a b ...). We now and these together, creating
;;; the the term (and a b ...), which was our original hypotheses!
(defun harvest-trigger (clause trigger-fn)
(if (endp clause)
nil
(if (eq (caar clause) trigger-fn)
(cons (car clause) (harvest-trigger (cdr clause) trigger-fn))
(harvest-trigger (cdr clause) trigger-fn))))
(defun others-to-negated-list (others)
(if (endp others)
nil
(if (equal (caar others) 'not) ; don't create ugly double not's
(cons (second (car others))
(others-to-negated-list (cdr others)))
(cons (list 'not (car others))
(others-to-negated-list (cdr others))))))
(defun others-to-hyps (others)
(if (endp others)
t
(let ((negated (others-to-negated-list others)))
(if (endp (cdr negated)) ; don't wrap single literals in and's
(car negated)
(cons 'and (others-to-negated-list others))))))
;;; Absolute Restrictions:
;;;
;;; Collection predicate must have a first argument which is the
;;; collection to traverse!!
;;;
;;; Need to be able to create hint for predicate as well.
;;; Building Hints
;;;
;;; Our ultimate goal now is to be able to create functional
;;; instantiation hints for each trigger which was found. In other
;;; words, we now have a set of triggers which look like the following:
;;;
;;; ((collection-P-tag col1 [extra-args1])
;;; (collection-P-tag col2 [extra-args2])
;;; ...)
;;;
;;; We want to instantiate generic theorems of the form:
;;;
;;; (defthm generic-theorem
;;; (implies (hyps)
;;; (collection-P-tag (collection) [extra-args])))
;;;
;;; Where we have the following generic constraint:
;;;
;;; (implies (hyps)
;;; (implies (in a (collection))
;;; (predicate a)))
;;;
;;; So, the functional instantiation hints we want to create will look
;;; like the following:
;;;
;;; (:functional-instance generic-theorem
;;; (hyps (lambda () [substitution for hyps]))
;;; (collection (lambda () [substitution for collection]))
;;; (predicate (lambda (x) [substitution for predicate]))
;;; (collection-P (lambda (x) [substitution for collection-P])))
;;;
;;; Lets consider how we can build these substitutions for some
;;; trigger = (collection-P-tag col1 [extra-args1]). Some of this
;;; is easy:
;;;
;;; The substitution for hyps is actually built using the process
;;; described above, e.g., they are extracted from the clause and
;;; eventually restored to normal using others-to-hyps, so I will
;;; not spend any time on them.
;;;
;;; The collection is simply (second trigger), since we require that
;;; the collection predicate has the collection as its first
;;; argument.
;;;
;;; The substitution for collection-P is also fairly easy. Since
;;; we require that the collection function's first argument is
;;; the collection under examination, we simply need to write
;;; (lambda (?x) (actual-collection-P ?x [extra-args])), where the
;;; extra arguments are taken from the trigger we are looking at.
;;;
;;; This leaves us with predicate. The substitution for predicate
;;; is difficult, because we want to support very flexible
;;; predicates involving many arguments and various weird terms.
;;; To do this, we will allow the user to provide a rewrite rule
;;; that says how to handle the predicate.
;;;
;;; In other words, given the trigger (trigger-term col a0 a1 a2
;;; ... an) we will create the following "base predicate" to
;;; rewrite:
;;;
;;; (predicate ?x a0 a1 a2 ... an)
;;;
;;; Where "predicate" is literally the name of the generic
;;; predicate. The user can then provide a substitution such
;;; as:
;;;
;;; (predicate ?x ?y) -> (not (integer-lessp ?x ?y))
;;;
;;; And this will transform the above into the desired result.
(defun build-hint (trigger ; list, the actual trigger to use
generic-theorem ; symbol, the name of generic-theorem
generic-hyps ; symbol, the name of (hyps)
generic-collection ; symbol, the name of (collection)
generic-predicate ; symbol, the name of predicate
generic-collection-P ; symbol, the name of collection-P
collection-P-sub ; symbol, name of actual collection-P
hyps-sub ; the computed substitution for hyps
predicate-rewrite) ; rewrite rule for predicate
(let* ((base-pred (cons generic-predicate (cons '?x (cddr trigger))))
(pred-sub (instance-rewrite base-pred predicate-rewrite)))
`(:functional-instance
,generic-theorem
(,generic-hyps
(lambda () ,hyps-sub))
(,generic-collection
(lambda () ,(second trigger)))
(,generic-collection-P
(lambda (?x) ,(cons collection-P-sub (cons '?x (cddr trigger)))))
(,generic-predicate
(lambda (?x) ,pred-sub)))))
(defun build-hints (triggers
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
hyps-sub
predicate-rewrite)
(if (endp triggers)
nil
(cons (build-hint (car triggers)
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
hyps-sub
predicate-rewrite)
(build-hints (cdr triggers)
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
hyps-sub
predicate-rewrite))))
(defconst *message*
"~|~%We suspect this conjecture sould be proven by functional ~
instantiation of ~x0. This suspicion is caused by ~x2, so ~
if this is not what you want to do, then you should disable ~
~x2. Accordingly, we suggest the following hint: ~
~%~%~x1~%")
;;; Of course, some of those hints can be computed. Here we write a function
;;; to actually provide these hints and install the computed hint function.
(defun automate-instantiation-fn (new-hint-name
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-P
collection-P-sub
predicate-rewrite
trigger-symbol
tagging-theorem)
`(encapsulate ()
(defun ,new-hint-name (id clause world stable)
(declare (xargs :mode :program)
(ignore world))
(if (not stable)
nil
(let ((triggers (harvest-trigger clause ,trigger-symbol)))
(if (not triggers)
nil
(let* ((others (set-difference-equal clause triggers))
(hyps (others-to-hyps others))
(phrase (string-for-tilde-@-clause-id-phrase id))
(fi-hints (build-hints triggers
,generic-theorem
,generic-hyps
,generic-collection
,generic-predicate
,generic-collection-P
,collection-P-sub
hyps
,predicate-rewrite))
(hints (list :use fi-hints
:expand triggers)))
(prog2$ (cw *message*
,generic-theorem
(list phrase hints)
,tagging-theorem)
hints))))))
(add-default-hints!
'((,new-hint-name id clause world stable-under-simplificationp)))
))
(defmacro automate-instantiation (&key new-hint-name
generic-theorem
generic-hyps
generic-collection
generic-predicate
generic-collection-predicate
actual-collection-predicate
predicate-rewrite
actual-trigger
tagging-theorem)
(automate-instantiation-fn new-hint-name
(list 'quote generic-theorem)
(list 'quote generic-hyps)
(list 'quote generic-collection)
(list 'quote generic-predicate)
(list 'quote generic-collection-predicate)
(list 'quote actual-collection-predicate)
(list 'quote predicate-rewrite)
(list 'quote actual-trigger)
(list 'quote tagging-theorem)))