to_additive

Stream: general

[Patrick Massot]

Is there any hope to_additive could be improved to avoid things like https://github.com/leanprover/mathlib/blob/2594f48f20392f84b0743eb0867c030913eca627/group_theory/quotient_group.lean#L40-L47?

[Mario Carneiro]

@Simon Hudon Would you like to take a look at this? I am thinking that the to_additive attribute should recursively copy any suffixed versions of the input mapping that happen to be in the term being traversed. For example if you are translating foo => bar and you run across foo._match_1, and this does not already have a translation, then it should translate foo._match_1 => bar._match_1 and then try again

[Simon Hudon]

Interesting! Sure, I'll have a look. I assume at the moment, it only does the foo => bar translation?

[Mario Carneiro]

yes

[Simon Hudon]

Cool, I'll look into it.

[Simon Hudon]

Do you have an example that's giving you trouble now?

[Mario Carneiro]

Well, any definition or theorem that contains (usually autogenerated) sub-definitions. In Patrick's example, it is because it is an instance with a data type and some proofs; in this case the proofs are automatically turned into sub-lemmas. The same sort of thing happens if you use match or \lam <a, b>, ... in a proof, or use the equation compiler

[Simon Hudon]

Sorry I missed Patrick's initial comment

[Johan Commelin]

We have the following code in mathlib:

/-- An ordered (additive) commutative monoid is a commutative monoid
  with a partial order such that addition is an order embedding, i.e.
  `a + b ≤ a + c ↔ b ≤ c`. These monoids are automatically cancellative. -/
class ordered_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
(add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)

https://github.com/leanprover-community/mathlib/blob/0de4bba3208ee0bd8a78adf4396aa5cb083ffdf2/src/algebra/ordered_group.lean#L17-L22

Of course, this is an abomination.

[Johan Commelin]

So I replaced it with:

/-- An ordered commutative monoid is a commutative monoid
  with a partial order such that multiplication is an order embedding, i.e.
  `a * b ≤ a * c ↔ b ≤ c`. These monoids are automatically cancellative. -/
@[to_additive add_ordered_comm_monoid]
class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
(mul_le_mul_left       : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c)

[Johan Commelin]

I was very excited that this didn't give a failure. Being prudent, I wrote:

#print prefix ordered_comm_monoid
#print prefix add_ordered_comm_monoid

[Johan Commelin]

The output of the first command is:

ordered_comm_monoid : Type u_1 → Type u_1
ordered_comm_monoid.cases_on : Π {α : Type u_1} {C : ordered_comm_monoid α → Sort l} (n : ordered_comm_monoid α),
  (Π (mul : α → α → α) (mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) (one : α)
   (one_mul : ∀ (a : α), 1 * a = a) (mul_one : ∀ (a : α), a * 1 = a) (mul_comm : ∀ (a b : α), a * b = b * a)
   (le lt : α → α → Prop) (le_refl : ∀ (a : α), a ≤ a)
   (le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
   (lt_iff_le_not_le :
     auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous))
   (le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b)
   (mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b)
   (lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c),
     C
       {mul := mul,
        mul_assoc := mul_assoc,
        one := one,
        one_mul := one_mul,
        mul_one := mul_one,
        mul_comm := mul_comm,
        le := le,
        lt := lt,
        le_refl := le_refl,
        le_trans := le_trans,
        lt_iff_le_not_le := lt_iff_le_not_le,
        le_antisymm := le_antisymm,
        mul_le_mul_left := mul_le_mul_left,
        lt_of_mul_lt_mul_left := lt_of_mul_lt_mul_left}) →
  C n
