1 files changed, 110 insertions, 0 deletions
diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
new file mode 100644
index 00000000..794e461f
--- /dev/null
+++ b/doc/refman/Nsatz.tex
@@ -0,0 +1,110 @@
+\achapter{Nsatz: tactics for proving equalities in integral domains}
+\aauthor{Loīc Pottier}
+
+The tactic \texttt{nsatz} proves goals of the form
+
+\[ \begin{array}{l}
+  \forall X_1,\ldots,X_n \in A,\\
+   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 and A is an integral
+domain, i.e. a commutative ring with no zero divisor. For example, A can be
+$\mathbb{R}$, $\mathbb{Z}$, of $\mathbb{Q}$. Note that the equality $=$ used in these
+goals can be any setoid equality 
+(see \ref{setoidtactics})
+, not only Leibnitz equality.
+
+It also proves formulas
+\[ \begin{array}{l}
+  \forall X_1,\ldots,X_n \in A,\\
+   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.
+ 
+\asection{Using the basic tactic \texttt{nsatz}}
+\tacindex{nsatz}
+
+Load the
+\texttt{Nsatz} module: \texttt{Require Import Nsatz}.\\
+ and use the tactic \texttt{nsatz}.
+
+\asection{More about \texttt{nsatz}}
+
+Hilbert's Nullstellensatz theorem shows how to reduce proofs of equalities on
+polynomials on a commutative ring A with no zero divisor to algebraic computations: it is easy to see that if a polynomial
+$P$ in $A[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} S_i P_i$, with $c
+\in A$, $c \not = 0$, $r$ a positive integer, and the $S_i$s in
+$A[X_1,\ldots,X_n]$, then $P$ is zero whenever polynomials $P_1,...,P_s$  are
+zero (the converse is also true when A is an algebraic closed field:
+the method is complete). 
+
+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-Q_1,...,P_s-Q_s$, with an adapted version of the Buchberger
+algorithm.
+
+This computation is done after a step of {\em reification}, which is
+performed using {\em Type Classes} 
+(see \ref{typeclasses})
+.
+
+The \texttt{Nsatz} module defines the generic tactic
+\texttt{nsatz}, which uses the low-level tactic \texttt{nsatz\_domainpv}: \\
+\vspace*{3mm}
+\texttt{nsatz\_domainpv pretac rmax strategy lparam lvar simpltac domain}
+
+where:
+
+\begin{itemize}
+    \item \texttt{pretac} is a tactic depending on the ring A; its goal is to
+make apparent the generic operations of a domain (ring\_eq, ring\_plus, etc),
+both in the goal and the hypotheses; it is executed first. By default it is \texttt{ltac:idtac}.
+
+    \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.
+		\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 \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.
+
+    \item \texttt{simpltac} is a tactic depending on the ring A; its goal is to
+simplify goals and make apparent the generic operations of a domain after
+simplifications. By default it is \texttt{ltac:simpl}.
+
+ \item \texttt{domain} is the object of type Domain representing A, its
+operations and properties of integral domain.
+
+\end{itemize}
+
+See file \texttt{Nsatz.v} for examples.
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: