safe version of evalExpr

Stream: new members

[Caroline]

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 Exprs or Terms, which rejects unsafe inputs?

[Kyle Miller]

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]

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]

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

[Eric Wieser]

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

[Kyle Miller]

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

Eric Wieser said:

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

Sure, because evalExpr is a thin wrapper around it.

[Kyle Miller]

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]

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]

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]

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]

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

[Caroline]

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]

It's not really meaningful to eval theorems. Propositions don't get evaluated, they're "computationally irrelevant"

[Kyle Miller]

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]

ToExpr is a class for reflecting values and types to Exprs. Not everything can be reflected, notably functions.

[Kyle Miller]

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]

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]

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]

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

[Mario Carneiro]

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]

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 ?

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.