Derive plugin: document new syntax.

1 files changed, 26 insertions, 23 deletions

diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex
index c852708957..6ce4ee4801 100644
--- a/doc/refman/Misc.tex
+++ b/doc/refman/Misc.tex
@@ -3,35 +3,35 @@
 \asection{Program derivation}
 
 Coq comes with an extension called {\tt Derive}, which supports
-program derivation. Typically in the style of Bird and Meertens. 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.
+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$ From \term$_1$ Upto \term$_2$ As \ident$_2$]
-       {\tt Derive \ident$_1$ From \term$_1$ Upto \term$_2$ As \ident$_2$\comindex{Derive}}
+\subsection[\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$]
+       {\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}}
 
-This commands opens a new proof with two goals. The first one has, as
-conclusion, the type of $\term_1$, but is shelved (see
-Section~\ref{shelve}). The visible goal has type {\tt \term$_2$
-\term$_1$ ?x} where {\tt ?x} is the existential variable
-corresponding to the shelved goal.
+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
+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$_1$
-  \term$_2$ \ident$_1$}, 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}.
+  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 Coq.Numbers.Natural.Peano.NPeano.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
 
 Section P.
 
@@ -39,9 +39,10 @@ Variables (n m k:nat).
 
 \end{coq_example*}
 \begin{coq_example}
-Derive p From ((k*n)+(k*m)) Upto eq As h.
+Derive p SuchThat ((k*n)+(k*m) = p) As h.
 Proof.
-rewrite <- Mult.mult_plus_distr_l.
+rewrite <- Nat.mul_add_distr_l.
+subst p.
 reflexivity.
 \end{coq_example}
 \begin{coq_example*}
@@ -55,5 +56,7 @@ Print p.
 Check h.
 \end{coq_example}
 
-As $\term_2$ does not need to be a symmetric relation, the
-{\tt Derive} extension may also be used for program refinement.
+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.