Use Tactic inside simproc

Stream: metaprogramming / tactics

[Moritz R]

Is there any way to call an arbitrary tactic inside a simproc? E.g. to discharge the following goal1 with a fresh simp_all call or grind instead of simps built in discharger that i currently use

def dosimp (F : Q(ℕ → Type*)) (α : Q(Type*)) (opair : (OrientedPair F α)) (b1 b2 : Bool) :
    SimpM (Result) := do
  let L1 : Q(Literal $F $α) := ...
  let goal1 : _ := q(Literal.toPos $L1 = Literal.pos (Sym2.mk $opair.big $opair.small))
  let discharge := (← Simp.getMethods).discharge?
  let some hL1 ← discharge goal1 | throwError "proof of `{ppgoal1}` (hL1) didn't succeed"

[Henrik Böving]

SimpM is just a stack on top of MetaM so you can do whatever you want with MetaM tactics.

[Joachim Breitner]

Well, you can do anything, but not everything will work well. In particular if the result depends on the local context (eg assumption) you have to remember to tell simp that it should not cache the result (forgot how precisely to do that).