documentation tactique gappa

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

3 files changed, 61 insertions, 0 deletions

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
index 85811c1450..461e8e6d0c 100644
--- a/doc/refman/AddRefMan-pre.tex
+++ b/doc/refman/AddRefMan-pre.tex
@@ -48,6 +48,8 @@ Manual.
   tactic to do rewriting on types equipped with specific (only partially
   substitutive) equality. The chapter is contributed by Clément Renard.
 
+\item[Calling external provers] This chapter describes several tactics
+  which call external provers.
 
 \end{description}
 
diff --git a/doc/refman/ExternalProvers.tex b/doc/refman/ExternalProvers.tex
new file mode 100644
index 0000000000..b1a9a37407
--- /dev/null
+++ b/doc/refman/ExternalProvers.tex
@@ -0,0 +1,58 @@
+
+\achapter{Calling external provers}
+
+\asection{The \texttt{gappa} tactic}
+\aauthor{Sylvie Boldo, Guillaume Melquiond, Jean-Christophe Filliâtre}
+\tacindex{gappa}
+
+The \texttt{gappa} tactic invokes the Gappa
+tool\footnote{\url{http://lipforge.ens-lyon.fr/www/gappa/}} to solve
+properties about floating-point or fixed-point arithmetic. It can also
+solve simple inequalities over real numbers.
+
+The Gappa tool must be installed and its executable (called
+\texttt{gappa}) must be in the user program path. The Coq support
+library for Gappa must also be installed (it is available from Gappa's
+web site). This library provides a \texttt{Gappa\_tactic} module,
+which must be loaded for the tactic to work properly.
+
+The \texttt{gappa} tactic only handles goals and hypotheses that are
+double inequalities $f_1 \le e \le f_2$ where $f_1$ and $f_2$ are
+dyadic constants and $e$ a real-valued expression. Here is an example
+of a goal solved by \texttt{gappa}:
+\begin{verbatim}
+Lemma test_gappa : 
+  forall x y:R,
+  3/4 <= x <= 3 -> 
+  0 <= sqrt x <= 1775 * (powerRZ 2 (-10)).
+Proof.
+  gappa.
+Qed.
+\end{verbatim}
+
+Gappa supports floating-point rounding operations (as functions over
+real numbers). Here is an example involving double-precision
+floating-point numbers with rounding toward zero:
+\begin{verbatim}
+Definition rnd := gappa_rounding (rounding_float roundZR 53 1074).
+
+Lemma test_gappa2 :
+  forall a_ b_ a b : R,
+  a = rnd a_ ->
+  b = rnd b_ ->
+  52 / 16 <= a <= 53 / 16 ->
+  22 / 16 <= b <= 30 / 16 ->
+  0 <= rnd (a - b) - (a - b) <= 0.
+Proof.
+  unfold rnd; gappa.
+Qed.
+\end{verbatim}
+The function \texttt{gappa\_rounding} declares a rounding mode
+recognized by the \texttt{gappa} tactic. Rounding modes are built
+using constants such as \texttt{rounding\_float} and
+\texttt{roundZR} provided by the Gappa support library.
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 61ad66a9cd..530a58b131 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -109,6 +109,7 @@ Options A and B of the licence are {\em not} elected.}
 \include{Program.v}%
 \include{Polynom.v}%  = Ring
 \include{Setoid.v}% Tactique pour les setoides
+\include{ExternalProvers}% Tactiques appelant des prouveurs externes
 %BEGIN LATEX
 \RefManCutCommand{ENDADDENDUM=\thepage}
 %END LATEX