diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-30 17:34:50 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-05 08:36:57 +0200 |
commit | ad702b290fcee29305b8a83b7530e24d655b2d7d (patch) | |
tree | 320dc621864286250b393e5f6e289da26f60ab42 /doc/sphinx/addendum | |
parent | 42253af97391efff691f7966c25c9625593a9301 (diff) |
[Sphinx] Move chapter 30 to new infrastructure
Diffstat (limited to 'doc/sphinx/addendum')
-rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 63 |
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. |