Expr antiquotations

Stream: lean4

[Mario Carneiro]

Is there a syntax for interpolating an Expr into a Syntax for use in elabTerm? In lean 3 you could do this using the %% notation, and it would generate an as_is macro in the pre-expression. Is there an analogue in lean 4? Some random grepping didn't show anything relevant, but I can't imagine this is not done somewhere in lean already.

[Sebastian Ullrich]

No, this is in fact not done in Lean already. We anticipated we might need it, but then it just didn't come up even once. Can you use an mvar/fvar to represent the term in your use case?

[Gabriel Ebner]

This is indeed more complicated. A common trick is to assign the expression to a metavariable, and then put the metavariable into the syntax:

let mvar ← elabTerm `(?m) none
assignExprMVar mvar.mvarId! myExpr
`( ... ?m ...)

[Gabriel Ebner]

This trick only works if you share the same metavar context though. It won't work if you generate command syntax for example.

[Mario Carneiro]

Oh, that's a useful trick. I guess it could even be wrapped up into a antiquoteExpr : Expr -> TermElabM Syntax function

[Ian Benway]

I'm trying to use the trick above but I'm getting a bit confused. If I wanted to do something like

def foo : Expr → TacticM Expr
| `(%%a < %%b) => pure $ mkApp (mkConst ``coolFunc) a
| `(%%a > %%b) => pure $ mkApp (mkConst ``coolFunc) b
| e => throwError ":)"

what would that look like?

[Arthur Paulino]

I think Gabriel's lib (quote4) might be helpful

[Dan Velleman]

This looks like a very useful trick, but I don't quite understand it. In let mvar ← elabTerm `(?m) none, what is `(?m)? It looks like it's supposed to be Syntax for a metavariable, but when I try using this command in a tactic I get an error message about the argument to elabTerm being the wrong type--it has type ?m.3004 Syntax but is expected to have type Syntax. What am I doing wrong?

[Henrik Böving]

Dan Velleman said:

This looks like a very useful trick, but I don't quite understand it. In let mvar ← elabTerm `(?m) none, what is `(?m)? It looks like it's supposed to be Syntax for a metavariable, but when I try using this command in a tactic I get an error message about the argument to elabTerm being the wrong type--it has type ?m.3004 Syntax but is expected to have type Syntax. What am I doing wrong?

the `(?m) quotation syntax is in fact a monadic function due to hygiene, if you want to obtain the syntax from it you have to bind on the variable so e.g.

let foo <- `(Nat.add 1 2)

will, if you are working in a monad that implements docs4#Lean.MonadQuotation, let foo have type Syntax, in this specific use case you might also consider to bind inline or w/e.

[Dan Velleman]

Thanks Henrik. That seems to work.

[Mac]

Henrik Böving said:

the `(?m) quotation syntax is in fact a monadic function due to hygiene, if you want to obtain the syntax from it you have to bind on the variable so e.g.

let foo <- `(Nat.add 1 2)

Note that if you don't need hygiene, there is docs4#Lean.Unhygienic to get pure synax:

let foo := Lean.Unhygienic.run `(Nat.add 1 2)

[Dan Velleman]

It looks like this trick won't help with the application I have in mind. In Lean 3, it was possible to write a tactic like this:

meta def tactic.interactive.dm
        (h : interactive.parse lean.parser.ident) : tactic unit :=
do H ← get_local h,
  t ← tactic.infer_type H,
  match t with
    | ‵(¬(%%l ∧ %%r)) := tactic.interactive.have none ‵‵(¬ %%l ∨ ¬ %%r) ‵‵(not_and_distrib.mp %%H)
    | ‵(¬(%%l ∨ %%r)) := tactic.interactive.have none ‵‵(¬ %%l ∧ ¬ %%r) ‵‵(not_or_distrib.mp %%H)
    | _ := fail "De Morgan′s laws don′t apply"
end

Notice that this tactic uses antiquotation to insert expressions into the preexpressions that are passed to the have tactic. To do something similar in Lean 4, it seems like I need to insert expressions into the Syntax that is passed to Lean.Elab.Tactic.evalTactic, but I don't think inserting a metavariable in that Syntax works. So is there another way to get the result I'm after? Is there a way, in a tactic, to call another tactic, passing it arguments, other than Lean.Elab.Tactic.evalTactic?

[Jannis Limperg]

Rather than calling the tactic via evalTactic, you could look at the the corresponding MetaM tactic in Lean/Meta/Tactic/. Often (but unfortunately not always) the interactive version of the tactic just amounts to some elaboration plus a call to the MetaM version. This is similar to the difference, in Lean 3, between tactic.interactive.apply and tactic.apply.

This way certainly is more cumbersome, so maybe someone else has a clever suggestion.

[Dan Velleman]

After further experimentation, I think the metavariable trick will work with evalTactic! I think I just wasn't doing it carefully enough before.

[Logan Murphy]

Hope it's okay to revive this thread, I'm also just trying go adapt my Lean3 metaprogramming habits to Lean4.

In Lean 3, if I wanted to check whether the type of a proposition is a "forall", I would do something like

meta def pattern_match : expr -> bool
| `(forall _ :  _ ,  _ ) := tt
| _ := ff

So my understanding is that in Lean 4, I don't do this kind of pattern matching on terms of type Expr, but rather, on the different kinds of Syntax (e.g. Term). So if I get an Expr (e.g. the goal), I would either need to somehow translate it to a syntax term, or I can use Gabrield's Qq library. I've tried the first approach with the toSyntax() method from Std4, but the resulting syntax is something like (Term.syntheticHole "?" a._@.myProject.myFile._hyg.735)`, which I guess is something related to hygenic macros I don't yet understand.

Is the only (or best) way to do this kind of pattern matching on Expr's still to use Qq?

[Mario Carneiro]

You should not translate exprs to syntax just to use pattern matching on them, that sounds backwards

[Tomas Skrivan]

(deleted)

[Mario Carneiro]

Qq is indeed intended to do pattern matching on exprs

[Logan Murphy]

Ah I see, so the options are either to use Qq or to use this style from Arthur's answer in another thread

def matchAndReducing (e : Expr) : MetaM (Option (Expr × Expr)) := do
  let e ← whnf e
  match e with
  | (.app (.app (.const ``And _) P) Q) => return some (P, Q)
  | _ => return none

[Mario Carneiro]

You can pattern match on Expr directly, e.g. | .forall .. => true, this is what isForall will do, but this is usually not the right thing because the expr might have an .mdata or other annotation on it that you want to ignore. Usually you want to call whnfR and then pattern match the result

[Logan Murphy]

Gotcha. Thanks folks

[Mario Carneiro]

There is also getAppFnArgs in mathlib which makes for slightly nicer pattern matches

[Mario Carneiro]

which would look like this:

def matchAndReducing (e : Expr) : MetaM (Option (Expr × Expr)) := do
  let e ← whnf e
  match e.getAppFnArgs with
  | (``And, #[P, Q]) => return some (P, Q)
  | _ => return none

[Logan Murphy]

You should not translate exprs to syntax just to use pattern matching on them, that sounds backwards

So that pattern of antiquotations on syntax is really only used for syntax-related macros, not this kind of metaprogramming with exprs. I see