to_additive heresy

Stream: general

[Yaël Dillies]

Dear all,

Am I an heretic?

import algebra.group.with_one

variables {α : Type*} [has_involutive_inv α]

@[simp, to_additive] lemma inv_comp_inv :
  has_inv.inv ∘ has_inv.inv = @id α :=
inv_involutive.comp_self

local attribute [reducible] with_zero

attribute [to_additive] with_zero.has_inv

@[to_additive] -- additivizing `with_zero` gives... `with_zero`
instance : has_involutive_inv (with_zero α) :=
{ inv_inv := λ a, (option.map_map _ _ _).trans $ by simp_rw [inv_comp_inv, option.map_id, id],
  ..with_zero.has_inv }

[Kevin Buzzard]

I thought all groups had a one? Oh wooah that really is a valid import, I'm not sure I've ever seen that file!

[Eric Rodriguez]

file#algebra/group/with_one

[Johan Commelin]

regex fail?! edit: aah, you need /s

[Eric Rodriguez]

I never remmeber which is which :b

[Yaël Dillies]

So do we not care about such cases where an additive lemma/instance comes from two multiplicative ones?

[Floris van Doorn]

I briefly had a case like that, we have docs#has_compact_mul_support.mul and docs#has_compact_support.add, and briefly I had has_compact_support.mul that additivized would also give has_compact_support.add. But now there are two lemmas docs#has_compact_support.mul_right and docs#has_compact_support.mul_left.

I think it's best to to_additivize the most multiplicative one, and not add the attribute for the other ones: I think they will often not compile, because they are not semantically equivalent. So in this case with_zero.has_involutive_neg should come from with_one.has_involutive_inv.

[Yaël Dillies]

In my case it seems to work fine, but fair.