ordered_comm_monoid.has_sizeof_inst : Π (α : Type u_1) [α_inst : has_sizeof α], has_sizeof (ordered_comm_monoid α)
ordered_comm_monoid.le : Π {α : Type u_1} [c : ordered_comm_monoid α], α → α → Prop
ordered_comm_monoid.le_antisymm : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a b : α), a ≤ b → b ≤ a → a = b
ordered_comm_monoid.le_refl : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a : α), a ≤ a
ordered_comm_monoid.le_trans : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
ordered_comm_monoid.lt : Π {α : Type u_1} [c : ordered_comm_monoid α], α → α → Prop
ordered_comm_monoid.lt._default : Π {α : Type u_1}, (α → α → Prop) → α → α → Prop
ordered_comm_monoid.lt._default.equations._eqn_1 : ∀ {α : Type u_1} (le : α → α → Prop), ordered_comm_monoid.lt._default le = id (partial_order.lt._default le)
ordered_comm_monoid.lt_iff_le_not_le : ∀ (α : Type u_1) [c : ordered_comm_monoid α],
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)
ordered_comm_monoid.lt_of_mul_lt_mul_left : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a b c_1 : α), a * b < a * c_1 → b < c_1
ordered_comm_monoid.mk : Π {α : Type u_1} (mul : α → α → α) (mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) (one : α)
(one_mul : ∀ (a : α), 1 * a = a) (mul_one : ∀ (a : α), a * 1 = a) (mul_comm : ∀ (a b : α), a * b = b * a)
(le lt : α → α → Prop) (le_refl : ∀ (a : α), a ≤ a)
(le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
(lt_iff_le_not_le :
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous))
(le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b),
  (∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b) →
  (∀ (a b c : α), a * b < a * c → b < c) → ordered_comm_monoid α
ordered_comm_monoid.mk.inj : ∀ {α : Type u_1} {mul : α → α → α} {mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)} {one : α}
{one_mul : ∀ (a : α), 1 * a = a} {mul_one : ∀ (a : α), a * 1 = a} {mul_comm : ∀ (a b : α), a * b = b * a}
{le lt : α → α → Prop} {le_refl : ∀ (a : α), a ≤ a}
{le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c}
{lt_iff_le_not_le :
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)}
{le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b}
{mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b}
{lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c} {mul_1 : α → α → α}
{mul_assoc_1 : ∀ (a b c : α), a * b * c = a * (b * c)} {one_1 : α} {one_mul_1 : ∀ (a : α), 1 * a = a}
{mul_one_1 : ∀ (a : α), a * 1 = a} {mul_comm_1 : ∀ (a b : α), a * b = b * a} {le_1 lt_1 : α → α → Prop}
{le_refl_1 : ∀ (a : α), a ≤ a} {le_trans_1 : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c}
{lt_iff_le_not_le_1 :
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)}
{le_antisymm_1 : ∀ (a b : α), a ≤ b → b ≤ a → a = b}
{mul_le_mul_left_1 : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b}
{lt_of_mul_lt_mul_left_1 : ∀ (a b c : α), a * b < a * c → b < c},
  {mul := mul,
     mul_assoc := mul_assoc,
     one := one,
     one_mul := one_mul,
     mul_one := mul_one,
     mul_comm := mul_comm,
     le := le,
     lt := lt,
     le_refl := le_refl,
     le_trans := le_trans,
     lt_iff_le_not_le := lt_iff_le_not_le,
     le_antisymm := le_antisymm,
     mul_le_mul_left := mul_le_mul_left,
     lt_of_mul_lt_mul_left := lt_of_mul_lt_mul_left} =
    {mul := mul_1,
     mul_assoc := mul_assoc_1,
     one := one_1,
     one_mul := one_mul_1,
     mul_one := mul_one_1,
     mul_comm := mul_comm_1,
     le := le_1,
     lt := lt_1,
     le_refl := le_refl_1,
     le_trans := le_trans_1,
     lt_iff_le_not_le := lt_iff_le_not_le_1,
     le_antisymm := le_antisymm_1,
     mul_le_mul_left := mul_le_mul_left_1,
     lt_of_mul_lt_mul_left := lt_of_mul_lt_mul_left_1} →
  mul = mul_1 ∧ one = one_1 ∧ le = le_1 ∧ lt = lt_1
