Regression in 3.4.1 vs 3.4.0 - interval proof not successful
I have a regression of an interval proof (actually quite a few, say 30% of what I have) in 3.4.1 vs 3.4.0.
For 3.4.0 I am using the version of Interval delivered with the Coq 64 bit Windows installer version 8.9.1. For 3.4.1 I used a build which should be identical to the CI artifact of https://github.com/coq/coq/pull/10522 (in progress).
Here is an example Coq script to repdroduce the regression:
Require Import Reals.
Require Import Interval.Interval_tactic.
Require Import List.
Import ListNotations.
Open Scope R_scope.
Fixpoint MakePoly_r (n : nat) (b : nat) (coeff : list R) (x : R) : R :=
match coeff with
| h :: t => h/2^b*x^n + (MakePoly_r (1+n) b t x)
| nil => 0
end.
Definition MakePoly := MakePoly_r 0.
Definition fs x := sin (atan (1 / (x + sqrt (1 + x^2)))).
(* 2nd order approximation in range 0 <= x <= 1/512 *)
Definition fs512_c := [ 3037000500; -1518501474; -377954992 ].
Definition fs512_a := MakePoly 32 fs512_c.
Lemma ErrorBound_fs512_a :
forall x:R, 0 <= x <= 1/512 -> Rabs ( (fs x) - (fs512_a x)) < 1 / (2^34).
Proof.
intros.
unfold fs,fs512_a,fs512_c,MakePoly,MakePoly_r.
Time interval with (i_prec 60, i_depth 5, i_bisect_taylor x 2).
Qed.