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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
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:
|
