Zulip Chat Archive

Stream: lean4

Topic: Display of quantified statements


Dan Velleman (Oct 03 2022 at 17:32):

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 (Oct 03 2022 at 17:35):

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 (Oct 03 2022 at 17:37):

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 (Oct 03 2022 at 17:41):

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

Adam Topaz (Oct 03 2022 at 17:44):

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

Dan Velleman (Oct 03 2022 at 18:05):

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 (Oct 03 2022 at 18:05):

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

Dan Velleman (Oct 03 2022 at 19:16):

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 (Oct 03 2022 at 19:22):

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 (Oct 03 2022 at 19:30):

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 (Oct 03 2022 at 19:31):

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

Dan Velleman (Oct 03 2022 at 19:42):

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 (Oct 03 2022 at 19:43):

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 (Oct 03 2022 at 19:45):

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

Mario Carneiro (Oct 03 2022 at 19:48):

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

Mario Carneiro (Oct 03 2022 at 19:48):

cc: @Sebastian Ullrich

Sebastian Ullrich (Oct 03 2022 at 20:06):

It works correctly with pp.analyze

Dan Velleman (Oct 24 2022 at 20:53):

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 (Jan 18 2023 at 14:12):

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?


Last updated: Dec 20 2023 at 11:08 UTC