Zulip Chat Archive

Stream: general

Topic: Interaction between `to_` attributes

Yaël Dillies (Nov 29 2021 at 14:18):

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 (Nov 29 2021 at 15:31):

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 (Nov 29 2021 at 16:05):

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 (Nov 29 2021 at 16:10):

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

Last updated: Aug 03 2023 at 10:10 UTC