The 4.6.0 release of Interval comes with two new features.
First, the *_intro tactics as well as their degenerate forms (for tactic-in-term uses) can now represent enclosure bounds using decimal numbers, for extra readability. This feature is enabled by passing the i_decimal option to the tactics.
From Coq Require Import Reals.
From Interval Require Import Tactic.
Open Scope R_scope.
Definition foo x `(3 <= x <= 4) :=
ltac:(root (tan (x/4) = exp (sin x)) with i_decimal).
(* foo: forall x:R, 3 <= x <= 4 -> tan (x / 4) = exp (sin x) ->
3.141592653589374 <= x <= 3.141592653589830 *)
Second, Interval now supports the rounding operators from Flocq, which means that one can use the tactics to formally verify floating-point algorithms. Note that the floating-point model is a bit naive, so enclosures of rounding errors might not be as tight as those that would be proved by Gappa. Nevertheless, the whole machinery of Interval is available for the proofs, e.g., Taylor models. As a consequence, when rounding errors are somehow negligible with respect to method errors, combining both tactics interval and gappa is no longer needed; enclosures can be verified directly using interval.
From Coq Require Import Reals.
From Interval Require Import Tactic.
Open Scope R_scope.
Notation "x = y ± z" := (Rle (Rabs (x - y)) z) (at level 70, y at next level).
From Flocq Require Import Core.
Notation round := (round radix2 (FLT_exp (-1074) 53) ZnearestE).
Definition fadd x y := round (x + y).
Definition fmul x y := round (x * y).
Goal
forall x, -1/256 <= x <= 1/256 ->
let c2 := 9007164895206513 * bpow radix2 (-54) in
fadd 1 (fmul x (fadd 1 (fmul x c2))) = exp x ± 1/100000000.
Proof.
intros x Hx c2.
unfold fadd, fmul, c2.
interval with (i_taylor x).
Qed.