0
$\begingroup$

My lean4 code:

def f (x : Real) : Real := x
#check f
#eval f 3  -- works

noncomputable def g (x : ℝ) : ℝ := 1 / x
#check g
#eval g 3  -- fails

but the second fails although it would work for x=3. Why and how do I fix this?

error

compiler IR check failed at '_eval', error: unknown declaration 'g'
$\endgroup$

3 Answers 3

2
$\begingroup$

I was told

noncomputable means pretty much exactly “cannot eval/compile”. you can only prove things about them 5:10 so you could prove it equals 1/3 or reduce it or use tactics like normnum but no eval

$\endgroup$
1
$\begingroup$

In Lean, the real numbers are defined as quotients of Cauchy sequences or something like that, so they don't really have a good machine representation to compute with. In Python, math.pi is a floating point number that is approximately equal to $\pi$, but not exactly. Even 0.1 in Python isn't exactly equal to $1/10$ and that can lead to all sorts of headaches, especially in accounting software. But in Lean, you need, say, Real.pi to be the true number $\pi$, 1/3 to be the true rational $1/3$, and 0.1 to be the true decimal 1/10, so that means you can't use floating point numbers, or really any finite computable representation of the reals.

Since the definitions for the operations on the reals like division use the axiom of choice, any definition using them can't be compiled to executable code and needs to be marked noncomputable. (Why does real division use the axiom of choice? You can't programmatically decide if a real number is zero or not from its Cauchy sequence. It might be zero, or it might be just really close to zero. So one needs to use the axiom of choice to decide this.) The short answer is that you shouldn't use Real for computation in the compiler or interpreter (#eval), nor does rfl usually work for reals. But, many tactics like norm_num are really good at "symbolic computation" where they symbolically reduce the Lean expression, so you can prove say Real.pi / 2 * 2 = Real.pi with norm_num.


I'm a bit surprised at the error message you are getting. The error message in Lean 4.6.0 is a bit better now:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'g', and it does not have executable code

It still doesn't say that #eval isn't working since your definition is non-computable, but it suggests non-computability is a concern. What it is sort of saying is that it can't compile the code you are trying to evaluate.

Also, I'm a bit surprised that your #eval f 3 works. It gives the same output as #eval (3 : Real), but as you can see the "output" is an infinite Cauchy sequence, so not really something useful for computation.

Real.ofCauchy (sorry /- 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, ... -/)
$\endgroup$
1
$\begingroup$

The answer is that it can't be fixed, since equality of real numbers is not decidable. A Cauchy sequence which does not converge to 0 has (in Lean) a simple definition of the inverse, which is to apply the inverse pointwise to each term in the Cauchy sequence. Because the reciprocal is continuous at all points other than 0, this will work for such points. It also doesn't take much to see that this preserves equivalence under the quotient. However, consider the sequence $a_n = \frac{(-1)^n}{n}$. This sequence is Cauchy, and it converges to 0, but applying the reciprocal to each term in the sequence gives a sequence which diverges. However, there's no way to compute whether any arbitrary Cauchy sequence converges to 0, and so no way to actually compute this function. The first example works because of how Lean treats quotients and definitional equality - the result of the function is definitionally equal to the real number 3. I'm not sure if this would also work for addition, subtraction, etc. on real numbers, which are also computable functions.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.