simps bug

Stream: general

[Kevin Buzzard]

import tactic

variables (M : Type*) [comm_monoid M]

/-- The `n`th power map on a commutative monoid for a natural `n`, considered as a morphism of
monoids. -/
@[to_additive nsmul_add_monoid_hom "Multiplication by a natural `n` on a commutative additive
monoid, considered as a morphism of additive monoids.", simps]
def pow_monoid_hom (n : ℕ) : M →* M :=
{ to_fun := (^ n),
  map_one' := one_pow _,
  map_mul' := λ a b ,mul_pow a b n }

#check pow_monoid_hom_apply -- works
#check nsmul_add_monoid_hom_apply -- doesn't work
#check pow_add_monoid_hom_apply -- oops
/-
pow_add_monoid_hom_apply :
  ∀ (M : Type u_2) [_inst_1 : add_comm_monoid M] (n : ℕ) (_x : M),
  ⇑(nsmul_add_monoid_hom M n) _x = n • _x
-/

[Kevin Buzzard]

Maybe to_additive should change pow to nsmul and gpow to gsmul? Not sure though. Whether or not it does, I guess simps should spot the human-generated name?

[Johan Commelin]

Does it work if you put simps before to_additive?

[Johan Commelin]

Or do you just not get any lemma at all?

[Yakov Pechersky]

Can you do simps attribute tagging as a separate command as a stopgap in the meantime?

[Johan Commelin]

You mean, no simps at all on the definition, and then below the def'n write

attribute [simps] pow_monoid_hom nsmul_add_monoid_hom

I guess that should work? :thumbs_up:

[Yakov Pechersky]

Or simps prior to to_additive, and a separate tag on the nsmul generated hom

[Johan Commelin]

But that breaks symmetry :wink:

[Eric Wieser]

Yakov Pechersky said:

Or simps prior to to_additive, and a separate tag on the nsmul generated hom

simps complains if you put it before to_additive, so this isn't an option.

[Eric Wieser]

here's a much shorter version of the bug:

-- subtype is the easiest way I could think of to get a simps lemma
@[to_additive bar, simps]
def foo (M : Type*) [comm_monoid M] : subtype (λ f : M, true) := ⟨1, trivial⟩

which errors with to_additive: can't transport foo_coe to itself.

[Floris van Doorn]

Fixed in #8457

[Floris van Doorn]

@Johan Commelin Your suggestion still generates the lemma pow_add_monoid_hom_apply.

[Johan Commelin]

Huh? I don't understand how that can happen. If you call

attribute [simps] nsmul_add_monoid_hom

then it shouldn't put the pow back into the name, right?

[Floris van Doorn]

attribute [simps] pow_monoid_hom generates that lemma. If a declaration is tagged with @[to_additive] and then with @[simps] then simps automatically additivizes all generated simps-lemmas. Before #8457 it would just use the auto-generated name by to_additive.

[Johan Commelin]

Aah, now I see.