Generating `Expr` terms by quoting

Stream: lean4

[Anand Rao]

I have some code operating on terms of the Expr type. I would like to test this with a few examples to see if it is working as intended, but I am facing some difficulty in creating Expr terms.

In Lean3, I could wrap a term e around using a back-quote with parentheses (like this - `(e)) to generate the expression corresponding to e. However, trying the same in Lean4 gives me a complicated term with the Syntax type.

Is there an easy way to convert a term to its corresponding Expr in Lean4? Thanks in advance.

[Jannis Limperg]

Gabriel's quotation library is probably relevant: https://github.com/gebner/quote4

With builtin Lean 4 tools, use elabTerm to elaborate the Syntax you get out of the quotation.

[Anand Rao]

Thank you.

I am having a bit of trouble specifying the expected type to the elabTerm function, since it requires the expected type to be quoted as an expression:

import Lean
open Lean
open Expr
open Elab

/-
If the expression is of the form
A₁ → A₂ → A₃ → … → Aₙ → … → B,
the output of `target` is `B`.

Essentially, it recovers the term at the end of a series of nested implications.
-/
def target : Expr → Expr
  | lam n t b d => target b
  | forallE n t b d => target b
  | e => e

#check Term.elabTerm

example : TermElabM Expr := do
  let s := `(λ (x : Nat) => x + 2)
  let (e : Expr) ← Term.elabTerm s (Option.some sorry)
  return (target e)

Specifically, I do not know how to replace the sorry above with Nat -> Nat (the expected type) quoted as an expression.

[Siddhartha Gadgil]

You can use ← mkArrow (mkConst ``Nat) (mkConst ``Nat) to get Nat -> Nat. You may need to open Meta.

[Siddhartha Gadgil]

There is another issue with let s. Here is a version with the two corrections.

def target : Expr → Expr
  | Expr.lam n t b d => target b
  | Expr.forallE n t b d => target b
  | e => e

#check Term.elabTerm

example : TermElabM Expr := do
  let s ←  `(λ (x : Nat) => x + 2)
  let (e : Expr) ← Term.elabTerm s (Option.some (← mkArrow (mkConst ``Nat) (mkConst ``Nat)))
  return (target e)

[Siddhartha Gadgil]

Another thing: if you are pattern matching on expressions, you should first reduce them (and often take whnf). For instance, you can compare with and without the additional line with reduce in the following.

def target : Expr → Expr
  | Expr.lam n t b d => target b
  | Expr.forallE n t b d => target b
  | e => e

#check Term.elabTerm

def tst : TermElabM Expr := do
  let s ←  `(λ (x : Nat) => x + 2)
  let (e : Expr) ← Term.elabTerm s (Option.some (← mkArrow (mkConst ``Nat) (mkConst ``Nat)))
  let e ←  reduce e
  return (target e)

#eval tst

[Siddhartha Gadgil]

Incidentally, a trick I use to test this by getting a term is to write a small elaborator. In this case it shows a bug (this is code after the above).

elab "tst!" : term => do
  tst

#eval tst!

However I assume this was just an exercise with syntax. If you try to compute the target this way, another issue is that you will have bound variables in the expression, which have no meaning (or the wrong meaning due to de Bruijn indexing) outside their context and so will give an error.

[Anand Rao]

Thank you very much. It turns out that with this fix to the let expression, the elabTermalso accepts Option.none as its second argument (presumably because it has now managed to infer the type of the expression s correctly). I see why my usage of := instead of <- in that example was incorrect.

[Anand Rao]

Thank you for pointing out the issue with the bound variables. In my actual use case (which is to write a small tactic in Lean4), I will be trying to extract the target type (and not the target). Most of my inputs will not be dependent types, so I hope the issues with bound variables do not arise.

[Jannis Limperg]

Anand Rao said:

Most of my inputs will not be dependent types, so I hope the issues with bound variables do not arise.

Note that even just polymorphism requires you to handle dependencies: your target does not work on forall α, List α -> List α. So it's unlikely that you can avoid this complication. You should probably be using forallTelescope or one of its variants.