Substitute upper bounds and lower bounds for subterms in comparisons.
Replace expressions by upper and lower bounds for them inside inequalities. Usage, as a computed hint:
(rewrite-bounds ((<= a 10) ;; replace the variable a by 10 in upper-boundable contexts (:free (b) (> (foo b c) (bar b))) ;; replace (foo b c), for any b, by (bar b) in ;; lower-boundable contexts (note: C is not a free variable) ...) ;; optional keywords: ;; theory to use in addition to the bound-rewrite meta rule ;; -- default is (enable), i.e., the ambient theory for the ;; event :in-theory (enable foo bar) ;; wait until stable under simplification (default t) :wait-til-stablep nil ;; look for constant bounds assumed in the clause :clause-auto-bounds nil ;; look for constant bounds from linear rules :linear-auto-bounds nil ;; use both of these kinds of automatic bounds :auto-bounds nil)
Here, lower-boundable contexts are locations where decreasing the subexpression makes the goal stronger, and upper boundable contexts are locations where increasing the value of the subexpression makes the goal stronger (the new goal implies the original goal). More on this below.
Note that performing such replacements may change a theorem to a
non-theorem. Actually, this procedure leaves the original literals behind
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
The rules used for determining which contexts are upper or lower boundable are as follows.