Make some :pick-a-point rules
I described how the pick-a-point method can be useful for proving subsets in the 2004 ACL2 Workshop Paper: Finite Set Theory based on Fully Ordered Lists. Essentially, the idea is to you should be able to prove (subset x y) by just knowing that forall a, (in a x) implies (in a y). Since writing that paper, I have found the pick a point method to be widely useful in other contexts that involve extending a predicate to some data structure.
Often we will have some simple predicate, say
Because all of the variables in our :rewrite rules must be universally
quantified. The :pick-a-point rules in Adviser are designed to make exactly
this kind of reduction. As an example, I'll now elaborate on how to set up
such a reduction for
We begin with our definition of all-integerp. (We do not use integer-listp because it requires its argument to be a true-listp.)
Our first task is to write our ``forall'' statement as a constraint theorem about encapsulated functions. Becuase we are quantifying over all ``a'', it will be a variable in this constrained theorem. However, since ``x'' is not being quantified, we will create a constrained function for it. For reasons we will explain later, we will also have one more constrianed function called ``hyps''. In all, we come up with the following encapsulate:
(encapsulate (((intlist-hyps) => *) ((intlist-list) => *)) (local (defun intlist-hyps () nil)) (local (defun intlist-list () nil)) (defthm intlist-constraint (implies (and (intlist-hyps) (member intlist-element (intlist-list))) (integerp intlist-element)) :rule-classes nil))
Our next goal is to prove that, given this constraint, it must be the case that (integer-listp (intlist-list)) is true. The proof is not entirely straightforward, but follows the same script each time. Basically, we first set up a ``badguy'' function that will go through and find an element that violates our constraint if one exists. We show that the badguy finds such an element whenever ``all-integerp'' is not satisifed. Then, we just use the instance of our constraint to show that all-integerp must be true for (intlist-list).
(local (defun badguy (x) (if (endp x) nil (if (integerp (car x)) (badguy (cdr x)) (car x))))) (local (defthm badguy-works (implies (not (all-integerp x)) (and (member (badguy x) x) (not (integerp (badguy x))))))) (defthm intlist-by-membership-driver (implies (intlist-hyps) (all-integerp (intlist-list))) :rule-classes nil :hints(("Goal" :use (:instance intlist-constraint (intlist-element (badguy (intlist-list)))))))
At this point, we have essentially shown ACL2 that ``all-integerp`` can be shown as long as we can show our constraint is true. The missing step is for ACL2 to actually try this approach for us. But we can't write a rewrite rule that says ``try to functionally instantiate this theorem whenever you are trying to prove (all-integerp x).''
That's where Adviser comes in. We just give it the following rule:
(ADVISER::defadvice intlist-by-membership (implies (intlist-hyps) (all-integerp (intlist-list))) :rule-classes (:pick-a-point :driver intlist-by-membership-driver))
Because we used defadvice, rather than defthm, this rule is for Adviser to add to its database. Adviser will set up a new trigger for all-integerp, and whenever it sees that trigger as the target that we are trying to prove, it will functionally instantiate the driver theorem. We can now conduct membership based proofs of all-integerp.
For example, in the following script we can prove that (all-integerp (rev x)) exactly when (all-integerp x) without inducting over either function, because we can just consider membership.
(defthm equal-of-booleans-rewrite (implies (and (booleanp x) (booleanp y)) (equal (equal x y) (iff x y))) :rule-classes ((:rewrite :backchain-limit-lst 0))) (defthm member-of-all-integerp-1 (implies (and (member a x) (all-integerp x)) (integerp a))) (defthm member-of-all-integerp-2 (implies (and (all-integerp x) (not (integerp a))) (not (member a x)))) (in-theory (disable all-integerp)) (defund rev (x) (if (endp x) x (append (rev (cdr x)) (list (car x))))) (defthm member-of-rev (iff (member a (rev x)) (member a x)) :hints(("Goal" :in-theory (enable rev)))) (encapsulate () (local (defthm lemma1 (implies (all-integerp x) (all-integerp (rev x))))) (local (defthm lemma2 (implies (all-integerp (rev x)) (all-integerp x)) :hints(("Subgoal 1" :use (:instance member-of-all-integerp-1 (a intlist-element) (x (rev x))))))) (defthm all-integerp-of-rev (equal (all-integerp (rev x)) (all-integerp x))) )