doc du nouveau ring

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

2 files changed, 403 insertions, 251 deletions

diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 70889c9d45..49616ff69d 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -1,10 +1,13 @@
 \achapter{The \texttt{ring} tactic}
-\aauthor{Patrick Loiseleur and Samuel Boutin}
+\aauthor{Bruno Barras, Benjamin Gr\'egoire and Assia
+  Mahboubi\footnote{based on previous work from
+  Patrick Loiseleur and Samuel Boutin}}
 \label{ring}
 \tacindex{ring}
 
 This chapter presents  the \texttt{ring} tactic.
 
+
 \asection{What does this tactic?}
 
 \texttt{ring} does associative-commutative rewriting in ring and semi-ring
@@ -14,20 +17,21 @@ $\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and
 $\otimes$. A \textit{polynomial} is an expression built on variables $V_0, V_1,
 \dots$ and constants by application of $\oplus$ and $\otimes$.
 
-Let an {\it ordered product} be a product of variables $V_{i_1} \otimes
-\ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le i_n$. Let a
-\textit{monomial} be the product of a constant (possibly equal to 1, in
-which case we omit it) and an ordered product.  We can order the
-monomials by the lexicographic order on products of variables. Let a
-\textit{canonical sum} be an ordered sum of monomials that are all
-different, i.e. each monomial in the sum is strictly less than the
-following monomial according to the lexicographic order. It is an easy
-theorem to show that every polynomial is equivalent (modulo the ring
-properties) to exactly one canonical sum. This canonical sum is called
-the \textit{normal form} of the polynomial. So what does \texttt{ring}? It
-normalizes polynomials over any ring or semi-ring structure. The basic
-use of \texttt{ring} is to simplify ring expressions, so that the user
-does not have to deal manually with the theorems of associativity and
+Let an {\it ordered product} be a product of variables $V_{i_1}
+\otimes \ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le
+i_n$. Let a \textit{monomial} be the product of a constant and an
+ordered product.  We can order the monomials by the lexicographic
+order on products of variables. Let a \textit{canonical sum} be an
+ordered sum of monomials that are all different, i.e. each monomial in
+the sum is strictly less than the following monomial according to the
+lexicographic order. It is an easy theorem to show that every
+polynomial is equivalent (modulo the ring properties) to exactly one
+canonical sum. This canonical sum is called the \textit{normal form}
+of the polynomial. In fact, the actual representation shares monomials
+with same prefixes. So what does \texttt{ring}? It normalizes
+polynomials over any ring or semi-ring structure. The basic use of
+\texttt{ring} is to simplify ring expressions, so that the user does
+not have to deal manually with the theorems of associativity and
 commutativity.
 
 \begin{Examples}
@@ -90,64 +94,339 @@ this paragraph and use the tactic according to your intuition.
 
 \asection{Concrete usage in \Coq}
 
-Under a session launched by \texttt{coqtop} or \texttt{coqtop -full},
-load the \texttt{ring} files with the command:
+The {\tt ring} tactic solves equations upon polynomial expressions of
+a ring (or semi-ring) structure. It proceeds by normalizing both hand
+sides of the equation (w.r.t. associativity, commutativity and
+distributivity, constant propagation) and comparing syntactically the
+results.
+
+{\tt ring\_simplify} applies the normalization procedure described
+above to the terms given. The tactic then replaces all occurrences of
+the terms given in the conclusion of the goal by their normal
+forms. If no term is given, then the conclusion should be an equation
+and both hand sides are normalized.
+
+The tactic must be loaded by \texttt{Require Import Ring}. The ring
+structures must be declared with the \texttt{Add Ring} command (see
+below). The ring of booleans is predefined; if one wants to use the
+tactic on \texttt{nat} one must first require the module
+\texttt{NewArithRing}; for \texttt{Z}, do \texttt{Require Import
+NewZArithRing}; for \texttt{N}, do \texttt{Require Import
+NewNArithRing}.
+
+\Example
+\begin{coq_eval}
+Reset Initial.
+Require Import ZArith.
+Open Scope Z_scope.
+\end{coq_eval}
+\begin{coq_example}
+Require Import NewZArithRing.
+Goal forall a b c:Z,
+  (a + b + c) * (a + b + c) =
+  a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
+\end{coq_example}
+\begin{coq_example}
+intros; ring.
+\end{coq_example}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
 
