Pretty-printing of sums

Stream: mathlib4

[Heather Macbeth]

Is it a known issue that Finset.sum does not pretty-print? Consider

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Tactic.Linarith

open Finset BigOperators

example (n : ℕ) : 2 * ∑ i in range (n + 1), i = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ n IH => rw [sum_range_succ] ; linarith

The goal at the start of the proof displays as

(2 * Finset.sum (range (n + 1)) fun i ↦ i) = n * (n + 1)

[Heather Macbeth]

I noticed !4#2724, "Pretty printing for functors and other nested structures" -- not sure if this is the same issue.

[Eric Wieser]

Is this caused by the ↦ delaborator?

[Kyle Miller]

As far as I know there's no delaborator for Finset.sum, which is what's needed for pretty printing.

[Heather Macbeth]

Perhaps this can be my opportunity to learn what a delaborator is.

[Heather Macbeth]

What's a delaborator and why didn't we need them in Lean 3?

[Heather Macbeth]

Should we be requiring that every new notation in mathlib come with a delaborator?

[Thomas Murrills]

This section of the metaprogramming book might be particularly relevant! Basically, as you might have guessed from the name, a delaborator does the opposite of elaboration; that means it turns Exprs back into Syntax for display.

[Heather Macbeth]

OK, but

Heather Macbeth said:

why didn't we need them in Lean 3?

?

[Patrick Massot]

This is the price to pay for Lean 4's much greater notation flexibility I think.

[Thomas Murrills]

As a non-lean 3 user, my best guess is the handwavey “new metaprogramming framework!” answer 😅

[Heather Macbeth]

So:

Heather Macbeth said:

Should we be requiring that every new notation in mathlib come with a delaborator?

[Thomas Murrills]

I’m under the impression that the notation command introduces delaborators, but I could be wrong. Let me check…

[Patrick Massot]

It does, but only in simple cases.

[Heather Macbeth]

Is there a way to get the notation command to throw an error if it can't autogenerate the appropriate delaborator and there is no accompanying delaborator?

[Patrick Massot]

I'm far from an expert in this, but maybe detecting failure isn't so easy. The command probably generates something, but it may not be good enough.

[Thomas Murrills]

It looks like mkUnexpander is the thing that generates the delaborator, and is allowed to succeed or fail when the notation is made. Not sure if successes in mkUnexpander might still nonetheless be “not good enough”/the “wrong” delaborator, though.

[Thomas Murrills]

I second the notion of at least reporting that failure though! :)

[Thomas Murrills]

Though, that’s in core; maybe in the meantime it would make sense to have a mathlib-based command notation? like simps? which displayed any delaborators made?

[Heather Macbeth]

Let's also think about a way to track this. It seems like it will come up all the time. Should we have a missing-delaborator tracking issue, like we had a tactic porting issue?

[Thomas Murrills]

I would support that. :)

[Thomas Murrills]

Oh, another idea: what about a linter to check when notation failed to generate an unexpander? We could probably do this just by re-running mkUnexpander on the right arguments.

[Thomas Murrills]

(Or, if we have access to it, we could just check how many children the syntax node generated by notation produces—it’s 2 if there’s no delaborator and 3 if there is. I’m still not sure how linters work, tbh. 😁)

[Sebastian Ullrich]

A message or linter is possible, but a bit besides the original point: the Finset.sum notation is not a notation, but a non-trivial macro with custom binding syntax, whereas all of this was built-in in Lean 3. So this is already a somewhat advanced example and one really shouldn't expect Lean to automatically construct an unexpander here. Though I wonder whether someone has explored autogenerating unexpanders from macro_rules yet.

[Patrick Massot]

Sebastian, from a user's perspective it is still hard to understand why Lean 3 had a way for users to define such a notation and get an unexpander for free and Lean 4 doesn't.

[Patrick Massot]

It's great that we can have more complicated notations now, but it would be even greater if simple things could remain simple.

[Heather Macbeth]

Indeed ... is it not possible or is the answer is just "we haven't got round to it yet"?

[Heather Macbeth]

(Of course I appreciate that it is nontrivial work to offer features like this.)

