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 0b45b9ceca..fc791ce1c0 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 ab00fbfe37..0000000000 --- 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 7e68dd7524..e511160075 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 0000000000..ab00fbfe37 --- /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 From cfde2528ba4e93795df50356d47fbc9ced62e517 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 30 Mar 2018 17:36:36 +0200 Subject: [Sphinx] Add chapter 30 Thanks to Paul Steckler for porting this chapter. --- doc/sphinx/addendum/miscellaneous-extensions.rst | 118 ++++++++++++----------- doc/sphinx/index.rst | 1 + 2 files changed, 62 insertions(+), 57 deletions(-) diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index ab00fbfe37..b0343a8f01 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,63 +1,67 @@ -\achapter{\protect{Miscellaneous extensions}} -%HEVEA\cutname{miscellaneous.html} +.. include:: ../replaces.rst -\asection{Program derivation} +.. _miscellaneousextensions: -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. +Miscellaneous extensions +======================= -\subsection[\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$] - {\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}} +:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html +:Converted by: Paul Steckler -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}). +.. contents:: + :local: + :depth: 1 +---- + +Program derivation +----------------- + +|Coq| comes with an extension called ``Derive``, which supports program +derivation. Typically in the style of Bird and Meertens or derivations +of program refinements. To use the Derive extension it must first be +required with ``Require Coq.Derive.Derive``. When the extension is loaded, +it provides the following command: + +.. cmd:: Derive @ident SuchThat @term As @ident + +The first `ident` can appear in `term`. This command opens a new proof +presenting the user with a goal for term in which the name `ident` is +bound to an existential variable `?x` (formally, there are other goals +standing for the existential variables but they are shelved, as +described in Section :ref:`TODO-8.17.4`). 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. + ++ The first one is named using the first `ident` and is defined as the proof of the + shelved goal (which is also the value of `?x`). It is always + transparent. ++ The second one is named using the second `ident`. It has type `term`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with ``Qed``, and transparent if the proof ends with ``Defined``. + +.. example:: + .. coqtop:: all + + Require Coq.derive.Derive. + Require Import Coq.Numbers.Natural.Peano.NPeano. + + Section P. + + Variables (n m k:nat). + + Derive p SuchThat ((k*n)+(k*m) = p) As h. + Proof. + rewrite <- Nat.mul_add_distr_l. + subst p. + reflexivity. + Qed. + + End P. + + Print p. + Check h. + +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/sphinx/index.rst b/doc/sphinx/index.rst index 3dd4f80200..db03693ff9 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -55,6 +55,7 @@ Table of contents addendum/nsatz addendum/generalized-rewriting addendum/parallel-proof-processing + addendum/miscellaneous-extensions .. toctree:: :caption: Reference -- cgit v1.2.3