-\begin{quotation}
+\Warning \texttt{ring\_simplify $term_1$; ring\_simplify $term_2$} is
+not equivalent to \texttt{ring\_simplify $term_1$ $term_2$}. In the
+latter case the variables map is shared between the two terms, and
+common subterm $t$ of $term_1$ and $term_2$ will have the same
+associated variable number. So the first alternative should be
+avoided for terms belonging to the same ring theory.
+
+\begin{ErrMsgs}
+\item \errindex{not a valid ring equation}
+  The conclusion of the goal is not provable in the corresponding ring
+  theory.
+\item \errindex{arguments of ring\_simplify do not have all the same type}
+  {\tt ring\_simplify} cannot simplify terms of several rings at the
+  same time. Invoke the tactic once per ring structure.
+\item \errindex{cannot find a declared ring structure over {\tt term}}
+  No ring has been declared for the type of the terms to be
+  simplified. Use {\tt Add Ring} first.
+\item \errindex{cannot find a declared ring structure for equality
+  {\tt term}}
+  Same as above is the case of the {\tt ring} tactic.
+\end{ErrMsgs}
+
+\asection{Adding a ring structure}
+
+Declaring a new ring consists in proving that a ring signature (a
+carrier set, an equality, and ring operations: {\tt
+Ring\_th.ring\_theory} and {\tt Ring\_th.semi\_ring\_theory})
+satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are
+also supported. The equality can be either Leibniz equality, or any
+relation declared as a setoid (see~\ref{setoidtactics}). The definition
+of ring and semi-rings (see module {\tt Ring\_th}) is:
 \begin{verbatim}
-Require Ring.
+ Record ring_theory : Prop := mk_rt {
+    Radd_0_l    : forall x, 0 + x == x;
+    Radd_sym    : forall x y, x + y == y + x;
+    Radd_assoc  : forall x y z, x + (y + z) == (x + y) + z;
+    Rmul_1_l    : forall x, 1 * x == x;
+    Rmul_sym    : forall x y, x * y == y * x;
+    Rmul_assoc  : forall x y z, x * (y * z) == (x * y) * z;
+    Rdistr_l    : forall x y z, (x + y) * z == (x * z) + (y * z);
+    Rsub_def    : forall x y, x - y == x + -y;
+    Ropp_def    : forall x, x + (- x) == 0
+ }.
+
+Record semi_ring_theory : Prop := mk_srt {
+    SRadd_0_l   : forall n, 0 + n == n;
+    SRadd_sym   : forall n m, n + m == m + n ;
+    SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
+    SRmul_1_l   : forall n, 1*n == n;
+    SRmul_0_l   : forall n, 0*n == 0; 
+    SRmul_sym   : forall n m, n*m == m*n;
+    SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
+    SRdistr_l   : forall n m p, (n + m)*p == n*p + m*p
+  }.
 \end{verbatim}
-\end{quotation}
 
