Chapter 24 Nsatz: tactics for proving equalities in integral domains

# Coq Reference Manual

# 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

∀ X1,…,Xn ∈ A,
P1(X1,…,Xn) = Q1(X1,…,Xn) , … , Ps(X1,…,Xn) =Qs(X1,…,Xn)
⊢ P(X1,…,Xn) = Q(X1,…,Xn)

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 25.7) , not only Leibnitz equality.

It also proves formulas

∀ X1,…,Xn ∈ A,
P1(X1,…,Xn) = Q1(X1,…,Xn) ∧ … ∧ Ps(X1,…,Xn) =Qs(X1,…,Xn)
→ P(X1,…,Xn) = Q(X1,…,Xn)

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[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 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 Si (Pi − Qi)
- `strategy` gives the order on variables X1,...Xn 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 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.

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