MetaM and tactics

Stream: lean4

[Guilherme Silva]

How can I use MetaM as a tactic?

I have seen that most of the tactics are defined as MetaM in Lean 4 like simp, rewrite. But I copy and paste in my code and modified it a little bit and it is not working when I try to use it as a tactic.

Can someone give me a simple example of defining a small MetaM tactic and using it later?

[Daniel Selsam]

import Lean
open Lean Lean.Meta Lean.Elab.Tactic

def Meta.myTriv (mvarId : MVarId) : MetaM Unit := do
  let mvarType ← getMVarType mvarId
  if mvarType.isConstOf `True then
    assignExprMVar mvarId (mkConst `True.intro [])
  else
    throwTacticEx `myTriv mvarId "goal does not have type `True`"

syntax (name := myTriv) "myTriv" :  tactic

@[tactic myTriv] def evalMyTriv : Tactic := fun stx => do
  let mvarId ← getMainGoal
  Meta.myTriv mvarId

example : True := by myTriv

[Mario Carneiro]

import Lean
open Lean Elab Tactic Meta

def trivMetaM (mvarId : MVarId) : MetaM Unit := do
  assignExprMVar mvarId (mkConst ``True.intro)

def trivTacticM : TacticM Unit :=
  liftMetaMAtMain trivMetaM

syntax (name := triv) "triv" : tactic

@[tactic «triv»] def evalTriv : Tactic := fun stx =>
  match stx with
  | `(tactic| triv) => trivTacticM
  | _               => throwUnsupportedSyntax

example : True := by triv

[Mario Carneiro]

dang

[Mario Carneiro]

same example too

[Daniel Selsam]

Ha. We need a better system. Next time I will type <SPACE> before I head to emacs, so it looks like I am typing in Zulip.

[Mario Carneiro]

it's good though, we need more examples of this stuff

[Mario Carneiro]

it's not clear to me whether macro can be used here

[Daniel Selsam]

Mario Carneiro said:

it's not clear to me whether macro can be used here

Can you clarify your question? This works:

macro "myTriv" : tactic => `(exact True.intro)
example : True := by myTriv

[Mario Carneiro]

my version has a bug though, I guess assignExprMVar doesn't check the types

[Mario Carneiro]

I mean for "proper" tactics, not macro tactics

[Mario Carneiro]

like what goes on the right of the arrow there? can some computation happen?

[Daniel Selsam]

Lean is expecting MacroM Syntax : Type

[Mario Carneiro]

I don't really know what that means though

[Daniel Selsam]

abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception Macro.State)

[Mario Carneiro]

eh... yes

[Daniel Selsam]

It can perform some computation, but has no access to MetaM and must return Syntax

[Mario Carneiro]

so it's a pure function?

[Daniel Selsam]

Yes.

[Mario Carneiro]

I guess that's a bit more restrained than the lean 3 parser monad, which had access to the tactic state and a bunch of other stuff

[Mario Carneiro]

I mean, it's probably a good idea not to let the macros get too crazy but it might make some porting things tricky

[Daniel Selsam]

I think the idea is to separate concerns: have parsers parse and produce syntax, and then have elaborators map syntax to expressions.

[Mario Carneiro]

which is part of why I don't anticipate there being much use of macro tactics besides ad-hoc tactics that are done with `[ ... ] today

[Mario Carneiro]

Even for something like triv, if I actually cared to make a fast tactic with good error messages I wouldn't implement it as a macro tactic

[Daniel Selsam]

There are a bunch of "macro tactics" in Init, e.g. https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L289-L305

[Mario Carneiro]

yes, and most of them will have to be replaced in mathlib... or at least that's my prediction

[Mario Carneiro]

it's not clear how to "scope creep" with those definitions

[Daniel Selsam]

(deleted)

[Sebastian Ullrich]

The point about "tactics are macros" is not that you have to write every tactic as a pure macro, but that it gives you a uniform macro/elaborator infrastructure shared with term elaboration, including the hygiene scheme. You can always "escalate" from a pure macro to an elaborator by throwing the syntax quotation in evalTactic, then refine on top of that. For tactics that will probably happen more often than for terms, yes.

[Guilherme Silva]

I was looking at rewrite tactics and it returns MetaM RewriteResult. So it looks like that transforming this MetaM into a tactic will not be a simple transformation. Where can I find some examples of a tactic that just changes a goal to a simpler goal?

[Daniel Selsam]

import Lean
open Lean Lean.Elab Lean.Elab.Tactic Lean.Meta

syntax (name := rewriteSimple) "rewriteSimple" term : tactic

@[tactic rewriteSimple] def evalRewriteSimple : Tactic := fun stx => do
  Term.withSynthesize <| withMainContext do
    let e ← elabTerm stx[1] none true
    let r ← rewrite (← getMainGoal) (← getMainTarget) e
    let mvarId' ← replaceTargetEq (← getMainGoal) r.eNew r.eqProof
    replaceMainGoal (mvarId' :: r.mvarIds)

example (m n : Nat) (h : m = n) : m + m = n + n := by
  rewriteSimple h
  rfl

[Guilherme Silva]

Thanks for the example.
Do you know how to trace information? So I can understand what is going on.

[Sebastian Ullrich]

For unconditional tracing, you can use something like

    logInfo m!"{e}: {r.eNew}"

See also https://leanprover.github.io/lean4/doc/debugging.html (additions welcome)

[Guilherme Silva]

Thank you for your suggestion. logInfo is working inside Tactic and dbg_trace is very useful when there is no logInfo available.
Does MetaM have some kind of log? Because I have tried to use logInfo inside it and it is not working :cry: . I received this error:

failed to synthesize instance
  Lean.Elab.MonadLog (ReaderT.{0 0} Lean.Meta.Context (StateRefT' IO.RealWorld Lean.Meta.State Lean.Core.CoreM))

[Guilherme Silva]

I figure out that I can just rename MetaM to TacticM that it works. So it is possible to use all TacticM features :smiley:

[Yakov Pechersky]

There's also liftMetaAtMain to lift MetaM to TacticM

[Guilherme Silva]

@Yakov Pechersky , thanks for the suggestion.

I have found in the definition of MetaMthat they use StateRefT, but my VSCode can't find the definition of it when I press F12.
What is that? Why can't my VS Code find this definition?

[Mario Carneiro]

make sure you are up to date?

[Leonardo de Moura]

Guilherme Silva said:

Yakov Pechersky , thanks for the suggestion.

I have found in the definition of MetaMthat they use StateRefT, but my VSCode can't find the definition of it when I press F12.
What is that? Why can't my VS Code find this definition?

StateRefT is currently a macro. This is a temporary workaround. Not sure whether it is still needed after all the recent improvements. Note that it is highlighted as a keyword.
We don't support goto definitions for macros yet.