[Sphinx] Add chapter 25

Thanks to Laurent Théry for porting this chapter.

2 files changed, 730 insertions, 695 deletions

diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index d9b8b8c52..b861892cb 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -1,736 +1,770 @@
-\achapter{The \texttt{ring} and \texttt{field} tactic families}
-%HEVEA\cutname{ring.html}
-\aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia
-  Mahboubi, Laurent Th\'ery\footnote{based on previous work from
-  Patrick Loiseleur and Samuel Boutin}}
-\label{ring}
-\tacindex{ring}
+.. include:: ../replaces.rst
+.. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}`
+.. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}`
+.. |eq| replace:: `=`:sub:`(by the main correctness theorem)`
+.. |re| replace:: ``(PEeval`` `v` `ap`\ ``)``
+.. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))``
+
+
+.. _theringandfieldtacticfamilies:
+
+The ring and field tactic families
+====================================
+
+:Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_
 
 This chapter presents the tactics dedicated to deal with ring and
 field equations.
 
-\asection{What does this tactic do?}
-
-\texttt{ring} does associative-commutative rewriting in ring and semi-ring
-structures. Assume you have two binary functions $\oplus$ and $\otimes$
-that are associative and commutative, with $\oplus$ distributive on
-$\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 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}
-\item In the ring of integers, the normal form of 
-$x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$.
-\end{Examples}
-
-\texttt{ring} is also able to compute a normal form modulo monomial 
-equalities. For example, under the hypothesis that $2x^2 = yz+1$,
- the normal form of $2(x + 1)x - x - zy$ is $x+1$.
-
-\asection{The variables map}
-
-It is frequent to have an expression built with + and
-  $\times$, but rarely on variables only.
-Let us associate a number to each subterm of a ring
-expression in the \gallina\ language. For example in the ring
-\texttt{nat}, consider the expression:
-
-\begin{quotation}
-\begin{verbatim}
-(plus (mult (plus (f (5)) x) x)
-      (mult (if b then (4) else (f (3))) (2)))
-\end{verbatim}
-\end{quotation}
-
-\noindent As a ring expression, it has 3 subterms. Give each subterm a
-number in an arbitrary order:
-
-\begin{tabular}{ccl}
-0 & $\mapsto$ & \verb|if b then (4) else (f (3))| \\
-1 & $\mapsto$ & \verb|(f (5))| \\
-2 & $\mapsto$ & \verb|x| \\
-\end{tabular}
-
-\noindent Then normalize the ``abstract'' polynomial 
-
-$$((V_1 \otimes V_2) \oplus V_2) \oplus (V_0 \otimes 2) $$
-
-\noindent In our example the normal form is:
-
-$$(2 \otimes V_0) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2)$$
-
-\noindent Then substitute the variables by their values in the variables map to
+What does this tactic do?
+------------------------------
+
+``ring`` does associative-commutative rewriting in ring and semi-ring
+structures. Assume you have two binary functions :math:`\oplus` and
+:math:`\otimes` that are associative and commutative, with :math:`\oplus`
+distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for
+:math:`\oplus` and :math:`\otimes`. A polynomial is an expression built on
+variables :math:`V_0`, :math:`V_1`, :math:`\dots` and constants by application
+of :math:`\oplus` and :math:`\otimes`.
+
+Let an ordered product be a product of variables :math:`V_{i_1} \otimes \dots
+\otimes V_{i_n}` verifying :math:`i_1 ≤ i_2 ≤ \dots ≤ i_n` . Let a 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 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 normal form of the polynomial. In fact, the actual representation shares
+monomials with same prefixes. So what does ring? It normalizes polynomials over
+any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring
+expressions, so that the user does not have to deal manually with the theorems
+of associativity and commutativity.
+
+
+.. example::
+
+   In the ring of integers, the normal form of 
+     :math:`x (3 + yx + 25(1 − z)) + zx` 
+   is 
+     :math:`28x + (−24)xz + xxy`.
+
+
+``ring`` is also able to compute a normal form modulo monomial equalities.
+For example, under the hypothesis that :math:`2x^2 = yz+1`, the normal form of
+:math:`2(x + 1)x − x − zy` is :math:`x+1`.
+
+The variables map
+----------------------
+
+It is frequent to have an expression built with :math:`+` and :math:`\times`,
+but rarely on variables only. Let us associate a number to each subterm of a
+ring expression in the Gallina language. For example in the ring |nat|, consider
+the expression:
+
+
+::
+
+    (plus (mult (plus (f (5)) x) x)
+          (mult (if b then (4) else (f (3))) (2)))
+
+
+As a ring expression, it has 3 subterms. Give each subterm a number in
+an arbitrary order:
+
+=====  ===============  =========================
+0      :math:`\mapsto`  if b then (4) else (f (3))
+1      :math:`\mapsto`  (f (5))
+2      :math:`\mapsto`  x
+=====  ===============  =========================
+
+Then normalize the “abstract” polynomial
+:math:`((V_1 \otimes V_2 ) \oplus V_2) \oplus (V_0 \otimes 2)`
+In our example the normal form is:
+:math:`(2 \otimes V_0 ) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2 )`.
+Then substitute the variables by their values in the variables map to
 get the concrete normal polynomial:
 
