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

You can use `Rlt_dec`

for this. Defined in `Coq.Reals.RIneq`

.

Stéphane Desarzens said:

You can use

`Rlt_dec`

for this. Defined in`Coq.Reals.RIneq`

.

Thanks.

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

you can't compute with R

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

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

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: Jun 25 2024 at 18:02 UTC