\achapter{\protect{Miscellaneous extensions}}

\asection{Program derivation}

Coq comes with an extension called {\tt Derive}, which supports
program derivation. Typically in the style of Bird and Meertens. To
use the {\tt Derive} extension it must first be required with
{\tt Require Coq.Derive.Derive}. When the extension is loaded, it
provides the following command.

\subsection[\tt Derive \ident$_1$ From \term$_1$ Upto \term$_2$ As \ident$_2$]
       {\tt Derive \ident$_1$ From \term$_1$ Upto \term$_2$ As \ident$_2$\comindex{Derive}}

This commands opens a new proof with two goals. The first one has, as
conclusion, the type of $\term_1$, but is shelved (see
Section~\ref{shelve}). The visible goal has type {\tt \term$_2$
\term$_1$ ?x} where {\tt ?x} is the existential variable
corresponding to the shelved goal.

When the proof ends two constants are defined
\begin{itemize}
\item The first one is name $\ident_1$ and is defined as the proof of
  the shelved goal (which is also the value of {\tt ?x}). It is always
  transparent.
\item The second one is name $\ident_2$. It has type {\tt \term$_1$
  \term$_2$ \ident$_1$}, and its body is the proof of the initially
  visible goal. It is opaque if the proof ends with {\tt Qed}, and
  transparent if the proof ends with {\tt Defined}.
\end{itemize}

\Example
\begin{coq_example*}
Require Coq.Derive.Derive.
Require Coq.Numbers.Natural.Peano.NPeano.

Section P.

Variables (n m k:nat).

\end{coq_example*}
\begin{coq_example}
Derive p From ((k*n)+(k*m)) Upto eq As h.
Proof.
rewrite <- Mult.mult_plus_distr_l.
reflexivity.
\end{coq_example}
\begin{coq_example*}
Qed.

End P.

\end{coq_example*}
\begin{coq_example}
Print p.
Check h.
\end{coq_example}

As $\term_2$ does not need to be a symmetric relation, the
{\tt Derive} extension may also be used for program refinement.