Zulip Chat Archive

Stream: general

Topic: What is `to_additive`?

Kevin Buzzard (Jul 14 2020 at 19:30):

I realise in my talk I call it a "tactic" but I'm not at all sure that that's what it is. What's the correct name for it?

Simon Hudon (Jul 14 2020 at 19:30):

An attribute

Chris Hughes (Jul 14 2020 at 19:31):

But a tactic is executed every time an attribute is given right?

Kevin Buzzard (Jul 14 2020 at 19:32):

As opposed to tagging something with simp, where nothing really happens until someone calls simp later on.

Floris van Doorn (Jul 14 2020 at 19:32):

For some attributes, correct (for other attributes the executed tactic is tactic.skip so then it's technically also correct)

Kevin Buzzard (Jul 14 2020 at 19:33):

So is there a tactic behind the [to_additive] attribute, which humans never run?

Simon Hudon (Jul 14 2020 at 19:35):

There's also a nuance between what you use in your proof scripts and what is used in an attribute. They are both using the tactic monad which encapsulates most of the meta programming features but I wouldn't say to_additive is a tactic

Floris van Doorn (Jul 14 2020 at 19:35):

yes, it's written in src#to_additive.attr

Simon Hudon (Jul 14 2020 at 19:35):

I would call it a code generator or a meta program if you want to be more specific than attribute

Rob Lewis (Jul 14 2020 at 19:51):

Yeah, I agree with Simon, "metaprogram" seems like the right term here.

Kevin Buzzard (Jul 14 2020 at 20:39):

Thanks all

Jasmin Blanchette (Jul 15 2020 at 08:04):

I agree with Rob, and disagree with Simon (metaprogram should be spelled as one word). ;)

Utensil Song (Jul 16 2020 at 07:31):

Would a more general version of to_additive be desirable?

To #xy my question, for example, C is equipped with a has_mul which forms a group, but if I need to define another multiplication for it and that multiplication also forms a multiplicative group, how can I do it? Should I use meta program to "copy" everything from the group for has_mul?

Simon Hudon (Jul 16 2020 at 13:17):

No you have to prove it all yourself if you have a new group. Then, many theorems are polymorphic and will work regardless of what your multiplicative group is.

Simon Hudon (Jul 16 2020 at 13:18):

You might want to define a type synonym for C to make it clear when you use one group vs the other

Utensil Song (Jul 17 2020 at 05:42):

Thanks, after some experiments locally, I figured out what you mean by:

  1. proving(via instance) group C with different mul than the mul in has_mul C (I must haven't pay enough attention when reading data.complex.basic)
  2. how to deal with the type synonym for C (I used def so everything has to be proven for C', although it also turns out that type synonym is not needed by 1 but only for making it more clear, just as you suggested literally).

Last updated: Dec 20 2023 at 11:08 UTC