-It does not work under \texttt{coqtop -opt} because the compiled ML
-objects used by the tactic are not linked in this binary image, and
-dynamic loading of native code is not possible in \ocaml.
+This implementation of {\tt ring} also features a notion of constant
+that can be parameterized. This can be used to improve the handling of
+closed expressions when operations are effective. It consists in
+introducing a type of \emph{coefficients} and an implementation of the
+ring operations, and a morphism from the coefficient type to the ring
+carrier type. The morphism need not be injective, nor surjective.  As
+an example, one can consider the real numbers. The set of coefficients
+could be the rational numbers, upon which the ring operations can be
+implemented. The fact that there exists a morphism is defined by the
+following properties:
+\begin{verbatim}
+ Record ring_morph : Prop := mkmorph {
+    morph0    : [cO] == 0;
+    morph1    : [cI] == 1;
+    morph_add : forall x y, [x +! y] == [x]+[y];
+    morph_sub : forall x y, [x -! y] == [x]-[y];
+    morph_mul : forall x y, [x *! y] == [x]*[y];
+    morph_opp : forall x, [-!x] == -[x];
+    morph_eq  : forall x y, x?=!y = true -> [x] == [y] 
+  }.
+
+ Record semi_morph : Prop := mkRmorph {
+    Smorph0 : [cO] == 0;
+    Smorph1 : [cI] == 1;
+    Smorph_add : forall x y, [x +! y] == [x]+[y];
+    Smorph_mul : forall x y, [x *! y] == [x]*[y];
+    Smorph_eq  : forall x y, x?=!y = true -> [x] == [y] 
+  }.
+\end{verbatim}
+where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set,
+{\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring
+operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is
+an implementation of this equality, and {\tt [x]} is a notation for
+the image of {\tt x} by the ring morphism.
+
+Since {\tt Z} is an initial ring (and {\tt N} is an initial
+semi-ring), it can always be considered as a set of
+coefficients. There are basically three kinds of (semi-)rings:
+\begin{description}
+\item[abstract rings] to be used when operations are not
+  effective. The set of coefficients is {\tt Z} (or {\tt N} for
+  semi-rings).
+\item[computational rings] to be used when operations are
+  effective. The set of coefficients is the ring itself. The user only
+  has to provide an implementation for the equality.
+\item[customized ring] for other cases. The user has to provide the
+  coefficient set and the morphism.
+\end{description}
+
+The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$
+($mod_1$,\dots,$mod_2$)}.  The name is not relevent. It is just used
+for error messages. $ring$ is a proof that the ring signature
+satisfies the (semi-)ring axioms. The optional list of modifiers is
+used to tailor the behaviour of the tactic. The following list
+describes their syntax and effects:
+\begin{description}
+\item[abstract] declares the ring as abstract. This is the default.
+\item[decidable \term] declares the ring as computational. \term{} is
+  the correctness proof of an equality test {\tt ?=!}. Its type should be of
+  the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}.
+\item[morphism \term] declares the ring as a customized one. \term{} is
+  a proof that there exists a morphism between a set of coefficient
+  and the ring carrier (see {\tt Ring\_th.ring\_morph} and {\tt
+  Ring\_th.semi\_morph}).
+\item[setoid \term$_1$ \term$_2$] forces the use of given
+  setoid. \term$_1$ is a proof that the equality is indeed a setoid
+  (see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the
+  ring operations are morphisms (see {\tt Ring\_th.ring\_eq\_ext} and
+  {\tt Ring\_th.sring\_eq\_ext}). This modifier need not be used if the
+  setoid and morphisms have been declared.
+\item[constants [\ltac]] specifies a tactic expression that, given a term,
+  returns either an object of the coefficient set that is mapped to
+  the expression via the morphism, or returns {\tt
+  Ring\_tac.NotConstant}. Abstract (semi-)rings need not define this.
+\item[preprocess [\ltac]]
+  specifies a tactic that is applied as a preliminary step for {\tt
+  ring} and {\tt ring\_simplify}. It can be used to transform a goal
+  so that it is better recognized. For instance, {\tt S n} can be
+  changed to {\tt plus 1 n}.
+\item[postprocess [\ltac]] specifies a tactic that is applied as a final step
+  for {\tt ring\_simplify}. For instance, it can be used to undo
+  modifications of the preprocessor.
+\end{description}
 
-In order to use \texttt{ring} on naturals, load \texttt{ArithRing}
-instead; for binary integers, load the module \texttt{ZArithRing}.
 
-Then, to normalize the terms $term_1$, \dots, $term_n$ in
-the current subgoal, use the tactic:
+\begin{ErrMsgs}
+\item \errindex{bad ring structure}
+  The proof of the ring structure provided is not of the expected type.
+\item \errindex{bad lemma for decidability of equality}
+  The equality function provided in the case of a computational ring
+  has not the expected type.
+\item \errindex{ring {\it operation} should be declared as a morphism}
+  A setoid associated to the carrier of the ring structure as been
+  found, but the ring operation should be declared as
+  morphism. See~\ref{setoidtactics}.
+\end{ErrMsgs}
 
-\begin{quotation}
-\texttt{ring} $term_1$ \dots{} $term_n$
-\end{quotation}
-\tacindex{ring}
+\asection{How does it work?}
 
-Then the tactic guesses the type of given terms, the ring theory to
-use, the variables map, and replace each term with its normal form.
-The variables map is common to all terms
+The code of \texttt{ring} is a good example of tactic written using
+\textit{reflection}.  What is reflection? Basically, it is writing
+\Coq{} tactics in \Coq, rather than in \ocaml. From the philosophical
+point of view, it is using the ability of the Calculus of
+Constructions to speak and reason about itself.  For the \texttt{ring}
+tactic we used \Coq\ as a programming language and also as a proof
+environment to build a tactic and to prove it correctness.
 
-\Warning \texttt{ring $term_1$; ring $term_2$} is not equivalent to 
-\texttt{ring $term_1$ $term_2$}. In the latter case the variables map
-is shared between the two terms, and common subterm $t$ of $term_1$
-and $term_2$ will have the same associated variable number.
+The interested reader is strongly advised to have a look at the file
+\texttt{Pol.v}. Here a type for polynomials is defined: 
 
-\begin{ErrMsgs}
-\item \errindex{All terms must have the same type}
-\item \errindex{Don't know what to do with this goal}
-\item \errindex{No Declared Ring Theory for \term.}
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+Inductive PExpr : Type :=
+  | PEc : C -> PExpr
+  | PEX : positive -> PExpr
+  | PEadd : PExpr -> PExpr -> PExpr
+  | PEsub : PExpr -> PExpr -> PExpr
+  | PEmul : PExpr -> PExpr -> PExpr
+  | PEopp : PExpr -> PExpr.
+\end{verbatim}
+\end{flushleft}
+\end{small}
 
-  \texttt{Use Add [Semi] Ring to declare it}
+Polynomials in normal form are defined as:
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+ Inductive Pol : Type :=
+  | Pc : C -> Pol 
+  | Pinj : positive -> Pol -> Pol                   
+  | PX : Pol -> positive -> Pol -> Pol.
+\end{verbatim}
+\end{flushleft}
+\end{small}
+where {\tt Pinj n P} denotes $P$ in which $V_i$ is replaced by
+$V_{i+n}$, and {\tt PX P n Q} denotes $P \otimes V_1^{n} \oplus Q'$,
+$Q'$ being $Q$ where $V_i$ is replaced by $V_{i+1}$. 
 
-  That happens when all terms have the same type \term, but there is
-  no declared ring theory for this set. See below.
-\end{ErrMsgs}
 
-\begin{Variants}
-\item \texttt{ring}
+Variables maps are represented by list of ring elements, and two
+interpretation functions, one that maps a variables map and a
+polynomial to an element of the concrete ring, and the second one that
+does the same for normal forms:
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+Definition PEeval : list R -> PExpr -> R := [...].
+Definition Pphi_dev : list R -> Pol -> R := [...].
+\end{verbatim}
+\end{flushleft}
+\end{small}
+
+A function to normalize polynomials is defined, and the big theorem is
+its correctness w.r.t interpretation, that is:
+
+\begin{small}
+\begin{flushleft}
+\begin{verbatim}
+Definition norm : PExpr -> Pol := [...].
+Lemma Pphi_dev_ok :
+   forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
+\end{verbatim}
+\end{flushleft}
+\end{small}
+
+So now, what is the scheme for a normalization proof? Let \texttt{p}
+be the polynomial expression that the user wants to normalize. First a
+little piece of ML code guesses the type of \texttt{p}, the ring
+theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
+variables map \texttt{v} such that \texttt{p} is
+$\beta\delta\iota$-equivalent to \verb|(PEeval v ap)|. Then we
+replace it by \verb|(Pphi_dev v (norm ap))|, using the
+main correctness theorem and we reduce it to a concrete expression
+\texttt{p'}, which is the concrete normal form of
+\texttt{p}. This is summarized in this diagram:
+\begin{center}
+\begin{tabular}{rcl}
+\texttt{p} & $\rightarrow_{\beta\delta\iota}$  
+   & \texttt{(PEeval v ap)} \\
+ & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
+\texttt{p'} 
+   & $\leftarrow_{\beta\delta\iota}$ 
+   & \texttt{(Pphi\_dev v (norm ap))}
+\end{tabular}
+\end{center}
+The user do not see the right part of the diagram. 
+From outside, the tactic behaves like a
+$\beta\delta\iota$ simplification extended with AC rewriting rules.
+Basically, the proof is only the application of the main
+correctness theorem to well-chosen arguments.
+
+
+\asection{Legacy implementation}
 
-  That works if the current goal is an equality between two
-  polynomials. It will normalize both sides of the
-  equality, solve it if the normal forms are equal and in other cases
-  try to simplify the equality using \texttt{congr\_eqT} and \texttt{refl\_equal}
-  to reduce $x + y = x + z$ to $y = z$ and $x * z = x * y$ to $y = z$.
+\Warning This tactic is the {\tt ring} tactic of previous versions of
+\Coq{} and it should be considered as deprecated. It will probably be
+removed in future releases. It has been kept only for compatibility
+reasons and in order to help moving existing code to the newer
+implementation described above. For more details, please refer to the
+Coq Reference Manual, version 8.0.
 
-  \ErrMsg\errindex{This goal is not an equality}
+
+\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$
+\tacindex{legacy ring}
+\comindex{Add Legacy Ring}
+\comindex{Add Legacy Semi Ring}}
+
+This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
+associative commutative rewriting on every ring.  The tactic must be
+loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
+the \texttt{Add Ring} command. The ring of booleans
+is predefined; if one wants to use the tactic on \texttt{nat} one must
+first require the module \texttt{ArithRing}; for \texttt{Z}, do
+\texttt{Require Import ZArithRing}; for \texttt{N}, do \texttt{Require
+Import NArithRing}.
+
+The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
+conclusion. The tactic \texttt{ring} normalizes these terms
+w.r.t. associativity and commutativity and replace them by their
+normal form.
+
+\begin{Variants}
+\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it
+  acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then
+  solves the equality by reflexivity.
+
+\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
+    S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
+  proof that \texttt{forall (n:nat), S n = plus (S O) n}.
 
 \end{Variants}
 
-\asection{Add a ring structure}
+You can have a look at the files \texttt{LegacyRing.v},
+\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
+\texttt{Add Ring} command.
+
+\subsection{Add a ring structure}
 
 It can be done in the \Coq toplevel (No ML file to edit and to link
 with \Coq). First, \texttt{ring} can handle two kinds of structure:
@@ -242,9 +521,9 @@ constructor.
 
 Finally to register a ring the syntax is:
 
-\comindex{Add Ring}
+\comindex{Add Legacy Ring}
 \begin{quotation}
-  \texttt{Add Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
+  \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
   \texttt{[} \textit{c1 \dots cn} \texttt{].}
 \end{quotation}
 
@@ -267,8 +546,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
 \texttt{(S (S O))}, \ldots
 
 \begin{Variants}
-\item \texttt{Add Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} 
-  \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Semi
+\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} 
+  \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi
     Ring}
   
   There are two differences with the \texttt{Add Ring} command: there
@@ -276,8 +555,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
   \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero
     Aeq}\texttt{)}.
 