[Heather Macbeth]

While we're at it, I noticed that Set.unionᵢ is apparently also missing its delaborator.

import Mathlib.Data.Set.Lattice

open Set

example : (⋃ i, {i, i + 1}) = univ := by
  -- goal is `(unionᵢ fun i ↦ {i, i + 1}) = univ`
  ext
  simp

[Sebastian Ullrich]

Well this has all been moved to std/mathlib4 so needs to be addressed there, but there is no intrinsic reason this should make creating notations with binders harder than in Lean 3. In fact I would hope it should become easier than in Lean 3 because who can ever remember what's going on in

notation `∑` binders `, ` r:(scoped:67 f, finset.sum finset.univ f) := r

So once we know what we actually want to end up with, this could be addressed in mathlib4.

[Sebastian Ullrich]

I think

scoped macro "∏ " x:extBinder ", " p:term:67 : term => ``(Finset.prod Finset.univ (fun $x ↦ $p))

would be a reasonable representation and only needs a missing TSyntax coercion to work in the forward direction. Then mathlib4 could either override the macro command (I think people avoid doing that, which is probably a good idea) or introduce a new attribute to autogenerate the unexpander from that by specifically looking for that coercion.

[Sebastian Ullrich]

And of course the more limited you want to make the abstraction, the simpler it can be. It could be as short as

bigop_notation "∏ ":67 => Finset.prod Finset.univ

to cover examples without extra in etc.

[Kyle Miller]

Heather Macbeth said:

What's a delaborator

Here are all the words in one place:

String ---(parser)---> Syntax ---(elaborator)---> Expr ---(delaborator)---> Syntax ---(formatter)---> String

The elaborator is flexible, and you can make your own plugins (themselves called elaborators) to extend it. One type of elaborator, a "macro", is a Syntax -> Syntax transformation.

The delaborator is also flexible. There's something like an antimacro, an "unexpander," also for Syntax -> Syntax transformations.

In Lean 3, there was much less flexibility. The above diagram looked like this:

String ---(parser)---> Expr ---(elaborator)---> Expr --(pretty printer)--> String

(There was no difference between unelaborated and elaborated Expr types.)

Notation in Lean 3 is completely handled by the parser and pretty printer. All the notations are stored in a single table, with high-level descriptions of how to parse each notation and how they expand into Exprs, and the parser and pretty printer have special code for how to interpret these descriptions. As Sebastian has been saying, the Lean 4 version is that we just need to get around to writing commands that add elaborators and delaborators automatically. This would replace the less flexible notation table in Lean 3.

[Kyle Miller]

At a high level, the point is that Lean 3's notation table was intrinsically invertible (at least in theory). Being able to define elaborators and delaborators separately is much more powerful, but you do lose that automatic invertibility.

[Heather Macbeth]

Would it be worth writing a special command for invertible notation, which works in a smaller set of cases but is more user-friendly (replicating the lean 3 experience) in those cases?

[Heather Macbeth]

If you have time, Kyle -- can you augment your explanation above with where notation fits into the story in Lean 4? Is notation a macro?

[Kyle Miller]

Heather Macbeth said:

Would it be worth writing a special command for invertible notation, which works in a smaller set of cases but is more user-friendly (replicating the lean 3 experience) in those cases?

Yeah, I think this is exactly what Sebastian is suggesting: figure out what would be a good notation command that would make things at least as user-friendly as the Lean 3 one (including invertibility).

[Kyle Miller]

Heather Macbeth said:

can you augment your explanation above with where notation fits into the story in Lean 4? Is notation a macro?

Indeed, the notation command is a macro that creates a macro and (hopefully) an unexpander. It looks like @Thomas Murrills already brought up mkUnexpander, which is a supporting function in that file to try to derive the unexpander to reverse the notation.

[Heather Macbeth]

I have also seen notation3 in use, and its docstring says

`notation3` declares notation using Lean 3-style syntax.

So should we maybe just make more extensive use of notation3? For example, we could switch the docs4#Set.unionᵢ and docs4#Finset.sum macros to use notation3?

[Kyle Miller]

