# Zulip Chat Archive

## Stream: new members

### Topic: safe version of evalExpr

#### Caroline (Jul 31 2023 at 14:17):

I noticed that `Lean.Meta.evalExpr`

is marked `unsafe`

, even when its `safety`

parameter is set to safe.

Is there a safe version of it I can use to safely evaluate arbitrary `Expr`

s or `Term`

s, which rejects unsafe inputs?

#### Kyle Miller (Jul 31 2023 at 14:32):

The `unsafe`

keyword means that it's a function that can't be used for mathematics, and the `safety`

parameter has to with whether what's being evaluated is using only mathematically meaningful definitions. Is that the kind of safety you are interested in?

#### Kyle Miller (Jul 31 2023 at 14:34):

The issue is that while `evalExpr`

evaluates expressions it's mathematically unsafe to depend on the results. It's possible to use it to create terms of empty types.

#### Eric Wieser (Jul 31 2023 at 14:35):

I don't think it's actually true that you can do that, is it?

#### Eric Wieser (Jul 31 2023 at 14:36):

The unsafeness is ultimately inherited from docs#Lean.Environment.evalConst

#### Kyle Miller (Jul 31 2023 at 14:51):

@Eric Wieser Maybe I don't have an example where you can literally get a term of an empty type, but this is definitely not good:

