		Search-engine friendly clone of the ACL2 documentation.

Proof-automation

Rewrite-bounds

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 (< a b) -- that is, a conclusion (< a b) or hypothesis (<= b a) -- we replace a by an upper bound and b by a lower bound; for a negated such literal we do the opposite. The resulting new clause then implies the old one. Actually, this isn't quite true -- we do the replacement via a meta rule, which replaces a non-negated literal (< a b) by (or (hide (< a b)) (< a-upper b-lower)), or a negated literal (< a b) by (and (hide (< a b)) (< a-lower b-upper)). These replacements are equivalent to the input literals because (< a-upper b-lower) implies (< a b) and (< a b) implies (< a-lower b-upper).

Note that performing such replacements (if we remove the hide terms from consideration) may change a theorem to a non-theorem. It therefore is best to be careful to apply this strategy only in the right places.

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.

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.

Future work

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