Set builder notation

Stream: mathlib4

[Bhavik Mehta]

It's frustrating that while the first three of these work, the fourth doesn't.

import Mathlib.Data.Set.Defs

variable {α : Type}

example (t : Nat) (g : Nat → Nat → Prop) : Prop :=
  ∃ (a : Nat) (b : Nat) (_ : a ≤ t) (_ : b ≤ t), g a b

example (t : Nat) (g : Nat → Nat → α) : Set α :=
  {g a b | (a : Nat) (b : Nat) (_ : a ≤ t) (_ : b ≤ t)}

example (t : Nat) (g : Nat → Nat → Prop) : Prop :=
  ∃ (a b : Nat) (_ : a ≤ t) (_ : b ≤ t), g a b

example (t : Nat) (g : Nat → Nat → α) : Set α :=
  {g a b | (a b : Nat) (ha : a ≤ t) (hb : b ≤ t)}

It looks to me like the difference occurs because set builder notation uses ∃ᵉ.

1. The error message here is incredibly unhelpful: "invalid pattern, constructor or constant marked with '[match_pattern]' expected". Is there a way to report something more useful?
2. Is there a way to make the fourth example work?
3. The documentation here says it is equivalent to a version with ∃; despite the above showing that it's not...

[Bhavik Mehta]

Oh, and I find it very frustrating that I need to write the underscore for the assumptions a ≤ t - is there a way of using this set notation without that? Further, the definition of the set isn't in simp-normal-form. And so in practice I usually find myself wanting to manually unfold the notation, at the cost of readability, so that it's nicer to actually prove things about the set.

[Kyle Miller]

Yeah, this is frustrating, and the issue is that the notation is defined in terms of extBinders, which only support a single identifier.

On the flip side, at least this means you can write

example (t : Nat) (g : Nat → Nat → α) : Set α :=
  {g a b | (a ≤ t) (b ≤ t)}

[Bhavik Mehta]

Indeed, in the simplified case where the conditions are actually just inequalities, it is nice. But unfortunately the example above was minimised from one where that doesn't work!

[Bhavik Mehta]

Actually, how feasible is it for extBinders to support multiple identifiers? Then we'd get the best of both worlds here.

[Ruben Van de Velde]

And make the default exists/for all use extBinders?

[Kyle Miller]

We're looking into improving the binder situation. It'd be nice if binders across all quantifiers could be more consistent!

I remember for BigOperators I made a variant of extBinders that had nicer properties, but I'd need to remind myself what they solved and why they didn't support x y z : T either. https://github.com/leanprover-community/mathlib4/blob/42ff2ccb6d99b39a65e43b8da21a60f8e7d3f9ca/Mathlib/Algebra/BigOperators/Group/Finset.lean#L93-L104

[Bhavik Mehta]

Okay great, is there an issue tracking this?

[Kyle Miller]

I don't believe so — I think you could say it's in the research phase

[Floris van Doorn]

Related: #mathlib4 > uniformize binders