max and min delaborators

Stream: mathlib4

[Patrick Massot]

Nowadays every teaching or propaganda file that I write starts with

open Lean PrettyPrinter Delaborator SubExpr in
@[app_delab Max.max]
def delabMax : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity ``Max.max 4
  let m := mkIdent `max
  let x ← withNaryArg 2 delab
  let y ← withNaryArg 3 delab
  `($(m) $(x) $(y))

open Lean PrettyPrinter Delaborator SubExpr in
@[app_delab Min.min]
def delabMin : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity ``Min.min 4
  let m := mkIdent `min
  let x ← withNaryArg 2 delab
  let y ← withNaryArg 3 delab
  `($(m) $(x) $(y))

Is it already somewhere in Mathlib but scoped?

[Patrick Massot]

For people who are not used to delaborators: the purpose of this snippet is to bring back max x y in the infoview instead of the lattice notation for sup.

[Floris van Doorn]

I'm quite sure it's not, but I think it would be nice to have as scoped delaborators!

[Patrick Massot]

@Kyle Miller do you prefer to fix my delaborators here or on GitHub?

[Eric Wieser]

I think these could be unscoped if they tried to synth a LinearOrder

[Eric Wieser]

Arguably we should be adjusting the sup and inf delaborators to not replace the default one though

[Kyle Miller]

Let's make an option that conditionally enables/disables the linked sup/inf delaborators. That will work better than creating a delaborator that creates application syntax

[Kyle Miller]

This would mean

• changing those infix commands to be equivalent syntaxes
• creating a new option (pp.mathlib.minMaxAsLattice?)
• writing a delaborator for these notations and make them conditional on the option

For the third point, we can't use an app unexpanders since they currently can't be conditional on options. For the first, we don't currently have infixl:69 (print := false) " ⊓ " => Min.min notation (but we ought to!)

[Jovan Gerbscheid]

Eric Wieser said:

I think these could be unscoped if they tried to synth a LinearOrder

I've implemented this here: #23558

[Kevin Buzzard]

That's very cool but I wonder if it will cause more confusion?

[Jovan Gerbscheid]

Well, the status quo is already confusing.

Do you have a suggestion for what to add to the doc-strings to make the new delaborator less confusing?

[Eric Wieser]

The docstrings for sup or for max?

[Floris van Doorn]

It is true that the status quo (with many sup/inf lemmas still named using "max"/"min") is confusing.
If we want to keep these naming conventions (which I think we do??) then this delaborator might actually make the lemma names less confusing. I'm getting less skeptical about this delaborator by the minute :-)

[Notification Bot]

5 messages were moved here from #mathlib4 > sup/inf or max/min for set interval lemmas? by Eric Wieser.

[Jovan Gerbscheid]

Eric Wieser said:

The docstrings for sup or for max?

