## Stream: Coq users

### Topic: Comparing real numbers

#### GTR (Jun 27 2022 at 23:05):

Hi all,
I have a very basic question how can we compare two real numbers in coq?
If r1, r2 are real numbers then I cannot use (r1 <? r2) since <? is only defined for natural numbers.
Ideally, I would like to have something like
For r1 r2 :R
..
match (r1 <? r2) with
|true => something
|false => something else

#### Stéphane Desarzens (Jun 28 2022 at 06:01):

You can use `Rlt_dec` for this. Defined in `Coq.Reals.RIneq`.

#### GTR (Jun 28 2022 at 14:20):

Stéphane Desarzens said:

You can use `Rlt_dec` for this. Defined in `Coq.Reals.RIneq`.

Thanks.

#### GTR (Jun 28 2022 at 15:50):

Stéphane Desarzens said:

You can use `Rlt_dec` for this. Defined in `Coq.Reals.RIneq`.

I tried the following

``````Definition a_leq_b (x y : R) : bool:=
match Rlt_dec x y with
|left a =>  true
|right b =>  false
end.
``````

but it did not work as I thought it would. For example:

``````Compute a_leq_b 3.2 5.4
``````

the above is supposed to return "true" but it returns the following.

``````     = if
Rlt_dec
((R1 + R1) * (R1 + (R1 + R1) * ((R1 + R1) * ((R1 + R1) * (R1 + R1)))) *
/ ((R1 + R1) * (R1 + (R1 + R1) * (R1 + R1))))
((R1 + R1) *
((R1 + R1) * (R1 + (R1 + R1) * ((R1 + R1) * (R1 + (R1 + R1))))) *
/ ((R1 + R1) * (R1 + (R1 + R1) * (R1 + R1))))
then true
else false
: bool
``````

#### Gaëtan Gilbert (Jun 28 2022 at 15:56):

you can't compute with R

#### Karl Palmskog (Jun 28 2022 at 18:44):

more precisely, if you want to compute with R, you need to use constructive R from for example CoRN: https://github.com/coq-community/corn

The stdlib does not provide R that one can compute with in the same way as can be done with Z/nat

#### Guillaume Melquiond (Jun 29 2022 at 05:21):

No, as Gaëtan said, you cannot compute with R. Even if you use CoRN, you will not get a proper comparison function that actually computes. You will at best get approximations that behave as follows: "if the result is true then x < y, otherwise y < x + 1".

#### Michael Soegtrop (Jun 29 2022 at 07:42):

There is the tactic `lra` which can evaluate goals like "3.2<5.4" and conclude - as long as a conclusion is possible with linear arithmetic.

As Guillaume wrote, with CoRN a comparison can only be decided with an overlap (the 1 in Guillaume's example), but it can be arbitrary small.

Last updated: Oct 01 2023 at 18:01 UTC