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 xshould be replaced byi_bisect x, i_autodiff x. -
i_bisect_taylor x 3should 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 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.