Unparsing the arguments for tactic writing

Stream: general

[Bolton Bailey]

I have a project which uses requires me to simplify several expressions of the form mv_polynomial.coeff .... Currently, I just call something like
simp [mv_polynomial.smul_eq_C_mul, mv_polynomial.X_pow_eq_single, finsupp.single_eq_single_iff]
In multiple locations.

I'm trying to write a tactic to automate this, ideally I would like to start with something like

meta def coeff_simplify : tactic unit :=
  tactic.interactive.simp [mv_polynomial.smul_eq_C_mul, mv_polynomial.X_pow_eq_single, mv_polynomial.coeff_monomial, finsupp.single_eq_single_iff]

but this doesn't work - simp expects several parse types as inputs which prevent this tactic definition from working. Is there any quick way to tell this tactic definition that I just want it to do the same thing as simp [... my_lemmas ...]?

[Scott Morrison]

The really cheap way is to write `[simp [lemma1, lemma2]].

[Scott Morrison]

The `[...] notation packages up interactive tactics.

[Scott Morrison]

Once you're in the non-interactive world, it's probably better to use the non-interactive tactics, however, so use tactic.simp rather than tactic.interactive.simp, etc.

[Scott Morrison]

Rather than "by-hand" building the set of lemmas you want to pass to simp, you may find it easiest (and cleaner!) to create a custom attribute, tag the relevant lemmas, and then use the version of tactic.simp that lets you pass lemmas by an attribute name.

[Scott Morrison]

(Then you're only passing a name, rather than building some expr objects.)