GroupTheory.GroupAction.SubMulAction.Pointwise

Stream: mathlib4

[Moritz Firsching]

In mathlib4#1893, the only thing left is the following instance:

instance : Monoid (SubMulAction R M) :=
  { SubMulAction.Semigroup,
    SubMulAction.MulOneClass with
    mul := (· * ·)
    one := 1 }

In mathlib3 this was

instance : monoid (sub_mul_action R M) :=
{ mul := (*),
  one := 1,
  ..sub_mul_action.semigroup,
  ..sub_mul_action.mul_one_class }

and it says

unknown constant 'SubMulAction.MulOneClass'
unknown constant 'SubMulAction.Semigroup'

and expected structure, although I thought 'SubMulAction.MulOneClass' and 'SubMulAction.Semigroup' were defined just above.
Any hints how to fix this?

[Adam Topaz]

I think it's just the names. You can use #synth to get the instance names

[Adam Topaz]

in this case, this works:

instance : Monoid (SubMulAction R M) :=
  { instSemigroupSubMulActionToSMul,
    instMulOneClassSubMulActionToSMul with
    mul := (· * ·)
    one := 1 }

[Arien Malec]

or. better yet, rename the initial instances to something that isn't instSemigroupSubMulActionToSMulDivByInfinity

[Arien Malec]

you do that by, e.g. instance semiGroup: Semigroup (SubMulAction R M) <rest of declaration>

[Adam Topaz]

Or this

instance : Monoid (SubMulAction R M) :=
  { (inferInstance : Semigroup (SubMulAction R M)),
    (inferInstance : MulOneClass (SubMulAction R M)) with
    mul := (· * ·)
    one := 1 }

[Adam Topaz]

french quotes in the following variant

instance : Monoid (SubMulAction R M) :=
  { ‹Semigroup (SubMulAction R M)›,
    (inferInstance : MulOneClass (SubMulAction R M)) with
    mul := (· * ·)
    one := 1 }

gives a mysterious error:

type mismatch
  Semigroup.mul_assoc
has type
  ∀ (a b c : SubMulAction R M), a * b * c = a * (b * c) : Prop
but is expected to have type
  ∀ (a b c : SubMulAction R M), a * b * c = a * (b * c) : Prop

[Arien Malec]

naming the instances is better for multiple reasons:
1) Avoids future exponential name explosion
2) Easier to read in the doc search autocomplete
3) Reduces burden on downstream porting

[Jireh Loreaux]

4) Avoids calling TC inference (well, at least partially)

[Adam Topaz]

See the following related discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Syntax.20for.20unpacking.20structures/near/316074906

[Adam Topaz]

BTW, the mul and one fields are not necessary here.

[Adam Topaz]

but maybe they should stick around for consistency with mathlib3.

[Jireh Loreaux]

The point of repeating the mul and one fields is to give better definitional unfolding. I guess maybe this no longer matters because of eta for structures?

[Moritz Firsching]

ok, great, I added names for the instances and now everything seems to work!
Thanks for the explanations

[Eric Wieser]

Jireh Loreaux said:

The point of repeating the mul and one fields is to give better definitional unfolding. I guess maybe this no longer matters because of eta for structures?

I think this still matters, but new-style structures make it more confusing.