\[\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.
    Toplevel input, characters 27-37: > From Stdlib Require Import Znumtheory. > ^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Znumtheory with prefix Stdlib.
  From Stdlib Require Import ZArith.
    Toplevel input, characters 27-33: > From Stdlib Require Import ZArith. > ^^^^^^ Error: Cannot find a physical path bound to logical path ZArith with prefix Stdlib.
  From Stdlib Require Import ZNsatz.
    Toplevel input, characters 27-33: > From Stdlib Require Import ZNsatz. > ^^^^^^ Error: Cannot find a physical path bound to logical path ZNsatz with prefix Stdlib.
  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.
    Toplevel input, characters 21-22: > 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. > ^ Error: The reference Z was not found in the current environment.
  Proof.
    Toplevel input, characters 0-6: > Proof. > ^^^^^^ Error: Command not supported (No proof-editing in progress).
  nsatz.
    Toplevel input, characters 0-5: > nsatz. > ^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
  Qed.
    Toplevel input, characters 0-4: > Qed. > ^^^^ Error: No focused proof (No proof-editing in progress).

  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.
    Toplevel input, characters 27-37: > From Stdlib Require Import Znumtheory. > ^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Znumtheory with prefix Stdlib.
  From Stdlib Require Import ZArith.
    Toplevel input, characters 27-33: > From Stdlib Require Import ZArith. > ^^^^^^ Error: Cannot find a physical path bound to logical path ZArith with prefix Stdlib.
  From Stdlib Require Import ZNsatz.
    Toplevel input, characters 27-33: > From Stdlib Require Import ZNsatz. > ^^^^^^ Error: Cannot find a physical path bound to logical path ZNsatz with prefix Stdlib.
  From Stdlib Require Import ENsatzTactic.
    Toplevel input, characters 27-39: > From Stdlib Require Import ENsatzTactic. > ^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path ENsatzTactic with prefix Stdlib.
  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.
    Toplevel input, characters 28-29: > 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. > ^ Error: The reference Z was not found in the current environment.
  Proof.
    Toplevel input, characters 0-6: > Proof. > ^^^^^^ Error: Command not supported (No proof-editing in progress).
  ensatz.
    Toplevel input, characters 0-6: > ensatz. > ^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
  Qed.
    Toplevel input, characters 0-4: > Qed. > ^^^^ Error: No focused proof (No proof-editing in progress).

  The tactic can also solve goals with existential variables.

  Example

  From Stdlib Require Import Znumtheory.
    Toplevel input, characters 27-37: > From Stdlib Require Import Znumtheory. > ^^^^^^^^^^ Error: Cannot find a physical path bound to logical path Znumtheory with prefix Stdlib.
  From Stdlib Require Import ZArith.
    Toplevel input, characters 27-33: > From Stdlib Require Import ZArith. > ^^^^^^ Error: Cannot find a physical path bound to logical path ZArith with prefix Stdlib.
  From Stdlib Require Import ZNsatz.
    Toplevel input, characters 27-33: > From Stdlib Require Import ZNsatz. > ^^^^^^ Error: Cannot find a physical path bound to logical path ZNsatz with prefix Stdlib.
  From Stdlib Require Import ENsatzTactic.
    Toplevel input, characters 27-39: > From Stdlib Require Import ENsatzTactic. > ^^^^^^^^^^^^ Error: Cannot find a physical path bound to logical path ENsatzTactic with prefix Stdlib.
  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.
    Toplevel input, characters 28-29: > 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. > ^ Error: The reference Z was not found in the current environment.
  Proof.
    Toplevel input, characters 0-6: > Proof. > ^^^^^^ Error: Command not supported (No proof-editing in progress).
  intros.
    Toplevel input, characters 0-6: > intros. > ^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
  eexists.
    Toplevel input, characters 0-7: > eexists. > ^^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
  ensatz.
    Toplevel input, characters 0-6: > ensatz. > ^^^^^^ Error: Syntax error: illegal begin of toplevel:vernac_toplevel.
  Qed.
    Toplevel input, characters 0-4: > Qed. > ^^^^ Error: No focused proof (No proof-editing in progress).

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

Tactic nsatz_compute one_term

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF