COMPOUND-RECOGNIZER

make a rule used by the typing mechanism 
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :compound-recognizer rule might be built is: 

Example: 
(implies (alistp x)         When (alistp x) is assumed true,
         (true-listp x))    add the additional hypothesis that x
                            is of primitive type true-listp.

Before presenting the General Forms, we start with a motivating example. The following provides a nice example of a :compound-recognizer rule that is built into ACL2. 

(defthm natp-compound-recognizer
  (equal (natp x)
         (and (integerp x)
              (<= 0 x)))
  :rule-classes :compound-recognizer)
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 weaken it a little to ``and concl is a non-tautological conjunction or 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)
  negative integers   (and (integerp x) (< x 0))
  positive integers   (and (integerp x) (> x 0))
  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, a suitable concl to recognize the naturals would be (or (equal x 0) (and (integerp x) (> x 0))) but it turns out that we also permit (and (integerp x) (>= x 0)). 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). When time permits we will 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.