Hello. I'm playing with coq-interval and am kind of surprised it can't solve some goals, to the point I'm wondering whether I'm missing something. For example, it doesn't seem able to deal with
0 <= 0 + 0:
From Coq Require Import Reals. From Interval Require Import Tactic. Open Scope R_scope. Goal 0 <= 0 + 0. Fail interval. Abort.
Is this some weird consequence of addition on the reals or something?
interval is not very good at proving large inequality where equality can actually happen. In your case, It seems that it is making a small rounding error when adding two constant intervals as you can seen when doing
interval_intro (0 + 0). Anyway, @Guillaume Melquiond will tell us more about this.
Indeed, rounding errors, are the explanation. Changing the precision to use emulated floats instead of primitive floats is enough to solve the goal (with just 1 bit of precision):
Goal 0 <= 0 + 0. Proof. interval with (i_prec 1). Qed.
Just to stress Pierre's answer, the important point is the "emulated floats" part; it would work with any precision that is large enough (which is >= 1 in this trivial case).
something I don´t understood though is why we don't have "round(0 + 0) = 0" with the primitive floats..
You do have it. What you do not have is
pred (round (0 + 0)) = 0, which is what
interval needs to prove the goal.
(Primitive floats only round to nearest.)
ok now I understand, it is because you only have rounding to nearest that you create the interval
[pred(round(0 + 0)), succ(round (0+ 0)]
Right. And it might even be worse than that, since the
0 input itself was presumably overestimated when enclosed into an interval.
Last updated: Oct 04 2023 at 22:01 UTC