Zulip Chat Archive

Stream: new members

Topic: Code generation failed error


view this post on Zulip ROCKY KAMEN-RUBIO (May 28 2020 at 17:53):

I'm trying to work with sequences that use the quadratic formula recursively. When I try to have a simple function like below, I get a code generation failed, VM does not have code for 'classical.indefinite_description' error and haven't been able to find anything on why this is happening.

import data.real.basic
import tactic
noncomputable theory
def f :  := (- pn - real.sqrt (pn^2 - 4*qn))/2

#eval f 2 1

view this post on Zulip Chris Hughes (May 28 2020 at 17:55):

Reals in Lean are the actual mathematical definition of the reals, they're not floats or any computable definition. This means you can only prove theorems about them, but not compute with them.

view this post on Zulip Reid Barton (May 28 2020 at 17:56):

If you hadn't written noncomputable theory you'd have to put noncomputable before f, and that would be a clue

view this post on Zulip ROCKY KAMEN-RUBIO (May 28 2020 at 18:18):

Removing the noncomputable theory I get f' is noncomputable, it depends on 'real.division_ring'. Does that mean this just isn't something lean can do?

More context: I'd like to show that a sequence formed by recursively applying functions similar to this eventually produces a complex result. Is that just not something mathlib can support yet?

view this post on Zulip Bryan Gin-ge Chen (May 28 2020 at 18:24):

You could definitely formalize such a theorem about that sequence in Lean. You just can't use #eval on any functions that use real s.

view this post on Zulip Alex J. Best (May 28 2020 at 18:34):

Eval is a very specific thing, if you just want lean to simplify and tell you the answer in a proved manner one can do:

example : f 2 1 = 1 :=
begin
rw f,
conv_lhs{
norm_num,},
end

of course 1 is not the answer, but after norm_num lean has simplified the expression.

view this post on Zulip Jalex Stark (May 29 2020 at 02:52):

to try to cut to the core of the confusion:
how do you expect Lean to do what you've asked? like what algorithm do you expect it to run?
(also I'm guessing you meant to write def f (pn qn : ℝ) : ℝ := (- pn - real.sqrt (pn^2 - 4*qn))/2 in your first message? test your code when you post a question!)


Last updated: May 13 2021 at 19:20 UTC