## Stream: new members

### Topic: Using result of #eval

#### Kunwar Shaanjeet Singh Grover (Jan 31 2022 at 17:36):

[Lean3]

Hi! Is it possible to obtain the result of the evaluation and use it further? What would be the best way to do something like this:

def add (a : nat) (b : nat) : nat :=
a + b

def x := #eval add 1 2

#### Arthur Paulino (Jan 31 2022 at 17:37):

def x := add 1 2 should work :thinking:

(checking)

#### Arthur Paulino (Jan 31 2022 at 17:38):

def add (a : nat) (b : nat) : nat :=
a + b

def x := add 1 2

#eval x -- 3

#### Kunwar Shaanjeet Singh Grover (Jan 31 2022 at 17:39):

Yes, that works. But I want to eval it in between and then use it. Maybe I did not take a great example for this. But I would like to evaluate it before the assignment to x and use the result. Although I'm not sure if lean3 can do this.

#### Kunwar Shaanjeet Singh Grover (Jan 31 2022 at 17:39):

I was looking for something general to obtain the result of instructions like #reduce, #eval, #check.

#### Mario Carneiro (Jan 31 2022 at 17:40):

There isn't a packaged tactic for it but you can write one

#### Mario Carneiro (Jan 31 2022 at 17:41):

you can use tactic.eval_expr to evaluate the expression and then reflect e to turn it back into something that can be fed to exact

#### Mario Carneiro (Jan 31 2022 at 17:41):

That does #eval. For #reduce the nearest approximation is whnf e on the input

#### Mario Carneiro (Jan 31 2022 at 17:42):

For #check there is nothing to be done, that's just exact

#### Kunwar Shaanjeet Singh Grover (Jan 31 2022 at 17:43):

Right. I will look at this. Thanks a lot! I love how the community responds so fast <3

#### Arthur Paulino (Jan 31 2022 at 17:44):

Out of curiosity, what would be the type of #check add (for the application you're interested)?

Type maybe?

#### Arthur Paulino (Jan 31 2022 at 17:54):

I see. Just to make sure you're aware, you won't be able to prove results about your definitions if they use the meta keyword:

meta def my_meta_def := 1
example : my_meta_def = 1 := rfl
-- invalid definition, it uses untrusted declaration 'my_meta_def'

#### Arthur Paulino (Jan 31 2022 at 18:59):

Arthur Paulino said:

def x := add 1 2 should work :thinking:

Wait, now I'm confused. Isn't this already evaluating add 1 2 before assigning it to x? Or is Lean lazy?

#### Patrick Johnson (Jan 31 2022 at 20:46):

Wait, now I'm confused. Isn't this already evaluating add 1 2 before assigning it to x? Or is Lean lazy?

Informally speaking, Lean is lazy for terms, but eager for types:

def N := 10000

def x := 0 + N * N
#check x -- succeeds

def y := (rfl : N * N = 0 + N * N)
#check y -- deep recursion error

#### Marc Huisinga (Jan 31 2022 at 21:10):

Lean's evaluation semantics are not lazy. The following (Lean 4 code) loops infinitely:

partial def infiniteLoop (n : Nat) : Nat := infiniteLoop (n + 1)

-- some complex function to avoid inlining
def foo (n a b : Nat) : Nat :=
match n with
| 0 => a
| n + 1 => foo n a b

#eval foo 10 1 (infiniteLoop 2) -- loops

I think the same is true for Lean 3?

#### Mario Carneiro (Jan 31 2022 at 21:16):

What I suggested is a way of "macro-expanding" the definition of the term, kind of like what you would get with a C++ constexpr function call. The evaluation semantics are the same either way, but one produces def f := add 1 2 and the other produces def f := 3

#### Mario Carneiro (Jan 31 2022 at 21:17):

This is usually not necessary, and Lean 4 will automatically precompute closed terms (although I think the computation still happens, once, at runtime)

#### Mario Carneiro (Jan 31 2022 at 21:18):

additionally it has the disadvantage that f will unfold to 3 instead of add 1 2 which is bad if you have some property of f you want to prove based on the properties of add

#### Mario Carneiro (Jan 31 2022 at 21:19):

since we've just generated a different term there isn't an equality proof add 1 2 = 3 to use either

#### Arthur Paulino (Jan 31 2022 at 21:24):

Before this thread I thought that this code would loop:

partial def infiniteLoop (n : Nat) : Nat := infiniteLoop n + 1

def bar := 1 + infiniteLoop 2 -- doesn't loop

But it only loops if I do #eval bar

#### Arthur Paulino (Jan 31 2022 at 21:26):

I love to be surprised by these small discoveries :D

#### Marc Huisinga (Jan 31 2022 at 21:28):

Arthur Paulino said:

Before this thread I thought that this code would loop:

partial def infiniteLoop (n : Nat) : Nat := infiniteLoop n + 1

def bar := 1 + infiniteLoop 2 -- doesn't loop

But it only loops if I do #eval bar

OTOH, #reduce bar doesn't loop :-)

#### Marc Huisinga (Jan 31 2022 at 21:30):

... which is because of Lean not even unfolding infiniteLoop since it's partial, I think

#### Arthur Paulino (Jan 31 2022 at 21:31):

