Real.ofCauchy issue + understanding of uncomputable

Stream: mathlib4

[Bach Hoang]

Hi,
Here is some code that I wrote in Lean

def  f (t : ℝ) : ℝ := 2 * t
#eval f 2
#eval f 2 > 3

In line 2, I notice that Lean showed me Real.ofCauchy (sorry /- 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, ... -/) and in Line 3 showed me an error : "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.decidableLT', and it does not have executable code"

I wonder why #eval returns the value of f(2) to a Real.ofCauchy (I wonder if this showed as a Cauchy sequence) and if it is the reason that it cannot compare with a real value in line 3.

In addition, I want to understand more about 'Real.decidableLT' and 'noncomputable' as I want to change the value of f(2) to real numbers to compare with other real values

Please correct me if I have any false statements.
Thanks

[Notification Bot]

This topic was moved here from #lean4 > Real.ofCauchy issue + understanding of uncomputable by Jireh Loreaux.

[Jireh Loreaux]

When you ask lean to #eval something, you are asking it to actually compute the result. The issue is that docs#Real.decidableLT involves the law of excluded middle, which is noncomputable.

Think about it this way: let's say I give you two Cauchy sequences x y : ℕ → ℚ. Can you provide an algorithm which will determine whether Real.ofCauchy x < Real.ofCauchy y? Note that this is equivalent to ∃ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x n < y n.

The answer is: no, you can't. The idea being that you have no information about how fast each Cauchy sequence settles down. No matter how far out you go in each sequence, and no matter the behavior of the sequences up to that point, it may be the case that somewhere past that point the behavior of the sequences changes.

[Yury G. Kudryashov]

Even if we rewrite the definition so that the sequences converge at predictable rate (e.g., we require that |x i - x j| < 1 / 2^n whenever i > n and j > n), this won't be enough. You start computing the sequence, and you get 0 all the time. When should you stop and say "OK, now I'm sure that it's not positive"? What if the next term is 1 / 2^(n + 1)?

[Bach Hoang]

I have tried to change that function from R to N and everything works. What is the difference between R and N when representing in Lean?

[Giacomo Stevanato]

Bach Hoang said:

I have tried to change that function from R to N and everything works. What is the difference between R and N when representing in Lean?

N is represented as a simple inductive type where every number is uniquely identified by being either 0 or the successor of some other natural number. This is much better for algorithms than an infinite sequence like Cauchy's

[Bach Hoang]

Giacomo Stevanato said:

Bach Hoang said:

I have tried to change that function from R to N and everything works. What is the difference between R and N when representing in Lean?

N is represented as a simple inductive type where every number is uniquely identified by being either 0 or the successor of some other natural number. This is much better for algorithms than an infinite sequence like Cauchy's

Ah I see. Thank you. But what if I want to perform relations between reals such as x > y in Lean. What should I do then ?

[Kevin Buzzard]

You can use x > y just fine -- for example, in a proof -- you just can't #eval it.