
# Nsatz: tactics for proving equalities in integral domains¶

Author: Loïc Pottier
nsatz

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.

You can load the Nsatz module with the command Require Import Nsatz.

## 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.

Variant 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 $$c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)$$

• strategy gives the order on variables $$X_1,\ldots,X_n$$ and the strategy used in Buchberger algorithm (see [GMN+91] 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 $$X_{i_1},\ldots,X_{i_k}$$ among $$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 $$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.

• variables is the list of the variables in the decreasing order in which they will be used in the Buchberger algorithm. If variables = (@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.