\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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: a solver for equalities in integral domains

Author:: Loïc Pottier, Laurent Thery and Lionel Blatter

Note

The tactics described in this chapter require the Stdlib library.

This chapter presents the tactics dedicated to deal with equalities in integral domains.

What does this tactics do?

On a commutative ring $A$ with no zero divisors, 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).

In the same setting, if a polynomial $P$ in $A[X_1,\ldots,X_n]$ verifies

\[c P = \sum_{i=1}^{s} S_i P_i,\]

with $c \in A$, $c = 1$ or $c = -1$, then $\exists Y_1, \dots, Y_m, P = \sum_{i=1}^{m} Y_i P_i$

The nsatz and ensatz tactics finds $S_1, \ldots, S_s$, $c$ and $r$ by the computation of a Gröbner basis of the ideal generated by $P_1,...,P_s$. This is done using an adapted version of the Buchberger algorithm. The witnesses returned by the Buchberger algorithm are checked to be correct solutions to the inital problem.

This computation is done after a step of reification.

Concrete usage

To use the tactic nsatz described in this section, load the Nsatz module with the command Require Import Nsatz. Alternatively, if you prefer not to transitively depend on the files that declare the axioms used to define the real numbers, you can Require Import NsatzTactic instead; this will still allow nsatz to solve goals defined about $\mathbb{Z}$, $\mathbb{Q}$ and any user-registered rings.

To use the tactic ensatz described in this section, use in addition the command Require Import ENsatzTactic.

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

This tactic is for solving goals of the form

\[P(\bar{X}) = Q(\bar{X}),\]

given the premises $P_i(\bar{X}) = Q_i(\bar{X})$, which may be part of the goal or already in the hypotheses or a mix of both, $A$ an integral domain, i.e. a commutative ring with no zero divisors, $\bar{X} \in A^n$, and all $P$ and $Q$ are polynomials. 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.

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

Example

From Stdlib Require Import Znumtheory.: [Loading ML file rocq-runtime.plugins.ring ... done] [Loading ML file rocq-runtime.plugins.zify ... done] [Loading ML file rocq-runtime.plugins.micromega_core ... done] [Loading ML file rocq-runtime.plugins.micromega ... done]
From Stdlib Require Import ZArith.: [Loading ML file rocq-runtime.plugins.btauto ... done] [Loading ML file rocq-runtime.plugins.nsatz_core ... done] [Loading ML file rocq-runtime.plugins.nsatz ... done]
From Stdlib Require Import ZNsatz.
Goal forall (x y z : Z), ( x + y + z = 0 -> x * y + x * z + y * z = 0 -> x * y * z = 0 -> x * x * x = 0)%Z.: 1 goal ============================ forall x y z : Z, x + y + z = 0 -> x * y + x * z + y * z = 0 -> x * y * z = 0 -> x * x * x = 0
Proof.
nsatz.: No more goals.
Qed.

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

Tactic ensatz with strategy := one_term?

Solves goals of the form

\[\exists Y_1, \ldots, Y_m \in A, P(\bar{X}) = Q(\bar{X}) + \sum_{i=1}^{m} Y_i * I_i(\bar{X})\]

given the premises $P_i(\bar{X}) = Q_i(\bar{X})$, which may be part of the goal or already in the hypotheses or a mix of both, $A$ an integral domain, i.e. a commutative ring with no zero divisors, $\bar{X} \in A^n$, and all $P$, $Q$ and $I$ are polynomials. 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.

For the strategy parameter, see the desciption for the nsatz tactic.

Example

From Stdlib Require Import Znumtheory.
From Stdlib Require Import ZArith.
From Stdlib Require Import ZNsatz.
From Stdlib Require Import ENsatzTactic.
Goal forall a b n j x y z : Z, a - j = x * n -> b - y = z * n -> exists k : Z, a * b - j * y = k * n.: 1 goal ============================ forall a b n j x y z : Z, a - j = x * n -> b - y = z * n -> exists k : Z, a * b - j * y = k * n
Proof.
ensatz.: No more goals.
Qed.

The tactic can also solve goals with existential variables.

Example

From Stdlib Require Import Znumtheory.
From Stdlib Require Import ZArith.
From Stdlib Require Import ZNsatz.
From Stdlib Require Import ENsatzTactic.
Goal forall a b n j x y z : Z, a - j = x * n -> b - y = z * n -> exists k : Z, a * b - j * y = k * n.: 1 goal ============================ forall a b n j x y z : Z, a - j = x * n -> b - y = z * n -> exists k : Z, a * b - j * y = k * n
Proof.
intros.: 1 goal a, b, n, j, x, y, z : Z H : a - j = x * n H0 : b - y = z * n ============================ exists k : Z, a * b - j * y = k * n
eexists.: 1 focused goal (shelved: 1) a, b, n, j, x, y, z : Z H : a - j = x * n H0 : b - y = z * n ============================ a * b - j * y = ?k * n
ensatz.: No more goals.
Qed.

See the file ENsatz.v and EENsatz.v for examples.

Tactic nsatz_compute one_term