doc Nstaz updated

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

1 files changed, 45 insertions, 41 deletions

diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index 7e0dfa896b..211c767649 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -1,56 +1,56 @@
 \achapter{Nsatz: tactics for proving equalities in $\mathbb{R}$ and $\mathbb{Z}$}
 \aauthor{Loïc Pottier}
 
-The tactic {\tt nsatz} proves formulas of the form
+The tactic \texttt{nsatz} proves formulas of the form
 
 \[ \begin{array}{l}
-  \forall X_1,\ldots,X_n \in R,\\
-   P_1(X_1,\ldots,X_n) = 0 \wedge \ldots \wedge  P_s(X_1,\ldots,X_n) =0\\ 
- \Rightarrow P(X_1,\ldots,X_n) = 0\\
+  \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}
 \]
-where $R$ is $\mathbb{R}$ or $\mathbb{Z}$ and $P, P_1,\ldots,P_s$
-are polynomials.
+where $P,Q, P_1,Q_1,\ldots,P_s,Q_s$ are polynomials.
+ 
+The tactic \texttt{nsatzZ} proves the same formulas where the $X_i$ are in $\mathbb{Z}$.
 
-\asection{Using the basic tactic {tt nsatz}}
+\asection{Using the basic tactic \texttt{nsatz}}
 \tacindex{nsatz}
 
-If you work $\mathbb{R}$, load the {\tt NsatzR} module ({\tt Require
-NsatzR}.) and use the tactic {\tt nsatz} or {\tt nsatzR}.
+If you work in $\mathbb{R}$, load the
+\texttt{NsatzR} module: \texttt{Require
+NsatzR}.\\
+ and use the tactic \texttt{nsatz} or \texttt{nsatzR}.
+If you work in $\mathbb{Z}$ do the same thing {\em mutatis mutandis}.
 
-If you work $\mathbb{Z}$, load the {\tt NsatzZ} module ({\tt Require
-NsatzR}.) and use the tactic {\tt nsatzZ}.
-
-\asection{More about {tt nsatz}}
+\asection{More about \texttt{nsatz}}
 
 Hilbert's Nullstellensatz theorem shows how to reduce proofs of equalities on
-polynomials to algebraic computations: it is easy to see that if a polynomial
-$P$ in $R[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} Q_i P_i$, with $c
-\in R$, $c \not = 0$, $r$ a positive integer, and the $Q_i$s in
+polynomials on a ring R (with no zero divisor) to algebraic computations: it is easy to see that if a polynomial
+$P$ in $R[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} S_i P_i$, with $c
+\in R$, $c \not = 0$, $r$ a positive integer, and the $S_i$s in
 $R[X_1,\ldots,X_n]$, then $P$ is zero whenever polynomials $P_1,...,P_s$  are
 zero (the converse is also true when R is an algebraic closed field:
 the method is complete). 
 
-So, proving our initial problem reduces into finding $Q_1,\ldots,Q_s$, $c$
-and $r$ such that $c P^r = \sum_{i} Q_i P_i$, which will be proved by the
-tactic {\tt ring}.
+So, proving our initial problem can reduce into finding $S_1,\ldots,S_s$, $c$
+and $r$ such that $c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)$, which will be proved by the
+tactic \texttt{ring}.
 
 This is achieved by the computation of a Groebner basis of the
-ideal generated by $P_1,...,P_s$, with an adapted version of the Buchberger
+ideal generated by $P_1-Q_1,...,P_s-Q_s$, with an adapted version of the Buchberger
 algorithm.
 
 
-The {\tt NsatzR} module defines the tactics:
-{\tt nsatz},  {\tt nsatzRradical rmax}, {\tt nsatzRparameters lparam}, and
-the generic tactic {\tt nsatzRpv rmax strategy lparam lvar}.
+The \texttt{NsatzR} module defines the tactics
+\texttt{nsatz},  \texttt{nsatzRradical}, \texttt{nsatzRparameters}, and
+the generic tactic \texttt{nsatzRpv}, which are used as follows:
 
   \begin{itemize}
-  \item {\tt nsatzRpv rmax strategy lparam lvar}:
+  \item \texttt{nsatzRpv rmax strategy lparam lvar}:
     \begin{itemize}
-	\item {\tt rmax} is the maximum r when for searching r s.t.$c P^r =
-\sum_{i=1}^{s} Q_i P_i$
-	\item {\tt strategy} gives the order on variables of polynomials $P$
-and $P_i$ and the strategy of choice for s-polynomials during Buchberger algorithm: 
+	\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: 
 
      	\begin{itemize}
 		\item  strategy = 0: reverse lexicographic order and newest s-polynomial.
@@ -59,20 +59,24 @@ and $P_i$ and the strategy of choice for s-polynomials during Buchberger algorit
 	        \item   strategy = 3: pure lexicographic order and sugar strategy.
 	\end{itemize}
 
-	\item {\tt lparam} is the list of variables which are considered as
-   parameters. Computation will be performed with rational fractions in these
-   variables. 
-
-	\item {\tt lvar} islist of the variables of polynomial $P$ and $P_i$,
-in decreasing order, used in Buchberger algorithm. If {\tt lvar} = {(@nil
-R)}, then {\tt lvar} is replaced by all the variables which are not in lparam.
+	\item \texttt{lparam} is the list of variables
+$X_{i_1},\ldots,X_{i_k}$  among $X_1,...,X_n$ which are considered as
+   parameters: computation will be performed with rational fractions in these
+   variables, i.e. polynomials are considered with coefficients in
+$R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non
+constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal
+which states that $c$ is not zero.
+
+	\item \texttt{lvar} is the list of the variables
+in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{lvar} = {(@nil
+R)}, then \texttt{lvar} is replaced by all the variables which are not in lparam.
      \end{itemize}
-  \item {\tt nsatzRparameters lparam} is equivalent to 
-        {\tt nsatzRpv nsatzRpv 6\%N 1\%Z lparam (@nil R)}
-  \item {\tt nsatzRradical rmax} is equivalent to 
-	{\tt nsatzRpv rmax 1\%Z (@nil R) (@nil R)}
-  \item {\tt nsatz} is equivalent to 
-	{\tt nsatzRpv 6\%N 1\%Z (@nil R) (@nil R)}
+  \item \texttt{nsatzRparameters lparam} is equivalent to 
+        \texttt{nsatzRpv 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)}
   \end{itemize}
 
 %%% Local Variables: