Tactic as macro

Stream: general

[Nima]

Is there anyway I can define a tactic (or something local to a proof) that does a fixed number of steps, so I would not need to repeat the whole thing multiple times? For example, a tactic or local definition name finish_it that does the following:

cases ind1
; cases ind2
; cases ind3
; unfold func at hh
; try { contradiction }
; done

[Kenny Lau]

iterate

[Kevin Buzzard]

I am concerned that your tactic might need to take some inputs (ind1, ind2 etc).

[Kevin Buzzard]

if it didn't take any inputs then Programming In Lean explains how to do this

[Kenny Lau]

iterate 3 { cases ind1
; cases ind2
; cases ind3
; unfold func at hh
; try { contradiction }
; done }

[Kenny Lau]

to define tactics locally, (make sure that the names will not change), and then just do

def finish_it : tactic unit := `[ code ]

[Kevin Buzzard]

see lines 88 to 91 of

[Kevin Buzzard]

https://github.com/kbuzzard/mathlib/commit/5ff51dc6993990e600ddee4857a2e207e62f35d1#diff-26b4491c757c999172218bc6c4da2cb0R88

[Kevin Buzzard]

to see how I wrote a basic tactic, knowing nothing about metaprogramming in Lean

[Kevin Buzzard]

see lines 101 to 105 for the application

[Nima]

Thanks, `[code] did the trick.
Now I can write finish_it and the proof is complete.
But suppose I remove the last two lines from finish_it (try { contradiction } and done). Why I cannot write finish_it ; try { ... }. I mean, ; does not work, but , does.

[Mario Carneiro]

This is because try { ... } is an interactive mode tactic, so you need the interactive mode ;, so finish_it needs to also be defined in the interactive namespace (tactic.interactive.finish_it) if you want to use it in tactics. If you say finish_it in a begin ... end or by ... block and tactic.interactive.finish_it doesn't exist, then it will assume it is a term of type tactic unit and will find it in the current namespace, but since it's using regular term parsing you won't get nice syntaxes like try { ... } that only work in interactive mode.