## NON-LINEAR-ARITHMETIC

Non-linear Arithmetic
Major Section:  MISCELLANEOUS

This documentation topic is divided into two parts. We first discuss the practical aspect of how to use the non-linear arithmetic extension to ACL2, and then the theory behind it. We assume that the reader is familiar with the material in linear-arithmetic and that on :linear rules.

We begin our discussion of how to use non-linear arithmetic with a simple example. Assume that we wish to prove:

(thm
(implies (and (rationalp x)
(rationalp y)
(rationalp z)
(< 0 y)
(< x (* y z)))
(< (floor x y) z)))

Note that (floor x y) <= (/ x y). Note also that if we divide both sides of x < (* y z) by y, since 0 < y, we obtain (/ x y) < z. By chaining these two inequalities together, we get the inequality we desired to prove.

We now proceed with our example session:

(skip-proofs
(progn

; Since the truth of this theorem depends on the linear properties ; of floor, we will need the linear lemma:

(defthm floor-bounds-1 (implies (and (rationalp x) (rationalp y)) (and (< (+ (/ x y) -1) (floor x y)) (<= (floor x y) (/ x y)))) :rule-classes ((:linear :trigger-terms ((floor x y)))))

; We now disable floor, so that the linear lemma will be used.

(in-theory (disable floor))

; We create five rewrite rules which we will use during non-linear ; arithmetic. The necessity for these is due to one of the differences in ; ACL2's behaviour when non-linear arithmetic is turned on. Although ; the conclusions of linear lemmas have always been rewritten before ; they are used, now, when non-linear arithmetic is turned on, the ; conclusions are rewritten under a different theory than under ``normal'' ; rewriting. This theory is also used in other, similar, circumstances ; described below.

(defthm |arith (* -1 x)| (equal (* -1 x) (- x)))

(defthm |arith (* 1 x)| (equal (* 1 x) (fix x)))

(defthm |arith (* x (/ x) y)| (equal (* x (/ x) y) (if (equal (fix x) 0) 0 (fix y))))

(defthm |arith (* y x)| (equal (* y x) (* x y)))

(defthm |arith (fix x)| (implies (acl2-numberp x) (equal (fix x) x)))) ) ; End skip-proofs.

; We disable the above rewrite rules from normal use.

(in-theory (disable |arith (* -1 x)| |arith (* 1 x)| |arith (* x (/ x) y)| |arith (* y x)| |arith (fix x)|))

; We create an arithmetic-theory. Note that we must give a quoted ; constant for the theory -- none of the normal theory-functions ; are applicable to in-arithmetic-theory.

(in-arithmetic-theory '(|arith (* -1 x)| |arith (* 1 x)| |arith (* x (/ x) y)| |arith (* y x)| |arith (fix x)|))

; We turn non-linear arithmetic on.

(set-non-linearp t)

; We can now go ahead and prove our theorem.

(thm (implies (and (rationalp x) (rationalp y) (rationalp z) (< 0 y) (< x (* y z))) (< (floor x y) z)))

The above example illustrates the two practical requirements for using non-linear arithmetic in ACL2. First, one must set up an arithmetic-theory. Usually, one would not set up an arithmetic-theory on one's own but would instead load a library book or books which do so. Second, one must turn the non-linear arithmetic extension on. This one must do explicitly -- no book can do this for you.

For a brief discussion of why this is so, even though (set-non-linearp t) is an embeddable event, see acl2-defaults-table (in particular, the final paragraph). (Note that (set-non-linearp t) modifies the acl2-defaults-table.) Also see set-non-linearp, see embedded-event-form, and see events.

You can also enable non-linear arithmetic with the hint :nonlinearp t. See hints. We, in fact, recommend the use of a hint which will enable nonlinear arithmetic only when the goal has stabilized under rewriting. Using default-hints can make this easier.

(defun nonlinearp-default-hint (stable-under-simplificationp hist pspv)
(cond (stable-under-simplificationp
(if (not (access rewrite-constant
(access prove-spec-var pspv :rewrite-constant)
:nonlinearp))
'(:computed-hint-replacement t :nonlinearp t)
nil))
((access rewrite-constant
(access prove-spec-var pspv :rewrite-constant)
:nonlinearp)
(if (not (equal (caar hist) 'SETTLED-DOWN-CLAUSE))
'(:computed-hint-replacement t :nonlinearp nil)
nil))
(t nil)))

(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp hist pspv)))

This has proven to be a helpful strategy which allows faster proof times.

We now proceed to briefly describe the theory behind the non-linear extension to ACL2. In linear-arithmetic it was stated that, ``[L]inear polynomial inequalities can be combined by cross-multiplication and addition to permit the deduction of a third inequality....'' That is, if

0 < poly1,
0 < poly2,
and c and d are positive rational constants, then
0 < c*poly1 + d*poly2.

Similarly, given the above,

0 < poly1*poly2.

In the linear arithmetic case, we are taking advantage of the facts that multiplication by a positive rational constant does not change the sign of a polynomial and that the sum of two positive polynomials is itself positive. In the non-linear arithmetic case, we are using the fact that the product of two positive polynomials is itself positive.

For example, suppose we have the three assumptions:

p1:  3*x*y + 7*a < 4
p2:            3 < 2*x  or p2': 0 < -3 + 2*x
p3:            1 < y    or p3': 0 < -1 + y,
and we wish to prove that a < 0. As described elsewhere (see linear-arithmetic), we proceed by assuming the negation of our goal:
p4:            0 <= a,