feat: delaborator for finset builder notation (#22076)

Author: YaelDillies

Mathlib/Algebra/BigOperators/Expect.lean

@@ -83,13 +83,13 @@ scoped macro_rules (kind := bigexpect)
 open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr
 open Batteries.ExtendedBinder
 
-/-- Delaborator for `Finset.expect`. The `pp.piBinderTypes` option controls whether
+/-- Delaborator for `Finset.expect`. The `pp.funBinderTypes` option controls whether
 to show the domain type when the expect is over `Finset.univ`. -/
 @[scoped app_delab Finset.expect] def delabFinsetExpect : Delab :=
   whenPPOption getPPNotation <| withOverApp 6 <| do
   let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
-  let ppDomain ← getPPOption getPPPiBinderTypes
+  let ppDomain ← getPPOption getPPFunBinderTypes
   let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
     return (i, ← delab)
   if s.isAppOfArity ``Finset.univ 2 then

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -231,13 +231,13 @@ end deprecated
 open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr
 open scoped Batteries.ExtendedBinder
 
-/-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether
+/-- Delaborator for `Finset.prod`. The `pp.funBinderTypes` option controls whether
 to show the domain type when the product is over `Finset.univ`. -/
 @[app_delab Finset.prod] def delabFinsetProd : Delab :=
   whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
-  let ppDomain ← getPPOption getPPPiBinderTypes
+  let ppDomain ← getPPOption getPPFunBinderTypes
   let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
     return (i, ← delab)
   if s.isAppOfArity ``Finset.univ 2 then
@@ -252,13 +252,13 @@ to show the domain type when the product is over `Finset.univ`. -/
     let ss ← withNaryArg 3 <| delab
     `(∏ $(.mk i):ident ∈ $ss, $body)
 
-/-- Delaborator for `Finset.sum`. The `pp.piBinderTypes` option controls whether
+/-- Delaborator for `Finset.sum`. The `pp.funBinderTypes` option controls whether
 to show the domain type when the sum is over `Finset.univ`. -/
 @[app_delab Finset.sum] def delabFinsetSum : Delab :=
   whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
-  let ppDomain ← getPPOption getPPPiBinderTypes
+  let ppDomain ← getPPOption getPPFunBinderTypes
   let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
     return (i, ← delab)
   if s.isAppOfArity ``Finset.univ 2 then

Mathlib/Data/Fintype/Defs.lean

@@ -110,7 +110,7 @@ theorem subset_univ (s : Finset α) : s ⊆ univ := fun a _ => mem_univ a
 end Finset
 
 namespace Mathlib.Meta
-open Lean Elab Term Meta Batteries.ExtendedBinder
+open Lean Elab Term Meta Batteries.ExtendedBinder Parser.Term PrettyPrinter.Delaborator SubExpr
 
 /-- Elaborate set builder notation for `Finset`.
 
@@ -131,8 +131,6 @@ See also
   `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
 * `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator handling syntax of the
   form `{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.
-
-TODO: Write a delaborator
 -/
 @[term_elab setBuilder]
 def elabFinsetBuilderSetOf : TermElab
@@ -162,6 +160,34 @@ def elabFinsetBuilderSetOf : TermElab
     elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) (singleton $a)ᶜ)) expectedType?
   | _, _ => throwUnsupportedSyntax
 
+/-- Delaborator for `Finset.filter`. The `pp.funBinderTypes` option controls whether
+to show the domain type when the filter is over `Finset.univ`. -/
+@[app_delab Finset.filter] def delabFinsetFilter : Delab :=
+  whenPPOption getPPNotation do
+  let #[_, p, _, t] := (← getExpr).getAppArgs | failure
+  guard p.isLambda
+  let i ← withNaryArg 1 <| withBindingBodyUnusedName (pure ⟨·⟩)
+  let p ← withNaryArg 1 <| withBindingBody i.getId delab
+  if t.isAppOfArity ``Finset.univ 2 then
+    if ← getPPOption getPPFunBinderTypes then
+      let ty ← withNaryArg 0 delab
+      `({$i:ident : $ty | $p})
+    else
+      `({$i:ident | $p})
+  -- check if `t` is of the form `s₀ᶜ`, in which case we display `x ∉ s₀` instead
+  else if t.isAppOfArity ``HasCompl.compl 3 then
+    let #[_, _, s₀] := t.getAppArgs | failure
+    -- if `s₀` is a singleton, we can even use the notation `x ≠ a`
+    if s₀.isAppOfArity ``Singleton.singleton 4 then
+      let t ← withNaryArg 3 <| withNaryArg 2 <| withNaryArg 3 delab
+      `({$i:ident ≠ $t | $p})
+    else
+      let t ← withNaryArg 3 <| withNaryArg 2 delab
+      `({$i:ident ∉ $t | $p})
+  else
+    let t ← withNaryArg 3 delab
+    `({$i:ident ∈ $t | $p})
+
 end Mathlib.Meta
 
 open Finset Function

MathlibTest/Delab/FinsetBuilder.lean

@@ -0,0 +1,40 @@
+import Mathlib.Data.Fintype.Defs
+
+variable {α : Type*} [Fintype α] {p : α → Prop} {s : Finset α} {a : α}
+    [DecidablePred p] [DecidableEq α] [Singleton α (Finset α)] [HasCompl (Finset α)]
+
+/-- info: {x | p x} : Finset α -/
+#guard_msgs in
+#check ({x | p x} : Finset α)
+
+/-- info: {x ∈ s | p x} : Finset α -/
+#guard_msgs in
+#check ({x ∈ s | p x})
+
+/-- info: {x ≠ a | p x} : Finset α -/
+#guard_msgs in
+#check ({x ≠ a | p x} : Finset α)
+
+/-- info: {x ∉ s | p x} : Finset α -/
+#guard_msgs in
+#check ({x ∉ s | p x})
+
+/-- info: {x : α | p x} : Finset α -/
+#guard_msgs in
+set_option pp.funBinderTypes true in
+#check ({x | p x} : Finset α)
+
+/-- info: {x ∈ s | p x} : Finset α -/
+#guard_msgs in
+set_option pp.funBinderTypes true in
+#check ({x ∈ s | p x})
+
+/-- info: {x ≠ a | p x} : Finset α -/
+#guard_msgs in
+set_option pp.funBinderTypes true in
+#check ({x ≠ a | p x} : Finset α)
+
+/-- info: {x ∉ s | p x} : Finset α -/
+#guard_msgs in
+set_option pp.funBinderTypes true in
+#check ({x ∉ s | p x})