\problemdata     
{computation-7}           
{functions, recursive definitions}              
{}              
{S02 in-class Week 5} 		
{S02 Meyer}        	

\newcommand{\ms}[1]{\mathop{\text{#1}}}
\providecommand{\ide}{\ms{id}}
\providecommand{\EF}{\ms{F18}}
\providecommand{\T}{\ms{ST}}
\providecommand{\leaves}{\ms{leaves}}
\providecommand{\nodes}{\ms{nodes}}
\providecommand{\makeb}{\ms{makeboth}}
\newcommand{\membern}{\ms{member}}
\newcommand{\makeleft}{\ms{makeleft}}
\newcommand{\makeright}{\ms{makeright}}
\newcommand{\deriv}{\frac{d}{dx}}
\renewcommand{\paren}[1]{\left(#1\right)}
\newcommand{\setl}{\mathbb{L}}
\newcommand{\setlone}{\mathbb{\ell}_1}
\newcommand{\setltwo}{\mathbb{\ell}_2}


\begin{problem}





The Elementary 18.01 Functions ($\EF$'s) are the set of functions of
one real variable defined recursively as follows:
\begin{enumerate}
\item The identity function, $\ide(x) \eqdef x$ is an $\EF$,\label{identfunc}

\item any the constant function is an $\EF$,\label{const}

\item $\sin, \cos, e^x$ are $\EF$'s,\label{basefunc} 

     and if $f,g$ are $\EF$'s, then so are

\item $f + g$, $f-g$, $fg$, $f/g$\label{+-}

\item the inverse function $f^{-1}$,\label{inversefunc}

\item the composition $f \compose g$.\label{cmp}
\end{enumerate}

Show that the Elementary 18.01 Functions are \emph{closed under taking
derivatives}.  That is, show that if $f$ is an $\EF$, then so is $df/dx$.

\solution{
\begin{proof}
By Structural Induction on def of $\EF$.
\begin{description}

\item[Base Cases:] We want to show that the derivatives of all the
functions mentioned in rules \ref{identfunc},\ref{const}, \ref{basefunc} are in $\EF$. This is easy: for
example, $\deriv \ide(x) = 1$ (constant) and so by rule \ref{const}, it is in
$\EF$. Similarly, $\deriv \cos(x) = -\sin(x)$ which is also in $\EF$
since $\sin(x)\in \EF$ by rule 3 and therefore $-\sin(x)$ as well (by
rule \ref{+-}). 

\item[Induction Case:] ($f^{-1}$).  Assume $df/dx \in \EF$ to prove
$\deriv f^{-1}(x) \in \EF$.  We know that $\deriv f^{-1}(x) =
1/(df/dx)$. Since $df/dx \in \EF$ (by assumption), so is $\frac{1}{df/dx}$ (by~\ref{+-}). 

\item[Induction Case:] ($f \compose g$).  Assume $df/dx, dg/dx \in \EF$
to prove $\deriv(f\compose g) \in \EF$. $\deriv(f\compose g)=\deriv
\paren{f(g)}=\frac{d}{dg}f(g)\cdot\frac{dg}{dx}$ which is in $\EF$  by~\ref{cmp}
and~\ref{+-}. The other cases are similar.
\end{description}
\end{proof}


}
\end{problem}
