## LINEAR

make some arithmetic inequality rules
```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 `:linear` rule might be built is:

```Example:
(implies (and (eqlablep e)           if inequality reasoning begins to
(true-listp x))        consider how (length (member a b))
(>= (length x)              compares to any other term, add to
(length (member e x)))) set of known inequalities the fact
that it is no larger than (length b),
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 a linear arithmetic decision procedure during rewriting. We describe the procedure very roughly here. Fundamental to the procedure is the notion of a linear polynomial inequality. A ``linear polynomial'' is a sum of terms, each of which is the product of a rational constant and an ``unknown.'' The ``unknown'' is permitted to be `1` simply to allow a term in the sum to be constant. Thus, an example linear polynomial is `3*x + 7*a + 2`; here `x` and `a` are the (interesting) unknowns. In our case, the unknowns need not be variable symbols. For example, `(length x)` might be used as an unknown in a linear polynomial. Thus, another linear polynomial is `3*(length x) + 7*a`. A ``linear polynomial inequality'' is an inequality (either `<` or `<=`) relation between two linear polynomials. Certain linear polynomial inequalities can be combined by cross-multiplication and addition to permit the deduction of a third linear inequality polynomial with fewer unknowns. If this deduced inequality is manifestly false, a contradiction has been deduced from the assumed inequalities.

For example, suppose we have three assumptions:

```p1:  3*x + 7*a <  4
p2:          3 <  2*x
p3:          0 <= a.
```
By cross-multiplying and adding the first two (that is, multiplying `p1` by `2`, `p2` by `3` and adding the respective sides), we deduce the intermediate result
```p4:  6*x + 14*a + 9 < 8 + 6*x
```
which, after cancellation, is
```p4:        14*a + 1 <  0.
```
If we then cross-multiply and add `p3` to `p4`, we get
```p5:               1 <= 0,
```
a contradiction. Thus, we have proved that `p1` and `p2` imply the negation of `p3`.

All of the unknowns of a polynomial must be eliminated by cancellation in order to produce a constant inequality. We can choose to eliminate the unknowns in any order. We eliminate them in term-order, largest unknowns first. (See term-order.) Now suppose that this procedure does not produce a contradiction but instead yields a set of nontrivial inequalities. A contradiction might still be deduced if we could add to the set some additional inequalities allowing additional cancellation. That is where `:linear` lemmas come in. When the set of inequalities has stabilized under cross-multiplication and addition and no contradiction is produced, we search the data base of `:linear` rules for rules about the unknowns that are candidates for cancellation (i.e., are the largest unknowns in their respective inequalities).

If the trigger term of some `:linear` rule can be instantiated to yield a candidate for cancellation, we so instantiate that rule, attempt to relieve the hypotheses with general-purpose rewriting, and, if successful, convert the concluding inequality into a polynomial inequality and add it to the set. This may let cancellation continue. See the discussion of ``Linear Arithmetic Rules'' pp 242 of A Computational Logic Handbook for more details.

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.

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 largest unknown in some inequality in the set of assumed inequalities, 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 this inequality will not be used until that term is eliminated by cancellation with some other inequality. It is generally best to specify as a trigger term one of the ``maximal'' terms of the polynomial, as described below.

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 numeric constant, is in all cases 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 then all the variables in `concl` are instantiated, and (c) any instantiation of the term is always at least as ``large'' (see term-order for a description of the order used) as the corresponding instantiations of any other addend in `concl`.