Function.comp pretty printing

Stream: lean4

[Patrick Massot]

I don't remember whether I already reported that. Lean 4 doesn't like displaying an applied function composition:

variable (f : α → β) (g : β → γ) (x : α)

#check g ∘ f -- display ok: g ∘ f : α → γ
#check (g ∘ f) x -- display not ok: Function.comp g f x : γ

This happens with #check but also in tactic state.

[Henrik Böving]

Right now function composition is just a normal infix notation command so it's pretty printer is auto generated and does not end up recognizing the second pattern. If we want to display the 2nd thing correctly we would need to build custom delaborators instead.

[Eric Rodriguez]

so every infix ever now needs custom delaborators instead of it just working out the box?

[Eric Rodriguez]

this seems like a regression

[Henrik Böving]

No, as you can see the infix notation does delaborate correctly in the normal case

[Henrik Böving]

infix is a macro for notation and notation auto generates a delaborator, that delaborator just doesn't catch the 2nd pattern that patrick is showing. There went a little effort on my side into it already to make it better at auto generating that delaborator but I am not sure whether it is possible to extend it to what patrick is demanding here since it is more of a special case where the thing your notation generates happens to be a function so it makes sense to write it in the above way.

[Henrik Böving]

docs4#Lean.Elab.Command.mkSimpleDelab is the function in charge of doing this

[Kyle Miller]

This will also affect what we call "pi instances". For example, if f g : α -> Nat, then (f + g) x = f x + g x won't pretty print properly if I'm understanding the issue with Function.comp.

[Sebastian Ullrich]

This is a simple bug, it's supposed to work https://github.com/leanprover/lean4/issues/1367

[Patrick Massot]

Should I open a new bug report then?

[Sebastian Ullrich]

Please do, it's too late for actually writing code :)

[Patrick Massot]

I opened lean4#2045

[Dan Velleman]

I posted a solution to this problem here

A new unexpander will fix it.

[Dan Velleman]

But perhaps you are looking for a more general solution.

[Patrick Massot]

Could you add this comment one the GitHub issue?

[Mario Carneiro]

There is a general mechanism for this in std, pending a move to core

[Mario Carneiro]

it basically amounts to using a delaborator combinator that has built in over-application handling

[Patrick Massot]

Do you say this can be fixed by importing something from std?

[Mario Carneiro]

docs4#Lean.PrettyPrinter.Delaborator.withOverApp

[Mario Carneiro]

no, this is a combinator that has to be retrofitted into affected delaborators

[Mario Carneiro]

to get support for arbitrary infix notations this combinator has to be used by the autogenerated delaborator

[Patrick Massot]

I suspect @Heather Macbeth would like to see this fixed rather soon for her teaching.

[Heather Macbeth]

Thanks for the alert. Indeed I would (and I am sure @Dan Velleman and @Rob Lewis would too), I have added it to the list where I track issues relating to teaching. However, for me personally, if I teach in Lean 4 this semester (still not sure), I will not get to function composition until March or April.

[Dan Velleman]

Was this supposed to be fixed by #2046? I think that was merged on Jan. 26, but I just tried it (with leanprover/lean4:nightly-2023-01-29) and it's not working:

variable (f : α → β) (g : β → γ) (x : α)

#check (g ∘ f) x   --Function.comp g f x : γ

Is there something else I'm supposed to do to get pretty printing of function composition to work?