Here's an implementation of some Finset.prod and Finset.sum delaborators:

namespace BigOperators
open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr
open Std.ExtendedBinder

@[scoped delab app.Finset.prod] def delabFinsetProd : Delab := do
  let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
  guard <| f.isLambda
  let ppDomain ← getPPOption getPPPiBinderTypes
  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
    let body ← delab
    return (i, body)
  if s.isAppOfArity ``Finset.univ 2 then
    let binder ← if ppDomain then
      let ty ← withAppArg <| withBindingDomain <| delab
      `(extBinder| $(.mk i):ident : $ty)
    else
      `(extBinder| $(.mk i):ident)
    `(∏ $binder, $body)
  else
    let ss ← withAppFn <| withAppArg <| delab
    `(∏ $(.mk i):ident in $ss, $body)

@[scoped delab app.Finset.sum] def delabFinsetSum : Delab := do
  let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
  guard <| f.isLambda
  let ppDomain ← getPPOption getPPPiBinderTypes
  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
    let body ← delab
    return (i, body)
  if s.isAppOfArity ``Finset.univ 2 then
    let binder ← if ppDomain then
      let ty ← withAppArg <| withBindingDomain <| delab
      `(extBinder| $(.mk i):ident : $ty)
    else
      `(extBinder| $(.mk i):ident)
    `(∑ $binder, $body)
  else
    let ss ← withAppFn <| withAppArg <| delab
    `(∑ $(.mk i):ident in $ss, $body)

end BigOperators

[Kyle Miller]

You can put this right after the end BigOperators in Mathlib/Algebra/BigOperators/Basic.lean, and it becomes active when you do open BigOperators, just like the syntax.

[Eric Wieser]

Sebastian Ullrich said:

I think

scoped macro "∏ " x:extBinder ", " p:term:67 : term => ``(Finset.prod Finset.univ (fun $x ↦ $p))

would be a reasonable representation and only needs a missing TSyntax coercion to work in the forward direction.

I don't think this works; don't you need to fold over extBinder? ∏ i j, f i j is Finset.prod Finset.univ (fun i, Finset.prod Finset.univ (fun j, f i j))

[Heather Macbeth]

Kyle Miller said:

You can put this right after the end BigOperators in Mathlib/Algebra/BigOperators/Basic.lean, and it becomes active when you do open BigOperators, just like the syntax.

@Kyle Miller Are you saying that you're looking for a volunteer to PR this for you?

[Kyle Miller]

I'm saying you can test it out if you want Right Now. (There are some fixable spacing issues due to the syntax, just so you know.)

[Kyle Miller]

I'll create a PR

[Heather Macbeth]

OK, thanks, even better :-)

[Heather Macbeth]

For later: will copy-pasta do Set.unionᵢ, integrals, etc?

[Eric Wieser]

On a related note, is mathlib3's ∑ i j : Fin 3, (i + j) something we can have back in mathlib4?

[Heather Macbeth]

Ah ... is this not supported by Kyle's version?

[Kyle Miller]

Eric Wieser said:

I don't think this works; don't you need to fold over extBinder?

extBinder is only for a single binder, and it's what the sum syntax is using right now. I don't see why sum/prod syntax couldn't eventually support multiple binders.

[Kyle Miller]

mathlib4#3772

[Mario Carneiro]

Heather Macbeth said:

I have also seen notation3 in use, and its docstring says

`notation3` declares notation using Lean 3-style syntax.

So should we maybe just make more extensive use of notation3? For example, we could switch the docs4#Set.unionᵢ and docs4#Finset.sum macros to use notation3?

In one sense, yes notation3 is exactly what you need to get an unexpander automatically since the allowed syntax there is rigid enough that we know what to generate. On the other hand, this won't work because notation3 does not implement any unexpander, only the elaborator.

[Mario Carneiro]

I think it would not be too difficult to adapt Kyle's unexpander to work on arbitrary notation3s

[Kyle Miller]

It'd be great if we could get notation3 to (finally) let us use ∑ x ∈ s, f x notation in a robust way. Maybe that could be done with some custom elaborator after notation3's expansion?

