existsi for already elaborated Expr

Stream: lean4

[David Renshaw]

In my work-in-progress on mk_iff, I have the following function:

def existsi (mvar : MVarId) (e : Expr) : MetaM MVarId := do
  let (subgoals,_) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mvar do
    Elab.Tactic.evalTactic (←`(tactic| refine ⟨?_,?_⟩))
  let [sg1, sg2] := subgoals | throwError "expected two subgoals"
  sg1.assign e
  pure sg2

Is there a better way to do this? I kinda want to call the existing existsi tactic, but that would involve delaborating e from Expr back to Syntax, and it feels wrong.

(I've been in this situation a few times lately, where I'm working in MetaM and everything is already elaborated, and I want to call some tactics that only defined to operate on syntax.)

[Mario Carneiro]

A trick you can do to interpolate exprs into syntax is to use assigned metavars. You create a new metavar, immediately assign it, and then use the ?a syntax to refer to the metavar by name in the syntax

[David Renshaw]

Like this?

def existsi (mvar : MVarId) (e : Expr) : MetaM MVarId := do
  let mvar' ← mkFreshExprMVar none
  let mvarId' := mvar'.mvarId!
  mvarId'.assign e
  let (subgoals,_) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mvar do
    Elab.Tactic.evalTactic (←`(tactic| refine ⟨ ???, ?_⟩))
  let [sg] := subgoals | throwError "expected one subgoal"
  pure sg

[David Renshaw]

what goes in the ??? in the tactic syntax ?

[Mario Carneiro]

I think ?$(mkIdent mvarId'.name)

[David Renshaw]

Hm. I have

def existsi (mvar : MVarId) (e : Expr) : MetaM MVarId := do
  let mvar' ← mkFreshExprMVar none (kind := MetavarKind.synthetic)
  let mvarId' := mvar'.mvarId!
  mvarId'.assign e

  let (subgoals,_) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mvar do
    Elab.Tactic.evalTactic (←`(tactic| refine ⟨?$(mkIdent mvarId'.name):ident, ?_⟩))
  let [sg] := subgoals | throwError "expected one subgoal"
  pure sg

and it's giving me an error because it's still producing two subgoals, rather than just one.

[Gabriel Ebner]

It's usually easiest to create the synthetic metavatiable using elabTerm, something like this should work:

withFreshMacroScope do
let mvar' ← elabTerm (←`(?a))
let mvarId' := mvar'.mvarId!
mvarId'.assign e
evalTactic (← `(tactic| refine ⟨?a, ?_⟩))

[David Renshaw]

yep, this seems to work

def existsi (mvar : MVarId) (e : Expr) : MetaM MVarId := do
  let (subgoals,_) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mvar do
    withFreshMacroScope do
      let mvar' ← Elab.Tactic.elabTerm (←`(?a)) none
      let mvarId' := mvar'.mvarId!
      mvarId'.assign e
      Elab.Tactic.evalTactic (←`(tactic| refine ⟨?a,?_⟩))
  let [sg] := subgoals | throwError "expected one subgoal"
  pure sg

[David Renshaw]

Is the withFreshMacroScope so that the mvar name ?a does not collide with any existing mvars?

[Scott Morrison]

You could even factor that out as a MetaM level refine, so that others don't have to jump through the same hoops. :-)

[Thomas Murrills]

This technique is really neat. It seems like a generic way to “use Exprs directly in syntax” during elaboration, which I’ve found myself wanting to do a couple times even in my short time metaprogramming in Lean!

I wonder if it warrants being packaged into something that wraps around `() somehow…like a special kind of “let”/“with”/“where”. It’d be neat to write something vaguely like

`(f ?a + ?b) with ?a := e, ?b := e'

where e e' : Expr.

[Mario Carneiro]

well that e would have to be Syntax...

[Mario Carneiro]

I think a reasonable way to package this up would be a function like:

def toSyntax (e : Expr) : TermElabM Syntax := withFreshMacroScope do
  let stx ← `(?a)
  let mvar ← elabTerm stx none
  mvar.mvarId!.assign e
  pure stx

so you could just write

def existsi (mvar : MVarId) (e : Expr) : MetaM MVarId := do
  let (subgoals, _) ← Elab.Term.TermElabM.run $ Elab.Tactic.run mvar do
    Elab.Tactic.evalTactic (←`(tactic| refine ⟨$(← toSyntax e), ?_⟩))
  let [sg] := subgoals | throwError "expected one subgoal"
  pure sg

[Thomas Murrills]

well that e would have to be Syntax...

I was imagining that that with could be a macro that did what needed to be done with an Expr e behind the scenes to have this effect, but toSyntax is nicer and keeps the types clean and visible! :)

[Thomas Murrills]

However, I am worried about the macro scopes…does toSyntax automatically create the scopes necessary to avoid conflict with goals named a?

[David Renshaw]

I think the withFreshMacroScope in the first line of toSyntax handles that.

[Thomas Murrills]

Oops—I’m on mobile and hadn’t realized that that code block scrolls right, lol!

[Thomas Murrills]

Anyway, would love to see this become part of Lean 4, as it’s super convenient. :)