diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-22 15:09:00 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-29 17:44:31 +0200 |
commit | 729c4847ef3736829727948cd2c542149432970d (patch) | |
tree | 0c75cf6190b23131c9d10e9e4e1ee217a0ffeff6 /doc/sphinx/addendum | |
parent | f84eda17d1e1d15248bab4fb41941b2d6da77ddb (diff) |
[Sphinx] Move chapter 26 to new infrastructure
Diffstat (limited to 'doc/sphinx/addendum')
-rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst new file mode 100644 index 000000000..1401af10f --- /dev/null +++ b/doc/sphinx/addendum/nsatz.rst @@ -0,0 +1,102 @@ +\achapter{Nsatz: tactics for proving equalities in integral domains} +%HEVEA\cutname{nsatz.html} +\aauthor{Loïc Pottier} + +The tactic \texttt{nsatz} proves 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 divisor. For example, A can be +$\mathbb{R}$, $\mathbb{Z}$, of $\mathbb{Q}$. Note that the equality $=$ used in these +goals can be any setoid equality +(see \ref{setoidtactics}) +, not only Leibnitz 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. + +\asection{Using the basic tactic \texttt{nsatz}} +\tacindex{nsatz} + +Load the +\texttt{Nsatz} module: \texttt{Require Import Nsatz}.\\ + and use the tactic \texttt{nsatz}. + +\asection{More about \texttt{nsatz}} + +Hilbert's Nullstellensatz theorem shows how to reduce proofs of equalities on +polynomials on a commutative ring A with no zero divisor 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,...,P_s$ are +zero (the converse is also true when A is an algebraic closed field: +the method is complete). + +So, proving our initial problem can reduce into 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 \texttt{ring}. + +This is achieved by the computation of a Groebner 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 {\em reification}, which is +performed using {\em Type Classes} +(see \ref{typeclasses}) +. + +The \texttt{Nsatz} module defines the tactic +\texttt{nsatz}, which can be used without arguments: \\ +\vspace*{3mm} +\texttt{nsatz}\\ +or with the syntax: \\ +\vspace*{3mm} +\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\ +where: + +\begin{itemize} + \item \texttt{radicalmax} is a bound when for searching r s.t.$c (P-Q)^r = +\sum_{i=1..s} S_i (P_i - Q_i)$ + + \item \texttt{strategy} gives the order on variables $X_1,...X_n$ and +the strategy used in Buchberger algorithm (see +\cite{sugar} for details): + + \begin{itemize} + \item strategy = 0: reverse lexicographic order and newest s-polynomial. + \item strategy = 1: reverse lexicographic order and sugar strategy. + \item strategy = 2: pure lexicographic order and newest s-polynomial. + \item strategy = 3: pure lexicographic order and sugar strategy. + \end{itemize} + + \item \texttt{parameters} is the list of variables +$X_{i_1},\ldots,X_{i_k}$ among $X_1,...,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 +$R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non +constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal +which states that $c$ is not zero. + + \item \texttt{variables} is the list of the variables +in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil +R)}, then \texttt{lvar} is replaced by all the variables which are not in +parameters. + +\end{itemize} + +See file \texttt{Nsatz.v} for many examples, specially in geometry. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |