The Gappa Coq
Library adds a `gappa`

tactic to the Coq Proof Assistant. This tactic
invokes Gappa to solve properties about floating-point or fixed-point
arithmetic. It can also solve simple inequalities over real
numbers.

The tactic is provided by the `Gappa_tactic`

module. It
expects to find a Gappa executable (called `gappa`

) in the
user program path.

Require Import Reals. Require Import Fcore. Require Import Gappa_tactic. Open Scope R_scope. Goal forall x y : R, 3/4 <= x <= 3 -> 0 <= sqrt x <= 1775 * (powerRZ 2 (-10)). Proof. gappa. Qed.

The tactic recognizes fully-applied `rounding_fixed`

and
`rounding_float`

functions as rounding operators.

The script below proves that the difference between two double precision floating-point numbers in [math] and [math] is exactly representable as a double-precision floating-point number. (Rounding direction does not matter for this example; it has been arbitrarily chosen as rounding toward zero.)

Definition rnd := rounding_float rndZR 53 (-1074). Goal forall a_ b_ a b : R, a = rnd a_ -> b = rnd b_ -> 52 / 16 <= a <= 53 / 16 -> 22 / 16 <= b <= 30 / 16 -> rnd (a - b) = (a - b). Proof. unfold rnd; gappa. Qed.

The tactic handles goals and hypotheses that are either equalities of real numbers, [math], or pairs of inequalities on real numbers, [math], or inequalities expressing relative errors, [math]. For inequalities, the [math] bounds have to be explicit dyadic numbers. The tactic also recognizes properties written as [math] as syntactic sugar for [math].

The tactic is built on Flocq's formalism and uses the same rounding operators and formats. The previous goal could therefore have been written in a slightly more natural way.

Definition format := generic_format radix2 (FLT_exp (-1074) 53). Goal forall a b : R, format a -> format b -> 52 / 16 <= a <= 53 / 16 -> 22 / 16 <= b <= 30 / 16 -> format (a - b). Proof. intros a b Ha Hb Ia Ib. refine (sym_eq (_ : rnd (a - b) = a - b)). revert Ia Ib. replace a with (rnd a). replace b with (rnd b). unfold rnd ; gappa. Qed.