Theorem Proving with Differential Equations
Post Metadata
Once UW kicks off the school year at the end of this month, I’ll officially be a second-year PhD student It’s a scary, yet exciting, thought! There will be loads of new incoming students, interesting research, and many surprises in store! This is also the perfect time to think critically about my goals in the PhD. One of them is building a larger theme for my research. I’m not committing to a thesis topic here. Rather, I’m searching for a concise, ideally pithy, way to describe my research. This blog post is a trial run for one theme: Real Analysis through the lens of Programming Languages.
From this perspective, my last blog post (where I talked about polynomials and a special data structure to represent them) is really about implementation challenges of computational real analysis. The key idea there was that traditional intermediate representations (IR) are insufficient for analyzing polynomial code so we needed to augment our IR with a multiset.
With that enriched IR, we can start blending ideas from PL and Real Analysis. As you might have guessed from the title of this blog post, one of those ideas is to use differential equations (specifically Initial Value Problems) to prove mathematical identities. If the thought of solving diff-eqs brings back terrible memories, don’t worry. That’s the really cool part: You don’t have to solve the diff-eq to use it in proving other identities.
From here, I’ll guide you through:
- Defining functions implicitly from their differential equation
- Specifying constraints on that function to ensure its a unique solution to the diff-eq
- A proof technique relying on diff eqs and functions defined by diff eqs
Our end goal will be to prove:
\[\cos(\arcsin x) = \sqrt{1 - x^2}\]And we’ll define all of our functions (cos, arcsin, and sqrt) from diff eqs all along the way!
Defining Solutions to ODEs
The governing ordinary differential equation (ODE) we need is
\[x''(t) + x(t) = 0\]This equation says that the independent variable is t and the function described is x(t). It says that the second derivative of x with respect to t and the original function sum to zero.
This actually describes a family of functions, not a particular solution. For instance, if a function f satisfies this equation then so does 2*f or 3*f. In fact, any function of the form n * f will satisfy the equation. That constant n is the “constant of integration” from integral calculus.
To specify a particular solution, we need a set of constraints to solve for a particular constant of integration. Typically, a set of point evaluations are used. In this case, if we use the point evaluations:
\[\begin{aligned} y(0) &= 0 \\ y'(0) &= 1 \end{aligned}\]We call the solution to this ODE with these constraints sin.
If we swap the point evaluations to be
\[\begin{aligned} y(0) &= 1 \\ y'(0) &= 0 \end{aligned}\]We call this solution, cos.
Relating Sine and Cosine with Derivatives
Now, in our quest to prove trig properties from ODEs, we have a
big problem. Our ODE for sin and cos tell us about the zero-th and second derivative, but they don’t specify anything about the first derivative. At this point, we have no idea that
the derivative of sin is cos. As far as we’ve seen, these functions are different solutions to the same ODE, but don’t have any other relation. Let’s fix that.
We’re going to do our first proof using only the ODE and point evaluations from above.
Here’s the claim:
| Claim | Facts |
|---|---|
| \[\sin'(t) = \cos(t)\] | \[\begin{aligned} \sin''(t) &= -\sin(t) \\ \cos''(t) &= -\cos(t) \\ \sin(0) &= 0 \\ \sin'(0) &= 1 \\ \cos(0) &= 1 \\ \cos'(0) &= 0 \end{aligned}\] |
In order to show that sin and cos are described by the same ODE, we will search for the ODE describing sin' and show that it’s the same ODE as cos. Because ODEs have unique solutions (given some continuity conditions we can ignore for this blog post) they must be the same function.
The search procedure is as simple as taking derivatives and pattern matching. Here’s the proof:
\[\begin{aligned} \sin' &= \cos \\ \partial( \sin' &= \cos ) \\ \sin'' &= \cos' \\ -\sin &= \cos' \qquad \mathrm{by} ~ \sin'' = -\sin \end{aligned}\]Interestingly, we haven’t defined cos' yet. This might raise some mental alarm bells, but it will be resolved by taking a second derivative. Continuing the proof:
Now, here’s where things get interesting. As we just observed, we took two derivatives of the left-hand-side (cos'' to -cos) and we get back the negative of the original function. This is the property of the original ODE of cos (y'' = -y). We can also see that the right-hand-side of our equality has the exact same property, (sin')'' = -sin'. This pattern means both cos and sin' are solutions to the same ODE.
We’ve haven’t established, however, that
cos and sin' are the same solution. To do that, we need to show sin' meets the point evaluation constraints for cos. Specifically we need to show
sin'(0) = 1sin''(0) = 0
The first fact is immediate from the definition of sin. The second fact follows from sin''(t) = -sin(t) and sin(0) = 0.
Just to step back, we defined two functions as the particular solution to an ODE.
We used only those definitions (and calculus) to do a proof that sin' is cos.
This idea is actually very general and next we’ll do a proof that’s a little
more involved but fundamentally the same. This next time, we won’t know what the ODE is and we’ll need to find it!
Constructing ODEs for Inverse Functions
In general, inverse functions are defined by this property:
\[x - f (f^{\mathrm{inv}} (x)) = 0\]Fortunately, we can build a general ODE formula from this definition using Implicit Differentiation. Here’s the idea:
\[\begin{aligned} x - f (f^{\mathrm{inv}} (x)) &= 0 \\ \frac{d}{dx}( x - f (f^{\mathrm{inv}} (x)) &= 0 ) \\ 1 - f' (f^{\mathrm{inv}} (x)) \cdot f^{\mathrm{inv}} (x)'&= 0 % \frac{1}{f' (f_{\mathrm{inv}} x)} &= (f^{\mathrm{inv}})' x \end{aligned}\]Notice that when we differentiated, we needed to apply the chain rule to the f(f^inv(x)) term, which produces the derivative of the inverse function.
Constructing an ODE for Sqrt
The essential property of sqrt is
From this, we can apply our function inverse derivative from the definition of sqrt giving:
Rewriting this into a more standard form:
\[(\sqrt{x})' = \frac{1}{2\sqrt{x}}\]To see that this really describes an ODE, let’s replace sqrt(x) with y which gives the non-linear ODE:
Here we defined sqrt from an inverse property. We could have, however, defined sqrt as the solution to the ODE we derived. Let’s add a particular point evaluation so we can use the inverse and ODE definitions interchangeably. We might be tempted to use sqrt(0) = 0 but the derivative of sqrt at zero is not defined there. We can’t use an undefined point to define a particular solution. Let’s use sqrt(1) = 1 which is well defined.
Constructing an ODE for Arcsine
We can construct inverse-sine (arcsin) via the same procedure
Applying the derivative of an inverse formula we get:
\[1 - \cos(\arcsin(x))(\arcsin(x))' = 0\]Which in standard form is
\[\arcsin' x = \frac{1}{\cos(\arcsin x)}\]Like sqrt this is a non-linear ODE which is made more obvious by substituting arcsin(x) for y:
Proving Trig Identities
Here’s our ultimate goal:
| Claim | Facts |
|---|---|
| \[\cos(\arcsin x) = \sqrt{1 - x^2}\] | \[\begin{aligned} \sin' &= \cos \\ \cos' &= -\sin \\ (\sqrt x)' &= 1 / (2\sqrt{x}) \\ \arcsin' x &= 1/\cos(\arcsin x) \\ \sin(0) &= 0 \\ \cos(0) &= 1 \\ \sqrt{1} &= 1 \\ (\sqrt{x})^2 &= x \\ \arcsin(0) &= 0 \\ \sin(\arcsin x) &= x \\ \end{aligned}\] |
The only operation we know how to apply to our defined functions is the derivative. Let’s see what happens taking a derivative to our goal and mechanically applying our rules.
\[\begin{aligned} \frac{d}{dx} (y = \cos(\arcsin x) &= \sqrt{1 - x^2}) \\ y' = -\sin(\arcsin x) \cdot \frac{1}{\cos(\arcsin x)} &= \frac{1}{2\sqrt{1 - x^2}} \cdot -2x \\ y' = \frac{-x}{\cos(\arcsin x)} &= \frac{-x}{\sqrt{1 - x^2}} \end{aligned}\]It seems that both the left-hand side and right-hand side of our proposition follow a similar pattern, specifically:
\[y' = \frac{-x}{y}\]or in canonical ODE form
\[x + yy' = 0\]We’ve discovered the ODE that both sides of our proposition satisfy. We can’t forget about ensuring they are the same particular solution. Let’s test out x = 0:
We’ve proven an incredible trig identity from first principles using only the facts we’ve already proven. It only required taking a single derivative instead of a complex chain of rewrites and other algebraic trickery.
The Details of Function Domain
A note of caution! We never talked about where functions are defined. For inverse functions (arcsin, sqrt, etc.), this is a critical consideration that we completely ignored. Implicitly, we said that our final identity cos(arscin x) = sqrt(1 - x*x) is true for all x. This is simply not true. It’s only the case for x on the interval [0, 1]. That’s the final piece of this technique that’s missing, and it’s essential for correctness. Unfortunately, I don’t have an answer for you right now but I’m actively working on through the details. It’s fun challenge that’s full of subtlety!
Conclusion
It turns out that you don’t need to solve an ODE in order for it to be useful, which is beneficial because most differential equations don’t have a simple solution. Put another way, we can prove theorems of transcendental functions using only a few ingredients. Because of this, you might imagine automating this procedure as a tactic in a theorem prover. That brings us back to the theme in the beginning of this post: connecting the abstract mathematics to program analysis and transforms. So many more possibilities await!