Our implementation of the intermediate value theorem uses the bisection method, and follows the proof outline given in an earlier system [3]. The theorem is:
The procedure is to let c be the midpoint of a and b, and
decide if |f(c)| < 
. If so then we are done, and otherwise
|f(c)| > 0 by pos_quasi_decidable. It follows easily that either
f(c) > 0 or -(f(c)) > 0. In the former case consider the interval
[c,b], and in the latter, [a,c], and repeat the procedure on this new
interval. To see that this terminates, note that the diameter of the intervals
goes to zero, and by continuity the diameter of the range of f goes to
zero as well. This range always includes both positive and negative values, so
eventually it lies wholly inside (-
, 
).
The proof generating this algorithm is an induction proof with the following induction hypothesis:
The proof that this holds for all n is interesting in that the base case and the induction step are almost identical. The base case is the lemma bisection_step, and in the induction step we just instantiate this lemma on the appropriate sub-interval.
The lemma that tells us how many steps to take is
and together with continuity and the following lemma provide all that is necessary to complete the proof.
Now we can look at the details, though perhaps some explanation is in order.
A Nuprl proof is a tree where each node has a numbered list of hypotheses and declarations, a conclusion (or goal), and a tactic name. If a tactic succeeds in proving the goal from the hypotheses then the node becomes a leaf. Otherwise the tactic generates one or more subgoals which, if proven, are sufficient to justify the claim of the current node. Thus the overall idea is to start with the statement of the theorem at the root and gradually reduce it to trivialities by applying tactics.
In reading this proof, the easiest way to understand what the tactics do is probably to just look past them and see what subgoals they generate.