-\begin{quotation}
-\begin{verbatim}
-(plus (mult (2) (if b then (4) else (f (3)))) 
-      (plus (mult (f (5)) x) (mult x x))) 
-\end{verbatim}
-\end{quotation}
+::
+
+    (plus (mult (2) (if b then (4) else (f (3)))) 
+          (plus (mult (f (5)) x) (mult x x))) 
+
 
-\asection{Is it automatic?}
+Is it automatic?
+---------------------
 
 Yes, building the variables map and doing the substitution after
-normalizing is automatically done by the tactic. So you can just forget
-this paragraph and use the tactic according to your intuition.
-
-\asection{Concrete usage in \Coq
-\tacindex{ring}
-\tacindex{ring\_simplify}}
-
-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, rewriting of monomials) 
-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 can also be applied in a hypothesis.
-
-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{ArithRing} (exported by \texttt{Arith});
-for \texttt{Z}, do \texttt{Require Import
-ZArithRing} or simply \texttt{Require Import ZArith}; 
-for \texttt{N}, do \texttt{Require Import NArithRing} or 
-\texttt{Require Import NArith}.
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Require Import ZArith.
-\end{coq_example*}
-\begin{coq_example}
-Open Scope Z_scope.
-Goal forall a b c:Z,
-  (a + b + c)^2  =
-  a * a + b^2 + 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}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Goal forall a b:Z, 2*a*b = 30 ->
-        (a+b)^2 = a^2 + b^2 + 30.
-\end{coq_example}
-\begin{coq_example}
-intros a b H; ring [H].
-\end{coq_example} 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{Variants}
-  \item {\tt ring [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
-    terms modulo ring operations and rewriting of the equalities
-    defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
-    {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
-    where $m$ is a monomial (after ``abstraction''),
-    $p$ a polynomial and $=$ the corresponding equality of the ring structure.
-
-  \item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_m$ in 
-{\ident}}
-     performs the simplification in the hypothesis named {\tt ident}.
-\end{Variants}
-
-\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
+normalizing is automatically done by the tactic. So you can just
+forget this paragraph and use the tactic according to your intuition.
+
+Concrete usage in Coq
+--------------------------
+
+.. tacn:: ring
+
+The ``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, rewriting of monomials) and
+comparing syntactically the results.
+
+.. tacn:: ring_simplify
+
+``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 can also be applied in a hypothesis.
+
+The tactic must be loaded by ``Require Import Ring``. The ring structures
+must be declared with the ``Add Ring`` command (see below). The ring of
+booleans is predefined; if one wants to use the tactic on |nat| one must
+first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do
+``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do
+``Require Import NArithRing`` or ``Require Import NArith``.
+
+
+.. example::
+
+  .. coqtop:: all
+
+    Require Import ZArith.
+    Open Scope Z_scope.
+    Goal forall a b c:Z, 
+        (a + b + c) ^ 2 = 
+         a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
+    intros; ring.
+    Abort.
+    Goal forall a b:Z, 
+         2 * a * b = 30 -> (a + b) ^ 2 = a ^ 2 + b ^ 2 + 30.
+    intros a b H; ring [H].
+    Abort.
+
+
+.. tacv:: ring [{* @term }] 
+ 
+decides the equality of two terms modulo ring operations and 
+the equalities defined by the :n:`@term`\ s.
+Each :n:`@term` has to be a proof of some equality `m = p`, where `m` is a monomial (after “abstraction”), `p` a polynomial and `=` the corresponding equality of the ring structure.
+
+.. tacv:: ring_simplify [{* @term }] {* @term } in @ident
+ 
+performs the simplification in the hypothesis named :n:`@ident`.
+
+
+.. note:: 
+
+  .. tacn::  ring_simplify @term1; ring_simplify @term2 
+
+  is not equivalent to 
+
+  .. tacn:: ring_simplify @term1 @term2
+
+  In the latter case the variables map
+  is shared between the two terms, and common subterm `t` of :n:`@term1` and :n:`@term2`
+  will have the same associated variable number. So the first
+  alternative should be avoided for terms belonging to the same 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
-\comindex{Add Ring}}
+
+
+Error messages:
+
+
+.. exn:: not a valid ring equation
+
+  The conclusion of the goal is not provable in the corresponding ring theory.
+
+.. exn:: arguments of ring_simplify do not have all the same type 
+  
+  ``ring_simplify`` cannot simplify terms of several rings at the same
+  time. Invoke the tactic once per ring structure.
+
+.. exn:: cannot find a declared ring structure over @term
+
+  No ring has been declared for the type of the terms to be simplified.
+  Use ``Add Ring`` first.
+
+.. exn:: cannot find a declared ring structure for equality @term 
+
+  Same as above is the case of the ``ring`` tactic.
+
+
+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\_theory.ring\_theory} and {\tt Ring\_theory.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\_theory}) is:
-\begin{verbatim}
-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}
-
-This implementation of {\tt ring} also features a notion of constant
-that can be parameterized. This can be used to improve the handling of
+carrier set, an equality, and ring operations: ``Ring_theory.ring_theory``
+and ``Ring_theory.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:`tactics-enabled-on-user-provided-relations`). The definition of ring and semi-rings (see module
+``Ring_theory``) is:
+
+.. coqtop:: in
+
+    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
+    }.
+
+
+This implementation of ``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 needs 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
+introducing a type of *coefficients* and an implementation of the ring
+operations, and a morphism from the coefficient type to the ring
+carrier type. The morphism needs 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:
+
+.. coqtop:: in 
+
+    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]
+    }.
+
+
+where ``c0`` and ``cI`` denote the 0 and 1 of the coefficient set, ``+!``, ``*!``, ``-!``
+are the implementations of the ring operations, ``==`` is the equality of
+the coefficients, ``?+!`` is an implementation of this equality, and ``[x]``
+is a notation for the image of ``x`` by the ring morphism.
+
+Since |Z| is an initial ring (and |N| is an initial semi-ring), it can
+always be considered as a set of coefficients. There are basically
+three kinds of (semi-)rings:
+
+abstract rings
+  to be used when operations are not effective. The set
+  of coefficients is |Z| (or |N| for semi-rings).
+
+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.
+
+customized ring
+  for other cases. The user has to provide the
   coefficient set and the morphism.
