1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
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:
|
