1 files changed, 63 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
new file mode 100644
index 000000000..ab00fbfe3
--- /dev/null
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -0,0 +1,63 @@
+\achapter{\protect{Miscellaneous extensions}}
+%HEVEA\cutname{miscellaneous.html}
+
+\asection{Program derivation}
+
+Coq comes with an extension called {\tt Derive}, which supports
+program derivation. Typically in the style of Bird and Meertens or
+derivations of program refinements. 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$ SuchThat \term{} As \ident$_2$]
+       {\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}}
+
+The name $\ident_1$ can appear in \term. This command opens a new
+proof presenting the user with a goal for \term{} in which the name
+$\ident_1$ is bound to a existential variables {\tt ?x} (formally,
+there are other goals standing for the existential variables but they
+are shelved, as described in Section~\ref{shelve}).
+
+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}, 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 Import Coq.Numbers.Natural.Peano.NPeano.
+
+Section P.
+
+Variables (n m k:nat).
+
+\end{coq_example*}
+\begin{coq_example}
+Derive p SuchThat ((k*n)+(k*m) = p) As h.
+Proof.
+rewrite <- Nat.mul_add_distr_l.
+subst p.
+reflexivity.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+
+End P.
+
+\end{coq_example*}
+\begin{coq_example}
+Print p.
+Check h.
+\end{coq_example}
+
+Any property can be used as \term, not only an equation. In
+particular, it could be an order relation specifying some form of
+program refinement or a non-executable property from which deriving a
+program is convenient.