## Coq and Gappa

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 $[\frac{52}{16}, \frac{53}{16}]$ and $[\frac{22}{16}, \frac{30}{16}]$ 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, $e_1 = e_2$, or pairs of inequalities on real numbers, $b_1 \le e \le b_2$, or inequalities expressing relative errors, $|e_1 - e_2| \le b \cdot |e_2|$. For inequalities, the $b$ bounds have to be explicit dyadic numbers. The tactic also recognizes properties written as $|e| \le b$ as syntactic sugar for $0 \le |e| \le b$.

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.