Mechanism of to_additive

Stream: mathlib4

[The-Anh Vu-Le]

Hi, I am currently reading Mathematics in Lean. In Chapter 7, they introduce the @[to_additive] attribute and I am curious about its mechanism.

Specifically, for this piece of code:

class AddSemigroup₃ (α : Type) extends Add α where
/-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
/-- Multiplication is associative -/
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

Can someone explain what to_additive will do? Like, I don't think it will "create" AddSemigroup₃ (because we already define that right above) and so maybe it will create a link? Does it do something else? Also, how does Lean/Mathlib know mul_assoc₃ is to be "linked" to add_assoc₃ (does it?)

Finally, for this part

whatsnew in
@[to_additive]
lemma left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]

How does it know to replace inv with neg? Is it hardcoded to find and replace all invs with negs?

Many thanks.

[Kevin Buzzard]

Yes there's a big dictionary inv->neg, mul->add etc. It's in the code somewhere! Just right-click on to_additive, jump to the definition and poke around!

[The-Anh Vu-Le]

Thanks! But I would also like to know what @[to_additive AddSemigroup₃] does and why we need to define class AddSemigroup₃ before that (won't the same mechanism applicable to auto-generate an AddSemigroup₃ definition)?

Edit: I kinda see that maybe you want to add more things to a class (AddSemigroup₃) so it's better to not rely on automation for class definition, but it works better for theorems.

[Yury G. Kudryashov]

At the time this attribute was written, lean didn't provide enough metaprogramming API to conveniently create structures in meta code. Do, for structures (incl. classes), to_additive just adds the names to its big dictionary. It would be nice to auto generate structures one day, but it's easy to work around, so nobody made this change yet.

[Yury G. Kudryashov]

For definitions and lemmas, the attribute translates all names like Inv.inv to their additive counterparts, both in the type and in the definition or proof, then adds the resulting definition to the environment.

[The-Anh Vu-Le]

One further question

class AddSemigroup₃ (α : Type) extends Add α where
/-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
/-- Multiplication is associative -/
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α

@[to_additive AddMonoid₃]
class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α

attribute [to_additive existing] Monoid₃.toMulOneClass

export Semigroup₃ (mul_assoc₃)
export AddSemigroup₃ (add_assoc₃)

whatsnew in
@[to_additive]
lemma left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]

#check left_neg_eq_right_neg'

Let's say I change all mul_assoc₃ to m_assoc₃. It will still successfully generate left_neg_eq_right_neg'. I find this very interesting, how did it get the proof/how did it relate m_assoc₃ with add_assoc₃?

Edit: seems like they do positional mapping as well.

[Yury G. Kudryashov]

Whenever to_additive deals with a structure, it records correspondence between its fields with same indexes.

[Floris van Doorn]

Correct (that happens in these lines of code)