Substitute upper bounds and lower bounds for subterms in comparisons.

Try to solve inequalities by replacing their subexpressions with upper and lower bounds. Usage, as a computed hint:

(rewrite-bounds ;; optional list of user-suggested bounds, of the forms ;; (rel bounded-term bound) or (:free (vars) (rel bounded-term bound)) ((<= a 10) ;; use 10 as the upper bound for variable A if we can prove it by backchaining (:free (b) (> (foo b c) (bar b))) ;; use (bar b) as the lower bound for (foo b c), for any b, ;; as long as (bar b) is a ground term that evaluates to a rational ;; and we can prove it by backchaining. ...) ;; optional keywords: ;; theory to use in addition to the bound-rewrite meta rule ;; -- default is (enable bound-rewrite), i.e., the ambient theory for the ;; event plus the bound-rewrite rule. Must result in bound-rewrite enabled ;; or this won't work. :in-theory-override (enable foo bar bound-rewrite) ;; wait until stable under simplification (default t) :wait-til-stablep nil ;; look for constant bounds assumed in the clause (recommended) :clause-auto-bounds nil ;; look for constant bounds from linear rules (not recommended) :linear-auto-bounds nil ;; use both of these kinds of automatic bounds (not recommended) :auto-bounds nil ;; do not let auto-bounds add bounds for these terms :auto-bounds-omit ((+ a b) (foo c)))

This form enables a meta rule that tries to rewrite literals of the goal
clause that are inequalities so as to prove the clause. Specifically, it tries
to replace the two sides of each inequality with constant upper or lower
bounds. The replacement depends on the sense of the literal. For a
non-negated literal

Note that performing such replacements (if we remove the

The bounds for each such literal are determined by an abstract interpretation of the term, which recursively finds upper and lower bounds. For a term that is an application of a supported arithmetic operator, we first find upper and lower bounds for each argument and then use those bounds to determine the bounds for that operator application. For other terms, bounds may be found by user suggestions (verified using backchaining), linear rules, and type reasoning.

ACL2 has a powerful nonlinear arithmetic decision procedure, but often it stalls on relatively simple proofs. For example, it goes out to lunch on this problem:

(defthm hard-nonlinear-problem (implies (and (rationalp a) (rationalp b) (rationalp c) (<= 0 a) (<= 0 b) (<= 1 c) (<= a 10) (<= b 20) (<= c 30)) (<= (+ (* a b c) (* a b) (* b c) (* a c)) (+ (* 10 20 30) (* 10 20) (* 20 30) (* 10 30)))) :hints ((and stable-under-simplificationp '(:nonlinearp t))))

This can be proved using a fairly simple argument: each variable only occurs in the conclusion in a context where the LHS expression increases monotonically as it increases (because the rest of the variables are nonnegative). Therefore, to find the upper bound for the LHS expression, set each variable to its upper bound. This upper bound is the same as the RHS, and the comparison is non-strict, so the conclusion holds.

The computed hint

(rewrite-bounds ((<= a 10) (<= b 20) (<= c 30)))

This instructs our metafunction to replace

A final detail: Observe that the occurrence of

- Add better control over replacements
- Add more boundable contexts
- Add more smarts to prevent bad replacements.