Pretty printing of existential quantifier broken

Stream: mathlib4

[Dan Velleman]

Pretty printing of the existential quantifier seems to be broken. I wonder if it is #617 that broke it.
Consider this example:

example : ∃ (x : Nat), x = 0 := by

If I don't import Mathlib, the goal is listed as ∃ x, x = 0. If I import Mathlib, the goal is listed as Exists fun x ↦ x = 0. I'm guessing that it's the introduction of ↦ that is causing the problem. The unexpander for Exists isn't expecting that symbol, so it's not working.
I don't know all of Lean + Mathlib that well, but I wonder if there are other things that were written expecting =>, and are now broken. (I wrote an unexpander for some notation I introduced in a project I'm working on, and that one was broken by this change as well.)

[Dan Velleman]

There are other unexpanders that expect => rather than ↦, so I suspect they have the same problem, although I haven't tested them: unexpandSigma, unexpandPSigma, unexpandSubtype. I have filed an issue.
Is there anything other than unexpanders that is affected #617? I don't know of anything, but I hope someone more knowledgeable than me is thinking about it.

[Yury G. Kudryashov]

I saw (⋅≤⋅) pretty printed with fun ... ↦

[Kyle Miller]

issue: mathlib4#780

[Kyle Miller]

My understanding of delaboration is the following:

• Every basic expression type (like app, pi, lambda, etc) has its own collection of delaborators. These are (modulo monads) functions Expr -> Syntax. Delaborators are registered using an attribute, and each delaborator gets a chance to try to process an expression before letting the next delaborator have a try.
• The main app delaborator also has a collection of "unexpanders." These are collections of functions Syntax -> Syntax that try to do reverse macro expansions for application syntax.

This mapsto notation is implemented as a lambda delaborator, but things like exists are unexpanders for the app delaborator. The main app delaborator for an exists will delaborate the whole app, and then the exists unexpander sees the result and tries to unexpand. But this means the mapsto delaborator has processed already before the exists unexpander has a chance to do its work.

If I understand things correctly, then this mapsto delaborator ought to be processed in a pass after all the unexpanders have done their work. Maybe a new kind of thing called a post_unexpander?

[Kyle Miller]

Barring finding other fixes, it seems like the right thing to do in the short term disable docs4#Mathlib.Util.MapsTo.delabLam (then mapsto is only accepted as notation but not pretty printed). Otherwise it seems like a lot of work to track down every place that accepts =>...

[Kyle Miller]

(pinging @Gabriel Ebner)

[Dan Velleman]

Could the pretty printing of => as ↦ be done by an unexpander for fun ..., rather than a delaborator? Would one have to ensure that other unexpanders go first, so that Exists and others would work correctly, and then any instances of fun ... that have not been eliminated by other unexpanders would then be converted to ↦?

[Kyle Miller]

No, because unexpanders are associated to the app delaborator, but fun is handled by a lam delaborator, since it's a lambda function and not an application.

[Kyle Miller]

The unexpanders are run at the end of this app delaborator: https://github.com/leanprover/lean4/blob/cbf7da0f6ef35774407132cf8f5802daf2c9a39b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean#L207, and I believe that's the only place.

[Mario Carneiro]

This is why I said we should wait until it becomes an official part of lean 4. This stuff is all handled by the unicodeSymbol combinator which is used for things like →/->