modifs de nsatz suggerees par Hugo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13194 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 28 insertions, 10 deletions

diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index 211c767649..be93d5dd74 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -1,23 +1,30 @@
 \achapter{Nsatz: tactics for proving equalities in $\mathbb{R}$ and $\mathbb{Z}$}
 \aauthor{Loïc Pottier}
 
-The tactic \texttt{nsatz} proves formulas of the form
+The tactic \texttt{nsatz} proves goals of the form
 
 \[ \begin{array}{l}
   \forall X_1,\ldots,X_n \in \mathbb{R},\\
-   P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) \wedge \ldots \wedge  P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ 
- \Rightarrow P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\
+   P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) , \ldots ,  P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ 
+ \vdash P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\
   \end{array}
 \]
 where $P,Q, P_1,Q_1,\ldots,P_s,Q_s$ are polynomials.
+It also proves formulas
+\[ \begin{array}{l}
+  \forall X_1,\ldots,X_n \in \mathbb{R},\\
+   P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) \wedge \ldots \wedge  P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ 
+ \rightarrow P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\
+  \end{array}
+\] doing automatic introductions.
  
-The tactic \texttt{nsatzZ} proves the same formulas where the $X_i$ are in $\mathbb{Z}$.
+The tactic \texttt{nsatzZ} proves the same goals where the $X_i$ are in $\mathbb{Z}$.
 
 \asection{Using the basic tactic \texttt{nsatz}}
 \tacindex{nsatz}
 
 If you work in $\mathbb{R}$, load the
-\texttt{NsatzR} module: \texttt{Require
+\texttt{NsatzR} module: \texttt{Require Import
 NsatzR}.\\
  and use the tactic \texttt{nsatz} or \texttt{nsatzR}.
 If you work in $\mathbb{Z}$ do the same thing {\em mutatis mutandis}.
@@ -48,9 +55,11 @@ the generic tactic \texttt{nsatzRpv}, which are used as follows:
   \begin{itemize}
   \item \texttt{nsatzRpv rmax strategy lparam lvar}:
     \begin{itemize}
-	\item \texttt{rmax} is the maximum r when for searching r s.t.$c (P-Q)^r =
-\sum_{i=1}^{s} S_i (P_i - Q_i)$
-	\item \texttt{strategy} gives the order on variables $X_1,...X_n$ and the strategy of choice for s-polynomials during Buchberger algorithm: 
+	\item \texttt{rmax} is a bound when for searching r s.t.$c (P-Q)^r =
+\sum_{i=1..s} S_i (P_i - Q_i)$
+	\item \texttt{strategy} gives the order on variables $X_1,...X_n$ and
+the strategy used in Buchberger algorithm (see
+\cite{sugar} for details): 
 
      	\begin{itemize}
 		\item  strategy = 0: reverse lexicographic order and newest s-polynomial.
@@ -72,11 +81,11 @@ in the decreasing order in which they will be used in Buchberger algorithm. If \
 R)}, then \texttt{lvar} is replaced by all the variables which are not in lparam.
      \end{itemize}
   \item \texttt{nsatzRparameters lparam} is equivalent to 
-        \texttt{nsatzRpv nsatzRpv 6\%N 1\%Z lparam (@nil R)}
+        \texttt{nsatzRpv 6\%N 1\%Z lparam (@nil R)}
   \item \texttt{nsatzRradical rmax} is equivalent to 
 	\texttt{nsatzRpv rmax 1\%Z (@nil R) (@nil R)}
   \item \texttt{nsatz} is equivalent to 
-	\texttt{nsatzRpv 6\%N 1\%Z (@nil R) (@nil R)}
+	\texttt{nsatzRpv 6\%N 1\%Z (@nil R) (@nil R)}ls
   \end{itemize}
 
 %%% Local Variables: 
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 2e589e4716..f93b66f99b 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1237,6 +1237,15 @@ Languages},
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
 
+@INPROCEEDINGS{sugar,
+    author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso},
+    title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm},
+    booktitle = { Proceedings of the ISSAC'91, ACM Press},
+    year = {1991},
+    pages = {5--4},
+    publisher = {}
+}
+
 @Comment{cross-references, must be at end}
 
 @Book{Bastad92,