Creating aliases for a tactic

Stream: Lean for teaching

[Lucas Arruda]

Is there any easy way to do this? No change to behavior, just add a more convenient name for a tactic.

[Siddhartha Gadgil]

Yes.

macro "trust_me" : tactic => do
  `(tactic|sorry)

example: 1 =2 := by trust_me

[Siddhartha Gadgil]

If you want parameters:

macro "use_function" f:term : tactic => do
  `(tactic| apply $f)

example : 1 ≤ 1 := by use_function Nat.le_refl

[Patrick Massot]

To be honest, it can get more complicated if the tactic has complicated parameters, or optional ones. So don’t hesitate to ask here if you can get in macro world.

[Lucas Arruda]

I run into some problems when trying to create a macro that expands to intro something.

open Lean Elab

macro "mIntro " h:term : tactic => do
  `(tactic| intro $h)
-- application type mismatch
--  h.raw
-- argument
--  h
-- has type
--  TSyntax `term : Type
-- but is expected to have type
--  TSyntax `Lean.Parser.Term.matchAlts : Type

open Lean Elab
declare_syntax_cat Lean.Parser.Term.matchAlts
macro "mIntro " h:Lean.Parser.Term.matchAlts : tactic => do
  `(tactic| intro $h)
-- application type mismatch
--  h.raw
-- argument
--  h
-- has type
--  TSyntax `Lean.Parser.Term.matchAlts : Type
-- but is expected to have type
--  TSyntax `term : Type

[Patrick Massot]

intro is indeed a bit complicated since it can take several kind of arguments. Would you be happy with a version taking exactly one identifier?

[Lucas Arruda]

It would be a start, i guess. But it'd also be nice to have a version that can do exactly what intro does

[Patrick Massot]

Actually having multiple ones isn’t really harder:

[Patrick Massot]

macro "mIntro " h:term* : tactic => do
  `(tactic| intro $h:term*)

[Patrick Massot]

What won’t work is the pattern stuff.

[Patrick Massot]

I mean things like intro ⟨x, h⟩

[Patrick Massot]

We could make it work of course, but it will require copying stuff from the core intro elaborator.

[Lucas Arruda]

oh, that is already very useful! Thank you!

if i want to go ahead and try copying stuff from the core intro elaborator, could you give me some advice?

[Patrick Massot]

You can simply write intro in your proof and use go to definition to see the elaborator.

[Patrick Massot]

It should bring you to https://github.com/leanprover/lean4/blob/02b206af9b857a2bbc796394aec14fe192ab59d7/src/Lean/Elab/Tactic/BuiltinTactic.lean#L282

[Patrick Massot]

If you need more help about that, I recommend switching to the metaprogramming channel which is more suitable for technical meta-stuff.

[Lucas Arruda]

Thank you, again!

[Patrick Massot]

And zulip doesn’t want to create that link :sad:

[Kevin Buzzard]

#metaprogramming / tactics

I get it by #metaprogr and then tab and then tab again (but it still seems to link to "last message posted in the channel" as opposed to anything like an overview)