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
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 by
i_bisect x, i_autodiff x.
i_bisect_taylor x 3should 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.
i_degree is not specified, the degree of Taylor models defaults to 10.
Overhaul of quadrature algorithms
interval_intro no longer support the use of integrals in place of constants. Instead, some dedicated tactics
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_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).
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
(* 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.
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.
i_integral_deg has been renamed into
i_degree, as it plays the same role as the one from the
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).
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
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
No axioms were hurt in the process. They all come from the standard library of Coq.