delaborator for (∞ : ℝ≥0∞)

Stream: mathlib4

[Kevin Buzzard]

I've just noticed that even after open ENNReal, ∞ : ℝ≥0∞ gets prettyprinted as ⊤. This might confuse the poor authors of Annals papers who I am spamming with Lean code claiming to state their theorems. Is there some one-liner which can fix this, or are things not so simple?

import Mathlib

open ENNReal

#check (∞ : ℝ≥0∞) -- ⊤ : ℝ≥0∞

I think one fix might be changing this line in mathlib

/-- Notation for infinity as an `ENNReal` number. -/
scoped[ENNReal] notation "∞" => (⊤ : ENNReal)

to

/-- Notation for infinity as an `ENNReal` number. -/
scoped[ENNReal] notation3 "∞" => (⊤ : ENNReal)

but does this have unintended consequences?

[Kevin Buzzard]

In fact I am totally confused -- just above this we have

scoped[ENNReal] notation "ℝ≥0∞" => ENNReal

but this isn't notation3 and yet the notation sticks. Is it because one is a type and one a term?

[Yaël Dillies]

notation3 shouldn't have any unwanted consequences for such simple elab/delab pairs

[Floris van Doorn]

The delaborator that notation creates does roughly this: whenever it sees the syntax on the RHS (here (⊤ : ENNReal)), it will replace it with the notation you declared (here ∞). Note that this is an operation on syntax. If you write something on the RHS that elaborates to the same expression, but write it differently than how it is printed, then the delaborator will not fire. So the following notation commands all create delaborators that never(?) fire:

import Mathlib

notation "ℝ≥0∞" => @ENNReal

notation "∞" => @Top.top ENNReal instTopENNReal
notation "∞" => Top.top (α := ENNReal)
notation "∞" => (⊤ : ENNReal)

#check ENNReal -- ENNReal : Type
#check (⊤ : ℝ≥0∞) -- ⊤ : ℝ≥0∞

[Martin Dvořák]

IMO ⊤ is the symbol for the term whereäs ∞ is the symbol for the type [modifier]. I wouldn't use ∞ for both.

[Michael Rothgang]

Martin Dvořák said:

IMO ⊤ is the symbol for the term whereäs ∞ is the symbol for the type [modifier]. I wouldn't use ∞ for both.

I think you may be technically right, but I've never cared about this distinction in practice. If ∞ notation makes your code more approachable to Kevin's specialized audience, I wouldn't object.

[Martin Dvořák]

I understand the claim about the audience but consider that ℝ≥0∞ is not the only type with infinities.
There is also ℝ∞ and writing (∞ : ℝ∞) doesn't make sense.
Therefore, for consistency, I would avoid (∞ : ℝ≥0∞) as well.

[Eric Wieser]

@Floris van Doorn, I don't understand the point your code sample above is making; do you have an example where notation does work for delaborating as ∞?

[Eric Wieser]

I'm pretty sure no delaborators can inspect the original syntax in a #check to decide how to delaborate

[Michael Rothgang]

It's very clear what (∞ : ℝ∞) should mean --- so we could add notation for it if desired.

[Martin Dvořák]

Yeah but then (-∞ : ℝ∞) shoots you in the face.

[Michael Rothgang]

Indeed, \top and \bot being treated differently is unfortunate. I'm open to redefining EReal as WithTopBot Real.

[Martin Dvořák]

#general > WithBot (WithTop α)

[Jireh Loreaux]

Naming question: If we make ∞ delaborate for ℝ≥0∞, do we continue naming ENNReal lemmas with top or do we use infty?

[Rémy Degenne]

Could we go back to Kevin's question? ∞is already notation for infinity in ENNReal, and is already used everywhere in the code (although we use top in names). It's just not used by the infoview. I'd also like that to change (it would allow me to copy an paste without having to change it everywhere). Is using notation3 the right solution?

[Jireh Loreaux]

so notation3 creates an actual delaborator whereas notation creates a (reverse?) macro?

[Yaël Dillies]

notation also creates a delaborator. It's just not a very good one

[Martin Dvořák]

There is always time to fix our historical mistakes. And deprecating ∞ as the name of the term (constant) would be far less disruptive than changing definitions.

[Jireh Loreaux]

