Help with notation and notation3

Stream: mathlib4

[David Ang]

I'm trying to understand how to write custom notation. Here is my attempt so far at trying to do this for the kernel of multiplication by an integer n on an AddCommGroup (there seems to be at least three different ways of expressing the same map that are currently unrelated to one another by any lemma --- zsmulAddGroupHom, DistribMulAction.toAddMonoidHom, AddMonoidHom.smul --- but that's a story for another day):

import Mathlib.GroupTheory.Subgroup.Basic

variable (G : Type) [AddCommGroup G] (n : ℤ)

notation3 G "[" n "]1" => AddMonoidHom.ker (DistribMulAction.toAddMonoidHom G n)
notation G "[" n "]2" => AddMonoidHom.ker (DistribMulAction.toAddMonoidHom G n)
notation G "[" n "]3" => AddMonoidHom.ker (zsmulAddGroupHom (α := G) n)
notation3 G "[" n "]4" => AddMonoidHom.ker (zsmulAddGroupHom (α := G) n)

#check G[n]1 -- prints G[n]1
#check G[n]2 -- prints G[n]1
#check G[n]3 -- prints AddMonoidHom.ker (zsmulAddGroupHom n)
#check G[n]4 -- prints AddMonoidHom.ker (zsmulAddGroupHom n)

The numbering at the end is just to see what's going on more clearly. I was told that notation3 sometimes works when notation doesn't (e.g. G[n]2 doesn't work), but I can't figure out how to make it work in general (e.g. G[n]3), and set_option trace.notation3 true for the last one gives:

Could not elaborate pattern
  AddMonoidHom.ker (zsmulAddGroupHom (α := G) n)
Error: application type mismatch
  AddMonoidHom.ker (zsmulAddGroupHom n)
argument
  zsmulAddGroupHom n
has type
  @AddMonoidHom G G (@AddMonoid.toAddZeroClass G (@SubNegMonoid.toAddMonoid G SubtractionMonoid.toSubNegMonoid))
    AddMonoid.toAddZeroClass : Type ?u.13541
but is expected to have type
  @AddMonoidHom G G (@AddMonoid.toAddZeroClass G (@SubNegMonoid.toAddMonoid G AddGroup.toSubNegMonoid))
    AddMonoid.toAddZeroClass : Type ?u.13541

@Kyle Miller any ideas what's going on and how to make the last one work? I have to use zsmulAddGroupHom because I think there's no analogue of DistribMulAction.toAddMonoidHom for Monoid currently.

[Kyle Miller]

In example 4 I'm seeing an error on the notation3 command

application type mismatch
  AddMonoidHom.ker (zsmulAddGroupHom n)
argument
  zsmulAddGroupHom n
has type
  @AddMonoidHom G G (@AddMonoid.toAddZeroClass G (@SubNegMonoid.toAddMonoid G SubtractionMonoid.toSubNegMonoid))
    AddMonoid.toAddZeroClass : Type ?u.13462
but is expected to have type
  @AddMonoidHom G G (@AddMonoid.toAddZeroClass G (@SubNegMonoid.toAddMonoid G AddGroup.toSubNegMonoid))
    AddMonoid.toAddZeroClass : Type ?u.13462

[David Ang]

Yes I included the error message in my first post too :)

[Kyle Miller]

Right, so you did :upside_down:

One solution here is to give up on a notation that works for all G and focus on the local variable G

local notation3 "G[" n "]4" => AddMonoidHom.ker (zsmulAddGroupHom (α := G) n)

[Kyle Miller]

The issue appears to be that when it's trying to build the pattern, it needs an AddCommGroup instance available to the G variable in the notation, but there isn't a way to tell notation3 that there is one.

[Kyle Miller]

Usually notation3 can handle missing instances, but in this case the missing instance leads to a type error, because, presumably, it needs some definitional property that comes with an actual AddCommGroup instance

[Kyle Miller]

Another solution is to use notation and then write a custom pretty printer.

[David Ang]

Kyle Miller said:

Another solution is to use notation and then write a custom pretty printer.

I can't use the local notation because G could be anything - how would one do this?

[David Ang]

Is there no way to supply the necessary instances in the notation manually?

[Kyle Miller]

Just to be clear about notation/notation3 and variables, the the commands don't look at anything defined by variables, except for local notation3, so in your examples the variable command can come after all of them without any change to the meaning.

There's no feature right now for letting notation3 know that some variable must have some instance in scope. It might be a good improvement.

[Kyle Miller]

In the meantime, maybe you can find another way to express this map that it's able to elaborate?

[Kyle Miller]

The fundamental issue here as I understand it is that it's trying to elaborate the term on the right-hand side of the =>, and without extra information that we're not really able to provide it's failing.

[David Ang]

I might just have to cope with no pretty-printed notation...

[Kyle Miller]

It's possible to write a pretty printer for it, but you'd have to study the few @[delab ...] examples that are in mathlib, std, and lean

[Kyle Miller]

The notation3 command tries to generate one of these automatically, and a limitation is that it only works if it can elaborate the pattern, and a further limitation is that even if that works it might be too conservative and not apply in practice