Porting local tactics

Stream: mathlib4

[David Ang]

I have multiple simp only tactics in a local file that simply chains together multiple lemmas:

private meta def map_simp : tactic unit :=
`[simp only [map_one, map_bit0, map_bit1, map_neg, map_add, map_sub, map_mul, map_pow]]

What do I do with these for the corresponding file in mathlib4?

[Patrick Massot]

You can have a macro doing that.

[Patrick Massot]

A more annoying thing is the name map_bit0 and map_bit1 suggest relying on the way computation with Nat is implemented in Lean 3.

[Moritz Doll]

untested, but it should be something along the lines of

macro "map_simp " : tactic =>
  `(tactic|simp only [foo, bar])

[Jireh Loreaux]

Regarding the handling of numerals, I had to do some similar fidgeting when I ported the noncomm_ring tactic. I think I did it right (at least, it seemed to work on tests for noncomm_ring). If you want to have a look it's Tactic.NoncommRing.

[David Ang]

How would I make the macro private/local/scoped? I don't want it to be visible outside my file.

EDIT: seems like adding local might work? #lint doesn't complain that it doesn't have a docstring anymore.

[Yury G. Kudryashov]

Instead of bit0/bit1 lemmas, you should use lemmas for 0, 1, and docs#OfNat.ofNat

[Yury G. Kudryashov]

The latter is defeq to Nat.cast n given [n.AtLeastTwo]

[Yury G. Kudryashov]

docs#map_ofNat