LINEAR

make some arithmetic inequality rules 
Major Section:  RULE-CLASSES

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.

Example:
(defthm length-member-leq-length       If inequality reasoning begins to
  (implies (and (eqlablep e)           consider how (length (member a b))
                (true-listp x))        compares to any other term, add to
           (<= (length (member e x))   the set of known inequalities the fact
               (length x)))            that it is no larger than (length b),
  :rule-classes :linear)               provided (eqlablep a) and
                                       (true-listp b) rewrite to t.

General Form:
(and ...
     (implies (and ...hi...)
              (implies (and ...hk...)
                       (and ...
                            (rel lhs rhs)
                            ...)))
     ...)

Note: One :linear rule class object might create many linear arithmetic rules from the :corollary formula. To create the rules, we first flatten the and and implies structure of the formula, transforming it into a conjunction of formulas, each of the form 

(implies (and h1 ... hn) (rel lhs rhs))
where no hypothesis is a conjunction and rel is one of the inequality relations <, <=, =, >, or >=. If necessary, the hypothesis of such a conjunct may be vacuous. We create a :linear rule for each such conjunct, if possible, and otherwise cause an error.

Each rule has one or more ``trigger terms'' which may be specified by the user using the :trigger-terms field of the rule class or which may be defaulted to values chosen by the system. We discuss the determination of trigger terms after discussing how linear rules are used.

:Linear rules are used by an arithmetic decision procedure during rewriting. See linear-arithmetic and see non-linear-arithmetic. Here we assume that the reader is familiar with the material described in linear-arithmetic.

Recall that we eliminate the unknowns of an inequality in term-order, largest unknowns first. (See term-order.) In order to facilitate this strategy, we store the inequalities in ``linear pots''. For purposes of the present discussion, let us say that an inequality is ``about'' its largest unknown. Then, all of the inequalities about a particular unknown are stored in the same linear pot, and the pot is said to be ``labeled'' with that unknown. This storage layout groups all of the inequalities which are potential candidates for cancellation with each other into one place. It is also key to the efficient operation of :linear rules.

If the arithmetic decision procedure has stabilized and not yielded a contradiction, we scan through the list of linear pots examining each label as we go. If the trigger term of some :linear rule can be instantiated to match the label, we so instantiate that rule and attempt to relieve the hypotheses with general-purpose rewriting. If we are successful, we add the rule's instantiated conclusion to our set of inequalities. This may let cancellation continue.

Note: Problems may arise if you explicitly store a linear lemma under a trigger term that, when instantiated, is not the largest unknown in the instantiated concluding inequality. Suppose for example you store the linear rule (<= (fn i j) (/ i (* j j))) under the trigger term (fn i j). Then when the system ``needs'' an inequality about (fn a b), (i.e., because (fn a b) is the label of some linear pot, and hence the largest unknown in some inequality), it will appeal to the rule and deduce (<= (fn a b) (/ a (* b b))). However, the largest unknown in this inequality is (/ a (* b b)) and hence it will be stored in a linear pot labeled with (/ a (* b b)). The original, triggering inequality which is in a pot about (fn a b) will therefore not be cancelled against the new one. It is generally best to specify as a trigger term one of the ``maximal'' terms of the polynomial, as described below.

We now describe how the trigger terms are determined. Most of the time, the trigger terms are not specified by the user and are instead selected by the system. However, the user may specify the terms by including an explicit :trigger-terms field in the rule class, e.g., 

General Form of a Linear Rule Class:
(:LINEAR :COROLLARY formula
         :TRIGGER-TERMS (term1 ... termk))
Each termi must be a term and must not be a variable, quoted constant, lambda application, let-expression or if-expression. In addition, each termi must be such that if all the variables in the term are instantiated and then the hypotheses of the corollary formula are relieved (possibly instantiating additional free variables), then all the variables in the concluding inequality are instantiated. We generate a linear rule for each conjuctive branch through the corollary and store each rule under each of the specified triggers. Thus, if the corollary formula contains several conjuncts, the variable restrictions on the termi must hold for each conjunct.

If :trigger-terms is omitted the system computes a set of trigger terms. Each conjunct of the corollary formula may be given a unique set of triggers depending on the variables that occur in the conjunct and the addends that occur in the concluding inequality. In particular, the trigger terms for a conjunct is the list of all ``maximal addends'' in the concluding inequality.

The ``addends'' of (+ x y) and (- x y) are the union of the addends of x and y. The addends of (- x) and (* n x), where n is a rational constant, is just {x}. The addends of an inequality are the union of the addends of the left- and right-hand sides. The addends of any other term, x, is {x}.

A term is maximal for a conjunct (implies hyps concl) of the corollary if (a) the term is a non-variable, non-quote, non-lambda application, non-let and non-if expression, (b) the term contains enough variables so that when they are instantiated and the hypotheses are relieved (which may bind some free variables; see free-variables) then all the variables in concl are instantiated, and (c) no other addend is always ``bigger'' than the term, in the technical sense described below.

The technical notion referenced above depends on the notion of fn-count, the number of function symbols in a term, and pseudo-fn-count, which is essentially the number of function symbols implicit in a constant (see term-order, specifically the discussion of ``pseudo-function application count'' at the end). We say term1 is always bigger than term2 if all instances of term1 have a larger fn-count (actually lexicographic order of fn-count and pseudo-fn-count) than the corresponding instances of term2. This is equivalent to saying that the fn-count of term1 is larger than that of term2 (by ``fn-count'' here we mean the lexicographic order of fn-count and pseudo-fn-count) and the variable bag for term2 is a subbag of that for term1. For example, (/ a (* b b)) is always bigger than (fn a b) because the first has two function applications and {a b} is a subbag of a b b, but (/ a (* b b)) is not always bigger than (fn a x).