Intervals, bounder functions, and bounder correctness

Bounder Forms 1 and 2: (implies (and (tau-intervalp i1) ... (or (equal (tau-interval-dom i1) 'dom1-1) ...) ... (in-tau-intervalp x1 i1) ...) (and (tau-intervalp (bounder-fn i1 ...)) (in-tau-intervalptarget(bounder-fn i1 ...))))

where *target* is either *Form 1* or *Form
2* case, respectively. However, the shape above is meant just as a
reminder. Details are given below.

This topic first explains the basic shape of *Bounder Form 1*. Then
it illustrates *Bounder Form 2*. Finally, it deals briefly with proving
bounder correctness theorems. The community book
`+`, `*`, `/`, `floor`, `mod`, `logand`, `lognot`, `logior`, `logorc1`, `logeqv`, `logxor`, and `ash`. You might look at or include this
book to see more example theorems, to see how proofs of such theorems are
managed, and to experiment with their effects on proving theorems involving
arithmetic over finite or half-finite intervals.

A bounder correctness theorem establishes that *Form 2*, for the

Let us start with an example. Let `binary-+`). Consider the target term

Defining this precisely is more tedious than describing it in English
because one must make precise the notions of ``less restrictive'' domains,
``weaker'' relations, and the possibility that either or both of the bounds
could be ``infinite.'' But we can easily imagine defining the function

Then the following *Bounder Form 1* formula establishes the
correctness of

(implies (and (tau-intervalp intx) (tau-intervalp inty) (in-tau-intervalp x intx) (in-tau-intervalp y inty)) (and (tau-intervalp (bounder-for-+ intx inty)) (in-tau-intervalp (+ x y) (bounder-for-+ intx inty))))

For example, suppose we have a formula with the following hypotheses

(and (integerp a) (<= 0 a) (<= a 10) (rationalp b) (< 0 b) (<= b 20))

and suppose the tau system encounters the term

Thus, by defining bounder functions and proving them correct the user can give the tau system the ability to compute the bounds on function calls as a function of the known bounds on their actuals.

It is sometimes useful to restrict the domains of the intervals to be
considered. For example, in bounding

If we were to define

(implies (and (tau-intervalp intx) ; (a) (tau-intervalp inty) (or (equal (tau-interval-dom intx) 'INTEGERP) ; (b) (equal (tau-interval-dom intx) 'RATIONALP)) (or (equal (tau-interval-dom inty) 'INTEGERP) (equal (tau-interval-dom inty) 'RATIONALP)) (in-tau-intervalp x intx) ; (c) (in-tau-intervalp y inty)) (and (tau-intervalp (bounder-for-* intx inty)) ; (d) (in-tau-intervalp (* x y) ; (e) (bounder-for-* intx inty))))

In this case,

The above theorem for

The hypotheses of a bounder theorem must be a conjunction and the conjuncts must be partitionable into three parts, (a), (b), and (c). The conclusion, must be a conjunction, must contain at least two conjuncts, (d) and (e), and is allowed to contain others that are simply ignored for purposes of bounders. (See the note below about why we allow but ignore additional conjuncts in the conclusion.)

Part (a) introduces some distinct ``interval variables,'' here called
``ivars,'' that are known to denote intervals; for the example above, the
ivars are

Part (b) allows us to restrict the domains of some of the intervals. Each
hypothesis in part (b) must be a disjunction and each of the disjuncts must be
of the form

Part (c) consists of a set of

Part (d) introduces the name of the bounder function, here
`tau-intervalp` or `in-tau-intervalp`.

Part (e) introduces the name of the function being bounded, here

Thus, parts (c) and (e) together establish a mapping between the actuals of a call of the function being bounded and the intervals to be supplied to the bounder.

The parts identified above may be presented in any order and the literals
constituting those parts may be mingled. Thus, for example, here is another
version of the theorem above that generates the same bounding information for
the tau system. In this version, the hypotheses and conclusions are
rearranged,

(implies (and (tau-intervalp intx) ; (a) (or (equal (tau-interval-dom intx) 'INTEGERP) ; (b) (equal (tau-interval-dom intx) 'RATIONALP)) (in-tau-intervalp x intx) ; (c) (tau-intervalp inty) ; (a) (or (equal (tau-interval-dom inty) 'INTEGERP) ; (b) (equal (tau-interval-dom inty) 'RATIONALP)) (in-tau-intervalp y inty)) (and (in-tau-intervalp (* x y) ; (e) (bounder-for-* inty intx)) (tau-intervalp (bounder-for-* inty intx)) ; (d))) (or (equal (tau-interval-dom (bounder-for-* inty intx)) 'INTEGERP) (equal (tau-interval-dom (bounder-for-* inty intx)) 'RATIONALP))

*Note on why bounder forms allow additional conjuncts in the
conclusion*: It is often the case that one creates bounders by composing
other bounders. To prove compositional bounds correct one must often prove
more than the mere correctness of the components. For example, one might need
to prove that the domain of the new bounding interval is

*An Illustration of Bounder Form 2*: Suppose

(defun quad-bounds-0 (i) (cond ((and (tau-interval-lo i) (<= 0 (tau-interval-lo i))) (make-tau-interval 'integerp nil 0 nil (tau-interval-hi i))) (t (make-tau-interval nil nil nil nil nil)))) (defun quad-bounds-1 (i) (cond ((and (tau-interval-lo i) (<= 0 (tau-interval-lo i))) (make-tau-interval 'integerp nil 0 nil 3)) (t (make-tau-interval nil nil nil nil nil))))

Note that the bounders assume

As noted in the discussion below about how to prove bounder correctness theorems, proving these bounders correct will require an arithmetic book, e.g.,

(include-book "arithmetic-5/top" :dir :system)

Here then are two bounder correctness theorems of *Form 2*:

(defthm quad-bounds-0-correct (implies (and (tau-intervalp i) (equal (tau-interval-dom i) 'INTEGERP) (in-tau-intervalp x i)) (and (tau-intervalp (quad-bounds-0 i)) (in-tau-intervalp (mv-nth 0 (quad x)) (quad-bounds-0 i)))) :rule-classes :tau-system) (defthm quad-bounds-1-correct (implies (and (tau-intervalp i) (equal (tau-interval-dom i) 'INTEGERP) (in-tau-intervalp x i)) (and (tau-intervalp (quad-bounds-1 i)) (in-tau-intervalp (mv-nth 1 (quad x)) (quad-bounds-1 i)))) :rule-classes :tau-system)

As noted above, if these bounders are to be used in constructing other bounders, we might include (in the first theorem) an additional concluding conjunct, such as

(equal (tau-interval-dom (quad-bounds-0 i)) 'INTEGERP)

so that we can keep

:rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((quad-bounds-0 i))))

Since the theorem is being stored as some kind of rule and since it
satisfies the *Bounder Form 2* shape, it will additionally be stored as a

*Note on proving bounder theorems*: Proving bounder theorems is just
like proving any other arithmetic theorem and you will need whatever libraries
are appropriate for the problem domain you are working in. Do not expect the
tau system to be of much use in proving bounder theorems. A typical bounder
theorem might require you to prove a subgoal like *how to construct* bounded intervals from other
bounded intervals. So when you undertake to define a bounder and prove it
correct, go into the project with your eyes open!

But bounder functions can be broadly divided into two classes, those defined in terms of arithmetic on the interval bounds and those defined in terms of other bounders. For example, given that

(LOGXOR x y) = (LOGNOT (LOGEQV x y))

an interval for bounding

Regardless of which style of bounder we are dealing with, we have found it
useful to prove the basic theorems relating the tau interval accessors to
`make-tau-interval`, e.g.,

(equal (tau-interval-dom (make-tau-interval dom lo-rel lo hi-rel hi)) dom)

and then disable those functions to avoid seeing excessive

When dealing with bounders defined in the direct, arithmetic style, we tend
to keep `tau-intervalp` and `in-tau-intervalp` enabled so they
unfold and expose the algebra.

When dealing with bounders defined compositionally in terms of other
verified bounders, we tend to keep `tau-intervalp` and `in-tau-intervalp` disabled so we can rely on the previously proved bounder
theorems as rewrite and forward chaining rules.

Note that this last remark means that when you prove bounder correctness
theorems you should include corollaries that are useful