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.

  forall x y : R,
  3/4 <= x <= 3 ->
  0 <= sqrt x <= 1775 * (powerRZ 2 (-10)).

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).

  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).
  unfold rnd; gappa.

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).

  forall a b : R,
  format a -> format b ->
  52 / 16 <= a <= 53 / 16 ->
  22 / 16 <= b <= 30 / 16 ->
  format (a - b).
  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.