Division is multiplication by the reciprocal of a number, also called the additive inverse. So we should first define the reciprocal.
The approach we have taken with all the other operations so far is to take the bounds on the inputs at a particular step number and ask, if we know the inputs are within this interval, what are the smallest and largest possible values for the output? That gives us the interval for the output at the same step number.
Let's try the same thing with the reciprocal now. If we know our value is between r and s inclusive (r ≤ x ≤ s), what can we say about the value of its reciprocal?
If r and s are both positive, then we have bounds 1/s ≤ x ≤ 1/r.
If r and s are both negative, then we have bounds 1/s ≤ x ≤ 1/r again.
But what about when r is negative and s is positive? Then there's no lower or upper limit on what 1/x can be.
Division by zero is undefined, so if a number is zero, we shouldn't be trying to take its reciprocal in the first place. But some of the intervals for a nonzero number could contain zero. On the other hand, the intervals for a nonzero number can't contain zero forever. Eventually there has to be a lower bound greater than zero or an upper bound less than zero.
We can fix this issue by searching for that first interval which does not contain zero and using it as a replacement for all the prior intervals which do contain zero. After this preprocessing, we can use the usual approach.
While writing the comparison function, we've already written a function
>>8963 to perform this sort of search. It takes real numbers w, x, y, z and a proof of w < x or y < z, and finds the first k such that max(w[k]) < min(x[k]) or max(y[k]) < min(z[k]). By feeding it the numbers x, 0, 0, x and a proof of x <> 0 (defined as x < 0 or 0 < x), it is guaranteed to find a k such that max(x[k]) < 0 or 0 < min(x[k]), or in other words, 0 ∉ x[k]. Let's call this k value find_zeroless(x, p) where x is the number and p is the proof that x <> 0.
We'll adopt the practice used in Coq of denoting the reciprocal of x as /x to distinguish it from the division 1/x, which is to be defined in terms of /x as 1/x = 1 · /x. For division of rational numbers, Coq handles division by zero by simply assigning a bogus value of zero to the result. This won't work for real numbers because we need to explicitly use the proof that x <> 0, and there's no way to decide whether x <> 0 or x = 0 by an algorithm given x. So in order to compute the reciprocal of x, we'll need to pass both x and a proof p that x <> 0. Let's denote this as /x †p. Sometimes when writing about /x and find_zeroless, where there is no ambiguity, we will omit the proof argument for brevity, but it will still be there, at least until program extraction.
We define
¥ /[a, b]Q = [/b, /a]Q¥ (/x †p)[k] = /(x[max{k, find_zeroless(x, p)}])Our reciprocal operation on rational intervals behaves as we want provided 0 is not a member:
¥ r ∈ [a, b]Q implies /r ∈ /[a, b]Q provided 0 ∉ [a, b]Q.Either 0 < a ≤ r ≤ b or a ≤ r ≤ b < 0. In either case /b ≤ /r ≤ /a.
And in the cases we use it, 0 will indeed not be a member:
¥ If k ≥ find_zeroless(x), then 0 ∉ x[k].We already have 0 ∉ x[find_zeroless(x)]. Since x[k] ⊆ x[find_zeroless(x)], this implies 0 ∉ x[k].
In particular it follows that
¥ 0 ∉ x[max{k, find_zeroless(x)}].Now let's prove that /x meets the conditions to be a member of our real number type.
First, nestedness:
>That each interval contains the endpoints of itself and all subsequent intervals. That is, if k2 ≥ k1, then min(x[k2]) ∈ x[k1] and max(x[k2]) ∈ x[k1].Suppose k2 ≥ k1. Let k1' = max{k1, find_zeroless(x)} and k2' = max{k2, find_zeroless(x)}. We also have k2' ≥ k1', and thus min(x[k2']) ∈ x[k1'] and max(x[k2']) ∈ x[k1']. Since 0 ∉ x[k1'], it follows that
min((/x)[k2]) = /max(x[k2']) ∈ /(x[k1']) = (/x)[k1]
max((/x)[k2]) = /min(x[k2']) ∈ /(x[k1']) = (/x)[k1].
Some quick lemmas before proving the next part:
¥ If a ≤ b and 0 ∉ [a, b]Q, then min{a², b²} > 0.Either 0 < a ≤ b or a ≤ b < 0. In either case a² > 0 and b² > 0. Therefore min{a², b²} > 0.
¥ If r, s ∈ [a, b]Q and 0 ∉ [a, b]Q, then r·s ≥ min{a², b²}.Either 0 < a ≤ r, s, in which case r·s ≥ a·s ≥ a² ≥ min(a², b²}, or r, s ≤ b < 0, in which case r·s ≥ b·s ≥ b² ≥ min{a², b²}.
Now we can prove convergence:
>That for any positive rational number, there will eventually be an interval in the sequence whose width (maximum - minimum) is smaller than that number.Suppose eps > 0. Let n = find_zeroless(x) and c = min{min(x[n])², max(x[n])²}. Since min(x[n]) ≤ max(x[n]) and 0 ∉ x[n], we have c > 0. Thus eps·c > 0, and there exists a k such that width(x[k]) < eps·c. Let k' = max{k, n} and [a, b]Q = x[k']. Since a, b ∈ x[n] and 0 ∉ x[n], we have a·b ≥ c > 0 and a, b ≠ 0. Therefore
width(/(x[k'])) = 1/a - 1/b = (b - a) / (a·b) = width(x[k']) / (a·b) ≤ width(x[k]) / c < eps.
Thus /x as we have defined it is a real number.