Interaction between `to_` attributes

Stream: general

[Yaël Dillies]

We have to_additive and we want to_order_dual and to_right_action (see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/left.20vs.20right.20modules.20in.20tensor.20products). Surely they will at some point be used concurrently. Do we already know a way to make them interact properly? Typically, if I tag something @[to_additive, to_order_dual, to_right_action] I want 7 lemmas to be automatically generated, not 3.

[Alex J. Best]

I guess nobody has thought about this, after all these other tactics aren't written yet. That said it shouldn't be too hard to make this part of the spec, the second/third attributes should be able to see the resulting arguments of applying the first attribute and therefore be able to generate lemmas based on all of the already generated lemmas for the first attribute, it wouldn't be automatic however and some code would need to be added.
Maybe you should make a github issue for the creation of these other tactics (if there isn't one already), and add this to their spec?

[Yakov Pechersky]

One usage might be @[to[additive, dual]] where all the to_ tactics are plugins to some larger to tactic, which does the proper outer product.

[Johan Commelin]

I was just thinking similar thoughts :smiley: Similar to how we have a linter framework, there can maybe be a to_ framework.