-\end{description}
-
-This implementation of ring can also recognize simple 
-power expressions as ring expressions. A power function is specified by 
-the following property:
-\begin{verbatim}
-Section POWER.
-  Variable Cpow : Set.
-  Variable Cp_phi : N -> Cpow.
-  Variable rpow : R -> Cpow -> R.
-
-  Record power_theory : Prop := mkpow_th {
-    rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
-  }.
-
-End POWER.
-\end{verbatim}
-
-
-The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$
-($mod_1$,\dots,$mod_2$)}.  The name is not relevant. It is just used
-for error messages. The term $ring$ is a proof that the ring signature
-satisfies the (semi-)ring axioms. The optional list of modifiers is
-used to tailor the behavior 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. The expression 
-  \term{} is
-  the correctness proof of an equality test {\tt ?=!} (which should be
-  evaluable). 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. The expression 
-  \term{} is
-  a proof that there exists a morphism between a set of coefficient
-  and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt
-  Ring\_theory.semi\_morph}).
-\item[setoid \term$_1$ \term$_2$] forces the use of given setoid. The 
-  expression \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\_theory.ring\_eq\_ext} and
-  {\tt Ring\_theory.sring\_eq\_ext}). This modifier needs 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
-  InitialRing.NotConstant}. The default behavior is to map only 0 and
-  1 to their counterpart in the coefficient set. This is generally not
+
+
+This implementation of ring can also recognize simple power
+expressions as ring expressions. A power function is specified by the
+following property:
+
+.. coqtop:: in
+
+    Section POWER.
+      Variable Cpow : Set.
+      Variable Cp_phi : N -> Cpow.
+      Variable rpow : R -> Cpow -> R.
+    
+      Record power_theory : Prop := mkpow_th {
+        rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
+      }.
+    
+    End POWER.
+
+
+The syntax for adding a new ring is 
+
+.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}.
+
+The :n:`@ident` is not relevant. It is just used for error messages. The
+:n:`@term` is a proof that the ring signature satisfies the (semi-)ring
+axioms. The optional list of modifiers is used to tailor the behavior
+of the tactic. The following list describes their syntax and effects:
+
+.. prodn::
+   ring_mod ::= abstract %| decidable @term %| morphism @term
+                %| setoid @term @term 
+                %| constants [@ltac] 
+                %| preprocess [@ltac]
+                %| postprocess [@ltac]
+                %| power_tac @term [@ltac] 
+                %| sign @term
+                %| div @term
+
+
+abstract
+  declares the ring as abstract. This is the default.
+
+decidable :n:`@term`
+  declares the ring as computational. The expression
+  :n:`@term` is the correctness proof of an equality test ``?=!``
+  (which  hould be evaluable). Its type should be of the form 
+  ``forall x y, x ?=! y = true → x == y``.
+
+morphism :n:`@term`
+  declares the ring as a customized one. The expression
+  :n:`@term` is a proof that there exists a morphism between a set of
+  coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and
+  ``Ring_theory.semi_morph``).
+
+setoid :n:`@term` :n:`@term` 
+  forces the use of given setoid. The first
+  :n:`@term` is a proof that the equality is indeed a setoid (see
+  ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the
+  ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and 
+  ``Ring_theory.sring_eq_ext``).
+  This modifier needs not be used if the setoid and morphisms have been
+  declared.
+
+constants [:n:`@ltac`] 
+  specifies a tactic expression :n:`@ltac` that, given a
+  term, returns either an object of the coefficient set that is mapped
+  to the expression via the morphism, or returns
+  ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1
+  to their counterpart in the coefficient set. This is generally not
   desirable for non trivial computational rings.
