Chapter 25 Calling external provers
25.1 The gappa tactic
Sylvie Boldo, Guillaume Melquiond, Jean-Christophe Filliātre
The gappa tactic invokes the Gappa tool1 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 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 Gappa_tactic module, which must be loaded for the tactic to work properly.
The gappa tactic only handles goals and hypotheses that are double inequalities f1 ≤ e ≤ f2 where f1 and f2 are dyadic constants and e a real-valued expression. Here is an example of a goal solved by gappa:
Lemma test_gappa : forall x y:R, 3/4 <= x <= 3 -> 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)). Proof. gappa. Qed.
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:
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.
The function gappa_rounding declares a rounding mode recognized by the gappa tactic. Rounding modes are built using constants such as rounding_float and roundZR provided by the Gappa support library.