Display of quantified statements

Stream: lean4

[Dan Velleman]

Consider this example:

example : ∀ x, x ≥ 0 := by

In the tactic state, the goal is listed as ∀ (x : ℕ), x ≥ 0. That makes sense; Lean has inferred that x must have type Nat. But now change the example to:

example : ∃ x, x ≥ 0 := by

Now the goal is just ∃ x, x ≥ 0. Even if I write the example this way:

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

the goal is still just listed as ∃ x, x ≥ 0. Or consider this example:

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

The goal in the tactic state is ∃ x, x = x. But if I write

example : ∃ x, x = x := by

I get an error message. So Lean is displaying the goal in a form that it would not accept as input.

Shouldn't the pretty printer for existential quantifiers use the same style as universal quantifiers? Note that if the pretty printing of ∃ is changed, I assume the pretty printing of ∃! should also be changed.

[Adam Topaz]

Lean knows to expect a natural number when you write 0, but if you just write example : ∃ x, x = x := by, then Lean has no way to know what type x should have

[Adam Topaz]

And Lean will actually tell you this!

example : ∃ x, x = x := sorry

gives the error message:

22:10:
don't know how to synthesize implicit argument
  @Exists ?m.6717 fun x => x = x
context:
⊢ Sort ?u.6715
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
22:12:
failed to infer binder type
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
22:15:
don't know how to synthesize implicit argument
  @Eq ?m.6717 x x
context:
x : ?m.6717
⊢ Sort ?u.6715
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed

[Adam Topaz]

Or maybe I misunderstood. I guess the question is really about the pretty printer.

[Adam Topaz]

It seems that in Lean3, the type of x is displayed in the existential.

[Dan Velleman]

Yes, that's right, my question is about the pretty printer. Shouldn't Lean display the type of x, as it does for the universal?

[Adam Topaz]

The answer is "yes" if one wants to mimic the behavior from Lean3.

[Dan Velleman]

I think it's not just a matter of mimicking the behavior of Lean 3. It seems bizarre to me that Lean would display the formula ∃ x, x = x even though it would not accept that formula as input, since it can't infer the type of x.

[Adam Topaz]

Well, there are other (albeit more complicated) situations I've encountered (in Lean3) where the pretty-printed thing needs to be modified to be accepted as input, so I personally don't necessarily expect to be able to copy-and-paste stuff directly from the info-view.

[Mario Carneiro]

Any non-default implicit arguments aren't going to be reproduced in the pretty print, as well as proofs and a bunch of other things

[Mario Carneiro]

if you actually want copy-and-pastability you should use pp.all for best results

[Dan Velleman]

OK, maybe copy-and-pastability wasn't the best way to make my point. But I still think that the pretty printing of existential and universal quantifiers should work the same way--if the type of the quantified variable is displayed for universals, it should be displayed for existentials as well.

[Mario Carneiro]

I took a look at the code and it's not very simple to do so. The issue is that the exists notation is unexpanded from Exists fun x => p x -> ∃ x, p x, and the former expression generally won't use the type because Exists takes its type argument implicitly and function arrows usually don't need types because the context supplies them

[Mario Carneiro]

an expression of the form Exists fun (x : A) => p x does unexpand to ∃ (x : A), p x as you would expect

[Mario Carneiro]

although, Sigma seems to have a similar issue but it does print with the type so there might be more going on

[Mario Carneiro]

cc: @Sebastian Ullrich

[Sebastian Ullrich]

It works correctly with pp.analyze

[Dan Velleman]

Yes, pp.analyze fixes it. But it causes other problems. With pp.analyze, 1 ∈ {x : Nat | x > 0} gets displayed in the tactic state as Membership.mem (γ := Set ℕ) 1 { x | x > 0 }. Without pp.analyze, it's displayed as 1 ∈ { x | x > 0 }.

The fact that the existential quantifiers are displayed correctly with pp.analyze shows that it can be done. So can it be made the default, so we don't need pp.analyze?

[Dan Velleman]

I think I finally figured out how to get existential statements to display the type of the variable in the tactic state. The option to use is pp.funBinderTypes. As I understand it, this causes the delaborator to include the type of the variable when it delaborates a lambda expression. Then the type info is available to the unexpander for Exists, so the type gets included in the display.
Is that right? And is there a downside to using pp.funBinderTypes that I haven't thought of?