ordered_comm_monoid.mk.inj_arrow : Π {α : Type u_1} {mul : α → α → α} {mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)} {one : α}
{one_mul : ∀ (a : α), 1 * a = a} {mul_one : ∀ (a : α), a * 1 = a} {mul_comm : ∀ (a b : α), a * b = b * a}
{le lt : α → α → Prop} {le_refl : ∀ (a : α), a ≤ a}
{le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c}
{lt_iff_le_not_le :
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)}
{le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b}
{mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b}
{lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c} {mul_1 : α → α → α}
{mul_assoc_1 : ∀ (a b c : α), a * b * c = a * (b * c)} {one_1 : α} {one_mul_1 : ∀ (a : α), 1 * a = a}
{mul_one_1 : ∀ (a : α), a * 1 = a} {mul_comm_1 : ∀ (a b : α), a * b = b * a} {le_1 lt_1 : α → α → Prop}
{le_refl_1 : ∀ (a : α), a ≤ a} {le_trans_1 : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c}
{lt_iff_le_not_le_1 :
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)}
{le_antisymm_1 : ∀ (a b : α), a ≤ b → b ≤ a → a = b}
{mul_le_mul_left_1 : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b}
{lt_of_mul_lt_mul_left_1 : ∀ (a b c : α), a * b < a * c → b < c},
  {mul := mul,
     mul_assoc := mul_assoc,
     one := one,
     one_mul := one_mul,
     mul_one := mul_one,
     mul_comm := mul_comm,
     le := le,
     lt := lt,
     le_refl := le_refl,
     le_trans := le_trans,
     lt_iff_le_not_le := lt_iff_le_not_le,
     le_antisymm := le_antisymm,
     mul_le_mul_left := mul_le_mul_left,
     lt_of_mul_lt_mul_left := lt_of_mul_lt_mul_left} =
    {mul := mul_1,
     mul_assoc := mul_assoc_1,
     one := one_1,
     one_mul := one_mul_1,
     mul_one := mul_one_1,
     mul_comm := mul_comm_1,
     le := le_1,
     lt := lt_1,
     le_refl := le_refl_1,
     le_trans := le_trans_1,
     lt_iff_le_not_le := lt_iff_le_not_le_1,
     le_antisymm := le_antisymm_1,
     mul_le_mul_left := mul_le_mul_left_1,
     lt_of_mul_lt_mul_left := lt_of_mul_lt_mul_left_1} →
  Π ⦃P : Sort l⦄, (mul = mul_1 → one = one_1 → le = le_1 → lt = lt_1 → P) → P
ordered_comm_monoid.mk.sizeof_spec : ∀ (α : Type u_1) [α_inst : has_sizeof α] (mul : α → α → α)
(mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) (one : α) (one_mul : ∀ (a : α), 1 * a = a)
(mul_one : ∀ (a : α), a * 1 = a) (mul_comm : ∀ (a b : α), a * b = b * a) (le lt : α → α → Prop)
(le_refl : ∀ (a : α), a ≤ a) (le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
(lt_iff_le_not_le :
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous))
(le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b)
(mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c),
  ordered_comm_monoid.sizeof α
      {mul := mul,
       mul_assoc := mul_assoc,
       one := one,
       one_mul := one_mul,
       mul_one := mul_one,
       mul_comm := mul_comm,
       le := le,
       lt := lt,
       le_refl := le_refl,
       le_trans := le_trans,
       lt_iff_le_not_le := lt_iff_le_not_le,
       le_antisymm := le_antisymm,
       mul_le_mul_left := mul_le_mul_left,
       lt_of_mul_lt_mul_left := lt_of_mul_lt_mul_left} =
    1 + sizeof one
