missing delaborator for finsum

Stream: mathlib4

[Kevin Buzzard]

I sometimes whinge about missing delaborators but this time when I found one I thought I'd try and figure out how to add it myself. But it's completely hopeless. Here is what I think is a missing delaborator:

import Mathlib

section delaborator

variable (α β : Type) [AddCommMonoid β] (s : Set α) (f : α → β) in
#check ∑ᶠ a ∈ s, f a -- ∑ᶠ (a : α) (_ : a ∈ s), f a : β

end delaborator

and I looked at how the notation ∑ᶠ was defined but it's just some call to notation3 so I don't really know where to start. I would like it to delaborate as the input, if possible.

[Yaël Dillies]

Kevin Buzzard said:

I would like it to elaborate as the input, if possible.

"delaborate", you mean

[Yaël Dillies]

#22048 contains an example of doing something similar for docs#Finset.sum. Do you want to try adapting it?

[Kyle Miller]

Let's not go down a path of custom delaborators for every notation. I consider Finset.sum to be a special case since it's not able to use the more general system due to Finset complexities.

notation3 ought to help us out here, but the fundamental problem is that we don't have a mechanism to re-compress the binders. There are some ad hoc ones in Mathlib/Util/Delaborators.lean, but it would be nice to work out a general system to delaborate extended binders.

[Kevin Buzzard]

I am interpreting this as "don't make the PR doing this", which I'm happy to do, but I would like to extend the API for finsum in general (e.g. #23284) because I prefer it to Finset.sum so perhaps I'll just have it locally if I can figure it out.

[Kyle Miller]

Yes, don't make a PR making a custom delaborator.

However, if you copy the idea of the ad hoc delaborators in Mathlib/Util/Delaborators.lean (which run the main delaborator and then adjust the binders), create (or find) a mathlib issue that tracks the fact that notation3 can't join binders, and then label the binder-joining delaborator with this, I think that would be an acceptable PR-able short-term solution.

[Kevin Buzzard]

I looked at Yael's PR and at the file you suggested, and unfortunately I found them both completely incomprehensible with my current state of knowledge about these things, so I'm afraid that what will actually happen is that I'll do nothing :-(

[Kyle Miller]

Could you make sure there's a mathlib issue at least and paste the issue number here? I'd like this all to Just Work one day.

[Kevin Buzzard]

I'm afraid I know so little that I don't even understand whether #13496 is the relevant issue or whether we're talking about something else here.

[Kyle Miller]

I can tell you that one's different. It's saying that Π₀ i j, δ i j doesn't parse.

[Kyle Miller]

I think there are no pre-existing issues about this

[Kyle Miller]

It seems we're repeating ourselves a little: #mathlib4 > finsum delaborator @ 💬 :smile:

The general point is, whenever you run into problems with notation3 notations, please report them. I'd like it to be able to handle the majority of our notational needs. In the ideal world, we never have to write delaborators ourselves — whenever we write low-level code like delaborators, it is Lean failing to provide us necessary functionality.

A neat thing with this particular issue in the current thread is that it we'll be going beyond what Lean 3 ever had. We already do this for a handful of notations, but it's definitely possible to do it for notation3 notations too.

[Patrick Massot]

Kyle Miller said:

It seems we're repeating ourselves a little: #mathlib4 > finsum delaborator @ 💬 :smile:

:older_man:

[Kevin Buzzard]

I didn't know that this was the same issue: in my example in this thread, Lean does print a finsum symbol; in the other thread it printed the word finsum. So in fact it's not that I forgot that thread, it's that my understanding of what's going on is so poor that I didn't understand that the two problems had the same root cause (assuming that this is what Kyle is saying).

[Kyle Miller]

Oh no, I don't mean to say that. I just mean the core issue to both is "notation3 should be able to handle this, but it doesn't have that feature yet"

[Kyle Miller]

and the answer isn't "let's write a custom delaborator", but "let's improve notation3"

[Kevin Buzzard]

My effort to write the issue is #23311 but I do not understand some of the words I've written there (I just copied phrases from this thread) so please feel free to edit.

[Kyle Miller]

Sorry to make it seem like it was the same issue, rather than a class of issues. I don't expect people to be able to know whether notation3 should be able to support something, but it's reasonable assuming problems with notation3 notation are problems with notation3. I'd like to avoid a future where mathlib is full of custom delaborators that all do slightly different things, and also a future where people spend too much time learning how to write/maintain delaborators. It's really neat that we have the ability to customize pretty printing to this degree, but for mathlib purposes, these should be a last resort.

Sometimes there are notations that really are one-off and can't be generalized, and need a custom delaborator. However, finsum is like any other "big operator" that can expand through nesting, and notation3 aims to support all big operators.