notation and docstrings

Stream: Polynomial Freiman-Ruzsa conjecture

[Kalle Kytölä]

It is nice that the PFR formalization uses a lot of notation that makes it closer in appearance to pen-and-paper math.

However, when I jumped to a new local corner of the proof yesterday, I noticed that the heavy use of notation hinders the local readability unless one has a good global view of the proof that is sufficiently strong to aid memory with the notation (which I clearly didn't have :sweat_smile:).

On the other hand, one of the nice features of interactive theorem proving is that one can have a lot of information interactively available to the user, such as docs shows upon hovering on a notation. For instance hovering over I₁ could display "I₁ := I[X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂'], the conditional mutual information of X₁ + X₂ and X₁' + X₂ given the quadruple sum X₁ + X₂ + X₁' + X₂'.", and this would actually be better than reading a pen-and-paper statement.

Of course the go to definition works with notation, already. So ITP already has some of its niceness, hovers are just a small addition, but I believe they still make a difference.

Is a PR adding docstrings to local notations (such as k, I₁, I₂, U, V, W, S) and @[inherit_doc] to τ welcome? (Many other notations such as Rusza distance, entropies, ... had @[inherit_doc]s already.)

[Terence Tao]

Kalle Kytölä said:

It is nice that the PFR formalization uses a lot of notation that makes it closer in appearance to pen-and-paper math.

However, when I jumped to a new local corner of the proof yesterday, I noticed that the heavy use of notation hinders the local readability unless one has a good global view of the proof that is sufficiently strong to aid memory with the notation (which I clearly didn't have :sweat_smile:).

On the other hand, one of the nice features of interactive theorem proving is that one can have a lot of information interactively available to the user, such as docs shows upon hovering on a notation. For instance hovering over I₁ could display "I₁ := I[X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂'], the conditional mutual information of X₁ + X₂ and X₁' + X₂ given the quadruple sum X₁ + X₂ + X₁' + X₂'.", and this would actually be better than reading a pen-and-paper statement.

Of course the go to definition works with notation, already. So ITP already has some of its niceness, hovers are just a small addition, but I believe they still make a difference.

Is a PR adding docstrings to local notations (such as k, I₁, I₂, U, V, W, S) and @[inherit_doc] to τ welcome? (Many other notations such as Rusza distance, entropies, ... had @[inherit_doc]s already.)

I'd say that contributions to assist readability are just as welcome as contributions that fill in sorries, so I'd vote for adding whatever documentation you are willing to supply. (Many of the header docstrings for the files are also in need of an update - a byproduct of the project moving more quickly than expected.)

[Yaël Dillies]

This makes a lot of sense. Certainly, if it is not done now it will have to be done when upstreaming to mathlib.

[Scott Morrison]

(And not doing it now makes the upstreaming to mathlib more onerous, and thus less likely, and thus leading to great sadness. :-)

[Utensil Song]

It also makes sense to provide a notation table, mapping notations in LaTeX to the corresponding notational conventions in Lean heavily used in this project.