Chapter 25 Nsatz: tactics for proving equalities in integral domains
The tactic nsatz proves goals of the form
where P,Q, P1,Q1,…,Ps,Qs are polynomials and A is an integral domain, i.e. a commutative ring with no zero divisor. For example, A can be ℝ, ℤ, of ℚ. Note that the equality = used in these goals can be any setoid equality (see 26.7) , not only Leibnitz equality.
It also proves formulas
doing automatic introductions.
25.1 Using the basic tactic nsatz
Nsatz module: Require Import Nsatz.
and use the tactic nsatz.
25.2 More about 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[X1,…,Xn] verifies c Pr = ∑i=1s Si Pi, with c ∈ A, c ≠ 0, r a positive integer, and the Sis in A[X1,…,Xn], then P is zero whenever polynomials P1,...,Ps 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 S1,…,Ss, c and r such that c (P−Q)r = ∑i Si (Pi−Qi), which will be proved by the tactic ring.
This is achieved by the computation of a Groebner basis of the ideal generated by P1−Q1,...,Ps−Qs, with an adapted version of the Buchberger algorithm.
This computation is done after a step of reification, which is performed using Type Classes (see 19) .
The Nsatz module defines the tactic
nsatz, which can be used without arguments:
or with the syntax:
nsatz with radicalmax:=number%N strategy:=number%Z parameters:=list of variables variables:=list of variables
- radicalmax is a bound when for searching r s.t.c (P−Q)r = ∑i=1..s Si (Pi − Qi)
- strategy gives the order on variables X1,...Xn and
the strategy used in Buchberger algorithm (see
 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
Xi1,…,Xik among X1,...,Xn which are considered as
parameters: computation will be performed with rational fractions in these
variables, i.e. polynomials are considered with coefficients in
R(Xi1,…,Xik). In this case, the coefficient c can be a non
constant polynomial in Xi1,…,Xik, and the tactic produces a goal
which states that c is not zero.
- variables is the list of the variables in the decreasing order in which they will be used in Buchberger algorithm. If variables = (@nil R), then lvar is replaced by all the variables which are not in parameters.
See file Nsatz.v for many examples, specially in geometry.