Using result of #eval

Stream: new members

[Kunwar Shaanjeet Singh Grover]

[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]

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

[Arthur Paulino]

(checking)

[Arthur Paulino]

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

def x := add 1 2

#eval x -- 3

[Kunwar Shaanjeet Singh Grover]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kunwar Shaanjeet Singh Grover]

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

[Arthur Paulino]

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

[Kunwar Shaanjeet Singh Grover]

Type maybe?

[Arthur Paulino]

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]

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]

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]

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]

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]

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]

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]

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

[Arthur Paulino]

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]

I love to be surprised by these small discoveries :D

[Marc Huisinga]

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]

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

[Arthur Paulino]

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

[Mario Carneiro]

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]

Type checking a function is not the same as running it

[Mario Carneiro]

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

[Henrik Böving]

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

[Mario Carneiro]

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]

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]

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

[Henrik Böving]

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]

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

[Mario Carneiro]

@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]

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

[Marc Huisinga]

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

[Mario Carneiro]

call by name

[Mario Carneiro]

because it is repeated whnf to match up subterms

[Marc Huisinga]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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?

[Mario Carneiro]

yes

[Mario Carneiro]

this works as expected:

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

-- #eval isSome' foo -- slow

[Marc Huisinga]

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))

[Marc Huisinga]

Ah, I forgot about noinline