ajout oublie

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

1 files changed, 81 insertions, 0 deletions

diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
new file mode 100644
index 0000000000..7e0dfa896b
--- /dev/null
+++ b/doc/refman/Nsatz.tex
@@ -0,0 +1,81 @@
+\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
+
+\[ \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\\
+  \end{array}
+\]
+where $R$ is $\mathbb{R}$ or $\mathbb{Z}$ and $P, P_1,\ldots,P_s$
+are polynomials.
+
+\asection{Using the basic tactic {tt 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 $\mathbb{Z}$, load the {\tt NsatzZ} module ({\tt Require
+NsatzR}.) and use the tactic {\tt nsatzZ}.
+
+\asection{More about {tt 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
+$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}.
+
+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
+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}.
+
+  \begin{itemize}
+  \item {\tt 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: 
+
+     	\begin{itemize}
+		\item  strategy = 0: reverse lexicographic order and newest s-polynomial.
+		\item   strategy = 1: reverse lexicographic order and sugar strategy.
+	        \item  strategy = 2: pure lexicographic order and newest s-polynomial.
+	        \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.
+     \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)}
+  \end{itemize}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: