blob: b1a9a37407868938f0a8cbd8865376721a5342a4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
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:
|
