defining your own tactic in Lean 4

Stream: lean4

[Dean Young]

I want to combine

  repeat (rw [Id₁])
  repeat (rw [Id₂])
  repeat (rw [Ass])

into a single tactic called cat

Here's my mwe:

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Cmp {C : category} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g

theorem Id₁ {C : category} {X : C.Obj} { Y : C.Obj} {f : C.Hom X Y} :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem Id₂ {C : category} {X Y : C.Obj} {f : C.Hom X Y} :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem Ass {C : category} {W X Y Z : C.Obj} {f : C.Hom W X} {g : C.Hom X Y} {h : C.Hom Y Z} :
  ((h ∘_(C) g) ∘_(C) f) = (h ∘_(C) (g ∘_(C) f)) := (C.Ass W X Y Z f g h)

-- My tactic in action:
example {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {A : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z A}:
  (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) )) = ((i ∘_(C) h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by
  repeat (rw [Id₁])
  repeat (rw [Id₂])
  repeat (rw [Ass])

[Damiano Testa]

Does

open Lean Elab.Tactic in
elab (name := myTac) "myTac" : tactic => do
  evalTactic (← `(tactic|repeat (rw [Id₁]); repeat (rw [Id₂]) ; repeat (rw [Ass])))

example {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {A : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z A}:
  (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) )) = ((i ∘_(C) h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by
  myTac

help?

[Henrik Böving]

Note that you should be able to use just a macro and not a full elab Here.

[Dean Young]

like notation "cat" => repeat (rw [Id₁]); repeat (rw [Id₂]) ; repeat (rw [Ass])? that gives me expected term

thanks @Damiano Testa for the full answer. I might go with something simpler here though... I can't figure out macros for tactics.
@Henrik Böving can you modify this to a working macro?

notation "cat" => repeat (rw [Id₁]); repeat (rw [Id₂]) ; repeat (rw [Ass])

[Damiano Testa]

I suspect that Henrik had something along the lines of

macro "myTac" : tactic => `(tactic| repeat (rw [Id₁]) ; repeat (rw [Id₂]) ; repeat (rw [Ass]))

in mind...

[Dean Young]

Thanks Damiano that's perfect

[Dean Young]

I'll save your other answer for later

[Mario Carneiro]

beware, repeat (rw [Id₁]) ; repeat (rw [Id₂]) ; repeat (rw [Ass]) doesn't mean what you think

[Mario Carneiro]

(in fact @Damiano Testa 's macro line would not have parsed if it did)

[Mario Carneiro]

it is parsed as repeat (rw [Id₁]; repeat (rw [Id₂]; repeat (rw [Ass])))

[Mario Carneiro]

you should instead write (repeat rw [Id₁]); (repeat rw [Id₂]); (repeat rw [Ass]) if you want it on one line

[Mario Carneiro]

or

macro "myTac" : tactic => `(tactic| ((repeat rw [Id₁]); (repeat rw [Id₂]); (repeat rw [Ass])))

for the macro

[Damiano Testa]

Mario, thanks for the correction!