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 --- doc/sphinx/addendum/miscellaneous-extensions.rst | 63 ++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 doc/sphinx/addendum/miscellaneous-extensions.rst (limited to 'doc/sphinx') 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 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(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index ab00fbfe3..b0343a8f0 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 3dd4f8020..db03693ff 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