Documented type for Finset.sum_range etc.

Stream: mathlib4

[Terence Tao]

I am wondering if the documented type in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Fin.html for methods ilke Finset.sum_range is a little too terse? More precisely, I don't think the stated type

theorem Finset.sum_range{β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) :
(Finset.sum (Finset.range n) fun i => f i) = Finset.sum Finset.univ fun i => f ↑i

can actually be synthesized unambiguously; one needs something like

theorem Finset.sum_range{β : Type u_2} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) :
(Finset.sum (Finset.range n) fun i => f i) = Finset.sum Finset.univ fun i : Fin n => f ↑i

instead. Is this sort of terseness intentional in the Mathlib documentation? There are several further examples of this in Fin.html alone.

[Yaël Dillies]

This is a general issue with what's called "pretty-printing".

[Yaël Dillies]

Lean code is parsed using elaborators, which turn it into Lean syntax, represented as an abstract syntax tree. Tactics can do arbitrary manipulations on that AST. Then the AST is processed by delaborators to be pretty-printed in the infoview, or in the mathlib docs.

[Scott Morrison]

We had really hoped to have "round-tripping" pretty printing in Lean 4, i.e. anything that the pretty printer produced could be parsed correctly. As Mario said recently, that feature didn't ship. :-(

That said, the flexibility of the delaborator framework means we can usually make things better.

[Yaël Dillies]

Going from Lean code to Lean syntax and back to Lean code in a way that preserves the meaning is what's called round-tripping. One of the selling points of Lean 4 was that it would solve the round-tripping issues of Lean 3, but it hasn't so far.

[Terence Tao]

Yaël Dillies said:

Lean code is parsed using elaborators, which turn it into Lean syntax, represented as an abstract syntax tree. Tactics can do arbitrary manipulations on that AST. Then the AST is processed by delaborators to be pretty-printed in the infoview, or in the mathlib docs.

I see. I have noticed similar issues in directly using types from the infoview, mostly involving ambiguity in the ↑ operation. OK, I can work around this (though it adds to the pile of "minor stuff nobody tells you about that you have to figure out on your own".)

[Yaël Dillies]

Personally, I don't mind too much the lack of type ascription here, since one can easily reconstruct it from the lemma name. I find much more alarming the fact that the lemma doesn't get pretty-printed with ∑ notation. This is in my experience a much more annoying transformation to perform by hand (when done over many lemmas).

[Kevin Buzzard]

I find it very difficult to teach the pile of minor stuff which nobody tells you about, because it's a pretty big pile. Furthermore I am a victim of the phenomenon that I know most of the stuff in the pile and am forgetting what life was like when I didn't know it, making it more difficult to actually create a list of interesting things on the pile. This is why in my undergrad class I just get people writing Lean code by themselves ASAP and discovering this stuff themselves.

[Yaël Dillies]

Yaël Dillies said:

Personally, I don't mind too much the lack of type ascription here, since one can easily reconstruct it from the lemma name. I find much more alarming the fact that the lemma doesn't get pretty-printed with ∑ notation.

But maybe I care about the latter more because I know it's actionable.

[Terence Tao]

I actually started documenting what I could find of this pile while I learned Lean, before the "missing stair" effect kicked in: https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0 (in the "troubleshooting" tab mostly) . Will add this one to the list now.