1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
.. _nsatz_chapter:
Nsatz: a solver for 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``. 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
:tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
:math:`\mathbb{Q}` and any user-registered rings.
.. tacn:: nsatz {? with radicalmax := @one_term strategy := @one_term parameters := @one_term variables := @one_term }
This tactic is for solving 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_1, Q_1, \ldots, P_s, Q_s` are polynomials and :math:`A` is an integral
domain, i.e. a commutative ring with no zero divisors. 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 Leibniz 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.
`radicalmax`
bound when searching for r such that
:math:`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 :math:`X_1,\ldots,X_n` and the strategy
used in Buchberger algorithm (see :cite:`sugar` 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 :math:`X_{i_1},\ldots,X_{i_k}` among
:math:`X_1,\ldots,X_n`. Computation will be performed with
rational fractions in these parameters, i.e. polynomials have
coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient
:math:`c` can be a nonconstant 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`
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 <https://github.com/coq/coq/blob/master/test-suite/success/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 :math:`A` with no zero divisors
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 algebraically closed field: the method is
complete).
So, solving our initial problem reduces to 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`.
.. tacn:: nsatz_compute @one_term
:undocumented:
|
