Compound-recognizer
Make a rule used by the typing mechanism
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
Examples:
(defthm alistp-implies-true-listp-compound-recognizer
(implies (alistp x) ; When (alistp x) is assumed true, add
(true-listp x)) ; the additional hypothesis that x is
:rule-classes :compound-recognizer) ; of primitive type true-listp.
(defthm natp-compound-recognizer ; See discussion below.
(equal (natp x)
(and (integerp x)
(<= 0 x)))
:rule-classes :compound-recognizer)
Before presenting the General Forms, we start with a motivating example:
the second defthm form above, which provides a nice example of a
:compound-recognizer rule that is built into ACL2. To see how this rule
might be useful, consider the following (admittedly very simple) events.
(defun triple (x)
(* 3 x))
(defthm triple-preserves-integerp
(implies (integerp x)
(integerp (triple x))))
(in-theory (disable triple natp))
If the above :compound-recognizer rule is disabled, then the following
trivial theorem fails as shown; we explain below.
(thm (implies (natp x)
(integerp (triple x)))
:hints (("Goal" :in-theory (disable natp-compound-recognizer))))
The problem is that when ACL2 tries to rewrite the term (integerp
(triple x)) using the :rewrite rule
triple-preserves-integerp, it needs to rewrite the hypothesis
(integerp x) to t, but instead what is known is (natp x). If
we remove the hint, then the proof succeeds because the above
:compound-recognizer rule tells ACL2 that when assuming (natp x) to
be true, it should actually assume both (integerp x) and (<= 0 x) to
be true.
General Forms:
(implies (fn x) concl) ; (1)
(implies (not (fn x)) concl) ; (2)
(and (implies (fn x) concl1) ; (3)
(implies (not (fn x)) concl2))
(if (fn x) concl1 concl2) ; (4)
(iff (fn x) concl) ; (5)
(equal (fn x) concl) ; (6)
where fn is a Boolean valued function of one argument, x is a
variable symbol, and the system can deduce some restriction on the primitive
type of x from the assumption that concl holds. The last
restriction is vague but one way to understand it is to strengthen it a little
to ``and concl is a non-tautological disjunction of the primitive type
recognizers listed below.''
The primitive ACL2 types and a suitable primitive recognizing expression
for each are listed below.
type suitable primitive recognizer
zero (equal x 0)
one (equal x 1)
negative integers (and (integerp x) (< x 0))
positive integers > 1 (and (integerp x) (> x 1))
negative ratio (and (rationalp x)
(not (integerp x))
(< x 0))
positive ratio (and (rationalp x)
(not (integerp x))
(> x 0))
complex rational (complex-rationalp x)
nil (equal x nil)
t (equal x t)
other symbols (and (symbolp x)
(not (equal x nil))
(not (equal x t)))
proper conses (and (consp x)
(true-listp x))
improper conses (and (consp x)
(not (true-listp x)))
strings (stringp x)
characters (characterp x)
Thus, since the naturals comprise the types zero, one, and
positive integers > 1, a suitable concl to recognize the naturals
would be
(or (equal x 0)
(equal x 1)
(and (integerp x) (> x 1)))
However, it turns out that we also permit (and (integerp x) (>= x 0)),
i.e. concl doesn't literally need to be formed as a direct disjunction of
terms from the table above.
Similarly, the true-lists could be specified by
(or (equal x nil)
(and (consp x)
(true-listp x)))
but we in fact allow (true-listp x) as well. When time permits we
may document more fully what is allowed or implement a macro that permits
direct specification of the desired type in terms of the primitives.
There are essentially four forms of :compound-recognizer rules, as the
forms labeled (3) and (4) above are equivalent, as are those labeled (5) and
(6). We explain how such rules are used by considering the individual
forms.
Consider form (1), (implies (fn x) concl). The effect of such a rule
is that when the rewriter assumes (fn x) true, as it would while diving
through (if (fn x) xxx ...) to rewrite xxx, it restricts the type of
x as specified by concl. For example, if concl is the term
(integerp x), then when rewriting xxx, x will be assumed to be
an integer. However, when assuming (fn x) false, as necessary in (if
(fn x) ... xxx), the rule permits no additional assumptions about the type
of x. For example, if fn is primep, i.e., the predicate that
recognizes prime numbers, then (implies (primep x) (and (integerp x) (>= x
0))) is a compound recognizer rule of the first form. When (primep x)
is assumed true, the rewriter gains the additional information that x is
a natural number. When (primep x) is assumed false, no additional
information is gained — since x may be a non-prime natural or may
not even be a natural.
Form (2) is the symmetric case, when assuming (fn x) false permits
type restrictions on x but assuming (fn x) true permits no such
restrictions. For example, if we defined exprp to be the recognizer for
well-formed expressions for some language in which all symbols, numbers,
character objects and strings were well-formed — e.g., the
well-formedness rules only put restrictions on expressions represented by
consps — then the theorem (implies (not (exprp x)) (consp
x)) is a rule of the second form. Assuming (exprp x) true tells us
nothing about the type of x; assuming it false tells us x is a
consp.
Forms (3) and (4), which are really equivalent, address themselves to the
case where one type may be deduced from (fn x) and a generally unrelated
type may be deduced from its negation. If we modified the expression
recognizer above so that character objects are illegal, then rules of the
forms (3) and (4) are
(and (implies (exprp x) (not (characterp x)))
(implies (not (exprp x)) (or (consp x) (characterp x)))).
(if (exprp x)
(not (characterp x))
(or (consp x) (characterp x)))
Finally, rules of forms (5) and (6) address the case where fn
recognizes all and only the objects whose type is described. In these cases,
fn is really just a new name for some ``compound recognizers.'' The
classic example is (booleanp x), which is just a handy combination of two
primitive types:
(iff (booleanp x) (or (equal x t) (equal x nil))).
Often it is best to disable fn after proving that it is a compound
recognizer, since otherwise the term (fn x) will be expanded and thus
disappear.
Every time you prove a new compound recognizer rule about fn it
overrides all previously proved compound recognizer rules about fn.
Thus, if you want to establish the type implied by (fn x) and you want to
establish the type implied by (not (fn x)), you must prove a compound
recognizer rule of the third, fourth, fifth, or sixth forms. Proving a rule
of the first form followed by one of the second only leaves the second fact in
the database.
Compound recognizer rules can be disabled with the effect that older rules
about fn, if any, are exposed.
If you prove more than one compound recognizer rule for a function, you may
see a warning message to the effect that the new rule is not as
``restrictive'' as the old. That is, the new rules do not give the rewriter
strictly more type information than it already had. The new rule is stored
anyway, overriding the old, if enabled. You may be playing subtle games with
enabling or rewriting. But two other interpretations are more likely, we
think. One is that you have forgotten about an earlier rule and should merely
print it out to make sure it says what you intend, and then discard your new
rule. The other is that you meant to give the system more information and the
system has simply been unable to extract the intended type information from
the term you placed in the conclusion of the new rule. Given our lack of
specificity in saying how type information is extracted from rules, you can
hardly blame yourself for this problem. Sorry. If you suspect you've been
burned this way, you should rephrase the new rule in terms of the primitive
recognizing expressions above and see if the warning is still given. It would
also be helpful to let us see your example so we can consider it as we
redesign this stuff.
Compound recognizer rules are similar to :forward-chaining
rules in that the system deduces new information from the act of assuming
something true or false. If a compound recognizer rule were stored as a
forward chaining rule it would have essentially the same effect as described,
when it has any effect at all. The important point is that :forward-chaining rules, because of their more general and expensive form, are
used ``at the top level'' of the simplification process: we forward chain from
assumptions in the goal being proved. But compound recognizer rules are built
in at the bottom-most level of the simplifier, where type reasoning is done.
All that said, compound recognizer rules are a rather fancy, specialized
mechanism. It may be more appropriate to create :forward-chaining rules instead of :compound-recognizer rules.
