Control `to_additive`

Stream: general

[Pedro Minicz]

How can I tell to_additive to ignore some definitions?

[Pedro Minicz]

import group_theory.quotient_group
import set_theory.ordinal

open quotient_group

namespace cardinal

variables {α : Type*} [group α] {s : set α} [is_subgroup s]

@[to_additive]
lemma mk_group_eq_mk_quotient_mul_mk_subgroup :
  mk α = mk (quotient s) * mk s :=
begin
  rw [mul_def, cardinal.eq],
  exact ⟨is_subgroup.group_equiv_quotient_times_subgroup _⟩
end

[Pedro Minicz]

I am pretty sure that the problem in the example above is that to_additive changes * to +.

[Pedro Minicz]

The lemma is true for both group and add_group, but the cardinals should always be multiplied!

[Mario Carneiro]

See examples in algebra.group_power

[Patrick Massot]

I think you need to provide the additive proof by hand, but you can still add the attribute afterwards, so that it will be used by to_additive.

[Mario Carneiro]

state the lemma without to_additive, then state the additive version and prove it using the multiplicative version, then mark the multiplicative version as attribute [to_additive add_name] mul_name

[Pedro Minicz]

Works perfectly! Thank you!

[Bryan Gin-ge Chen]

This is sort of hinted at in the new tactic doc entry for to_additive in the sentence starting with "Even when..." but it might still be unclear. Suggestions for improvements are welcome!

[Yury G. Kudryashov]

It makes no sense to manually add to_additive if to_additive fails to correctly transport the type of the lemma. It makes sense if it transfers type but not proof.

[Mario Carneiro]

It is rare but possible for it to work even if it doesn't transfer the type, because two translated theorems can cancel each other out

[Yury G. Kudryashov]

Probably we should have an ignore list (nat, perm) but my meta programming skills are not good enough.

[Mario Carneiro]

actually, when it is a whole network of theorems it's not that unreasonable that the mystery type only appears in some defeq goal and not explicitly in the theorem