But Floris mentioned it creates an operation on syntax, whereas a delaborator should be Expr → Syntax?

[Jireh Loreaux]

Martin Dvořák said:

There is always time to fix our historical mistakes. And deprecating ∞ as the name of the term (constant) would be far less disruptive than changing definitions.

Who's talking about changing definitions? And I don't think deprecating ∞ is even on the table. Why would we want that?

[Martin Dvořák]

Because once writing (∞ : ℝ∞) becomes socially acceptable, it will be a slippery slope and (-∞ : ℝ∞) might start appearing in the code.

[Floris van Doorn]

Eric Wieser said:

Floris van Doorn, I don't understand the point your code sample above is making; do you have an example where notation does work for delaborating as ∞?

The point was to hopefully help Kevin understand why these delaborators don't help with pretty-printing (or at least, to tell him "if you use these things in the RHS of your notation command, it will probably not fire for pretty-printing").
I don't know know any way to tell notation to pretty-print ⊤ only for ENNReal, but not for any other types.
I agree that delaborators cannot look at the source syntax.

[Eric Wieser]

Yaël Dillies said:

notation also creates a delaborator. It's just not a very good one

This is untrue; it creates an unexpander, as can be seen with

whatsnew in
notation "∞" => Top.top (α := ENNReal)

[Eric Wieser]

And the unexpander is basically like writing a delaborator of the form

do
  let orig : Syntax <- delab
  run_the_unexpander orig

[Jakub Nowak]

Martin Dvořák said:

Yeah but then (-∞ : ℝ∞) shoots you in the face.

We could make "-∞" a notation too.

[Floris van Doorn]

Eric Wieser said:

This is untrue; it creates an unexpander, as can be seen with

Oops, yes. I meant "unexpander" when I wrote "delaborator".

[Yaël Dillies]

Ah sure, yes

[Yury G. Kudryashov]

I have no opinion about usage of ∞ for ENNReal. I mean, I can use this notation or \top. However, it's very useful for smoothness, as we have $C^n$, $C^\infty$, and $C^\omega$, where $\infty$ is in fact WithTop.some \top in WithTop ENat.

[Kevin Buzzard]

Yes I totally agree that the smoothness use of infinity is useful (as well as being confusing and poorly-documented). I'm specifically talking about making mathlib output in L^p analysis easier to read for mathematicians (who typically have no idea what \top is) and am asking whether changing to notation3 is desired.

[Jireh Loreaux]

I think the answer is yes.

[Jon Eugster]

stumbled across #34953, is there any difference between using notation3 and adding a small delaborator:

scoped[ENNReal] notation "∞" => (⊤ : ENNReal)

namespace ENNReal

open Lean Lean.PrettyPrinter.Delaborator Lean.PrettyPrinter.Delaborator.SubExpr in
/-- Delaborate `(top : ENNReal)` as `∞`. -/
@[app_delab Top.top]
meta def Mathlib.Meta.delabInftyENNReal : Delab :=
  whenNotPPOption getPPExplicit <|
  whenPPOption getPPNotation do
    let_expr Top.top α _ := ← getExpr | failure
    guard <| α.isConstOf ``ENNReal
    let stx ← `(∞)
    annotateGoToSyntaxDef stx

[Jovan Gerbscheid]

These are mostly the same indeed. If they are exactly the same, I'd suggest using notation3 for its simplicity, but if the notation3 version is missing some feature, then a delaborator is the way to go indeed.

[Jon Eugster]

Tbh I don't fully know if there are exactly the same, the implementation of notation3 is quite lengthy with sprinkled -- HACK comments, but I think they might be identical for this.

Thanks for the quick answer!

[Eric Wieser]

Why not use whatsnew to see what delaborator it generates?

[Jovan Gerbscheid]

I imagine that the annotateGoToSyntaxDef could give different behaviour - this would be easy to test.

[Jon Eugster]

apparently annotateGoToSyntaxDef has the effect that shift-clicking in the infoview goes to the notation, while for notation3 it goes to deriving Top in the ENNReal definition. But in the editor, both versions jump to deriving Top?

[Jovan Gerbscheid]

What you see in the editor is not related to the delaborator, it is just related to the syntax/elaborator. That one is more tricky to influence.