failure of dot notation

Stream: mathlib4

[Kevin Buzzard]

I think the following is well-understood, but not by me. Why does Lean 3 (category_of_elements.π X).left_op display as Functor.leftOp (CategoryOfElements.π X) in Lean 4? Dot notation is not being used. Is this something to do with "unexpanders", whatever they are? How can I fix this? This shows up in the unique broken proof in !4#3208 , which I'm trying to fix by comparing with the lean 3 proof, but the goals are displaying differently and it makes it more annoying to figure out what's going on.

[Eric Wieser]

What's the type of CategoryOfElements.π X?

[Kevin Buzzard]

Functor.Elements X ⥤ Cᵒᵖ, i.e. Functor ...

[Kevin Buzzard]

Another example in the same proof: Lean 3 (category_of_elements.map f).op.obj is displaying as (Functor.op (CategoryOfElements.map f)).obj in Lean 4.

[Adam Topaz]

@Kevin Buzzard you can add an unexpander similar to those in the file CategoryTheory/Functor/Basic

[Adam Topaz]

It's just the pretty printing that's different

[Eric Wieser]

It's not all dot notation that's broken though, is it?

[Kevin Buzzard]

/--
This unexpander will pretty print `F.obj X` properly.
Without this, we would have `Prefunctor.obj F.toPrefunctor X`.
-/
@[app_unexpander Prefunctor.obj] def
  unexpandFunctorObj : Lean.PrettyPrinter.Unexpander
  | `($_ $(F).toPrefunctor $(X)*)  => set_option hygiene false in `($(F).obj $(X)*)
  | _                           => throw ()

/--
This unexpander will pretty print `F.map f` properly.
Without this, we would have `Prefunctor.map F.toPrefunctor f`.
-/
@[app_unexpander Prefunctor.map] def
  unexpandFunctorMap : Lean.PrettyPrinter.Unexpander
  | `($_ $(F).toPrefunctor $(X)*)  => set_option hygiene false in `($(F).map $(X)*)
  | _                           => throw ()

This is gobbledegook to me.

[Adam Topaz]

1 sec

[Kevin Buzzard]

How do I go about understanding it? Sounds like ultimately I'm going to have to know what's going on here for teaching if I'm rolling my own stuff.

[Adam Topaz]

My naive understanding is that this (the first one) tells lean how to pretty print terms of the form
Prefunctor.obj F.toPrefunctor X Y Z ... and that it should be printed as F.obj X Y Z ....

[Adam Topaz]

So I think something similar to this would work for leftOp:

@[app_unexpander Functor.leftOp] def
  unexpandFunctorObj : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).leftOp $(X)*)
  | _                 => throw ()

[Eric Wieser]

How do I go about understanding it?

Maybe it helps to realize that docs4#Lean.PrettyPrinter.Unexpander is just an abbreviation for Lean.Syntax → Lean.PrettyPrinter.UnexpandM Lean.Syntax, whereLean.Syntax is roughly anything that can be quoted with `(...) , and UnexpandM is some monad you can probably just forget about, other than having throw () for failure

[Kevin Buzzard]

I'm afraid I don't know what "quoted" or ` means in this context, I'm totally lost. I don't know what Lean.Syntax is either. Where do I start?

[Kevin Buzzard]

What is $_? Is it related for some reason to @[app_unexpander Functor.leftOp]?

[Eric Wieser]

In Lean 3, `(foo bar %baz) matches the expr that you get when you write foo bar x, and it sets baz to the expr `(x) . Lean 4 is the same but with $ instead of %, and Syntax instead of Expr.

The $_ is just a wildcard, because we told lean to only call our function when the head symbol is Prefunctor.obj so we don't bother to match it again

[Kevin Buzzard]

What is X in $(X)*? Is * something like "one or more" or "zero or more" or something?

[Eric Wieser]

X is a binder like the n in Nat.succ n when matching a Nat

[Thomas Murrills]

Btw the metaprogramming book is a pretty good reference for most of these questions! :)

[Kevin Buzzard]

Why do we set_option hygiene false?

[Adam Topaz]

See here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unexpanders.20for.20functors/near/338793493

[Kevin Buzzard]

Oh thanks! That's also very helpful. I didn't really read that thread at the time because it was all beyond me, I was busy with non port things, and didn't need to know about it. Pretty much all those things have changed in the mean time :-)

At the end of the day, why is the user having to write this stuff at all? Why isn't dot notation just working? In the other thread someone referred to it as a feature request rather than a bug. Isn't my example above just a bug?

[Kyle Miller]

There's "dot notation" the convenient notation to write things and "dot notation" having Lean make use of it too when displaying things. The first one works fine, and just because Lean isn't yet using it itself doesn't mean anything is broken. (Your example is still correct, if unwieldy, output.)

[Kyle Miller]

I think Lean should definitely make use of dot notation when pretty printing. These unexpanders are a way to get that behavior on a case by case basis (cases where it's painful the feature is missing) until there is a general solution.

[Kevin Buzzard]

I see! Thanks everyone for this illuminating thread. I understand a lot better what's going on now.

[Kevin Buzzard]

OK so so far I have

@[app_unexpander Functor.leftOp] def
  unexpandFunctorleftOp : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).leftOp $(X)*)
  | _                 => throw ()

@[app_unexpander Functor.map] def
  unexpandFunctorMap : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).map $(X)*)
  | _                 => throw ()

@[app_unexpander Iso.toEquiv] def
  unexpandIsotoEquiv : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).toEquiv $(X)*)
  | _                 => throw ()

@[app_unexpander Iso.symm] def
  unexpandIsosymm : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).symm $(X)*)
  | _                 => throw ()

@[app_unexpander Equiv.trans] def
  unexpandEquivtrans : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).trans $(X)*)
  | _                 => throw ()

-- IsColimit.homIso'
@[app_unexpander IsColimit.homIso'] def
  unexpandIsColimithomIso' : Lean.PrettyPrinter.Unexpander
  | `($_ $F $(X)*)  => set_option hygiene false in `($(F).homIso' $(X)*)
  | _                 => throw ()

and I'm still not done (although it's working great!). Am I doing it wrong? Is the idea that we don't want these, or we do want these but we don't want to have to write them, or what?

By the way, I'm seeing ((blah).toEquiv).trans with brackets in Lean 4, whereas in Lean 3 I'm seeing (blah).to_equiv.trans. Is there anything I can do about this?