Set notation

Stream: mathlib4

[Dan Velleman]

I thought it would be good to be able to write definitions like this:

def inv {A B : Type} (R : Set (A × B)) : Set (B × A) :=
  {(b, a) : B × A | (a, b) ∈ R}

But this doesn't fit the pattern of set theory notation defined in Mathlib.Init.Set.lean. So I tried this:

syntax "{ " term " : " term " | " term " }" : term

macro_rules
  | `({ $pat:term : $t | $p }) => `(setOf fun x : $t => match x with | $pat => $p)

This seems to work, but then it creates problems for other set theory notation. Something like {x : Nat | x = 0} becomes ambiguous--I assume that's because it fits both the previous syntax pattern and the new one I have defined. Is there a way to eliminate the ambiguity?

[Thomas Murrills]

Allowing destructuring seems useful! Does it still work (as-is, not in a way that fixes the ambiguity) if you just use fun $pat : $t => $p on the rhs, since iirc fun allows destructuring as well? If so, maybe the ambiguity could be resolved by replacing the existing macro (which in this case would only differ by restricting $pat to be an ident).

I think the trick, though, would be to first check if $pat was a valid destructuring for the given type, and if not, throw-unsupported and allow the low-priority extBinders case to take over. (But I’m not sure how to do the first part, and maybe there’s a reason that all of this wouldn’t be a good idea that I haven’t thought of.)

[Thomas Murrills]

Though, thinking about it, maybe it’s Std.Util.ExtendedBinder that should allow destructuring in general instead of just idents? Not sure how much this would break or how feasible it would be, though…

[Dan Velleman]

Perhaps what I need is this:

elab "{ " pat:term " : " t:term " | " p:term " }" : term => do
  if pat.raw.isIdent then
    Lean.Elab.throwUnsupportedSyntax
  else
    Lean.Elab.Term.elabTerm (← `(setOf fun x : $t => match x with | $pat => $p)) none

This avoids creating a second possible interpretation for something like {x : Nat | x = 0}.

But would it make sense to add something like this to the Mathlib definition of set notation?

[Dan Velleman]

On the other hand, this isn't good enough:

elab "{ " pat:term " | " p:term " }" : term => do
  if pat.raw.isIdent then
    Lean.Elab.throwUnsupportedSyntax
  else
    Lean.Elab.Term.elabTerm (← `(setOf fun x => match x with | $pat => $p)) none

This causes {x > 0 | x < 10} to be ambiguous. I suppose a more complicated test could be used to avoid the ambiguity.

Is the binderPred notation really needed for anything? I'd rather have the destructuring notation than the binderPred notation.

[Dan Velleman]

After a lot of experimentation, here's what I've come up with:

elab "{ " pat:term " : " t:term " | " p:term " }" : term => do
  if pat.raw.isIdent then
    Lean.Elab.throwUnsupportedSyntax  --To avoid creating ambiguity with existing set notation
  else
    Lean.Elab.Term.elabTerm (← `(setOf fun x : $t => match x with | $pat => $p)) none

declare_syntax_cat identBinderPred
syntax ident binderPred : identBinderPred

elab "{ " pat:(identBinderPred <|> term) " | " p:term " }" : term => do
  match pat.raw with
    | .ident .. => Lean.Elab.throwUnsupportedSyntax  --To avoid ambiguity
    | .node _ `identBinderPred__ _ => Lean.Elab.throwUnsupportedSyntax  --To avoid ambiguity
    | _ =>
      let patTerm : Lean.Term := ⟨pat⟩
      Lean.Elab.Term.elabTerm (← `(setOf fun x => match x with | $patTerm => $p)) none

@[app_unexpander setOf]
def setOf.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ fun $_:ident =>
        match $_:ident with
        | $pat => $p) => `({ $pat:term | $p })
  | _ => throw ()

I don't understand all of this, but it seems to work. It allows me to write things like {(m, n) : Nat × Nat | m < n}

Is there any reason not to do this? Is there a better way to do it?