## 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