```
import Lean
def nAux := 1
@[implemented_by nAux]
def n := 0
unsafe def xAux : Fin n ⊕ Bool :=
if h : n = 1 then
Sum.inl ⟨0, by cases h⟩
else
Sum.inr true
@[implemented_by xAux]
def x : Fin n ⊕ Bool := Sum.inr true
#eval x
-- Sum.inl 0
open Lean Meta Elab Term
#eval do
evalExpr
(Fin n ⊕ Bool)
(expectedType := ← elabTerm (← `(Fin n ⊕ Bool)) none)
(value := ← elabTerm (← `(x)) none)
(safety := .safe)
-- Sum.inl 0
```

#### Kyle Miller (Jul 31 2023 at 14:53):

Eric Wieser said:

The unsafeness is ultimately inherited from docs#Lean.Environment.evalConst

Sure, because `evalExpr`

is a thin wrapper around it.

#### Kyle Miller (Jul 31 2023 at 14:53):

You can make a "safe" version of these by requiring that the result be `Inhabited`

, but I'm not sure this is the kind of safety that @Caroline is interested in.

#### Kyle Miller (Jul 31 2023 at 14:58):

```
unsafe def evalExprAux' (α) [Inhabited α] (expectedType : Expr) (value : Expr)
(safety := DefinitionSafety.safe) : MetaM α := evalExpr α expectedType value safety
/-- A "safe" version of `evalExpr`. -/
@[implemented_by evalExprAux']
opaque evalExpr' (α) [Inhabited α] (expectedType : Expr) (value : Expr)
(safety := DefinitionSafety.safe) : MetaM α
```

#### Caroline (Jul 31 2023 at 15:12):

Huh, that does work, but why does the type need to be inhabited?

I would like a way to call the core Lean interpreter on some arbitrary expression with an expected type, and get either a value of that type or an error.

Something in which I could procedurally feed expressions as syntax trees.

#### Kyle Miller (Jul 31 2023 at 15:18):

Inhabited means there's a term of that type, so `evalExpr'`

can theoretically be constructed. Then with `implemented_by`

you can give it an unrelated definition that is used by `eval`

. The `opaque`

keyword means that while it's theoretically safe to work with `evalExpr'`

, theorems can't see the definition.

#### Kyle Miller (Jul 31 2023 at 15:18):

Do you have a specific list of types you care about, or do you want to handle arbitrary types?

#### Caroline (Jul 31 2023 at 15:20):

I would like to handle arbitrary types.

This includes theorems, and theorems whose provability is unknown, so I can't restrict myself to inhabited types; though maybe wrapping them inside `Either · SomeError`

would be what I want then?

#### Kyle Miller (Jul 31 2023 at 15:23):

It's not really meaningful to `eval`

theorems. Propositions don't get evaluated, they're "computationally irrelevant"

#### Kyle Miller (Jul 31 2023 at 15:24):

By the way, here's a bit more convenient of a frontend to `evalExpr`

:

```
import Mathlib.Tactic.ToExpr
open Lean
unsafe def evalExpr' (α) [ToExpr α] (value : Expr) : MetaM α :=
Meta.evalExpr α (ToExpr.toTypeExpr α) value
```

#### Kyle Miller (Jul 31 2023 at 15:24):

`ToExpr`

is a class for reflecting values and types to `Expr`

s. Not everything can be reflected, notably functions.

#### Kyle Miller (Jul 31 2023 at 15:25):

There's also

```
unsafe def evalExpr'' (α) [ToExpr α] (value : Expr) : MetaM Expr := do
let val ← Meta.evalExpr α (ToExpr.toTypeExpr α) value
return toExpr val
```

if you want an `Expr`

#### Caroline (Jul 31 2023 at 16:05):

well, i'm thinking of things like for example demanding a `∃ x : Nat, x > 2^something ∧ prime x`

and then also *obtaining* that `x`

But I guess that can be not a thing because of law of excluded middle producing "uncomputable" disjunctions ?

#### Kevin Buzzard (Jul 31 2023 at 16:26):

If you prove `h : ∃ x : Nat, P x`

in Lean then the term `h`

has forgotten what `x`

was; if you could computably extract `x`

from `h`

then you could prove `∃ x : Nat, P x`

in two different ways (which would be equal according to Lean's type theory, because if `Q : Prop`

and `a : Q`

and `b : Q`

then `a = b`

and the proof is `rfl`

) and then get a contradiction by extracting out different data from the two equal proofs.

#### Eric Wieser (Jul 31 2023 at 17:00):

docs#Nat.find can give you the minimal such x

#### Mario Carneiro (Aug 01 2023 at 03:39):

Kyle Miller said:

The issue is that while

`evalExpr`

evaluates expressions it's mathematically unsafe to depend on the results. It's possible to use it to create terms of empty types.

I don't think that's the only reason it's unsafe. You can get an element of `Empty`

by lying about the type:

```
evalExpr
Empty
(expectedType := .const ``Unit [])
(value := .const ``Unit.unit [])
(safety := .safe)
```

and even if you match the type up you can get in trouble if the environment at run time (i.e. the one in the `MetaM`

state) does not match the one at compile time, because the `α`

is resolved using the types available at compile time while `expectedType`

is resolved at run time.

#### Niels Voss (Aug 01 2023 at 05:58):

well, i'm thinking of things like for example demanding a

`∃ x : Nat, x > 2^something ∧ prime x`

and then alsoobtainingthat`x`

But I guess that can be not a thing because of law of excluded middle producing "uncomputable" disjunctions ?

Because Lean is proof-irrelevant (see Kevin Buzzard's message above), a proof `h : ∃ x : Nat, x > 2^something ∧ prime x`

does not contain any data whatsoever on how to construct `x`

. Your options are essentially:

- Use
`Nat.find h`

(as mentioned above) to find the lowest possible such`n`

. This is computable, but only works on`Nat`

. I think using this to produce a value amounts to checking every single`Nat`

starting at`0`

to see if it is prime and greater than`2 ^ something`

, which could get very slow. - If you have a proof
`h : ∃ x : Nat, x > 2^something ∧ prime x`

, then you can use`Classical.choose h`

(previously called`classical.some`

) to produce such an`x`

using the axiom of choice.`Classical.choose_spec h`

is a proof that`Classical.choose h`

is prime and greater than`2 ^ something`

. Note that if the computer doesn't actually know how to calculate such an`x`

and if you use`Classical.choose`

in a`def`

you will need to mark it as noncomputable. - Create a function
`f : Nat -> Nat`

which takes in`z : Nat`

and outputs a prime`x`

. You can then prove that for all`z`

,`f z > 2 ^ z`

and for all`z`

,`prime (f z)`

. This is usually the best option if you are doing a constructive proof. - Create a function
`f : (z : Nat) -> {x : Nat // x > 2 ^ z ∧ prime x}`

. This is just the previous option but with the proof and function combined into one. You can think of the subtype`{x : Nat // x > 2 ^ z ∧ prime x}`

as just being the computable version of`∃ x : Nat, x > 2 ^ z ∧ prime x`

. In fact, the definitions of`Subtype`

and`Exists`

are almost exactly the same, with the only difference being that`Exists`

lives in`Prop`

.

Last updated: Dec 20 2023 at 11:08 UTC