From ad702b290fcee29305b8a83b7530e24d655b2d7d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 30 Mar 2018 17:34:50 +0200 Subject: [Sphinx] Move chapter 30 to new infrastructure --- Makefile.doc | 3 +- doc/refman/Misc.tex | 63 ------------------------ doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/miscellaneous-extensions.rst | 63 ++++++++++++++++++++++++ 4 files changed, 64 insertions(+), 66 deletions(-) delete mode 100644 doc/refman/Misc.tex create mode 100644 doc/sphinx/addendum/miscellaneous-extensions.rst diff --git a/Makefile.doc b/Makefile.doc index 0b45b9cec..fc791ce1c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,8 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Universes.v.tex \ - Misc.v.tex) + Universes.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex deleted file mode 100644 index ab00fbfe3..000000000 --- a/doc/refman/Misc.tex +++ /dev/null @@ -1,63 +0,0 @@ -\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. diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 7e68dd752..e51116007 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -118,7 +118,6 @@ Options A and B of the licence are {\em not} elected.} \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% \include{Universes.v}% Universe polymorphes -\include{Misc.v} %BEGIN LATEX \RefManCutCommand{ENDADDENDUM=\thepage} %END LATEX 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. -- cgit v1.2.3