-\item \texttt{Add Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv 
-    Aeq T}\texttt{.}\comindex{Add Abstract Ring}
+\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv 
+    Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring}
   
   This command should be used for when the operations of rings are not
   computable; for example the real numbers of
@@ -286,8 +565,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
   axioms. The argument \texttt{Aeq} is not used; a good choice for
   that function is \verb+[x:A]false+.
 
-\item \texttt{Add Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
-    Aeq T}\texttt{.}\comindex{Add Abstract Semi Ring}
+\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
+    Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring}
 
 \end{Variants}
 
@@ -318,90 +597,6 @@ booleans.
 load the module \texttt{ArithRing}, and for \texttt{Z},
 load the module \texttt{ZArithRing}.
 
-
-\asection{How does it work?}
-
-The code of \texttt{ring} is a good example of tactic written using
-\textit{reflection} (or \textit{internalization}, it is synonymous).
-What is reflection? Basically, it is writing \Coq{} tactics in \Coq,
-rather than in \ocaml. From the philosophical point of view, it is
-using the ability of the Calculus of Constructions to speak and reason
-about itself.  For the \texttt{ring} tactic we used \Coq\ as a
-programming language and also as a proof environment to build a tactic
-and to prove it correctness.
-
-The interested reader is strongly advised to have a look at the file
-\texttt{Ring\_normalize.v}. Here a type for polynomials is defined: 
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Inductive Type polynomial := 
-  Pvar : idx -> polynomial
-| Pconst : A -> polynomial
-| Pplus : polynomial -> polynomial -> polynomial
-| Pmult : polynomial -> polynomial -> polynomial
-| Popp : polynomial -> polynomial.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-There is also a type to represent variables maps, and an
-interpretation function, that maps a variables map and a polynomial to an
-element of the concrete ring:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Definition polynomial_simplify := [...]
-Definition interp : (varmap A) -> (polynomial A) -> A := [...]
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-A function to normalize polynomials is defined, and the big theorem is
-its correctness w.r.t interpretation, that is:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Theorem polynomial_simplify_correct : forall (v:(varmap A))(p:polynomial)
-  (interp v (polynomial_simplify p))
-  =(interp v p).
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-(The actual code is slightly more complex: for efficiency,
-there is a special datatype to represent normalized polynomials,
-i.e. ``canonical sums''. But the idea is still the same).
-
-So now, what is the scheme for a normalization proof? Let \texttt{p}
-be the polynomial expression that the user wants to normalize. First a
-little piece of ML code guesses the type of \texttt{p}, the ring
-theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
-variables map \texttt{v} such that \texttt{p} is
-$\beta\delta\iota$-equivalent to \verb|(interp v ap)|. Then we
-replace it by \verb|(interp v (polynomial_simplify ap))|, using the
-main correctness theorem and we reduce it to a concrete expression
-\texttt{p'}, which is the concrete normal form of
-\texttt{p}. This is summarized in this diagram:
-\begin{center}
-\begin{tabular}{rcl}
-\texttt{p} & $\rightarrow_{\beta\delta\iota}$  
-   & \texttt{(interp v ap)} \\
- & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
-\texttt{p'} 
-   & $\leftarrow_{\beta\delta\iota}$ 
-   & \texttt{(interp v (polynomial\_simplify ap))}
-\end{tabular}
-\end{center}
-The user do not see the right part of the diagram. 
-From outside, the tactic behaves like a
-$\beta\delta\iota$ simplification extended with AC rewriting rules.
-Basically, the proof is only the application of the main
-correctness theorem to well-chosen arguments.
-
 \asection{History of \texttt{ring}}
 
 First Samuel Boutin designed the tactic \texttt{ACDSimpl}. 
@@ -463,40 +658,26 @@ The tactic \texttt{ring} is not only faster than a classical one:
 using reflection, we get for free integration of computation and
 reasoning that would be very complex to implement in the classic fashion.
 
-Is it the ultimate way to write tactics? 
-The answer is: yes and no. The \texttt{ring} tactic
-uses intensively the conversion
-rule of \CIC, that is replaces proof by computation the most as it is
+Is it the ultimate way to write tactics?  The answer is: yes and
+no. The \texttt{ring} tactic uses intensively the conversion rule of
+\CIC, that is replaces proof by computation the most as it is
 possible. It can be useful in all situations where a classical tactic
-generates huge proof terms. Symbolic Processing and Tautologies are
-in that case. But there are also tactics like \texttt{Auto} or
-\texttt{Linear}: that do many complex computations, using side-effects
-and backtracking, and generate
- a small proof term. Clearly, it would be a non-sense to
-replace them by tactics using reflection.
-
-Another argument against the reflection is that \Coq, as a
-programming language, has many nice features, like dependent types, 
-but is very far from the
-speed and the expressive power of \ocaml. Wait a minute! With \Coq\
-it is possible to extract ML code from \CIC\ terms, right? So, why not
-to link the extracted code with \Coq\ to inherit the benefits of the
-reflection and the speed of ML tactics? That is called \textit{total
-  reflection}, and is still an active research subject. With these
-technologies it will become possible to bootstrap the type-checker of
-\CIC, but there is still some work to achieve that goal.
-
-Another brilliant idea from Benjamin Werner: reflection could be used
-to couple a external tool (a rewriting program or a model checker)
-with \Coq. We define (in \Coq) a type of terms, a type of
-\emph{traces}, and prove a correction theorem that states that
-\emph{replaying traces} is safe w.r.t some interpretation. Then we let 
-the external tool do every computation (using side-effects,
-backtracking, exception, or others features that are not available in
-pure lambda calculus) to produce the trace: now we replay the trace in
-Coq{}, and apply the correction lemma. So internalization seems to be
-the best way to import \dots{} external proofs!
-
+generates huge proof terms. Symbolic Processing and Tautologies are in
+that case. But there are also tactics like \texttt{auto} or
+\texttt{linear} that do many complex computations, using side-effects
+and backtracking, and generate a small proof term. Clearly, it would
+be significantly less efficient to replace them by tactics using
+reflection.
+
+Another idea suggested by Benjamin Werner: reflection could be used to
+couple a external tool (a rewriting program or a model checker) with
+\Coq. We define (in \Coq) a type of terms, a type of \emph{traces},
+and prove a correction theorem that states that \emph{replaying
+traces} is safe w.r.t some interpretation. Then we let the external
+tool do every computation (using side-effects, backtracking,
+exception, or others features that are not available in pure lambda
+calculus) to produce the trace: now we can check in Coq{} that the
+trace has the expected semantic by applying the correction lemma.
  
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2aa0b5b65a..85499fe100 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -756,7 +756,8 @@ performs the conversion in hypotheses $H_1\ldots H_n$.
 \dots\ \flag$_n$} and {\tt compute}
 \tacindex{cbv}
 \tacindex{lazy}
-\tacindex{compute}}
+\tacindex{compute}
+\tacindex{vm\_compute}}
 \label{vmcompute}
 
 These parameterized reduction tactics apply to any goal and perform
