Trying to understand exprs

Stream: new members

[Joe Palermo]

Hi,

I'm trying to develop a deeper understanding of expr. Would it be fair to say that the following expressions are equivalent?

#check λ {α : Sort 1}, α
#check expr.lam (mk_simple_name "α") binder_info.implicit (expr.sort $ level.succ level.zero) (expr.var 0)

I'm surprised to find that they don't type check to the same thing.

[Jason Rute]

An expression is a meta object in the sense that it is how Lean internally represents things. So the second is the internal representation of the first. They are related but not the same. For example, the first one has type Type -> Type (or at least a type equal to that) and the second has type expr tt (which is the same as expr since the tt is an optional parameter which defaults to true). Note, you can change the first to be an expr with the backquote trick: See here:

This has type Type -> Type
#check λ {α : Sort 1}, α

#check `(λ {α : Sort 1}, α)                 # this has type `reflected (λ {α : Type}, α)` which can be lifted to `expr`
#check (`(λ {α : Sort 1}, α) : expr)   # Here  we lift it to expr

#eval (`(λ {α : Sort 1}, α) : expr).to_raw_fmt.to_string   # we can see this is the desired expression

[Alex J. Best]

Yes I would say the expr on the second line represents the way you've defined a term on the first. But the second is only a syntactic representation so the two lines don't have the same type, as the first is some thing in the type theory, whereas the second is the internal way lean builds these terms.
Indeed if you reflect the first line to an expr using `(term), you can check that they are equal:

#eval to_bool ((`(λ {α : Sort 1}, α) : expr) = expr.lam (mk_simple_name "α") binder_info.implicit (expr.sort $ level.succ level.zero) (expr.var 0))

[Joe Palermo]

Thanks that helps @Jason Rute @Alex J. Best

[Joe Palermo]

So I see now that you can take a term and convert it into an expr by reflecting and lifting it. Can you reverse this process, and turn it back into a term?

[Mario Carneiro]

reflect will do that for some types

[Mario Carneiro]

er, it depends on what you mean by "term"

[Mario Carneiro]

for me "term" = expr

[Mario Carneiro]

I guess you mean the other direction, which means evaluating an expression into a given type. This is also only possible for some types but can be done using eval_expr

open tactic
set_option pp.numerals false
#eval trace (`(23:ℕ):expr) -- bit1 (bit1 (bit1 (bit0 has_one.one)))
#eval trace (reflect 23) -- bit1 (bit1 (bit1 (bit0 has_one.one)))

#eval do
  n : ℕ ← eval_expr ℕ (`(23:ℕ):expr),
  guard (n = 23)

[Joe Palermo]

Perhaps what I'm asking doesn't even make sense, but what I'm really asking is if one can take

(`(λ {α : Sort 1}, α) : expr)

and reverse the reflection + lifting to get back:

λ {α : Sort 1}, α

[Joe Palermo]

(deleted)

[Jason Rute]

In this case, I don't think so. First, you would have to know the type, which is (Type -> Type) and but I don't think eval_expr works with abstract types like that. Here is code which doesn't work:

open tactic
#eval do
  f : (Type -> Type) ← eval_expr (Type -> Type) (`(λ {α : Sort 1}, α) : expr),  -- doesn't work
  return ()

The problem is that Type -> Type is not reflectable. Without getting into the details, these are the sort of types that you can serialize into concrete data, like nat, or list bool. An abstract type like Type -> Type isn't going to work.

[Jason Rute]

Having said that, you are barking up the wrong tree. If I can read past your questions, I think you want to take an expression which is stored in a file and check that it is a valid proof. If that is correct, you can do that with infer_type:

#eval do
  let e := (`(λ {α : Sort 1}, α) : expr),
  tp <- tactic.infer_type e,  -- this is valid
  tactic.trace tp

#eval do
  let e := (expr.lam (mk_simple_name "α") binder_info.implicit (expr.sort $ level.succ level.zero) (@expr.var tt 0)),
  tp <- tactic.infer_type e,  -- this is valid
  tactic.trace tp

#eval do
  let e := (expr.lam (mk_simple_name "α") binder_info.implicit (expr.sort $ level.succ level.zero) (@expr.var tt 1)),
  tp <- tactic.infer_type e,  -- this is not valid, so it fails at this line
  tactic.trace tp

[Jason Rute]

I don't know how #check works exactly, but I'm pretty sure it uses infer_type or similar underneath.

[Jason Rute]

For your sort of projects, it is fine to work with expressions, instead of the objects they encode.

[Joe Palermo]

Thanks @Jason Rute. I was asking more out of pure curiosity than anything else, but yes that's right.

[Jason Rute]

Sorry, I likely jumped to the wrong conclusion then.

[Joe Palermo]

@Jason Rute No worries, it made me think and these examples are very helpful to see. Much appreciated.

[Joe Palermo]

Actually I'm wondering how make this one typecheck:

#eval do
  let e := (expr.lam (mk_simple_name "b") binder_info.implicit (expr.const bool [])
            (expr.app
              (expr.app
              (expr.app (expr.const eq.mp [level.zero])
                (expr.app (expr.const not []) (expr.app (expr.app (expr.app (expr.const eq [level.succ level.zero]) (expr.const bool [])) (@expr.var tt 0)) (expr.const bool.tt []))))
              (expr.app (expr.app (expr.app (expr.const eq [1]) (expr.const bool [])) (@expr.var tt 0)) (expr.const bool.ff [])))
              (expr.app (expr.const eq_ff_eq_not_eq_tt []) (@expr.var tt 0)))),
  tp <- tactic.infer_type e,  -- this is valid
  tactic.trace tp

Lean is complaining about the use of expr.const for some reason. Btw this proof corresponds to:

λ {b : bool}, @eq.mp.{0} (not (@eq.{1} bool b bool.tt)) (@eq.{1} bool b bool.ff) (eq_ff_eq_not_eq_tt b)

I simply printed this proof in raw_fmt, added expr prefixes and copied a few other things from the previous example (like using "@expr.var tt 0" instead of "expr.var 0") to try and get it to type check.

[Alex J. Best]

docs#expr.const needs a name as input whereas you are providing the literal term, you just have to prefix everything with a backtick to make this work though

import tactic
#eval do
  let e := (expr.lam (mk_simple_name "b") binder_info.implicit (expr.const `bool [])
            (expr.app
              (expr.app
              (expr.app (expr.const `eq.mp [level.zero])
                (expr.app (expr.const `not []) (expr.app (expr.app (expr.app (expr.const `eq [level.succ level.zero]) (expr.const `bool [])) (@expr.var tt 0)) (expr.const `bool.tt []))))
              (expr.app (expr.app (expr.app (expr.const `eq [level.succ level.zero]) (expr.const `bool [])) (@expr.var tt 0)) (expr.const `bool.ff [])))
              (expr.app (expr.const `eq_ff_eq_not_eq_tt []) (@expr.var tt 0)))),
  tp <- tactic.infer_type e,  -- this is valid
  tactic.trace tp