Calling Grind from MetaM

Stream: metaprogramming / tactics

[Tomaz Mascarenhas]

Suppose I have the following function:

def f (x : Nat) : Real := x

I can prove that f 2 = 2 with grind if I annotate f with grind:

@[grind]
def f (x: Nat) : Real := x

example : f 2 = 2 := by grind -- ok

I would like to write a tactic that adds to the context a hypothesis of type f 2 = 2, which is proved via grind. Importantly, the call to grind must be done in MetaM. This is my attempt:

import Lean.Elab.Tactic.Basic
import Qq

open Qq Lean Elab Tactic

syntax (name := foo) "foo" : tactic
@[tactic foo] def evalFoo : Tactic := fun stx => withMainContext do
  let main ← getMainGoal
  let goal : Q(Prop) := q(f 2 = 2)
  let mv ← Meta.mkFreshExprMVar goal
  let _ ← Meta.Grind.main mv.mvarId! (← Lean.Meta.Grind.mkDefaultParams default)
  let (_, mv') ← MVarId.intro1P $ ← main.assert (Name.mkSimple "h") goal mv
  replaceMainGoal [mv']

If I try to use it, I end up getting the error (kernel) declaration has metavariables '_example':

example : f 2 = 2 := by -- (kernel) declaration has metavariables '_example'
  foo
  exact h

I think it is because the grind is not expanding f internally, even after I annotate it, and I need to manually introduce it into grind's context. How could I do that?

[Aaron Liu]

it looks like grind failed

[Aaron Liu]

instead of using default as your docs#Lean.Grind.Config you should use {}

[Tomaz Mascarenhas]

oh wow, it works; thanks!