Zfloor: reasonable bounds without i_prec but rather bad bounds when i_prec 1000 is given
I have a weird case with Zfloor:
Require Import Interval.Tactic.
Require Import Reals.
Require Import Lra.
Open Scope R.
(* Try goal with interval *)
Example Interval_fail: forall (x:R), 0 <= x <= 1000 ->
0 <= (x - IZR (Raux.Zfloor x)) <= 1.
Proof.
intros x Hx.
interval_intro (x - IZR (Raux.Zfloor x)).
(* This one is very weird - it gives
-1000 <= x - IZR (Raux.Zfloor x) <= 1000 *)
interval_intro (x - IZR (Raux.Zfloor x)) with (i_prec 20).
(* This even more - it should be better than with default precision *)
interval_intro (x - IZR (Raux.Zfloor x)) with (i_prec 1000).
interval_intro (x - IZR (Raux.Zfloor x)) with (i_bisect x).
interval_intro (x - IZR (Raux.Zfloor x)) with (i_bisect x, i_prec 20).
interval_intro (x - IZR (Raux.Zfloor x)) with (i_taylor x).
interval_intro (x - IZR (Raux.Zfloor x)) with (i_taylor x, i_prec 20).
nra.
Qed.
All cases behave as expected, except the second and third one, which give a bound of -1000 <= term <= 1000
.