@@ -2675,70 +2676,29 @@ integers. This tactic must be loaded by the command \texttt{Require Import
   Omega}. See the additional documentation about \texttt{omega}
 (chapter~\ref{OmegaChapter}).
 
-\subsection{\tt ring \term$_1$ \dots\ \term$_n$
+\subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$}
 \tacindex{ring}
-\comindex{Add Ring}
-\comindex{Add Semi Ring}}
-
-This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
-associative commutative rewriting on every ring.  The tactic must be
-loaded by \texttt{Require Import Ring}. The ring must be declared in
-the \texttt{Add Ring} command (see \ref{ring}). The ring of booleans
-is predefined; if one wants to use the tactic on \texttt{nat} one must
-first require the module \texttt{ArithRing}; for \texttt{Z}, do
-\texttt{Require Import ZArithRing}; for \texttt{N}, do \texttt{Require
-Import NArithRing}.
-
-The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
-conclusion. The tactic \texttt{ring} normalizes these terms
-w.r.t. associativity and commutativity and replace them by their
-normal form.
+\tacindex{ring\_simplify}
+\comindex{Add Ring}}
 
-\begin{Variants}
-\item \texttt{ring} When the goal is an equality $t_1=t_2$, it
-  acts like \texttt{ring} $t_1$ $t_2$ and then simplifies or solves
-  the equality.
+The {\tt ring} tactic solves equations upon polynomial expressions of
+a ring (or semi-ring) structure. It proceeds by normalizing both hand
+sides of the equation (w.r.t. associativity, commutativity and
+distributivity, constant propagation) and comparing syntactically the
+results.
 
