From 8f4d4c66134804bbf2d2fe65c893b68387272d31 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 10 Jul 2010 15:57:24 +0100 Subject: Remove non-DFSG contents --- doc/refman/Nsatz.tex | 110 --------------------------------------------------- 1 file changed, 110 deletions(-) delete mode 100644 doc/refman/Nsatz.tex (limited to 'doc/refman/Nsatz.tex') diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex deleted file mode 100644 index 794e461f..00000000 --- a/doc/refman/Nsatz.tex +++ /dev/null @@ -1,110 +0,0 @@ -\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 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 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: - -\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}. - - \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 -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{lparam} 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{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. - - \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 -%%% TeX-master: "Reference-Manual" -%%% End: -- cgit v1.2.3