**Next:**Tactics

**Up:**Real Analysis in

**Previous:**Some Theorems

## The Intermediate Value Theorem

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.

**Next:**Tactics

**Up:**Real Analysis in

**Previous:**Some Theorems