-\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
-    S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
-  proof that \texttt{forall (n:nat), S n = plus (S O) n}.
+{\tt ring\_simplify} applies the normalization procedure described
+above to the terms given. The tactic then replaces all occurrences of
+the terms given in the conclusion of the goal by their normal
+forms. If no term is given, then the conclusion should be an equation
+and both hand sides are normalized.
 
-\end{Variants}
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-Require Import ZArith.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example}
-Require Import ZArithRing.
-Goal forall a b c:Z,
-  (a + b + c) * (a + b + c) =
-  a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
-\end{coq_example}
-\begin{coq_example}
-intros; ring.
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-You can have a look at the files \texttt{Ring.v},
-\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
-\texttt{Add Ring} command.
-
-\SeeAlso Chapter~\ref{ring} for more detailed explanations about this tactic.
+See chapter~\ref{ring} for more information on the tactic and how to
+declare new ring structures.
 
 \subsection{\tt field
-\tacindex{field}}
-
-This tactic written by David~Delahaye and Micaela~Mayero solves equalities
-using commutative field theory. Denominators have to be non equal to zero and,
-as this is not decidable in general, this tactic may generate side conditions
-requiring some expressions to be non equal to zero. This tactic must be loaded
-by {\tt Require Import Field}. Field theories are declared (as for {\tt ring}) with
-the {\tt Add Field} command.
+\tacindex{field}
+\comindex{Add Field}}
 
 \Example
 \begin{coq_example*}
