Ajout de Field

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

1 files changed, 68 insertions, 0 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 44f31379b1..d0f2ebb5f3 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1631,6 +1631,74 @@ You can have a look at the files \texttt{Ring.v},
 
 \SeeAlso Chapter~\ref{Ring} for more detailed explanations about this tactic.
 
+\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 Field}. Field theories are declared (as for {\tt Ring}) with
+the {\tt Add Field} command.
+
+\Example
+\begin{coq_example*}
+Require Reals.
+Goal (x,y:R)``x*y>0`` -> ``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``.
+\end{coq_example*}
+
+\begin{coq_example}
+Intros; Field.
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.  
+\end{coq_eval}
+
+\subsection{\tt Add Field}
+\comindex{Add Field}
+
+This vernacular command adds a commutative field theory to the database for the
+tactic {\tt Field}. You must provide this theory as follows:\\
+
+{\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
+Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
+
+\noindent where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}}
+is a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
+A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it Azero}} is a
+term of type {\tt A}, {\tt {\it Aopp}} is a term of type {\tt A->A}, {\tt {\it
+Aeq}} is a term of type {\tt A->bool}, {\tt {\it Ainv}} is a term of type {\tt
+A->A}, {\tt {\it Rth}} is a term of type {\tt (Ring\_Theory {\it A Aplus Amult
+Aone Azero Ainv Aeq})}, and {\tt {\it Tinvl}} is a term of type {\tt
+(n:{\it A})\~{}(n=={\it Azero})->({\it Amult} ({\it Ainv} n) n)=={\it Aone}}.
+To build a ring theory, refer to chapter~\ref{Ring} for more details.
+
+This command adds also an entry in the ring theory table if this theory is not
+already declared. So, it is useless to keep, for a given type, the {\tt Add
+Ring} command if you declare a theory with {\tt Add Field}, except if you plan
+to use specific features of {\tt Ring} (see chapter~\ref{Ring}). However, the
+module {\tt Ring} is not loaded by {\tt Add Field} and you have to make a {\tt
+Require 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}
+{\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}
+{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
+{\tt \phantom{Add 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.
+
+\SeeAlso theory {\tt theories/Reals} for many examples of use of {\tt Field}.
+
 \subsection{\tt AutoRewrite  [ \ident$_1$ \dots \ident$_n$ ]}
 \tacindex{AutoRewrite}