feat(widget): pretty printing restricted quantifiers

[EdAyers]

Eg converts ∀ (x : ℕ), x > 3 → ∃ (N : set ℕ), ∀ y, y ∈ N → x > 2
to ∀ (x > 3), ∃ (N : set ℕ), ∀ (y ∈ N), x > 2
in the widget view.

---

• depends on: [Merged by Bors] - chore(*): bump to lean-3.26.0 #5895
• add an option to disable
• automatically disable if pp.notation is off

[EdAyers]

I probably won't have time to work on this for a while so if anyone wants to pick it up; go nuts.

[robertylewis]

I'm unsure about this for two reasons. One, it suppresses information (the type of x) that's not necessarily obvious. Two, if this is how we want to display these quantifiers, it should probably be changed in the pretty printer, right? With an option to disable it?

[EdAyers]

Yeah @robertylewis I think these are valid concerns. The context of this is that @PatrickMassot noted that beginners find the non-compacted notation that the pretty printer generates to be confusing and its a sticking point for learning Lean. Perhaps you can weigh in Patrick?

In terms of not knowing the type, you can still inspect the expression in the widget view and see the type, although it is not immediate from a glance.

I agree that this should really belong in Lean's pretty printer C++ code. But this was just way simpler to implement in Lean as a post-processing step. There are already a few pretty-printer post-processing steps in use in the file: eg the lines above 303 in interactive_expr.lean. We can add an option to disable.

[PatrickMassot]

Yes, I think this would be a huge improvement for teaching, especially when existentials quantifiers will be handled, getting rid of the infamous ∃ (δ : ℝ) (H : δ > 0), .... I'm not worried about hiding information since the information is still accessible in the widget in the very rare cases where it could be needed. Of course it would be even nicer if there was a way to opt out, and even nicer if there was a way to do this more efficiently from C++. However it would also be very nice to have a clearer path for people who want to use widgets to implement custom pretty-printing. There could be many more tricks, although the issue tackled in this PR is, from my experience, the most pressing one.

[PatrickMassot]

Any news here? @EdAyers

[robertylewis]

Aren't the valid targets "everything with infix notation"?

[EdAyers]

Is there a programmatic way to test whether a given relation has an infix notation?

[robertylewis]

Not that I'm aware of. You could build a dummy application and see if it pretty prints differently than you expect, which is very hackish.

[PatrickMassot]

Ed, could you update the TODO list in the PR description?
Is there a test somewhere that ensures we won't forget to update this code when the addressing bug is fixed in Lean?

[EdAyers]

Ready for review

[robertylewis]

I'm still not really thrilled about this change.

My first worry is debatable, I know, but I feel like bundling this in the goal view really does obscure things in the logic and type theory. Maybe it helps for exists, but:

example : ∀ x : ℤ, x > 0 → true :=
begin 
  -- ∀ (x > 0), true
end 

In this example I don't see the type of x or the fact that I need to do two intros. It makes you totally dependent on clicking on widgets and "try intro, see what happens."

Worse, because this is implemented as widget post-processing, it doesn't interact well with pp options. This is ugly and doesn't round-trip:

set_option pp.notation false 

example : ∀ x : ℤ, x > 0 → true :=
begin 
  -- ∀ (gt x 0), true
end 

and pp.all makes it worse.

At a bare minimum, I think this feature needs an option to disable it. I'd prefer it disabled by default. Even better, I'd prefer it implemented as part of the pretty-printer so it interacted right with pp options.

[PatrickMassot]

I still think this is a great contribution, but of course it would be better to have an option controlling this. I think the pp.notation false issue is definitely not an argument for turning this PR off by default, since the issue shows off only when opting out of notations. The fact that some types are hidden is slightly more serious, but I think the PR still makes most situations less confusing and you have a clear path to investigate types if needed. So my favorite solution would be to provide a way to turn off this PR, but still have it on by default.

Note that in my course I ship everything with this PR included (not in mathlib, in my project).

[EdAyers]

To address some of Rob's concerns;

There are other existing cases where the pp system makes the types of expressions ambiguous. I agree that this one is particularly bad because the information it is hiding is something that the user could really do with knowing. There is not going to be a non-clunky way to reveal this information without being worse than the original uncollapsed notation. The community are going to have to make an aesthetic judgement call.

I agree that turning off pp.notation makes this ugly, hopefully it is possible for the tactic state to know whether pp.notation is set and turn off this feature in that case.

I agree it needs a disabling option.

In the small amount of Lean teaching that I have done I can concur with Patrick that students stumble on these non-collapsed quantifiers. So I do think that this addition has some merit for teaching purposes even at the expense of being bloat for the power users. Perhaps the tradeoff is not worth it, I am genuinely not sure.

[github-actions]

This PR/issue depends on:

• [Merged by Bors] - chore(*): bump to lean-3.26.0 #5895
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

Lean 4 handles nested binders completely differently, so this will have to be redone mostly from scratch. To be revisited after the port.