-\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
+
+preprocess [:n:`@ltac`]
+  specifies a tactic :n:`@ltac` that is applied as a
+  preliminary step for ``ring`` and ``ring_simplify``. It can be used to
+  transform a goal so that it is better recognized. For instance, ``S n``
+  can be changed to ``plus 1 n``.
+
+postprocess [:n:`@ltac`]
+  specifies a tactic :n:`@ltac` that is applied as a final
+  step for ``ring_simplify``. For instance, it can be used to undo
   modifications of the preprocessor.
-\item[power\_tac {\term} [\ltac]] allows {\tt ring} and {\tt ring\_simplify} to
-  recognize power expressions with a constant positive integer exponent 
-  (example: $x^2$). The term {\term} is a proof that a given power function
-  satisfies the specification of a power function ({\term} has to be a
-  proof of {\tt Ring\_theory.power\_theory}) and {\ltac} specifies a
-  tactic expression that, given a term, ``abstracts'' it into an
-  object of type {\tt N} whose interpretation via {\tt Cp\_phi} (the
-  evaluation function of power coefficient) is the original term, or
-  returns {\tt InitialRing.NotConstant} if not a constant coefficient
-  (i.e. {\ltac} is the inverse function of {\tt Cp\_phi}).
-  See files {\tt plugins/setoid\_ring/ZArithRing.v} and
-  {\tt plugins/setoid\_ring/RealField.v} for examples.
-  By default the tactic does not recognize power expressions as ring
-  expressions.
-\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
-  when outputting its normal form, i.e writing $x - y$ instead of $x + (-y)$.
-  The term {\term} is a proof that a given sign function indicates expressions
-   that are signed ({\term} has to be a
-  proof of {\tt Ring\_theory.get\_sign}). See  {\tt plugins/setoid\_ring/InitialRing.v} for examples of sign function.
-\item[div {\term}] allows  {\tt ring} and {\tt ring\_simplify} to use monomials
-with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function  satisfies the specification of an euclidean
-  division function  ({\term} has to be a
-  proof of {\tt Ring\_theory.div\_theory}). For example, this function is
-  called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
-   See  {\tt plugins/setoid\_ring/InitialRing.v} for examples of div function.
-  
-\end{description}
-
-
-\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}
-
-\asection{How does it work?}
-
-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.
-
-The interested reader is strongly advised to have a look at the file
-\texttt{Ring\_polynom.v}. Here a type for polynomials is defined: 
-
-\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
-  | PEpow : PExpr -> N -> PExpr.
-\end{verbatim}
-\end{flushleft}
-\end{small}
+
+power_tac :n:`@term` [:n:`@ltac`] 
+  allows ``ring`` and ``ring_simplify`` to recognize
+  power expressions with a constant positive integer exponent (example:
+  ::math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies
+  the specification of a power function (term has to be a proof of
+  ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression
+  that, given a term, “abstracts” it into an object of type |N| whose
+  interpretation via ``Cp_phi`` (the evaluation function of power
+  coefficient) is the original term, or returns ``InitialRing.NotConstant``
+  if not a constant coefficient (i.e. |L_tac| is the inverse function of
+  ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v``
+  and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic
+  does not recognize power expressions as ring expressions.
+
+sign :n:`@term`
+  allows ``ring_simplify`` to use a minus operation when
+  outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
+  term `:n:`@term` is a proof that a given sign function indicates expressions
+  that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See
+  ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
+
+div :n:`@term`
+  allows ``ring`` and ``ring_simplify`` to use monomials with
+  coefficient other than 1 in the rewriting. The term :n:`@term` is a proof
+  that a given division function satisfies the specification of an
+  euclidean division function (:n:`@term` has to be a proof of
+  ``Ring_theory.div_theory``). For example, this function is called when
+  trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See
+  ``plugins/setoid_ring/InitialRing.v`` for examples of div function.
+
+Error messages:
+
+.. exn:: bad ring structure
+
+  The proof of the ring structure provided is not
+  of the expected type.
+
+.. exn:: bad lemma for decidability of equality
+
+  The equality function
+  provided in the case of a computational ring has not the expected
+  type.
+
+.. exn:: ring operation should be declared as a morphism
+
+  A setoid associated to the carrier of the ring structure has been found, 
+  but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`.
+
+How does it work?
+----------------------
+
+The code of ring is a good example of tactic written using *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 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 ``Ring_polynom.v``. Here a type for polynomials is defined:
+
+
+.. coqtop:: in
+
+    Inductive PExpr : Type :=
+      | PEc : C -> PExpr
+      | PEX : positive -> PExpr
+      | PEadd : PExpr -> PExpr -> PExpr
+      | PEsub : PExpr -> PExpr -> PExpr
+      | PEmul : PExpr -> PExpr -> PExpr
+      | PEopp : PExpr -> PExpr
+      | PEpow : PExpr -> N -> PExpr.
+
 
 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}$. 
 
 
+.. coqtop:: in
+
+    Inductive Pol : Type :=
+      | Pc : C -> Pol 
+      | Pinj : positive -> Pol -> Pol                   
+      | PX : Pol -> positive -> Pol -> Pol.
+
+
+where ``Pinj n P`` denotes ``P`` in which :math:`V_i` is replaced by :math:`V_{i+n}` , 
+and ``PX P n Q`` denotes :math:`P \otimes V_1^n \oplus Q'`, `Q'` being `Q` where :math:`V_i` is replaced by :math:`V_{i+1}`.
+
 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}
+
+
+.. coqtop:: in
+
+
+    Definition PEeval : list R -> PExpr -> R := [...].
+    Definition Pphi_dev : list R -> Pol -> R := [...].
+
 
 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.
 
+.. coqtop:: in
+
+    Definition norm : PExpr -> Pol := [...].
+    Lemma Pphi_dev_ok :
+       forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
+
+
+So now, what is the scheme for a normalization proof? Let p be the
+polynomial expression that the user wants to normalize. First a little
+piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an
+abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|-
+equivalent to ``(PEeval`` `v` `ap`\ ``)``. Then we replace it by ``(Pphi_dev`` `v`
+``(norm`` `ap`\ ``))``, using the main correctness theorem and we reduce it to a
+concrete expression `p’`, which is the concrete normal form of `p`. This is summarized in this diagram:
+
+========= ======  ====
+`p`        |ra|   |re|            
+\          |eq|    \ 
+`p’`       |la|   |le|
+========= ======  ====
 
-\asection{Dealing with fields
-\tacindex{field}
-\tacindex{field\_simplify}
-\tacindex{field\_simplify\_eq}}
-
-
-The {\tt field} tactic is  an extension of the {\tt ring} to deal with
-rational expression. Given a rational expression $F=0$. It first reduces the
-expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring
-expressions.
-For example, if we take $F = (1 - 1/x) x - x + 1$, this gives 
-$ N= (x -1)  x - x^2 + x$ and $D= x$. It then calls {\tt ring} 
-to solve $N=0$. Note that {\tt field} also generates non-zero conditions
-for all the denominators it encounters in the reduction.
-In our example, it generates the condition $x \neq 0$. These
-conditions appear as one subgoal which is a conjunction if there are
-several denominators.
-Non-zero conditions are {\it always} polynomial expressions. For example 
-when reducing the expression $1/(1 + 1/x)$, two side conditions are
-generated: $x\neq 0$ and $x + 1 \neq 0$. Factorized expressions are
-broken since a field is an integral domain, and when the equality test
-on coefficients is complete w.r.t. the equality of the target field,
+The user do not see the right part of the diagram. From outside, the
+tactic behaves like a |bdi| simplification extended with AC rewriting
+rules. Basically, the proof is only the application of the main
+correctness theorem to well-chosen arguments.
+
+Dealing with fields
+------------------------
+
+.. tacn:: field
+
+The ``field`` tactic is an extension of the ``ring`` to deal with rational
+expression. Given a rational expression :math:`F = 0`. It first reduces the
+expression `F` to a common denominator :math:`N/D = 0` where `N` and `D`
+are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this
+gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve 
+:math:`N = 0`.
+Note that ``field`` also generates non-zero conditions for all the
+denominators it encounters in the reduction. In our example, it
+generates the condition :math:`x \neq 0`. These conditions appear as one subgoal
+which is a conjunction if there are several denominators. Non-zero
+conditions are always polynomial expressions. For example when
+reducing the expression :math:`1/(1 + 1/x)`, two side conditions are
+generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since
+a field is an integral domain, and when the equality test on
+coefficients is complete w.r.t. the equality of the target field,
 constants can be proven different from zero automatically.
 
-The tactic must be loaded by \texttt{Require Import Field}. New field
-structures can be declared to the system with the \texttt{Add Field}
-command (see below). The field of real numbers is defined in module
-\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported
-by module \texttt{Rbase}, so that requiring \texttt{Rbase} or
-\texttt{Reals} is enough to use the field tactics on real
-numbers. Rational numbers in canonical form are also declared as a
-field in module \texttt{Qcanon}.
-
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example*}
-Require Import Reals.
-\end{coq_example*}
-\begin{coq_example}
-Open Scope R_scope.
-Goal forall x,  x <> 0 ->
-   (1 - 1/x) * x - x + 1 = 0.
-\end{coq_example}
-\begin{coq_example}
-intros; field; auto.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Goal forall x y, y <> 0 -> y = x -> x/y = 1.
-\end{coq_example}
-\begin{coq_example}
-intros x y H H1; field [H1]; auto.
-\end{coq_example} 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{Variants}
-  \item {\tt field [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
-    terms modulo field operations and rewriting of the equalities
-    defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
-    {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
-    where $m$ is a monomial (after ``abstraction''),
-    $p$ a polynomial and $=$ the corresponding equality of the field structure.
-    Beware that rewriting works with the equality $m=p$ only if $p$ is a 
-    polynomial since rewriting is handled by the underlying {\tt ring}
-    tactic.
-  \item {\tt field\_simplify} 
-     performs the simplification in the conclusion of the goal, $F_1 = F_2$
-     becomes $N_1/D_1 = N_2/D_2$. A normalization step (the same as the
-     one for rings) is then applied to $N_1$, $D_1$, $N_2$ and
-     $D_2$. This way, polynomials remain in factorized form during the
-     fraction simplifications. This yields smaller expressions when
-     reducing to the same denominator since common factors can be
-     canceled.
-
-  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$]}
-     performs the simplification in the conclusion of the goal using
-    the equalities
-    defined by \term$_1$ {\ldots} \term$_n$.
-
-  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
-$t_m$}
-     performs the simplification in the terms $t_1$ \ldots $t_m$
-    of the conclusion of the goal using
-    the equalities
-    defined by \term$_1$ {\ldots} \term$_n$. 
-
-  \item {\tt field\_simplify in $H$}  
-     performs the simplification in the assumption $H$.
-
-  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$] in $H$}
-     performs the simplification in the assumption $H$ using
-    the equalities
-    defined by \term$_1$ {\ldots} \term$_n$. 
-
-  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
-$t_m$ in $H$}
-     performs the simplification in the terms $t_1$ \ldots $t_n$
-    of the assumption $H$ using
-    the equalities
-    defined by \term$_1$ {\ldots} \term$_m$. 
-
-  \item {\tt field\_simplify\_eq}
-     performs the simplification in the conclusion of the goal removing
-     the denominator. $F_1 = F_2$
-     becomes $N_1 D_2 = N_2  D_1$.
-
-  \item {\tt field\_simplify\_eq   [\term$_1$ {\ldots} \term$_n$]}
-     performs the simplification in the conclusion of the goal using
-    the equalities
-    defined by \term$_1$ {\ldots} \term$_n$. 
-
-  \item {\tt field\_simplify\_eq} in $H$
-     performs the simplification in the assumption $H$.
-
-  \item {\tt field\_simplify\_eq   [\term$_1$ {\ldots} \term$_n$] in $H$}
-     performs the simplification in the assumption $H$ using
-    the equalities
-    defined by \term$_1$ {\ldots} \term$_n$. 
-\end{Variants}
-
-\asection{Adding a new field structure
-\comindex{Add Field}}
+The tactic must be loaded by ``Require Import Field``. New field
+structures can be declared to the system with the ``Add Field`` command
+(see below). The field of real numbers is defined in module ``RealField``
+(in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so
+that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on
+real numbers. Rational numbers in canonical form are also declared as
+a field in module ``Qcanon``.
+
+
+.. example::
+
+  .. coqtop:: all
+
+    Require Import Reals.
+    Open Scope R_scope.
+    Goal forall x,
+           x <> 0 -> (1 - 1 / x) * x - x + 1 = 0.
+    intros; field; auto.
+    Abort.
+    Goal forall x y, 
+           y <> 0 -> y = x -> x / y = 1.
+    intros x y H H1; field [H1]; auto.
+    Abort.
+
+.. tacv:: field [{* @term}] 
+
+  decides the equality of two terms modulo
+  field operations and the equalities defined  
+  by the :n:`@term`\ s. Each :n:`@term` has to be a proof of some equality 
+  `m` ``=`` `p`, where `m` is a monomial (after “abstraction”), `p` a polynomial 
+  and ``=`` the corresponding equality of the field structure.
+
+.. note:: 
+
+   rewriting works with the equality  `m` ``=`` `p` only if `p` is a polynomial since
+   rewriting is handled by the underlying ring tactic.
+
+.. tacv:: field_simplify
+ 
+   performs the simplification in the conclusion of the
+   goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step
+   (the same as the one for rings) is then applied to :math:`N_1`, :math:`D_1`, 
+   :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during the
+   fraction simplifications. This yields smaller expressions when
+   reducing to the same denominator since common factors can be canceled.
+
+.. tacv:: field_simplify [{* @term }] 
+
+  performs the simplification in the conclusion of the goal using the equalities 
+  defined by the :n:`@term`\ s.
+
+.. tacv:: field_simplify [{* @term }] {* @term }
+
+   performs the simplification in the terms :n:`@terms`  of the conclusion of the goal
+   using the equalities defined by :n:`@term`\ s inside the brackets.
+
+.. tacv :: field_simplify in @ident
+
+   performs the simplification in the assumption :n:`@ident`.
+
+.. tacv :: field_simplify [{* @term }] in @ident 
+ 
+   performs the simplification
+   in the assumption :n:`@ident` using the equalities defined by the :n:`@term`\ s.
+
+.. tacv:: field_simplify [{* @term }] {* @term } in @ident
+
+   performs the simplification in the :n:`@term`\ s of the assumption :n:`@ident` using the
+   equalities defined by  the :n:`@term`\ s inside the brackets.
+
+.. tacv:: field_simplify_eq
+
+   performs the simplification in the conclusion of
+   the goal removing the denominator. :math:`F_1 = F_2` becomes :math:`N_1 D_2 = N_2 D_1`.
+
+.. tacv:: field_simplify_eq [ {* @term }]
+
+   performs the simplification in
+   the conclusion of the goal using the equalities defined by 
+   :n:`@term`\ s.
+
+.. tacv:: field_simplify_eq in @ident
+
+   performs the simplification in the assumption :n:`@ident`.
+
+.. tacv:: field_simplify_eq [{* @term}] in @ident
+
+   performs the simplification in the assumption :n:`@ident` using the equalities defined by
+   :n:`@terms`\ s and removing the denominator.
+
+
+Adding a new field structure
+---------------------------------
 
 Declaring a new field consists in proving that a field signature (a
-carrier set, an equality, and field operations: {\tt
-Field\_theory.field\_theory} and {\tt Field\_theory.semi\_field\_theory})
-satisfies the field axioms. Semi-fields (fields without $+$ inverse) are
+carrier set, an equality, and field operations:
+``Field_theory.field_theory`` and ``Field_theory.semi_field_theory``)
+satisfies the field axioms. Semi-fields (fields 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 fields and semi-fields is:
-\begin{verbatim}
-Record field_theory : Prop := mk_field {
-  F_R : ring_theory rO rI radd rmul rsub ropp req;
-  F_1_neq_0 : ~ 1 == 0;
-  Fdiv_def : forall p q, p / q == p * / q;
-  Finv_l : forall p, ~ p == 0 ->  / p * p == 1
-}.
-
-Record semi_field_theory : Prop := mk_sfield {
-  SF_SR : semi_ring_theory rO rI radd rmul req;
-  SF_1_neq_0 : ~ 1 == 0;
-  SFdiv_def : forall p q, p / q == p * / q;
-  SFinv_l : forall p, ~ p == 0 ->  / p * p == 1
-}.
-\end{verbatim}
+relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of
+fields and semi-fields is:
+
+.. coqtop:: in
+
+    Record field_theory : Prop := mk_field {
+      F_R : ring_theory rO rI radd rmul rsub ropp req;
+      F_1_neq_0 : ~ 1 == 0;
+      Fdiv_def : forall p q, p / q == p * / q;
+      Finv_l : forall p, ~ p == 0 ->  / p * p == 1
+    }.
+    
+    Record semi_field_theory : Prop := mk_sfield {
+      SF_SR : semi_ring_theory rO rI radd rmul req;
+      SF_1_neq_0 : ~ 1 == 0;
+      SFdiv_def : forall p q, p / q == p * / q;
+      SFinv_l : forall p, ~ p == 0 ->  / p * p == 1
+    }.
+
 
 The result of the normalization process is a fraction represented by
 the following type:
-\begin{verbatim}
-Record linear : Type := mk_linear {
-  num : PExpr C;
-  denum : PExpr C;
-  condition : list (PExpr C)
-}.
-\end{verbatim}
-where {\tt num} and {\tt denum} are the numerator and denominator;
-{\tt condition} is a list of expressions that have appeared as a
-denominator during the normalization process. These expressions must
-be proven different from zero for the correctness of the algorithm.
-
-The syntax for adding a new field is {\tt Add Field $name$ : $field$
-($mod_1$,\dots,$mod_2$)}.  The name is not relevant. It is just used
-for error messages. $field$ is a proof that the field signature
-satisfies the (semi-)field axioms. The optional list of modifiers is
-used to tailor the behavior of the tactic. Since field tactics are
-built upon ring tactics, all modifiers of the {\tt Add Ring}
-apply. There is only one specific modifier:
-\begin{description}
-\item[completeness \term] allows the field tactic to prove
-  automatically that the image of non-zero coefficients are mapped to
-  non-zero elements of the field. \term is a proof of {\tt forall x y,
-    [x] == [y] -> x?=!y = true}, which is the completeness of equality
-  on coefficients w.r.t. the field equality.
-\end{description}
-
-\asection{History of \texttt{ring}}
-
-First Samuel Boutin designed the tactic \texttt{ACDSimpl}. 
-This tactic did lot of rewriting. But the proofs
-terms generated by rewriting were too big for \Coq's type-checker.
-Let us see why:
-
-\begin{coq_eval}
-Require Import ZArith.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example}
-Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
-\end{coq_example}
-\begin{coq_example*}
-intros; rewrite (Z.mul_comm y z); reflexivity.
-Save toto.
-\end{coq_example*}
-\begin{coq_example}
-Print toto.
-\end{coq_example}
-
-At each step of rewriting, the whole context is duplicated in the proof
-term. Then, a tactic that does hundreds of rewriting generates huge proof
-terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it
-using reflection (see his article in TACS'97 \cite{Bou97}). Later, the
-stuff was rewritten by Patrick
-Loiseleur: the new tactic does not any more require \texttt{ACDSimpl}
-to compile and it makes use of $\beta\delta\iota$-reduction 
-not only to replace the rewriting steps, but also to achieve the
-interleaving of computation and 
-reasoning (see \ref{DiscussReflection}). He also wrote a
-few ML code for the \texttt{Add Ring} command, that allow to register
-new rings dynamically.
-
-Proofs terms generated by \texttt{ring} are quite small, they are
-linear in the number of $\oplus$ and $\otimes$ operations in the
-normalized terms. Type-checking those terms requires some time because it
-makes a large use of the conversion rule, but
-memory requirements are much smaller. 
-
-\asection{Discussion}
-\label{DiscussReflection}
-
-Efficiency is not the only motivation to use reflection
-here. \texttt{ring} also deals with constants, it rewrites for example the
-expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the
-tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the
-expression $34 + 2*(x - 1) + 12$ is interpreted as 
-$V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$, 
+
+.. coqtop:: in
+
+    Record linear : Type := mk_linear {
+      num : PExpr C;
+      denum : PExpr C;
+      condition : list (PExpr C)
+    }.
+
+
+where ``num`` and ``denum`` are the numerator and denominator; ``condition`` is a
+list of expressions that have appeared as a denominator during the
+normalization process. These expressions must be proven different from
+zero for the correctness of the algorithm.
+
+The syntax for adding a new field is 
+
+.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}.
+
+The :n:`@ident` is not relevant. It is just used for error
+messages. :n:`@term` is a proof that the field signature satisfies the
+(semi-)field axioms. The optional list of modifiers is used to tailor
+the behavior of the tactic.
+
+.. prodn::
+   field_mod := @ring_mod %| completeness @term
+
+Since field tactics are built upon ``ring``
+tactics, all modifiers of the ``Add Ring`` apply. There is only one
+specific modifier:
+
+completeness :n:`@term`
+  allows the field tactic to prove automatically
+  that the image of non-zero coefficients are mapped to non-zero
+  elements of the field. :n:`@term` is a proof of
+
+  ``forall x y, [x] == [y] ->  x ?=! y = true``, 
+
+  which is the completeness of equality on coefficients
+  w.r.t. the field equality.
+
+
+History of ring
+--------------------
+
+First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot
+of rewriting. But the proofs terms generated by rewriting were too big
+for |Coq|’s type-checker. Let us see why:
+
+.. coqtop:: all
+
+  Require Import ZArith.
+  Open Scope Z_scope.
+  Goal forall x y z : Z, 
+         x + 3 + y + y * z = x + 3 + y + z * y.
+  intros; rewrite (Zmult_comm y z); reflexivity.
+  Save foo.
+  Print  foo.
+
+At each step of rewriting, the whole context is duplicated in the
+proof term. Then, a tactic that does hundreds of rewriting generates
+huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote
+it using reflection (see his article in TACS’97 [Bou97]_). Later, it
+was rewritten by Patrick Loiseleur: the new tactic does not any
+more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not
+only to replace the rewriting steps, but also to achieve the
+interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote a
+few |ML| code for the ``Add Ring`` command, that allow to register new rings
+dynamically.
+
+Proofs terms generated by ring are quite small, they are linear in the
+number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking
+those terms requires some time because it makes a large use of the
+conversion rule, but memory requirements are much smaller.
+
+
+.. _discussion_reflection:
+
+
+Discussion
+----------------
+
+
+Efficiency is not the only motivation to use reflection here. ``ring``
+also deals with constants, it rewrites for example the expression 
+``34 + 2 * x − x + 12`` to the expected result ``x + 46``.
+For the tactic ``ACDSimpl``, the only constants were 0 and 1. 
+So the expression ``34 + 2 * (x − 1) + 12``
+is interpreted as :math:`V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3`\ ,
 with the variables mapping 
