Chapter 24 Nsatz: tactics for proving equalities in integral domains
Loïc Pottier
The tactic nsatz proves goals of the form

where P,Q, P_{1},Q_{1},…,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 ℝ, ℤ, of ℚ. Note that the equality = used in these goals can be any setoid equality (see 25.7) , not only Leibnitz equality.
It also proves formulas

doing automatic introductions.
24.1 Using the basic tactic nsatz
Load the
Nsatz module: Require Import Nsatz.
and use the tactic nsatz.
24.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[X_{1},…,X_{n}] verifies c P^{r} = ∑_{i=1}^{s} S_{i} P_{i}, with c ∈ A, c ≠ 0, r a positive integer, and the S_{i}s in A[X_{1},…,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},…,S_{s}, c and r such that c (P−Q)^{r} = ∑_{i} S_{i} (P_{i}−Q_{i}), which will be proved by the tactic 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 reification, which is performed using Type Classes (see 18) .
The Nsatz module defines the generic tactic
nsatz, which uses the lowlevel tactic nsatz_domainpv:
nsatz_domainpv pretac rmax strategy lparam lvar simpltac domain
where:
 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 ltac:idtac.
 rmax is a bound when for searching r s.t.c (P−Q)^{r} = ∑_{i=1..s} S_{i} (P_{i} − Q_{i})
 strategy gives the order on variables X_{1},...X_{n} and
the strategy used in Buchberger algorithm (see
[69] for details):
 strategy = 0: reverse lexicographic order and newest spolynomial.
 strategy = 1: reverse lexicographic order and sugar strategy.
 strategy = 2: pure lexicographic order and newest spolynomial.
 strategy = 3: pure lexicographic order and sugar strategy.
 lparam is the list of variables
X_{i1},…,X_{ik} 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_{i1},…,X_{ik}). In this case, the coefficient c can be a non
constant polynomial in X_{i1},…,X_{ik}, and the tactic produces a goal
which states that c is not zero.
 lvar is the list of the variables in the decreasing order in which they will be used in Buchberger algorithm. If lvar = (@nil R), then lvar is replaced by all the variables which are not in lparam.
 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 ltac:simpl.
 domain is the object of type Domain representing A, its operations and properties of integral domain.
See file Nsatz.v for examples.