\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

\[ \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}
\]
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 \texttt{nsatz}}
\tacindex{nsatz}

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}.

\asection{More about \texttt{nsatz}}

Hilbert's Nullstellensatz theorem shows how to reduce proofs of equalities on
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 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.


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 \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: 

     	\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.
     \end{itemize}
  \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: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: 