ordered_comm_monoid.mul : Π {α : Type u_1} [c : ordered_comm_monoid α], α → α → α
ordered_comm_monoid.mul_assoc : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
ordered_comm_monoid.mul_comm : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a b : α), a * b = b * a
ordered_comm_monoid.mul_le_mul_left : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
ordered_comm_monoid.mul_one : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a : α), a * 1 = a
ordered_comm_monoid.no_confusion : Π {α : Type u_1} {P : Sort l} {v1 v2 : ordered_comm_monoid α},
  v1 = v2 → ordered_comm_monoid.no_confusion_type P v1 v2
ordered_comm_monoid.no_confusion_type : Π {α : Type u_1}, Sort l → ordered_comm_monoid α → ordered_comm_monoid α → Sort l
ordered_comm_monoid.one : Π (α : Type u_1) [c : ordered_comm_monoid α], α
ordered_comm_monoid.one_mul : ∀ {α : Type u_1} [c : ordered_comm_monoid α] (a : α), 1 * a = a
ordered_comm_monoid.rec : Π {α : Type u_1} {C : ordered_comm_monoid α → Sort l},
  (Π (mul : α → α → α) (mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) (one : α)
   (one_mul : ∀ (a : α), 1 * a = a) (mul_one : ∀ (a : α), a * 1 = a) (mul_comm : ∀ (a b : α), a * b = b * a)
   (le lt : α → α → Prop) (le_refl : ∀ (a : α), a ≤ a)
   (le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
   (lt_iff_le_not_le :
     auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous))
   (le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a

[Johan Commelin]

The output of the second command is:

add_ordered_comm_monoid : Type u_1 → Type u_1

[Johan Commelin]

/me is :sad:

[Johan Commelin]

Is there any hope this could be fixed?

[Chris Hughes]

I think for structures you need to just define the second structure separately, and add the attribute afterwards. Also it should be called ordered_add_comm_monoid I think.

[Johan Commelin]

I think for structures you need to just define the second structure separately, and add the attribute afterwards. Also it should be called ordered_add_comm_monoid I think.

Ok, I'll rename.

[Johan Commelin]

So... if I add the attribute afterwards... does that match up all those auto-generated things? Or is it ok if those aren't matched up?

[Chris Hughes]

I think so. I guess that's how it works with group and all the other classes.

[Chris Hughes]

It won't match up the auto generated things actually. I misread the question.

[Johan Commelin]

I fear that will cause problems...

[Chris Hughes]

I think you have to do it by hand.
From algebra/group

attribute [to_additive add_group] group
attribute [to_additive add_group.mk] group.mk
attribute [to_additive add_group.to_has_neg] group.to_has_inv
attribute [to_additive add_group.to_add_monoid] group.to_monoid
attribute [to_additive add_group.add_left_neg] group.mul_left_inv
attribute [to_additive add_group.add] group.mul
attribute [to_additive add_group.add_assoc] group.mul_assoc
attribute [to_additive add_group.zero] group.one
attribute [to_additive add_group.zero_add] group.one_mul
attribute [to_additive add_group.add_zero] group.mul_one
attribute [to_additive add_group.neg] group.inv

[Patrick Massot]

Unfortunately, Simon never managed to complete https://github.com/leanprover-community/mathlib/pull/431

[Johan Commelin]

I dumped the output of that print command into a file called test.out.
And then

cat test.out| ./to_additive.sh ordered_comm_monoid ordered_add_comm_monoid
attribute [to_additive ordered_add_comm_monoid.cases_on] ordered_comm_monoid.cases_on
attribute [to_additive ordered_add_comm_monoid.has_sizeof_inst] ordered_comm_monoid.has_sizeof_inst
attribute [to_additive ordered_add_comm_monoid.le] ordered_comm_monoid.le
attribute [to_additive ordered_add_comm_monoid.le_antisymm] ordered_comm_monoid.le_antisymm
attribute [to_additive ordered_add_comm_monoid.le_refl] ordered_comm_monoid.le_refl
attribute [to_additive ordered_add_comm_monoid.le_trans] ordered_comm_monoid.le_trans
attribute [to_additive ordered_add_comm_monoid.lt] ordered_comm_monoid.lt
attribute [to_additive ordered_add_comm_monoid.lt._default] ordered_comm_monoid.lt._default
attribute [to_additive ordered_add_comm_monoid.lt._default.equations._eqn_1] ordered_comm_monoid.lt._default.equations._eqn_1
attribute [to_additive ordered_add_comm_monoid.lt_iff_le_not_le] ordered_comm_monoid.lt_iff_le_not_le
attribute [to_additive ordered_add_comm_monoid.lt_of_mul_lt_mul_left] ordered_comm_monoid.lt_of_mul_lt_mul_left
attribute [to_additive ordered_add_comm_monoid.mk] ordered_comm_monoid.mk
attribute [to_additive ordered_add_comm_monoid.mk.inj] ordered_comm_monoid.mk.inj
attribute [to_additive ordered_add_comm_monoid.mk.inj_arrow] ordered_comm_monoid.mk.inj_arrow
attribute [to_additive ordered_add_comm_monoid.mk.sizeof_spec] ordered_comm_monoid.mk.sizeof_spec
attribute [to_additive ordered_add_comm_monoid.mul] ordered_comm_monoid.mul
attribute [to_additive ordered_add_comm_monoid.mul_assoc] ordered_comm_monoid.mul_assoc
attribute [to_additive ordered_add_comm_monoid.mul_comm] ordered_comm_monoid.mul_comm
attribute [to_additive ordered_add_comm_monoid.mul_le_mul_left] ordered_comm_monoid.mul_le_mul_left
attribute [to_additive ordered_add_comm_monoid.mul_one] ordered_comm_monoid.mul_one
attribute [to_additive ordered_add_comm_monoid.no_confusion] ordered_comm_monoid.no_confusion
attribute [to_additive ordered_add_comm_monoid.no_confusion_type] ordered_comm_monoid.no_confusion_type
attribute [to_additive ordered_add_comm_monoid.one] ordered_comm_monoid.one
attribute [to_additive ordered_add_comm_monoid.one_mul] ordered_comm_monoid.one_mul
attribute [to_additive ordered_add_comm_monoid.rec] ordered_comm_monoid.rec
attribute [to_additive ordered_add_comm_monoid.rec_on] ordered_comm_monoid.rec_on
attribute [to_additive ordered_add_comm_monoid.sizeof] ordered_comm_monoid.sizeof
attribute [to_additive ordered_add_comm_monoid.to_comm_monoid] ordered_comm_monoid.to_comm_monoid
attribute [to_additive ordered_add_comm_monoid.to_partial_order] ordered_comm_monoid.to_partial_order

[Johan Commelin]

cat to_additive.sh
#!/bin/bash

MUL=$1
ADD=$2

grep "^$MUL" | sed "/$MUL : .*/d;s/$MUL.\([^ ]*\) : .*/attribute [to_additive $ADD.\1] $MUL.\1/"

[Johan Commelin]

That might be a snippet that we want to keep around as long as to_additive doesn't do this by itself.

[Johan Commelin]

Except that it is hopelessly broken :sad: I need recursion.

[Johan Commelin]

This is certainly not a stable approach

[Mario Carneiro]

I tried setting up to_additive to do this automatically, but it's too slow

[Mario Carneiro]

#print prefix is about as fast as printing all definitions in the environment

[Johan Commelin]

That is really very sad...
Can we have to_additive? that will trace the block of to_additive statements?
It would be quite helpful, I guess.

[Johan Commelin]

This example has been posted many times:

type mismatch at application
  semigroup._proof_1 α _inst_1
term
  _inst_1
has type
  add_semigroup α
but is expected to have type
  semigroup α

[Johan Commelin]

My question is: what is semigroup._proof_1?

[Johan Commelin]

If I try to #print it, I get unknown identifier semigroup._proof_1.

[Sebastian Ullrich]

It's a proof abstracted (extracted) from a definition

[Sebastian Ullrich]

This is done for all "non-trivial" proofs (i.e. terms of type Prop) inside a definition

[Johan Commelin]

But it's not a "known identifier"

[Sebastian Ullrich]

Yes, it's a hidden auxiliary definition. Users are not supposed to interact with it, though I suppose meta programs may still have to.

[Johan Commelin]

to_additive has a hard time interacting with it...
I can't write

attribute [to_additive add_semigroup._proof_1] semigroup._proof_1

[Mario Carneiro]

You should be able to see the definition. Possibly the error is causing the theorem to not be generated in the first place

[Kevin Buzzard]

I think it would be great to have a to_additive thing. There has been some talk about this recently. The current system is a bore:

import algebra.group.to_additive

structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] :=
(to_fun : M → N)
(map_one : to_fun 1 = 1)
(map_mul : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

infixr ` →* `:25 := monoid_hom

structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N] :=
(to_fun : M → N)
(map_zero : to_fun 0 = 0)
(map_add : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

infixr ` →+ `:25 := add_monoid_hom

-- #print prefix monoid_hom says this is everything (I think; it was generated manually)
attribute [to_additive add_monoid_hom] monoid_hom
attribute [to_additive add_monoid_hom.cases_on] monoid_hom.cases_on
attribute [to_additive add_monoid_hom.has_sizeof_inst] monoid_hom.has_sizeof_inst
attribute [to_additive add_monoid_hom.map_add] monoid_hom.map_mul
attribute [to_additive add_monoid_hom.map_zero] monoid_hom.map_one
attribute [to_additive add_monoid_hom.mk] monoid_hom.mk
attribute [to_additive add_monoid_hom.mk.inj] monoid_hom.mk.inj
attribute [to_additive add_monoid_hom.mk.inj_arrow] monoid_hom.mk.inj_arrow
attribute [to_additive add_monoid_hom.mk.inj_eq] monoid_hom.mk.inj_eq
attribute [to_additive add_monoid_hom.mk.sizeof_spec] monoid_hom.mk.sizeof_spec
attribute [to_additive add_monoid_hom.no_confusion] monoid_hom.no_confusion
attribute [to_additive add_monoid_hom.no_confusion_type] monoid_hom.no_confusion_type
attribute [to_additive add_monoid_hom.rec] monoid_hom.rec
attribute [to_additive add_monoid_hom.rec_on] monoid_hom.rec_on
attribute [to_additive add_monoid_hom.sizeof] monoid_hom.sizeof
attribute [to_additive add_monoid_hom.to_fun] monoid_hom.to_fun

namespace monoid_hom
variables {M : Type*} {N : Type*} [monoid M] [monoid N]

@[to_additive add_monoid_hom.id] -- the line causing the problem
def id (M : Type*) [monoid M] : M →* M :=
{ to_fun := id,
  map_one := rfl,
  map_mul := λ _ _, rfl }
/-
type mismatch at application
  id._proof_1 M _inst_3
term
  _inst_3
has type
  add_monoid M
but is expected to have type
  monoid M
-/

  end monoid_hom

Can I just not expect definitions to work automatically? I don't know how to debug the error. Does it just say "you can't do this -- you're going to have to make that definition manually and then do another bunch of to_additive stuff"?

[Johan Commelin]

@Yury G. Kudryashov Thanks for you amazing work. One little issue:
https://github.com/leanprover-community/mathlib/blob/c5128756d54f1f5207da88c6509647bbf1c57c2c/src/topology/algebra/open_subgroup.lean#L122
When I write V.prod, it says

/home/jmc/data/math/lean-perfectoid-spaces/src/for_mathlib/nonarchimedean/basic.lean:101:10: error:
invalid field notation, 'prod' is not a valid "field" because environment does not contain 'open_add_subgroup.prod'

[Johan Commelin]

I'm not sure where open_add_subgroup.prod went.

[Johan Commelin]

Aaah! The auto-naming turned prod into sum.

[Johan Commelin]

I'm not sure if that is what we want here.

[Patrick Massot]

Can't you state by hand the additive translation and tag it afterwards?

[Patrick Massot]

I sometimes do that when to_additive transform x*y⁻¹ into x + -y instead of x-y

[Johan Commelin]

I need to relearn how to use it (-;

[Johan Commelin]

How do I pass it a name nowadays?

[Johan Commelin]

If I just type something after to_additive I get the following warning:

`to_additive topological_group.nhds_translation_mul_inv_left`: remove `name` argument

[Johan Commelin]

Coming from the following code:

@[to_additive nhds_translation_add_neg_left]
lemma nhds_translation_mul_inv_left (g : G) :

[Patrick Massot]

The commit message from https://github.com/leanprover-community/mathlib/commit/c5128756d54f1f5207da88c6509647bbf1c57c2c is not very encouraging

[Patrick Massot]

But I guess to_additive would find the correct name in your case, right?

[Johan Commelin]

Aha, you have to remove all the names of all declarations that you depend on. Otherwise to_additive refuses to do its job.

[Johan Commelin]

@Yury G. Kudryashov Cool, it works! Thanks for this very useful change!

[Yury G. Kudryashov]

Hi, I should change trace message to “you may remove name argument”. It is issued, if the autogenerated name coincides with the manually provided one.

[Yury G. Kudryashov]

@Patrick Massot About x + -y vs x - y: probably we should change the default has_dvd instance from [comm_semiring α] to [group α] in the core, and add attribute [to_additive has_sub] has_dvd

[Yury G. Kudryashov]

@Johan Commelin See also Name generation section of the module docstring in src/algebra/group/to_additive.lean.

[Yury G. Kudryashov]

Briefly speaking, it tries to autogenerate the correct name. If you want to adjust the result, then you can either provide the last part of the new name (and it maps the prefix according to the current dictionary), or provide the full name.

[Johan Commelin]

But that's not enough. Because it actually didn't generate anything in those cases. So in later lemmas it would say "unknown identifier so_and_so"

[Yury G. Kudryashov]

Looks like a bug. Could you please repeat in which case it fails?

[Johan Commelin]

Hmm, let me see. I think it was in an example like this (don't have Lean at the moment):

namespace group
variables {G : Type} [group G]

@[to_additive add_foo]
lemma mul_foo (g : G) : g = g := rfl

@[to_additive add_bar]
lemma mul_bar (g : G) : g = g := mul_foo g

end group

I think I had homeomorphic example. And mul_bar would complain that it didn't know about mul_foo, or something like that.

[Yury G. Kudryashov]

Thanks, I'll look into this tonight.

[Kevin Buzzard]

import algebra.group

namespace group
variables {G : Type} [group G]

@[to_additive]
lemma mul_foo (g : G) : g = g := rfl

@[to_additive]
lemma mul_bar (g : G) : g = g := mul_foo g

end group

works for me

[Yaël Dillies]

If someone could diagnose what's going on with docs#list.prod_take_mul_prod_drop in #15676, that would be greatly appreciated. to_additive tries (and obviously fails) to additivize a docs#linear_ordered_comm_monoid_with_zero instance, but the lemma doesn't mention them anywhere! I suspect what's going on is that I removed docs#nat.le_zero_iff in favor of docs#le_zero_iff, and it tries to additivize it?

[Ruben Van de Velde]

Are those the same link?

[Yaël Dillies]

Fixed, sorry

[Eric Rodriguez]

yeah, it's that. you just have to squeeze the simps and then make it like @le_zero_iff ℕ

[Eric Rodriguez]

see the source of docs#monoid.exponent_exists_iff_ne_zero

[Yaël Dillies]

Eric, you can type src#monoid.exponent_exists_iff_ne_zero directly :smile:

[Eric Rodriguez]

woah that's neat

[Eric Rodriguez]

the old thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_additive.20.26.20exponents