 # CoqInterval 4.0 released

The CoqInterval library provides tactics for simplifying the proofs of inequalities on expressions of real numbers, for Coq 8.8 and later. See http://coq-interval.gforge.inria.fr/ for the documentation. As usual, it is available as the `coq-interval` Opam package.

Since this release comes with some major breaking changes, I am exceptionally announcing it here to help users with the transition.

## Overhaul of bisection algorithms

Bisection is now multi-dimensional. This is enabled by passing several parameters `i_bisect` to the tactic.

``````Goal forall x y, 9/10 <= x <= 11/10 -> 9/10 <= y <= 11/10 ->
ln (x * y) - (x + y) <= -199/100.
Proof.
intros.
interval with (i_bisect x, i_bisect y).
Qed.
``````

Note that the same variable can be passed several times to `i_bisect`. This causes the tactic to split the input domain along this variable more often. The maximum bisection depth is still controlled by `i_depth`.

The use of automatic differentiation and Taylor models no longer force a bisection along the corresponding variables. This has to be required explicitly, if actually needed. The name of the parameters also changed:

• `i_bisect_diff x` should be replaced by `i_bisect x, i_autodiff x`.
• `i_bisect_taylor x 3` should be replaced by `i_bisect x, i_taylor x, i_degree 3`.
``````Goal forall x, -1 <= x -> x < 1 + powerRZ x 3.
Proof.
intros. apply Rminus_lt.
interval with (i_bisect x, i_autodiff x).
Qed.
``````

When `i_degree` is not specified, the degree of Taylor models defaults to 10.

The tactics `interval` and `interval_intro` no longer support the use of integrals in place of constants. Instead, some dedicated tactics `integral` and `integral_intro` are provided to prove goals about integrals.

``````(* Ahmed's integral *)
Goal Rabs ((RInt (fun x => atan (sqrt (x*x + 2)) / (sqrt (x*x + 2) * (x*x + 1))) 0 1) - 5/96*PI*PI) <= 1/1000.
Proof.
Fail interval.
integral.
Qed.
``````

In previous releases of CoqInterval, integrals were bounded once and for all, and the computed enclosures were then used to try to prove the goal. In particular, one had to pass the parameters `i_integral_width` or `i_integral_prec` to make sure that the computed enclosures were sufficiently tight to prove the goal. With the `integral` tactic, enclosures of integrals are now refined until the goal is proved or `i_fuel` is exhausted (see below).

While `i_integral_width` and `i_integral_prec` are no longer needed for the `integral` tactic, they are still relevant for `integral_intro`, as there is no goal to prove. These parameters have been renamed into `i_width` and `i_relwidth`.

``````(* integral of atan t / (t * ln^2 t) between 2 and +oo, accurate to 6 decimal digits *)
Goal True.
integral_intro (RInt_gen (fun t => atan t / (t * ln t^2)) (at_point 2) (Rbar_locally p_infty))
with (i_relwidth 20) as HI.
(* HI : 8729100499931700 / 4503599627370496 <= ... <= 8729104739084880 / 4503599627370496 *)
Abort.
``````

The `i_integral_depth` parameter is no longer available, since the `i_fuel` parameter subsumes it. The `integral` tactic now splits the integration domain into the several subdomains, recursively splitting the one that contributes the most to the inaccuracy of the enclosure. The argument of `i_fuel` sets the maximum number of domains in the final subdivision.

Parameter `i_integral_deg` has been renamed into `i_degree`, as it plays the same role as the one from the `interval` tactic.

## Native floating-point support

Thanks to Érik Martin-Dorel and Pierre Roux, CoqInterval now performs computations using the floating-point unit of the processor instead of emulating FP arithmetic with integer computations. This should make proofs that do not need a high precision much faster. Support is enabled as soon as Coq is version 8.11 (or later) and Flocq is version 3.3 (or later).

Passing the `i_prec` parameter to the tactic reverts to emulating floating-point computations. This is especially needed if more than 53 bits of precision are needed to prove a goal.

``````(* integral of sin (t + exp t) between 0 and 8 *)
Goal Rabs ((RInt (fun t => sin (t + exp t)) 0 8) - 3474/10000) <= 1/10.
Proof.
integral with (i_fuel 600, i_prec 30). (* emulated 30-bit FP computations: 33.3s *)
Undo.
integral with (i_fuel 600). (* native FP computations: 3.7s; 9x faster! *)
Qed.

(* the first 51 decimal digits of PI *)
Goal IZR (Raux.Ztrunc (PI * powerRZ 10 50)) = 314159265358979323846264338327950288419716939937510.
Proof.
refine ((fun H => Rle_antisym _ _ (proj2 H) (proj1 H)) _).
interval with (i_prec 170). (* 53 bits of precision are not sufficient, so emulation *)
Qed.
``````

If native floating-point support is not available, the tactics default to `i_prec 53`. The default value was `i_prec 30` in the previous release. This change ensures that most proof scripts should behave in a way that does not depend on whether floating-point arithmetic is native or emulated.

In some corner cases, proofs performed using native floating-point computations might fail despite the needed precision being much lower than 53 bits.

``````Goal forall x, 1 <= 1 + x*x.
Proof.
intros x.
Fail interval with (i_autodiff x). (* failure with native FP computations *)
interval with (i_autodiff x, i_prec 5). (* success with emulation *)
Qed.
``````

Note that future versions of Flocq will presumably no longer provide support for the native floating-point arithmetic of Coq 8.11. Thus, if you are using Coq 8.11, you might need to force the version of Flocq, so as to benefit from hardware computations in CoqInterval:

``````opam install coq-flocq=3.3.1 coq-interval
``````

## Concluding remarks

This post only presents the main changes. There are also numerous minor changes all over the place, which might make porting some proofs from CoqInterval 3 difficult. Hopefully, this should be uncommon.

All the snippets of this post assume the following header:

``````From Coq Require Import Reals.
From Coquelicot Require Import Coquelicot.
From Interval Require Import Tactic.
Open Scope R_scope.
``````

Notice that the main file is no longer named `Interval.Interval_tactic` but just `Interval.Tactic`.

No axioms were hurt in the process. They all come from the standard library of Coq.

1 Like