@@ -2750,20 +2710,35 @@ Goal forall x y:R,
 \end{coq_example*}
 
 \begin{coq_example}
-intros; field.
+intros; legacy field.
 \end{coq_example}
 
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 
-\subsection{\tt Add Field
-\comindex{Add Field}}
+\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\
+\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
+field}.
+
+\subsection{\tt legacy field
+\tacindex{legacy field}}
+
+This tactic written by David~Delahaye and Micaela~Mayero solves equalities
+using commutative field theory. Denominators have to be non equal to zero and,
+as this is not decidable in general, this tactic may generate side conditions
+requiring some expressions to be non equal to zero. This tactic must be loaded
+by {\tt Require Import LegacyField}. Field theories are declared (as for
+{\tt legacy ring}) with
+the {\tt Add Legacy Field} command.
+
+\subsection{\tt Add Legacy Field
+\comindex{Add Legacy Field}}
 
 This vernacular command adds a commutative field theory to the database for the
 tactic {\tt field}. You must provide this theory as follows:
 \begin{flushleft}
-{\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
+{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
 Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
 \end{flushleft}
 where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
@@ -2786,28 +2761,24 @@ Require Import Ring} if you want to call the {\tt ring} tactic.
 
 \begin{Variants}
 
-\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
+\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
 {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
 {\tt \phantom{Add Field }with minus:={\it Aminus}}
 
 Adds also the term {\it Aminus} which must be a constant expressed by
 means of {\it Aopp}.
 
-\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
+\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
 {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Field }with div:={\it Adiv}}
+{\tt \phantom{Add Legacy Field }with div:={\it Adiv}}
 
 Adds also the term {\it Adiv} which must be a constant expressed by
 means of {\it Ainv}.
 
 \end{Variants}
 
-\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\
-\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
-field}.
-
 \SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
-field}.
+legacy field}.
 
 \subsection{\tt fourier
 \tacindex{fourier}}