-$\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is
-rewritten to $34 - x + 2*x + 12$, very far from the expected
-result. Here rewriting is not sufficient: you have to do some kind of
-reduction (some kind of \textit{computation}) to achieve the
-normalization.
-
-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
-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 significantly less efficient to replace them by tactics using
-reflection.
+:math:`\{V_0 \mapsto 34; V_1 \mapsto 2; V_2 \mapsto x; V_3 \mapsto 12\}`\ . 
+Then it is rewritten to ``34 − x + 2 * x + 12``, very far from the expected result. 
+Here rewriting is not sufficient: you have to do some kind of reduction
+(some kind of computation) to achieve the normalization.
+
+The tactic ``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 ``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 ``auto`` or ``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 an 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
-%%% TeX-master: "Reference-Manual"
-%%% End: 
+couple an external tool (a rewriting program or a model checker)
+with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and
+prove a correction theorem that states that *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.
+
+
+
+
+
+
+.. rubric:: Footnotes
+.. [#f1] based on previous work from Patrick Loiseleur and Samuel Boutin
+
+
+
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 6f4b28759..0757e5095 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -51,6 +51,7 @@ Table of contents
    addendum/micromega
    addendum/extraction
    addendum/program
+   addendum/ring
    addendum/nsatz
 
 .. toctree::