		Search-engine friendly clone of the ACL2 documentation.

Proof-automation

Rewrite-bounds

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 inside hide forms, but it still is best to be careful to apply this strategy in the right places.

Details

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 can run this sort of proof: it replaces subterms within comparisons with user-provided upper or lower bounds, depending on the context in which they occur. In this theorem all of the occurrences of the variables in the conclusion are upper-boundable instances, because replacing them by some larger expression results in a new conjecture that implies the original conjecture. So we can use the following hint to prove the theorem instantaneously:

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

This instructs our metafunction to replace a by 10, b by 20, and c by 30 when it encounters them in upper-boundable contexts. It will also only do the replacement if it can prove that the inequality holds in its context.

A final detail: Observe that the occurrence of a in (<= 0 a) is also an upper-boundable context. However, performing the replacement here would be bad because it would destroy the information that a is nonnegative. In particular, replacing a by its bound here would result in a trivially true hypothesis. The meta rule avoids making such replacements when it can determine that they are trivial.

Boundable Contexts

The rules used for determining which contexts are upper or lower boundable are as follows.

Preconditions	Results
(< a b) or (<= a b) in hypothesis/negated literal	a lower boundable, b upper boundable
(< a b) or (<= a b) in conclusion/non-negated literal	a upper boundable, b lower boundable
(+ a b) in upper/lower boundable context	a, b upper/lower boundable
(- a) in upper/lower boundable context	a lower/upper boundable
(* a b) in upper/lower boundable context, b nonnegative	a upper/lower boundable
(* a b) in upper/lower boundable context, b nonpositive	a lower/upper boundable
(/ a) in upper/lower boundable context, a positive/negative	a lower/upper boundable if bound is also positive/negative

Future work

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