Chapter 24  Nsatz: tactics for proving equalities in integral domains

• 24.1  Using the basic tactic nsatz
• 24.2  More about nsatz

Loïc Pottier

The tactic nsatz proves goals of the form

where P,Q, P₁,Q₁,…,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₁,…,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_is in A[X₁,…,X_n], then P is zero whenever polynomials P₁,...,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₁,…,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₁−Q₁,...,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 low-level 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₁,...X_n and the strategy used in Buchberger algorithm (see [69] 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.

• lparam is the list of variables X_i1,…,X_ik among X₁,...,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.