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