feat: long overdue delaborators (#7633)

This brings to Mathlib assorted delaborators written by @kmill for various projects including Mathematics in Lean. They mostly fix regressions compared to Lean 3.



Co-authored-by: Mario Carneiro <mcarneir@andrew.cmu.edu>

Mathlib/Data/Prod/Basic.lean

@@ -14,6 +14,7 @@ import Mathlib.Tactic.Inhabit
 # Extra facts about `Prod`
 
 This file defines `Prod.swap : α × β → β × α` and proves various simple lemmas about `Prod`.
+It also defines better delaborators for product projections.
 -/
 
 set_option autoImplicit true
@@ -414,3 +415,31 @@ theorem map_involutive [Nonempty α] [Nonempty β] {f : α → α} {g : β → 
 #align prod.map_involutive Prod.map_involutive
 
 end Prod
+
+section delaborators
+open Lean PrettyPrinter Delaborator
+
+/-- Delaborator for simple product projections. -/
+@[delab app.Prod.fst, delab app.Prod.snd]
+def delabProdProjs : Delab := do
+  let #[_, _, _] := (← SubExpr.getExpr).getAppArgs | failure
+  let stx ← delabProjectionApp
+  match stx with
+  | `($(x).fst) => `($(x).1)
+  | `($(x).snd) => `($(x).2)
+  | _ => failure
+
+/-- Delaborator for product first projection when the projection is a function
+that is then applied. -/
+@[app_unexpander Prod.fst]
+def unexpandProdFst : Lean.PrettyPrinter.Unexpander
+  | `($(_) $p $xs*) => `($p.1 $xs*)
+  | _ => throw ()
+
+/-- Delaborator for product second projection when the projection is a function
+that is then applied. -/
+@[app_unexpander Prod.snd]
+def unexpandProdSnd : Lean.PrettyPrinter.Unexpander
+  | `($(_) $p $xs*) => `($p.2 $xs*)
+  | _ => throw ()
+end delaborators

Mathlib/Data/Set/Lattice.lean

@@ -115,6 +115,68 @@ notation3 "⋃ "(...)", "r:60:(scoped f => iUnion f) => r
 /-- Notation for `Set.iInter`. Indexed intersection of a family of sets -/
 notation3 "⋂ "(...)", "r:60:(scoped f => iInter f) => r
 
+section delaborators
+
+open Lean Lean.PrettyPrinter.Delaborator
+
+/-- Delaborator for indexed unions. -/
+@[delab app.Set.iUnion]
+def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
+  let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.isLambda do failure
+  let prop ← Meta.isProp ι
+  let dep := f.bindingBody!.hasLooseBVar 0
+  let ppTypes ← getPPOption getPPFunBinderTypes
+  let stx ← SubExpr.withAppArg do
+    let dom ← SubExpr.withBindingDomain delab
+    withBindingBodyUnusedName $ fun x => do
+      let x : TSyntax `ident := .mk x
+      let body ← delab
+      if prop && !dep then
+        `(⋃ (_ : $dom), $body)
+      else if prop || ppTypes then
+        `(⋃ ($x:ident : $dom), $body)
+      else
+        `(⋃ $x:ident, $body)
+  -- Cute binders
+  let stx : Term ←
+    match stx with
+    | `(⋃ $x:ident, ⋃ (_ : $y:ident ∈ $s), $body)
+    | `(⋃ ($x:ident : $_), ⋃ (_ : $y:ident ∈ $s), $body) =>
+      if x == y then `(⋃ $x:ident ∈ $s, $body) else pure stx
+    | _ => pure stx
+  return stx
+
+/-- Delaborator for indexed intersections. -/
+@[delab app.Set.iInter]
+def sInter_delab : Delab := whenPPOption Lean.getPPNotation do
+  let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.isLambda do failure
+  let prop ← Meta.isProp ι
+  let dep := f.bindingBody!.hasLooseBVar 0
+  let ppTypes ← getPPOption getPPFunBinderTypes
+  let stx ← SubExpr.withAppArg do
+    let dom ← SubExpr.withBindingDomain delab
+    withBindingBodyUnusedName $ fun x => do
+      let x : TSyntax `ident := .mk x
+      let body ← delab
+      if prop && !dep then
+        `(⋂ (_ : $dom), $body)
+      else if prop || ppTypes then
+        `(⋂ ($x:ident : $dom), $body)
+      else
+        `(⋂ $x:ident, $body)
+  -- Cute binders
+  let stx : Term ←
+    match stx with
+    | `(⋂ $x:ident, ⋂ (_ : $y:ident ∈ $s), $body)
+    | `(⋂ ($x:ident : $_), ⋂ (_ : $y:ident ∈ $s), $body) =>
+      if x == y then `(⋂ $x:ident ∈ $s, $body) else pure stx
+    | _ => pure stx
+  return stx
+
+end delaborators
+
 @[simp]
 theorem sSup_eq_sUnion (S : Set (Set α)) : sSup S = ⋃₀S :=
   rfl

Mathlib/Order/CompleteLattice.lean

@@ -109,6 +109,67 @@ notation3 "⨆ "(...)", "r:60:(scoped f => iSup f) => r
 /-- Indexed infimum. -/
 notation3 "⨅ "(...)", "r:60:(scoped f => iInf f) => r
 
+section delaborators
+
+open Lean Lean.PrettyPrinter.Delaborator
+
+/-- Delaborator for indexed supremum. -/
+@[delab app.iSup]
+def iSup_delab : Delab := whenPPOption Lean.getPPNotation do
+  let #[_, _, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.isLambda do failure
+  let prop ← Meta.isProp ι
+  let dep := f.bindingBody!.hasLooseBVar 0
+  let ppTypes ← getPPOption getPPFunBinderTypes
+  let stx ← SubExpr.withAppArg do
+    let dom ← SubExpr.withBindingDomain delab
+    withBindingBodyUnusedName $ fun x => do
+      let x : TSyntax `ident := .mk x
+      let body ← delab
+      if prop && !dep then
+        `(⨆ (_ : $dom), $body)
+      else if prop || ppTypes then
+        `(⨆ ($x:ident : $dom), $body)
+      else
+        `(⨆ $x:ident, $body)
+  -- Cute binders
+  let stx : Term ←
+    match stx with
+    | `(⨆ $x:ident, ⨆ (_ : $y:ident ∈ $s), $body)
+    | `(⨆ ($x:ident : $_), ⨆ (_ : $y:ident ∈ $s), $body) =>
+      if x == y then `(⨆ $x:ident ∈ $s, $body) else pure stx
+    | _ => pure stx
+  return stx
+
+/-- Delaborator for indexed infimum. -/
+@[delab app.iInf]
+def iInf_delab : Delab := whenPPOption Lean.getPPNotation do
+  let #[_, _, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.isLambda do failure
+  let prop ← Meta.isProp ι
+  let dep := f.bindingBody!.hasLooseBVar 0
+  let ppTypes ← getPPOption getPPFunBinderTypes
+  let stx ← SubExpr.withAppArg do
+    let dom ← SubExpr.withBindingDomain delab
+    withBindingBodyUnusedName $ fun x => do
+      let x : TSyntax `ident := .mk x
+      let body ← delab
+      if prop && !dep then
+        `(⨅ (_ : $dom), $body)
+      else if prop || ppTypes then
+        `(⨅ ($x:ident : $dom), $body)
+      else
+        `(⨅ $x:ident, $body)
+  -- Cute binders
+  let stx : Term ←
+    match stx with
+    | `(⨅ $x:ident, ⨅ (_ : $y:ident ∈ $s), $body)
+    | `(⨅ ($x:ident : $_), ⨅ (_ : $y:ident ∈ $s), $body) =>
+      if x == y then `(⨅ $x:ident ∈ $s, $body) else pure stx
+    | _ => pure stx
+  return stx
+end delaborators
+
 instance OrderDual.supSet (α) [InfSet α] : SupSet αᵒᵈ :=
   ⟨(sInf : Set α → α)⟩
 

Mathlib/Util/PiNotation.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Std.Util.ExtendedBinder
+import Std.Classes.SetNotation
 
 /-! # Pi type notation
 
@@ -42,12 +42,33 @@ parse it by simply using the pre-existing forall parser. -/
   | .node info _ args => return .node info ``Lean.Parser.Term.forall args
   | _ => Lean.Macro.throwUnsupported
 
-/-- Override the Lean 4 pi notation delaborator with one that uses `Π`.
+/-- Override the Lean 4 pi notation delaborator with one that prints cute binders
+such as `∀ ε > 0`. -/
+@[delab forallE]
+def delabPi : Delab := whenPPOption Lean.getPPNotation do
+  let stx ← delabForall
+  match stx with
+  | `(∀ ($i:ident : $_), $j:ident ∈ $s → $body) =>
+    if i == j then `(∀ $i:ident ∈ $s, $body) else pure stx
+  | `(∀ ($x:ident : $_), $y:ident > $z → $body) =>
+    if x == y then `(∀ $x:ident > $z, $body) else pure stx
+  | `(∀ ($x:ident : $_), $y:ident < $z → $body) =>
+    if x == y then `(∀ $x:ident < $z, $body) else pure stx
+  | `(∀ ($x:ident : $_), $y:ident ≥ $z → $body) =>
+    if x == y then `(∀ $x:ident ≥ $z, $body) else pure stx
+  | `(∀ ($x:ident : $_), $y:ident ≤ $z → $body) =>
+    if x == y then `(∀ $x:ident ≤ $z, $body) else pure stx
+  | `(Π ($i:ident : $_), $j:ident ∈ $s → $body) =>
+    if i == j then `(Π $i:ident ∈ $s, $body) else pure stx
+  | _ => pure stx
+
+/-- Override the Lean 4 pi notation delaborator with one that uses `Π` and prints
+cute binders such as `∀ ε > 0`.
 Note that this takes advantage of the fact that `(x : α) → p x` notation is
 never used for propositions, so we can match on this result and rewrite it. -/
 @[scoped delab forallE]
-def delabPi : Delab := whenPPOption Lean.getPPNotation do
-  let stx ← delabForall
+def delabPi' : Delab := whenPPOption Lean.getPPNotation do
+  let stx ← delabPi
   -- Replacements
   let stx : Term ←
     match stx with
@@ -59,3 +80,51 @@ def delabPi : Delab := whenPPOption Lean.getPPNotation do
   | _ => pure stx
 
 end PiNotation
+
+section existential
+open Lean Parser Term PrettyPrinter Delaborator
+
+/-- Delaborator for existential quantifier, including extended binders. -/
+-- TODO: reduce the duplication in this code
+@[delab app.Exists]
+def exists_delab : Delab := whenPPOption Lean.getPPNotation do
+  let #[ι, f] := (← SubExpr.getExpr).getAppArgs | failure
+  unless f.isLambda do failure
+  let prop ← Meta.isProp ι
+  let dep := f.bindingBody!.hasLooseBVar 0
+  let ppTypes ← getPPOption getPPFunBinderTypes
+  let stx ← SubExpr.withAppArg do
+    let dom ← SubExpr.withBindingDomain delab
+    withBindingBodyUnusedName $ fun x => do
+      let x : TSyntax `ident := .mk x
+      let body ← delab
+      if prop && !dep then
+        `(∃ (_ : $dom), $body)
+      else if prop || ppTypes then
+        `(∃ ($x:ident : $dom), $body)
+      else
+        `(∃ $x:ident, $body)
+  -- Cute binders
+  let stx : Term ←
+    match stx with
+    | `(∃ $i:ident, $j:ident ∈ $s ∧ $body)
+    | `(∃ ($i:ident : $_), $j:ident ∈ $s ∧ $body) =>
+      if i == j then `(∃ $i:ident ∈ $s, $body) else pure stx
+    | `(∃ $x:ident, $y:ident > $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident > $z ∧ $body) =>
+      if x == y then `(∃ $x:ident > $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident < $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident < $z ∧ $body) =>
+      if x == y then `(∃ $x:ident < $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ≥ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ≥ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ≥ $z, $body) else pure stx
+    | `(∃ $x:ident, $y:ident ≤ $z ∧ $body)
+    | `(∃ ($x:ident : $_), $y:ident ≤ $z ∧ $body) =>
+      if x == y then `(∃ $x:ident ≤ $z, $body) else pure stx
+    | _ => pure stx
+  -- Merging
+  match stx with
+  | `(∃ $group:bracketedExplicitBinders, ∃ $groups*, $body) => `(∃ $group $groups*, $body)
+  | _ => pure stx
+end existential

test/delaborators.lean

@@ -0,0 +1,122 @@
+import Std.Tactic.GuardMsgs
+import Mathlib.Util.PiNotation
+import Mathlib.Data.Set.Lattice
+
+section PiNotation
+variable (P : Nat → Prop) (α : Nat → Type) (s : Set ℕ)
+
+/-- info: ∀ x > 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x, x > 0 → P x
+
+/-- info: ∀ x > 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x > 0, P x
+
+/-- info: ∀ x ≥ 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x, x ≥ 0 → P x
+
+/-- info: ∀ x ≥ 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x ≥ 0, P x
+
+/-- info: ∀ x < 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x < 0, P x
+
+/-- info: ∀ x < 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x, x < 0 → P x
+
+/-- info: ∀ x ≤ 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x ≤ 0, P x
+
+/-- info: ∀ x ≤ 0, P x : Prop -/
+#guard_msgs in
+#check ∀ x, x ≤ 0 → P x
+
+/-- info: ∀ x ∈ s, P x : Prop -/
+#guard_msgs in
+#check ∀ x ∈ s, P x
+
+/-- info: ∀ x ∈ s, P x : Prop -/
+#guard_msgs in
+#check ∀ x, x ∈ s → P x
+
+/-- info: (x : ℕ) → α x : Type -/
+#guard_msgs in
+#check (x : Nat) → α x
+
+open PiNotation
+
+/-- info: Π (x : ℕ), α x : Type -/
+#guard_msgs in
+#check (x : Nat) → α x
+
+/-- info: ∀ (x : ℕ), P x : Prop -/
+#guard_msgs in
+#check (x : Nat) → P x
+
+end PiNotation
+
+section UnionInter
+variable (s : ℕ → Set ℕ) (u : Set ℕ) (p : ℕ → Prop)
+
+/-- info: ⋃ n ∈ u, s n : Set ℕ -/
+#guard_msgs in
+#check ⋃ n ∈ u, s n
+
+/-- info: ⋂ n ∈ u, s n : Set ℕ -/
+#guard_msgs in
+#check ⋂ n ∈ u, s n
+
+end UnionInter
+
+section CompleteLattice
+/-- info: ⨆ i ∈ Set.univ, (i = i) : Prop -/
+#guard_msgs in
+#check ⨆ (i : Nat) (_ : i ∈ Set.univ), (i = i)
+
+/-- info: ⨅ i ∈ Set.univ, (i = i) : Prop -/
+#guard_msgs in
+#check ⨅ (i : Nat) (_ : i ∈ Set.univ), (i = i)
+
+end CompleteLattice
+
+section existential
+
+/-- info: ∃ i ≥ 3, i = i : Prop -/
+#guard_msgs in
+#check ∃ (i : Nat), i ≥ 3 ∧ i = i
+
+/-- info: ∃ i > 3, i = i : Prop -/
+#guard_msgs in
+#check ∃ (i : Nat), i > 3 ∧ i = i
+
+/-- info: ∃ i ≤ 3, i = i : Prop -/
+#guard_msgs in
+#check ∃ (i : Nat), i ≤ 3 ∧ i = i
+
+/-- info: ∃ i < 3, i = i : Prop -/
+#guard_msgs in
+#check ∃ (i : Nat), i < 3 ∧ i = i
+
+end existential
+
+section prod
+
+variable (x : ℕ × ℕ)
+
+/-- info: x.1 : ℕ -/
+#guard_msgs in
+#check x.1
+
+variable (p : (ℕ → ℕ) × (ℕ → ℕ))
+
+/-- info: p.1 22 : ℕ -/
+#guard_msgs in
+#check p.1 22
+
+end prod