| Author: | Loïc Pottier |
|---|
.. tacn:: nsatz
:name: nsatz
This tactic is for solving goals of the form
:math:`\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 :math:`P, Q, P_1, Q_1, \ldots, P_s, Q_s` are polynomials and :math:`A` is an integral
domain, i.e. a commutative ring with no zero divisors. For example, :math:`A`
can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`.
Note that the equality :math:`=` used in these goals can be
any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibniz equality.
It also proves formulas
:math:`\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.
You can load the ``Nsatz`` module with the command ``Require Import Nsatz``.
Hilbert’s Nullstellensatz theorem shows how to reduce proofs of equalities on polynomials on a commutative ring A with no zero divisors 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,\ldots,P_s are zero (the converse is also true when A is an algebraically closed field: the method is complete).
So, solving our initial problem reduces to 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 ring.
This is achieved by the computation of a Gröbner 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 reification, which is performed using :ref:`typeclasses`.
.. tacv:: nsatz with radicalmax:=@num%N strategy:=@num%Z parameters:=[{*, @ident}] variables:=[{*, @ident}]
Most complete syntax for `nsatz`.
* `radicalmax` is a bound when searching for r such that
:math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`
* `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy
used in Buchberger algorithm (see :cite:`sugar` for details):
* strategy = 0: reverse lexicographic order and newest s-polynomial.
* strategy = 1: reverse lexicographic order and sugar strategy.
* strategy = 2: pure lexicographic order and newest s-polynomial.
* strategy = 3: pure lexicographic order and sugar strategy.
* `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among
:math:`X_1,\ldots,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 :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient
:math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic
produces a goal which states that :math:`c` is not zero.
* `variables` is the list of the variables in the decreasing order in
which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`,
then `lvar` is replaced by all the variables which are not in
`parameters`.
See the file Nsatz.v for many examples, especially in geometry.