Makes sense! Indeed infiniteLoop 2 is there in the output of #reduce

#### Mario Carneiro (Jan 31 2022 at 21:32):

Arthur Paulino said:

Before this thread I thought that this code would loop:

partial def infiniteLoop (n : Nat) : Nat := infiniteLoop n + 1

def bar := 1 + infiniteLoop 2 -- doesn't loop

But it only loops if I do #eval bar

How could it loop if you don't run it?

#### Mario Carneiro (Jan 31 2022 at 21:32):

Type checking a function is not the same as running it

#### Mario Carneiro (Jan 31 2022 at 21:33):

in fact lean tries to do as little evaluation as it possibly can during typechecking

#### Henrik Böving (Jan 31 2022 at 21:34):

In which scenarios during type checking do you have to do evaluation?

#### Mario Carneiro (Jan 31 2022 at 21:34):

An example where lean would be forced to run the function is if you did something like

partial def infiniteLoop (n : Nat) : Nat := infiniteLoop n + 1

example : 1 + infiniteLoop 2 = 3 := rfl

#### Mario Carneiro (Jan 31 2022 at 21:35):

basically, lean has to unfold things in order to avoid a type error (here, we're using a proof of a = a to prove a = b so lean has to work out that a and b are actually the same thing)

#### Arthur Paulino (Jan 31 2022 at 21:35):

Yeah I sometimes mix concepts. In Python, bar = 1 + infinite_loop(2) would loop forever. But def introduces a function instead.

#### Henrik Böving (Jan 31 2022 at 21:36):

Mario Carneiro said:

An example where lean would be forced to run the function is if you did something like

partial def infiniteLoop (n : Nat) : Nat := infiniteLoop n + 1

example : 1 + infiniteLoop 2 = 3 := rfl

I thought you cant prove anything about partial functions in this way?

#### Mario Carneiro (Jan 31 2022 at 21:36):

The equivalent of bar = 1 + infinite_loop(2) in lean is let bar := 1 + infinite_loop 2as part of an #eval block

#### Mario Carneiro (Jan 31 2022 at 21:37):

@Henrik Böving Right, I was getting to that. For partial functions, they look like constants so they simply fail to unfold and that rfl would be rejected as a type error

#### Mario Carneiro (Jan 31 2022 at 21:37):

same thing if infiniteLoop was marked as an @[irreducible] def or constant

#### Marc Huisinga (Jan 31 2022 at 21:38):

@Mario Carneiro Semi-related; in which order does the kernel roughly reduce terms?

call by name

#### Mario Carneiro (Jan 31 2022 at 21:39):

because it is repeated whnf to match up subterms

#### Marc Huisinga (Jan 31 2022 at 21:39):

Ah, so I guess you could call that lazy then :)

#### Mario Carneiro (Jan 31 2022 at 21:40):

yeah, it's a very different "evaluation strategy" than the usual

#### Mario Carneiro (Jan 31 2022 at 21:40):

it's not even really evaluation, since it's actually going for unification of terms and will bail out as soon as it can

#### Mario Carneiro (Jan 31 2022 at 21:44):

Here's an example to show that lean does not fully evaluate terms if it can help it

def reallySlow : Nat  Bool
| 0 => true
| n+1 => reallySlow n

def foo := some (reallySlow (10^10))

-- #eval foo -- slow
example :  a, foo = some a := _, rfl -- fast
example : foo.isSome := rfl -- fast

#### Henrik Böving (Jan 31 2022 at 21:46):

Funky that this even works with the _ (before the edit) how does Lean figure out a value for the _? Does it just try the first constructor that's directly a value (i.e. not a function)?

#### Mario Carneiro (Jan 31 2022 at 21:48):

It does unification to find the _. It solves it to reallySlow (10^10) btw, not true

#### Mario Carneiro (Jan 31 2022 at 21:49):

It does this:

foo =?= some ?a
-> unfold foo
some (reallySlow (10^10)) =?= some ?a
-> some is a constructor, so apply congr
reallySlow (10^10) =?= ?a
-> assign ?a := reallySlow (10^10)

#### Mario Carneiro (Jan 31 2022 at 21:50):

By the way, I was going to write #eval foo.isSome -- slow in that example but the compiler is too smart and is spoiling my example

#### Marc Huisinga (Jan 31 2022 at 21:50):

Mario Carneiro said:

Here's an example to show that lean does not fully evaluate terms if it can help it

def reallySlow : Nat  Bool
| 0 => true
| n+1 => reallySlow n

def foo := some (reallySlow (10^10))

-- #eval foo -- slow
example : foo.isSome := rfl -- fast

#eval foo.isSome is also fast ... Probably because of inlining or something similar?

yes

#### Mario Carneiro (Jan 31 2022 at 21:51):

this works as expected:

@[noinline] def isSome' : Option α  Bool
| some _ => true
| none   => false

-- #eval isSome' foo -- slow

#### Marc Huisinga (Jan 31 2022 at 21:53):

Adjusting my example from earlier too:

def longLoop : Nat  Nat
| 0 => 0
| n + 1 => longLoop n

-- some complex function to avoid inlining
def foo (n a b : Nat) : Nat :=
match n with
| 0 => a
| n + 1 => foo n a b

#eval foo 10 1 (longLoop (10^10))