Nsatz: a solver for equalities in integral domains¶
- Author
Loïc Pottier
To use the tactics described in this section, load the Nsatz module with the
command Require Import Nsatz. Alternatively, if you prefer not to transitively depend on the
files that declare the axioms used to define the real numbers, you can
Require Import NsatzTactic instead; this will still allow
nsatz to solve goals defined about \(\mathbb{Z}\),
\(\mathbb{Q}\) and any user-registered rings.
-
Tactic
nsatz with radicalmax := one_term strategy := one_term parameters := one_term variables := one_term?¶ This tactic is for solving 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 divisors. For example, \(A\) can be \(\mathbb{R}\), \(\mathbb{Z}\), or \(\mathbb{Q}\). Note that the equality \(=\) used in these goals can be any setoid equality (see Tactics enabled on user provided relations) , not only Leibniz 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.
radicalmaxbound when searching for r such that \(c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)\). This argument must be of type
N(binary natural numbers).strategygives the order on variables \(X_1,\ldots,X_n\) and the strategy used in Buchberger algorithm (see [GMN+91] for details):
strategy := 0%Z: reverse lexicographic order and newest s-polynomial.strategy := 1%Z: reverse lexicographic order and sugar strategy.strategy := 2%Z: pure lexicographic order and newest s-polynomial.strategy := 3%Z: pure lexicographic order and sugar strategy.
parametersa list of parameters of type
R, containing the variables \(X_{i_1},\ldots,X_{i_k}\) among \(X_1,\ldots,X_n\). Computation will be performed with rational fractions in these parameters, i.e. polynomials have coefficients in \(R(X_{i_1},\ldots,X_{i_k})\). In this case, the coefficient \(c\) can be a nonconstant polynomial in \(X_{i_1},\ldots,X_{i_k}\), and the tactic produces a goal which states that \(c\) is not zero.variablesa list of variables of type
Rin the decreasing order in which they will be used in the Buchberger algorithm. If the list is empty, thenlvaris replaced by all the variables which are not inparameters.
See the file Nsatz.v for examples, especially in geometry.
More about 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 Typeclasses.