[Mario Carneiro]

I did actually spend some time thinking about what would be the best syntax for concisely declaring binder notations, and notation3 is the best I could come up with. It is a slightly simplified form of the lean 3 notation command

[Mario Carneiro]

I'm not sure exactly what you are after there. Is it about using binder predicates?

[Kyle Miller]

Yeah

[Kyle Miller]

In Lean 3, that would generate two levels of Finset.sum, which is not good if the domain is not a fintype

[Mario Carneiro]

I guess the (...) in notation3 syntax could just support binder_pred out of the box

[Mario Carneiro]

ah well that's a different issue

[Mario Carneiro]

I was assuming you want to generate the same thing as what lean 3 would do

[Mario Carneiro]

if you want to do something else, then you will have to specify what that is

[Mario Carneiro]

the current support for binder predicates certainly allows you to do something else, e.g. the \exists x, x \in s /\ p x thing that people have noticed

[Mario Carneiro]

but it's less obvious what syntax you want to use to specify that transformation, especially if it is a one-liner like notation3

[Kyle Miller]

I've posted some experiments occasionally over the last two years to convert Lean 3 expansions of the binder predicates into well-formed finset.sum expressions using some complicated typeclasses.

[Kyle Miller]

They were never really robust though

[Kyle Miller]

I think what could work is having a Finset.sum' that gives the sum if the function has finite support, 0 otherwise, and then have some elaborator for it that turns expressions involving Finset.sum' into Finset.sum wherever it's possible.

[Kyle Miller]

Then ∑ x ∈ s, f x for s : Finset X would be Finset.sum' (fun x => Finset.sum' (fun (h : x ∈ s) => f x)), and the elaborator could turn this into Finset.sum s (fun x => f x)

[Kyle Miller]

I don't really have a full design here -- the main goal is just to remove the irregularity of the in in sum/prod notation, while also allowing this to generalize to other sorts of decidable predicates with finite support.

[Scott Morrison]

Just noting that @Kevin Buzzard has been adding delaborators to his PR at https://github.com/leanprover-community/mathlib4/pull/3592.

@Kyle Miller, might you be able to look at this and decide what to do with them? Obviously we want this functionality, I'm just not certain whether the right action is:

• merge as is
• merge, but in some way keep track of wanting to replace these with a more general solution
• don't merge, and implement a general solution now

[Heather Macbeth]

I opened !4#3773 for this issue (in the general case, not just for sums). I think it's extremely high-priority. (I know Sebastian, Kyle, Mario and Scott are well aware of this ... thank you for thinking about it and also for explaining it carefully!)

[Patrick Massot]

@Kyle Miller does your pretty-printing magic trick also fix infi for Finset, as in ⨅ i ∈ s, f i not displaying ⨅ i, ⨅ h, f i?

[Eric Wieser]

I think this is a problem in general for ⨅ h : P, _ where P : Prop, and isn't restricted to finsets

[Patrick Massot]

No problem, I'd tolerate a fully general solution.

[Kyle Miller]

@Scott Morrison Here's a potential general-ish solution for simple dot notation delaborators mathlib4#3811

[Kyle Miller]

A big thing it does is define a delaborator that pretty prints projections in general with collapsed parent projections, so x.toC.toB.toA.val is x.val. It still has the limitation of the original version, where it can't handle projections that take any additional arguments.

The other thing it does is define a command so that you can get dot notation to work for specific functions, either projections that take additional arguments or functions that are used as generalized fields. For example, pp_extended_field_notation Prefunctor.obj for the first and pp_extended_field_notation Iso.app for the second. These interact with the projection delaborator, so, if F is a functor, then F.obj pretty prints as F.obj.

There's a little hack to get this last part to work, where it adds an extra rule that x.toPrefunctor.obj should be x.obj, no matter what x is. This is because the projection delaborator only collapses parent projections up to the last one. That is, x.toC.toB.toA is still x.toA, so you need to get rid of that last toA somehow. Since pp_extended_field_notation is defining an app unexpander, which is a syntax->syntax transformation, this extra rule is not guaranteed to be correct, though in practice it shouldn't be a problem.