\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Nsatz: tactics for proving equalities in integral domains

Author

Loïc Pottier

To use the tactics described in this section, load the Nsatz module with the command Require Import Nsatz.

Tactic nsatz with radicalmax := one_term strategy := one_term parameters := one_term variables := one_term?

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.

radicalmax

bound when searching for r such that \(c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)\). This argument must be of type N (binary natural numbers).

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%Z: reverse lexicographic order and newest s-polynomial.

  • strategy := 1%Z: reverse lexicographic order and sugar strategy.

  • strategy := 2%Z: pure lexicographic order and newest s-polynomial.

  • strategy := 3%Z: pure lexicographic order and sugar strategy.

parameters

a list of parameters of type R, containing the variables \(X_{i_1},\ldots,X_{i_k}\) among \(X_1,\ldots,X_n\). Computation will be performed with rational fractions in these parameters, i.e. polynomials have coefficients in \(R(X_{i_1},\ldots,X_{i_k})\). In this case, the coefficient \(c\) can be a nonconstant polynomial in \(X_{i_1},\ldots,X_{i_k}\), and the tactic produces a goal which states that \(c\) is not zero.

variables

a list of variables of type R in the decreasing order in which they will be used in the Buchberger algorithm. If the list is empty, then lvar is replaced by all the variables which are not in parameters.

See the file Nsatz.v for examples, especially in geometry.

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.