Well, any of them. But probably the sup/inf one should say something about how its delaborator works? I already gave them new doc-strings in the PR (which don't yet mention the delaboration).

[Bhavik Mehta]

Kevin Buzzard said:

That's very cool but I wonder if it will cause more confusion?

cc @Yaël Dillies, since we had exactly the same debate (we landed on the same conclusion that the delaborator was good, provided there's enough documentation about it, but at the time neither of us knew how to write it!). Is it possible for hovering on the notation to mention the delaborator (probably not by name), and the docstring on result of ctrl+click to mention this (whichever of sup or max it ends up being)? What I'd love is to give a beginner every opportunity to figure out what's going on by themselves.

[Jovan Gerbscheid]

The docstring on the syntax command is what you see when hovering, and the syntax command is also where a ctrl+click leads to. So we need that to have a good doc-string.

[Eric Wieser]

But of course, we can't have the max docstring say anything useful, because it lives in core which can't assume that mathlib exists

[Eric Wieser]

(or did the extra docstring feature land?)

[Kyle Miller]

It's possible to override the hover text of notations these days, in case that's helpful here.

Example code:

import Lean

open Lean PrettyPrinter Delaborator SubExpr

macro "baz " t:term : term => `(id $t)

@[app_delab id]
def delab_baz : Delab := withOverApp 2 do
  guard <| ((← getExpr).getArg! 0).isConstOf ``Nat
  let some n ← Meta.getNatValue? (← getExpr).appArg! | failure
  let nstx ← withAppArg delab
  let stx ← annotateCurPos <| ← `(baz $nstx)
  addDelabTermInfo (← getPos) stx (← getExpr)
    (docString? := s!"This is `baz` applied to the natural number {n}")
  return stx

#check id 3

image.png

[Eric Wieser]

Does this replace the docstring that would be found normally?

[Kyle Miller]

Yes

[Eric Wieser]

So I guess if you want the original, you should read it from the environment and append?

[Kyle Miller]

Yeah, that can be done. For example

@[app_delab id]
def delab_baz : Delab := withOverApp 2 do
  guard <| ((← getExpr).getArg! 0).isConstOf ``Nat
  let some n ← Meta.getNatValue? (← getExpr).appArg! | failure
  let nstx ← withAppArg delab
  let stx ← annotateCurPos <| ← `(baz $nstx)
  let docString? := (← findDocString? (← getEnv) ``id) |>.map (s!"\n\n----\n\n{·}") |>.getD ""
  addDelabTermInfo (← getPos) stx (← getExpr)
    (docString? := s!"This is `baz` applied to the natural number {n}.{docString?}")
  return stx

image.png

[Kyle Miller]

A downside to this is that the string will be computed even if it's never actually used

[Eric Wieser]

Should docstring? be changed to be CoreM (Option String)?

[Eric Wieser]

I guess that would make the infotree more than just data...

[Kyle Miller]

The docstring here also doesn't need to be dynamic, if there are just a few options. it could be stored on a dummy definition.

[Kyle Miller]

import Lean

open Lean PrettyPrinter Delaborator SubExpr

macro "baz " t:term : term => `(id $t)

@[app_delab id]
def delab_baz : Delab := withOverApp 2 do
  guard <| ((← getExpr).getArg! 0).isConstOf ``Nat
  let some n ← Meta.getNatValue? (← getExpr).appArg! | failure
  let nstx ← withAppArg delab
  let stx ← annotateCurPos <| ← `(baz $nstx)
  let docString? ← findDocString? (← getEnv) (Name.mkSimple s!"baz_docstring_{n}")
  addDelabTermInfo (← getPos) stx (← getExpr)
    (docString? := docString?)
  return stx

/-- This is baz applied to 2. -/
def baz_docstring_2 := ()
/-- This is baz applied to 3. -/
def baz_docstring_3 := ()

#check id 2
#check id 3

[Kyle Miller]

It would involve keeping some docstrings in sync though, assuming the idea is to have a docstring for Min/Max that appears in the inf/sup notation.

[Jovan Gerbscheid]

What is this idea for de docstring on the inf/sup notation? Can't we just use a normal doc-string on the notation/syntax?

[Kyle Miller]

The string could say something like "The infimimum, which is notation for min when there is no linear order."

[Kyle Miller]

I'm just mentioning this to give options. I have no idea if you need it. This lets you make the string depend on any specific information that was acted upon during elaboration.

[Jovan Gerbscheid]

In this case we already get a different doc-string for max (the one from Lean core) and ⊔ (the one from the syntax command) without special support.

[Eric Wieser]

Kyle's approach lets you have different docstrings in the infoview and the editor

[Eric Wieser]

Which is not necessarily to say that we want that

[Jovan Gerbscheid]

I now have the following doc-strings

/--
The supremum/join operation: `x ⊔ y`. It is notation for `max x y`
and should be used when the type is not a linear order.
-/
syntax:68 term:68 " ⊔ " term:69 : term

/--
The infimum/meet operation: `x ⊓ y`. It is notation for `min x y`
and should be used when the type is not a linear order.
-/
syntax:69 term:69 " ⊓ " term:70 : term

And some more explanation in the module doc-string of Mathlib.Order.Notation.

However, it seems that ctrl+click on the notation sends you to the definition of max/min, instead of the ⊔ and ⊓ syntax. :oh_no:

[Kyle Miller]

It's unclear whether this is a good idea, but it's possible to override the location for the syntax too:

import Lean

open Lean PrettyPrinter Delaborator SubExpr

/--
Baz
-/
macro (name := bazStx) "baz " t:term : term => `(id $t)

@[app_delab id]
def delab_baz : Delab := withOverApp 2 do
  guard <| ((← getExpr).getArg! 0).isConstOf ``Nat
  let nstx ← withAppArg delab
  let stx ← annotateCurPos <| ← `(baz $nstx)
  let module := (← findModuleOf? ``bazStx).getD (← getEnv).mainModule
  let some range ← findDeclarationRanges? ``bazStx | failure
  let location : DeclarationLocation := { module, range := range.selectionRange }
  addDelabTermInfo (← getPos) stx (← getExpr)
    (location? := some location)
  return stx

#check id 2

[Jovan Gerbscheid]

I think this is a good idea for ⊔ and ⊓ notation.

[Yaël Dillies]

Kyle, which wizard school did you go to?

[Johan Commelin]

It's called MIT, where they teach straight from the wizard book

[Patrick Massot]

I heard it’s some school in Boston.

[Patrick Massot]

And Johan also heard that rumor and was quicker.

[Eric Wieser]

We could go a step further here and make the sup notation (in the source, as opposed to the delaborator) emit a warning if a linear order is found

[Jovan Gerbscheid]

Would that be done with a custom delaborator instead of the macro_rules?

[Jovan Gerbscheid]

This would be good as a follow-up PR

[Eric Wieser]

elaborator, yes

[Jovan Gerbscheid]

I added the withGoToDef function

/-- Annotate the syntax `stx` with the go-to-def information of `target`. -/
def withGoToDef (stx : Term) (target : Name) : DelabM Term := do
  let stx ← annotateCurPos stx
  let module := (← findModuleOf? target).getD (← getEnv).mainModule
  let some range ← findDeclarationRanges? target | failure
  let location := { module, range := range.selectionRange }
  addDelabTermInfo (← getPos) stx (← getExpr) (location? := some location)
  return stx

And used it to have the ⊔ and ⊓ go to their notation when ctrl+clicking in the infoview. On the other hand, when ctrl+clicking in the editor, it leads to the macro_rules.

[Jovan Gerbscheid]

When hovering over a ⊔ b, the pop-up shows something like @max α SemilatticeSup.toMax a b : α, so you can still ctrl+click on the @max if you want.

[Jovan Gerbscheid]

Is this still waiting for something? @Kyle Miller, I think you have been assigned as a maintainer. (#23558)