diff options
| -rw-r--r-- | doc/refman/Nsatz.tex | 86 |
1 files changed, 45 insertions, 41 deletions
diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex index 7e0dfa896..211c76764 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: |