In my previous post I showed how to approximate the square root of a rational number with a fully computable error bound, and I formalized the results in the programming language Coq. The results of that experiment made me wonder just how far could I take the arguments of real analysis into the world of rational numbers. Here I document my attempt to formalize the intermediate value theorem on rational numbers.
Intuitively the intermediate value theorem states that if you have a smooth curve which crosses over a line, then there must be a point at which the curve and line intersect. This theorem may seem quite obvious if you try to visualize it, What makes it less obvious is that we are typically using real numbers to represent the line and curve, and so the intermediate value theorem confirms that there are no gaps in the real number system.
We know that the intermediate value theorem is true on real numbers, but the proof is nonconstructive - we can not produce an algorithm from it. If we restricted ourselves to rational numbers then we can produce an algorithm, but does it actually compute anything useful? The problem with rational numbers is that they have many gaps, for example the square root of almost every rational number is not itself rational (and so the intermediate value theorem would fail if e.g. the point of intersection occurs at the square root of such a rational number).
After doing a bit of Googling I found a constructive argument for the intermediate value theorem on a number system which is somewhere in between rational numbers and real numbers, namely computable real numbers. That argument may be found here (theorem 2.2). Just like in the square root example I showed here the argument shows an approximate result rather than exact result. Reading the argument I didn’t see any major barriers to reciting the whole thing on rational numbers.
I have a running Coq document formalizing such a result on Github. I will show here the basic outline of the document, and I will show how to approximate \(\pi\) and \(sqrt(3)\) using the code from the Coq document.
If you have no interest in formalized mathematics, you can skip to the final section where I give concrete numerical results.
I mentioned “smooth curves” in the introduction, here I take “smooth” to mean “uniformly continuous.” I will show here the mathematical definition of uniform continuity and then follow it with a formalization in Coq.
A function \(f\) is said to be uniformly continuous if for every \(\epsilon >0 \) there exists a \(\delta>0\) such that whenever \( |x-y|<\delta \) we have \( |f(x)-f(y)|<\epsilon \).
The translation of this to Coq is fairly straightforward:
Definition UniformlyContinuous (f:Q->Q) := forall e,
e>0 -> {d | 0<d /\ forall x x0, Qabs (x - x0) < d -> Qabs ( (f x) - (f x0) ) < e}.
Note that Q is the type of rational numbers defined in QArith, and Qabs is the absolute value function on rational numbers.
Surprisingly this is realy all we need to state the intermediate value theorem.
The constructive intermediate value theorem may be stated as follows:
Suppose that \(f\) is a uniformly continuous function, that \(f(0) < 0 \), and \(f(1) > 0 \). Then for every \(\epsilon>0\) there exists \(c \) with \( 0 < c < 1 \) such that \( |f(c)|<\epsilon \).
Which may be formalized in Coq as
Theorem intermediate_value_theorem : forall (f:Q->Q) (e:Q), UniformlyContinuous f -> e>0 -> (f 0) < 0 -> (f 1) > 0 ->
{ c | 0<c /\ c<1 /\ Qabs (f c) < e }.
We can easily generalize this to an interval different than \( [0,1] \) by coordinate transformation.
Unlike in classical mathematics on real numbers we can’t take the indirect route to proving existence. Here existence means I give you an actual function that accepts an \( \epsilon \) as input and outputs a \(c \) that satisfies the desired error properties. In other words, \(c \) must be computable.
I have a running document showing my progress making a full proof on github. At the time of this writing it is a little disorganized as I am still learning Coq and am still getting a feeling for best practices.
I haven’t completed the proof yet, but I have outlined it and proved the vast majority of the important lemmas. But in Coq a lot of situations arise which make completing the proof tricky, such as handling occurence of different integer types. This is a fixable situation, so if I develop enough motivation one day I believe I will complete it.
I reproduce here the function bisect_c which computes the approximate root, and I follow it with some numerical results.
Lemma useful_order_property : forall e r:Q, e>0 -> {r>-e} + {r<=e}.
Proof.
intros.
destruct (Qlt_le_dec 0 r).
* assert( -e < r) by lra. auto.
* assert( r<= e ) by lra. auto.
Defined.
Fixpoint bisect_c (f:Q->Q) (a:Q) (b:Q) (e:Q) (He:(e>0)) (m:nat) := match m with
0%nat => (1#2)*(a+b)
| S p =>
let mid := (1#2)*(a+b) in
if (useful_order_property e (f mid) He)
then (bisect_c f a mid e He p)
else (bisect_c f mid b e He p)
end.
For now the function requires a natural number input which tells Coq how many iterations of the bisection algorithm to run. Once the theorem is proved we may remove this argument and only input the desired error of the output. Also note this function does not strictly limit you to the inerval \( [0,1] \). I made that limitation in the theorem statement simply to make the proof a little cleaner, but no generality is lost in doing so.
I show below some simple calculations in Coq approximating irrational numbers. But unlike the square root case we can potentially approximate much more rich real numbers. For example the number \( \pi \) is not the root of a polynomial with rational coefficients. Here I will use the bisection algorithm implemented above to approximate \( \sqrt{2} \) and \( \pi \)
I now approximate \( \sqrt{2} \) by computing an approximate root of the function
\[ f(x) = x^2 - 2 \]
Definition sqrt_err (x:Q) := x*x-(2#1).
Eval vm_compute in (bisect_c sqrt_err 1 (2#1) err a_pos_err 10).
(*
output = 7886384135759669829227169901838660068704256/
5575186299632655785383929568162090376495104
*)
The output is
\[\sqrt{2} \approx \frac{7886384135759669829227169901838660068704256}{5575186299632655785383929568162090376495104}\]
which is approximately
\[1.41455078\]
Since \( \pi \) is a transcendental number, it is not the root of a fixed polynomial with rational coefficients. However if our polynomial is adadptive in the sense that it uses progressively higher orders to achieve better accuracy as needed, then we can resort to the taylor expansion of \(\sin\). Specifically I will seek a root of the function
\[ \sin(x) - \frac{1}{2} \approx \sum _ {n=0} ^ {N(x)} (-1)^n \frac{1}{(2n+1)!}x^{2n+1} - \frac{1}{2} \]
The root of this function is \( \pi/6 \). This may appear to be violating the transcendental nature of \( \pi \) because the right-hand-side appears to be a polynomial with rational coefficients. It is not however, because the summation limit depends on \( x \), and in fact for this particular way of computing \(sin\) the summation limit \(N(x)\) will grow without bound as \( x\) grows. One could use the alternating series theorem to compute an \(N(x)\) which gives an acceptable error threshold.
Without further delay however I show the Coq code and results
Fixpoint sin (n:nat) (x:Q) := match n with
0%nat => x
| S p => (sin p x) + ((-1%Q)^(Z.of_nat n))*(1#(Pos.of_nat (fact (2*n+1))))*(x^(Z.of_nat (2*n+1)))
end.
Eval vm_compute in ((bisect_c (fun x => (sin 4 x) - (1#2)) 0 1 err a_pos_err 10)).
(* output = 162147175555812138057465856 / 309485009821345068724781056 *)
The output is
\[ \frac{\pi}{6} \approx \frac{162147175555812138057465856}{309485009821345068724781056} \]
resulting in the following approximation for pi
\[ \pi \approx 3.14355469 \]
While I haven’t completely finished proving the theorem, I have worked it out fully on paper and got close enough on Coq that I am fairly sure that after some routine (but tedious) manipulations in Coq the fully formalized version will be complete. I will post a short update on my blog once I have finished that project.
What this shows me is that a fairly important theorem in real analysis can indeed be transported into the rational number setting. Suggesting to me that perhaps even more deep work could be done completely in rational numbers without needing to “pass to the limit” of real or computable real numbers. I will continue to think about this and see where it takes me.