.. include:: ../preamble.rst

.. _nsatz:

Nsatz: tactics for proving equalities in integral domains
===========================================================

:Author: Loïc Pottier

The tactic `nsatz` proves goals of the form

:math:`\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 :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is an integral
domain, i.e. a commutative ring with no zero divisor. For example, :math:`A`
can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`.
Note that the equality :math:`=` used in these goals can be
any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibnitz equality.

It also proves formulas

:math:`\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.


Using the basic tactic `nsatz`
------------------------------


Load the Nsatz module:

.. coqtop:: all

  Require Import Nsatz.

and use the tactic `nsatz`.

More about `nsatz`
---------------------

Hilbert’s Nullstellensatz theorem shows how to reduce proofs of
equalities on polynomials on a commutative ring :math:`A` with no zero divisor
to algebraic computations: it is easy to see that if a polynomial :math:`P` in
:math:`A[X_1,\ldots,X_n]` verifies :math:`c P^r = \sum_{i=1}^{s} S_i P_i`, with
:math:`c \in A`, :math:`c \not = 0`,
:math:`r` a positive integer, and the :math:`S_i` s in :math:`A[X_1,\ldots,X_n ]`,
then :math:`P` is zero whenever polynomials :math:`P_1,\ldots,P_s` are zero
(the converse is also true when :math:`A` is an algebraic closed field: the method is
complete).

So, proving our initial problem can reduce into finding :math:`S_1,\ldots,S_s`,
:math:`c` and :math:`r` such that :math:`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 :math:`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 :ref:`typeclasses`.

The ``Nsatz`` module defines the tactic `nsatz`, which can be used without
arguments, or with the syntax:

| nsatz with radicalmax:=num%N strategy:=num%Z parameters:= :n:`{* var}` variables:= :n:`{* var}`

where:

* `radicalmax` is a bound when for searching r s.t.
  :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`

* `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy
  used in Buchberger algorithm (see :cite:`sugar` 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 :math:`X_{i_1},\ldots,X_{i_k}` among
  :math:`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 :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient
  :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic
  produces a goal which states that :math:`c` is not zero.

* `variables` is the list of the variables in the decreasing order in
  which they will be used in Buchberger algorithm. If `variables` = `(@nil R)`,
  then `lvar` is replaced by all the variables which are not in
  `parameters`.

See file `Nsatz.v` for many examples, especially in geometry.