# 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) = 1`

`sin''(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!