Chapter 24  Nsatz: tactics for proving equalities in integral domains

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 cA, 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 (PQ)r = ∑i Si (PiQi), which will be proved by the tactic ring.

This is achieved by the computation of a Groebner basis of the ideal generated by P1Q1,...,PsQs, 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


See file Nsatz.v for examples.