Pattern matching in set-builder notation

Stream: mathlib4

[Adam Topaz]

Has anyone given any thought to making something like the following work?

variable {α β : Type} (f : α → β → Prop)

example : Set (α × β) := { (x,y) | f x y }

[Dan Velleman]

Yes, I do this in How To Prove It with Lean. Here's what I did:

macro (priority := low-1) "{ " pat:term " : " t:term " | " p:term " }" : term =>
  `({ x : $t | match x with | $pat => $p })

macro (priority := low-1) "{ " pat:term " | " p:term " }" : term =>
  `({ x | match x with | $pat => $p })

@[app_unexpander setOf]
def setOf.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ fun $x:ident => match $y:ident with | $pat => $p) =>
      if x == y then
        `({ $pat:term | $p:term })
      else
        throw ()  --Or could use `({ $x:ident | match $y:ident with | $pat => $p})
  | `($_ fun ($x:ident : $ty:term) => match $y:ident with | $pat => $p) =>
      if x == y then
        `({ $pat:term : $ty:term | $p:term })
      else
        throw ()
  | _ => throw ()

[Eric Wieser]

This works:

example : Set (α × β) := { (x,y) | (x) (y) (_ : f x y) }

[Adam Topaz]

@Dan Velleman I think something like this would be nice to have in mathlib.

[Dan Velleman]

Perhaps someone more knowledgeable than me could look this over and see if this is the right/best way to do it.

[Yaël Dillies]

This really is a question for @Kyle Miller

[Utensil Song]

Eric Wieser said:

This works:

example : Set (α × β) := { (x,y) | (x) (y) (_ : f x y) }

I have no idea what (dark) magic is happening after |, don't even know which part of Lean syntax to use for parsing it in my mind. Even if I interpret them as a Prop, still no idea why this helped pattern matching.

If I have only #check (x) (y) (_ : f x y), this doesn't type check, it reports unknown identifier, just like a raw (_ : f x y) inside the notation. What's special after |? (Particularly, this only works after importing Mathlib)

[Ruben Van de Velde]

{ f x y | (x : X) (y : Y) } is notation for the set of elements f x y constructed from the binders x and y, equivalent to {z : Z | ∃ x y, f x y = z}.

If f x y is a single identifier, it must be parenthesized to avoid ambiguity with {x | p x}; for instance, {(x) | (x : Nat) (y : Nat) (_hxy : x = y^2)}.

[Utensil Song]

Ruben Van de Velde said:

{ f x y | (x : X) (y : Y) } is notation for the set of elements f x y constructed from the binders x and y, equivalent to {z : Z | ∃ x y, f x y = z}.

If f x y is a single identifier, it must be parenthesized to avoid ambiguity with {x | p x}; for instance, {(x) | (x : Nat) (y : Nat) (_hxy : x = y^2)}.

Thanks, I see, they are binders in this case.

[Kyle Miller]

@Dan Velleman I'm not sure what's the best way, but the macros and unexpanders you have for set builder notation seem fine to me, and I think I'd write them the same as you did. (Note: your second case of the unexpander won't apply unless someone does set_option pp.funBinderTypes true. If you wanted, you could add an extra delaborator that sets this option right on that fun argument. We have such a delaborator hack here to conditionally add binder types for LinearIndependent.)

[Dan Velleman]

Thanks Kyle. In How To Prove It with Lean I do set_option pp.funBinderTypes true, because for educational purposes I think it's helpful to show types for all bound variables. That's why I wanted to include the case with the type specified.

[Kyle Miller]

That makes sense, and I figured you probably were using it somewhere. I'm passing along that delaborator hack in case you find it to be useful elsewhere (or at least to give you the idea that you could demand type hints in more places and that someone could get it to work.)

[Kyle Miller]

I'd like to see binders in Exists globally myself, so that it matches how foralls are printed.

[Dan Velleman]

#8850