Stream: Coq users

Topic: Simple things I can't get coq-interval to solve

Ana de Almeida Borges (Apr 12 2023 at 14:45):

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?

Laurent Théry (Apr 12 2023 at 18:52):

Usually 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.

Pierre Roux (Apr 12 2023 at 19:47):

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.

Guillaume Melquiond (Apr 13 2023 at 07:00):

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).

Laurent Théry (Apr 13 2023 at 07:03):

something I don´t understood though is why we don't have "round(0 + 0) = 0" with the primitive floats..

Guillaume Melquiond (Apr 13 2023 at 07:05):

You do have it. What you do not have is pred (round (0 + 0)) = 0, which is what interval needs to prove the goal.

Guillaume Melquiond (Apr 13 2023 at 07:05):

(Primitive floats only round to nearest.)

Laurent Théry (Apr 13 2023 at 07:10):

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)]

Guillaume Melquiond (Apr 13 2023 at 07:12):

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