|
|
|---|
|
|
|
|---|
Find and prove upper and lower bounds for an expression, following a series of simplification steps.
Usage:
(def-bounds my-bounds-theorem ;; Term to simplify and bound (* (foo x) (bar y)) ;; Assumption (default t) :hyp (foo-input-p x) ;; Simplification steps, each a hint keyword-value list :simp-hints ((:in-theory (enable foo-cancel)) (:expand ((bar y)))) ;; User-provided bound suggestions :user-bounds ((< a 10) ;; upper-bound exact term A by 10 (:free (c) (>= (bar c) (foo c))) ;; lower-bound (bar x) for any x by (foo x) if it reduces to a constant ;; Case splits, each either a list of cases or a ;; :ranges or :ranges-from-to-by form. :cases (((< (foo-prime x) 0)) (:ranges (bar-quotient y) -1000 -100 0 100 1000) (:ranges-from-to-by (bar-remainder y) #x-a000 #xa000 #x1000)) ;; Further simplification steps for after case splitting :post-cases-hints ((:in-theory (enable bar-remainder-when-foo-prime-negative))) ;; Choose to only bound in one direction or the other :skip-lower nil :skip-upper nil ;; Indicates that the term is always an integer :integerp t ;; Override rule-classes (default :linear) :rule-classes (:rewrite :linear) ;; Override theory when applying bound-rewriter (must enable REWRITE-BOUNDS) :in-theory-override (enable rewrite-bounds))
This applies the given simplification steps and case-splits, then uses rewrite-bounds to find an upper and lower bound for the resulting expression.
Then it replicates these steps in a