unification des tactiques nsatz pour R Z avec celle des anneaux integres

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13343 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 49 insertions, 33 deletions

diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index be93d5dd74..794e461f07 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -1,42 +1,44 @@
-\achapter{Nsatz: tactics for proving equalities in $\mathbb{R}$ and $\mathbb{Z}$}
+\achapter{Nsatz: tactics for proving equalities in integral domains}
 \aauthor{Loïc Pottier}
 
 The tactic \texttt{nsatz} proves goals of the form
 
 \[ \begin{array}{l}
-  \forall X_1,\ldots,X_n \in \mathbb{R},\\
+  \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.
+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 \mathbb{R},\\
+  \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.
  
-The tactic \texttt{nsatzZ} proves the same goals where the $X_i$ are in $\mathbb{Z}$.
-
 \asection{Using the basic tactic \texttt{nsatz}}
 \tacindex{nsatz}
 
-If you work in $\mathbb{R}$, load the
-\texttt{NsatzR} module: \texttt{Require Import
-NsatzR}.\\
- and use the tactic \texttt{nsatz} or \texttt{nsatzR}.
-If you work in $\mathbb{Z}$ do the same thing {\em mutatis mutandis}.
+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 ring R (with no zero divisor) to algebraic computations: it is easy to see that if a polynomial
-$P$ in $R[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} S_i P_i$, with $c
-\in R$, $c \not = 0$, $r$ a positive integer, and the $S_i$s in
-$R[X_1,\ldots,X_n]$, then $P$ is zero whenever polynomials $P_1,...,P_s$  are
-zero (the converse is also true when R is an algebraic closed field:
+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$
@@ -47,17 +49,27 @@ 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 generic tactic
+\texttt{nsatz}, which uses the low-level tactic \texttt{nsatz\_domainpv}: \\
+\vspace*{3mm}
+\texttt{nsatz\_domainpv pretac rmax strategy lparam lvar simpltac domain}
+
+where:
 
-The \texttt{NsatzR} module defines the tactics
-\texttt{nsatz},  \texttt{nsatzRradical}, \texttt{nsatzRparameters}, and
-the generic tactic \texttt{nsatzRpv}, which are used as follows:
+\begin{itemize}
+    \item \texttt{pretac} is a tactic depending on the ring A; its goal is to
+make apparent the generic operations of a domain (ring\_eq, ring\_plus, etc),
+both in the goal and the hypotheses; it is executed first. By default it is \texttt{ltac:idtac}.
 
-  \begin{itemize}
-  \item \texttt{nsatzRpv rmax strategy lparam lvar}:
-    \begin{itemize}
-	\item \texttt{rmax} is a bound when for searching r s.t.$c (P-Q)^r =
+    \item \texttt{rmax} 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
+	
+    \item \texttt{strategy} gives the order on variables $X_1,...X_n$ and
 the strategy used in Buchberger algorithm (see
 \cite{sugar} for details): 
 
@@ -78,15 +90,19 @@ which states that $c$ is not zero.
 
 	\item \texttt{lvar} is the list of the variables
 in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{lvar} = {(@nil
-R)}, then \texttt{lvar} is replaced by all the variables which are not in lparam.
-     \end{itemize}
-  \item \texttt{nsatzRparameters lparam} is equivalent to 
-        \texttt{nsatzRpv 6\%N 1\%Z lparam (@nil R)}
-  \item \texttt{nsatzRradical rmax} is equivalent to 
-	\texttt{nsatzRpv rmax 1\%Z (@nil R) (@nil R)}
-  \item \texttt{nsatz} is equivalent to 
-	\texttt{nsatzRpv 6\%N 1\%Z (@nil R) (@nil R)}ls
-  \end{itemize}
+R)}, then \texttt{lvar} is replaced by all the variables which are not in
+lparam.
+
+    \item \texttt{simpltac} is a tactic depending on the ring A; its goal is to
+simplify goals and make apparent the generic operations of a domain after
+simplifications. By default it is \texttt{ltac:simpl}.
+
+ \item \texttt{domain} is the object of type Domain representing A, its
+operations and properties of integral domain.
+
+\end{itemize}
+
+See file \texttt{Nsatz.v} for examples.
 
 %%% Local Variables: 
 %%% mode: latex