The CoqInterval library provides tactics for simplifying the proofs of inequalities on expressions of real numbers, for Coq 8.8 and later. See http://coqinterval.gforge.inria.fr/ for the documentation. As usual, it is available as the coqinterval
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 multidimensional. 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 byi_bisect x, i_autodiff x
. 
i_bisect_taylor x 3
should be replaced byi_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.
Overhaul of quadrature algorithms
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 floatingpoint support
Thanks to Érik MartinDorel and Pierre Roux, CoqInterval now performs computations using the floatingpoint 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 floatingpoint 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 30bit 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 floatingpoint 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 floatingpoint arithmetic is native or emulated.
In some corner cases, proofs performed using native floatingpoint 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 floatingpoint 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 coqflocq=3.3.1 coqinterval
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.