Make to_additive copy attribute

Stream: general

[Rémy Degenne]

I wrote a new tactic, with a corresponding attribute measurability, and I would like that attribute to be transported by to_additive when creating the additive version of a lemma. How would I do that?

import measure_theory.arithmetic
variables {α M : Type*} [measurable_space α] [measurable_space M] [has_mul M]

@[measurability, to_additive]
lemma measurable.const_mul' [has_measurable_mul M] {f : α → M} (hf : measurable f) (c : M) :
  measurable (λ x, c * f x) :=
(measurable_const_mul c).comp hf

#print measurable.const_mul'  -- shows measurability attribute
#print measurable.const_add'  -- does not have the measurability attribute. How do I fix that?

The continuity tactic also could be improved to have its attribute transported by to_additive.

[Johan Commelin]

I think to_additive already does this for simp. So maybe you can find out how it does that (I have no idea).

[Rémy Degenne]

I have been looking at the to_additive files, searching exactly for that, but I have difficulties finding out how it is done.

[Rémy Degenne]

Also I realize that my code is not a mwe, since the attribute measurability is not defined for anybody else.

[Rémy Degenne]

Here is the same example, but with the continuity attribute (which should not be used on that lemma, but it's just an example):

import measure_theory.arithmetic
variables {α M : Type*} [measurable_space α] [measurable_space M] [has_mul M]

@[continuity, to_additive]
lemma measurable.const_mul' [has_measurable_mul M] {f : α → M} (hf : measurable f) (c : M) :
  measurable (λ x, c * f x) :=
(measurable_const_mul c).comp hf

#print measurable.const_mul'  -- shows continuity attribute
#print measurable.const_add'  -- does not

[Scott Morrison]

Ah, that's a pity, I was going to suggest to see how it works for continuity. :-)

[Scott Morrison]

Have you tried adding measurability to lines 311-312 of algebra.group.to_additive?

[Scott Morrison]

If that works please do continuity too!

[Rémy Degenne]

Yes, I added it in that list. That did not work

[Kevin Buzzard]

This from monoid_localization

@[to_additive, ext] lemma ext {f g : localization_map S N} (h : ∀ x, f.to_map x = g.to_map x) :
  f = g :=
by cases f; cases g; simp only; exact funext h

attribute [ext] add_submonoid.localization_map.ext

suggests that ext also doesn't work.

[Kevin Buzzard]

This from the simps docstring:

* Use `@[to_additive, simps]` to apply both `to_additive` and `simps` to a definition, making sure
  that `simps` comes after `to_additive`. This will also generate the additive versions of all
  `simp` lemmas.

Counterintuitive!

[Kevin Buzzard]

From topology.algebra.monoid:

@[to_additive, continuity]
lemma continuous_multiset_prod {f : ι → X → M} (s : multiset ι) :
  (∀i ∈ s, continuous (f i)) → continuous (λ a, (s.map (λ i, f i a)).prod) :=
by { rcases s with ⟨l⟩, simpa using continuous_list_prod l }

attribute [continuity] continuous_multiset_sum

@[continuity, to_additive]
lemma continuous_finset_prod {f : ι → X → M} (s : finset ι) :
  (∀ i ∈ s, continuous (f i)) → continuous (λa, ∏ i in s, f i a) :=
continuous_multiset_prod _

-- should `to_additive` be doing this?
attribute [continuity] continuous_finset_sum

Both orders tried, neither works :-)

[Scott Morrison]

The example from monoid_localization shouldn't work: to_additive needs to come last.

[Yaël Dillies]

Random thought: does the tag order change anything? In Rémy's example, to_additive comes second while it comes first in the simps docstring.

[Kevin Buzzard]

Yes. Right now the rule is "to_additive always last, except when simps are involved"

[Scott Morrison]

Essentially "cleverest last" :-)

[Kevin Buzzard]

Yaël Dillies said:

Random thought: does the tag order change anything? In Rémy's example, to_additive comes second while it comes first in the simps docstring.

Yes, the tag order changes things. Stuff tagged before to_additive has a chance of being transferred.

[Yaël Dillies]

Oh okay. That's good to know! Is that referenced anywhere or is just folklore for now?

[Johan Commelin]

I think it's folklore

[Johan Commelin]

reassoc and simp also interact. I think reassoc is the "smart" kid in that case.

[Rémy Degenne]

The list of lines 312-313 in to_additive goes through two lemmas, apparently unaltered, and then gets fed into

attrs.mmap' (λ n, copy_attribute n src tgt)

so I thought that any attribute in the list would be copied. I don't understand why adding measurability to the list does not work.

[Rémy Degenne]

Perhaps it works only for attributes defined before to_additive?

[Scott Morrison]

Nor me. :-( I'm trying this out myself at the moment, but touching to_additive kills all the oleans.

[Alex J. Best]

We (I) need to revive #5487 I think. Rob and Floris left some good comments that I didn't have time to address back then but shouldn't take too long now, assuming the bitrot isn't too bad. I'll try and do so this week.

[Alex J. Best]

Some attributes have data attached iirc and the copy_attribute used by to_additive currently won't copy those is the problem.