Make some arithmetic inequality rules

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) ...))) ...)

We process the `corollary` formula of one `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 the term `<`, `<=`, `>`, or
`>=`; the negation of such a call; a call of `=` or `equal`;
or a negated call of `/=`. Note that we refer to all of these terms as
``inequalities'' below, even the equalities. If necessary, the hypothesis of
such a conjunct may be vacuous. We create a `<=`, `>`, and `>=`).

- Remove guard-holders such as
`prog2$`from the term to obtain(implies hyp concl) , wherehyp ist in the case of an unconditional rule. - If
concl is(not (not concl2)) , replaceconcl byconcl2 . - For the resulting
concl , replace`=`and`/=`by`equal`andnot equal , respectively. - Finally, the resulting
concl is processed (``linearized'') to attempt to create a corresponding polynomial or disjunction of two polynomials. This process includes the evaluation of ground subexpressions, for example replacing(* '3 '4) by'12 , and employs techniques that include type-set reasoning.

Each rule has one or more ``trigger terms'' which may be specified by the
user using the

`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

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

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

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

General Form of a Linear Rule Class: (:LINEAR :COROLLARY formula :TRIGGER-TERMS (term1 ... termk))

Each

If

The ``addends'' of

A term is maximal for a conjunct `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

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

We conclude by noting that linear rules are useless when all of the
polynomial's terms are provably non-numeric. If ACL2 determines that to be
the case for one or more of the conclusions, then it causes an error, except
when

- Force
- Identity function used to force a hypothesis
- Syntaxp
- Attach a heuristic filter on a rule
- Bind-free
- To bind free variables of a rewrite, definition, or linear rule
- Backchain-limit
- Limiting the effort expended on relieving hypotheses
- Non-linear-arithmetic
- Non-linear Arithmetic
- Linear-arithmetic
- A description of the linear arithmetic decision procedure
- Case-split
- Like force but immediately splits the top-level goal on the hypothesis
- Linear-arithmetic-with-complex-coefficients
- Some books for reasoning about arithmetic expressions with complex coefficients