feat: analysis delaborator for LinearIndependent (#8602)

This is an experimental delaborator that works by analyzing the expression and tagging it with `pp.analysis`-style hints.

This causes pretty printing `LinearIndependent` like `LinearIndependent K fun (b : ↑s) ↦ ↑b` rather than `LinearIndependent K fun b ↦ ↑b` and `LinearIndependent (ι := { x // x ∈ s }) K Subtype.val` rather than `LinearIndependent K Subtype.val`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib.lean

@@ -2254,6 +2254,7 @@ import Mathlib.Lean.EnvExtension
 import Mathlib.Lean.Exception
 import Mathlib.Lean.Expr
 import Mathlib.Lean.Expr.Basic
+import Mathlib.Lean.Expr.ExtraRecognizers
 import Mathlib.Lean.Expr.ReplaceRec
 import Mathlib.Lean.Expr.Traverse
 import Mathlib.Lean.IO.Process

Mathlib/Lean/Expr/ExtraRecognizers.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Mathlib.Lean.Expr.Basic
+import Mathlib.Data.Set.Basic
+
+/-!
+# Additional Expr recognizers needing theory imports
+
+-/
+
+namespace Lean.Expr
+
+/-- If `e` is a coercion of a set to a type, return the set.
+Succeeds either for `Set.Elem s` terms or `{x // x ∈ s}` subtype terms. -/
+def coeTypeSet? (e : Expr) : Option Expr := do
+  if e.isAppOfArity ``Set.Elem 2 then
+    return e.appArg!
+  else if e.isAppOfArity ``Subtype 2 then
+    let .lam _ _ body _ := e.appArg! | failure
+    guard <| body.isAppOfArity ``Membership.mem 5
+    let #[_, _, inst, .bvar 0, s] := body.getAppArgs | failure
+    guard <| inst.isAppOfArity ``Set.instMembershipSet 1
+    return s
+  else
+    failure
+
+end Lean.Expr

Mathlib/Lean/PrettyPrinter/Delaborator.lean

@@ -46,3 +46,10 @@ def withBindingBodyUnusedName' {α} (d : Syntax → Expr → DelabM α) : DelabM
   let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
   let stxN ← annotateCurPos (mkIdent n)
   withBindingBody' n $ d stxN
+
+/-- Update `OptionsPerPos` at the given position, setting the key `n`
+to have the boolean value `v`. -/
+def OptionsPerPos.setBool (opts : OptionsPerPos) (p : SubExpr.Pos) (n : Name) (v : Bool) :
+    OptionsPerPos :=
+  let e := opts.findD p {} |>.setBool n v
+  opts.insert p e

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -9,6 +9,7 @@ import Mathlib.LinearAlgebra.Prod
 import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.LinearCombination
+import Mathlib.Lean.Expr.ExtraRecognizers
 
 #align_import linear_algebra.linear_independent from "leanprover-community/mathlib"@"9d684a893c52e1d6692a504a118bfccbae04feeb"
 
@@ -100,6 +101,26 @@ def LinearIndependent : Prop :=
   LinearMap.ker (Finsupp.total ι M R v) = ⊥
 #align linear_independent LinearIndependent
 
+open Lean PrettyPrinter.Delaborator SubExpr in
+/-- Delaborator for `LinearIndependent` that suggests pretty printing with type hints
+in case the family of vectors is over a `Set`.
+
+Type hints look like `LinearIndependent fun (v : ↑s) => ↑v` or `LinearIndependent (ι := ↑s) f`,
+depending on whether the family is a lambda expression or not. -/
+@[delab app.LinearIndependent]
+def delabLinearIndependent : Delab :=
+  whenPPOption getPPNotation <|
+  whenNotPPOption getPPAnalysisSkip <|
+  withOptionAtCurrPos `pp.analysis.skip true do
+    let e ← getExpr
+    guard <| e.isAppOfArity ``LinearIndependent 7
+    let some _ := (e.getArg! 0).coeTypeSet? | failure
+    let optionsPerPos ← if (e.getArg! 3).isLambda then
+      withNaryArg 3 do return (← read).optionsPerPos.setBool (← getPos) pp.funBinderTypes.name true
+    else
+      withNaryArg 0 do return (← read).optionsPerPos.setBool (← getPos) `pp.analysis.namedArg true
+    withTheReader Context ({· with optionsPerPos}) delab
+
 variable {R} {v}
 
 theorem linearIndependent_iff : LinearIndependent R v ↔ ∀ l, Finsupp.total ι M R v l = 0 → l = 0 :=

test/delabLinearIndependent.lean

@@ -0,0 +1,21 @@
+import Mathlib.LinearAlgebra.LinearIndependent
+
+set_option pp.unicode.fun true
+
+variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V}
+
+variable (h : LinearIndependent K (fun b => b : s → V)) in
+/-- info: h : LinearIndependent K fun (b : ↑s) ↦ ↑b -/
+#guard_msgs in #check h
+
+variable (h : LinearIndependent K (Subtype.val : s → V)) in
+/-- info: h : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val -/
+#guard_msgs in #check h
+
+variable (h : LinearIndependent K (by exact Subtype.val : s → V)) in
+/-- info: h : LinearIndependent (ι := ↑s) K Subtype.val -/
+#guard_msgs in #check h
+
+variable (h : LinearIndependent K (fun b => (fun b => b : s → V) b)) in
+/-- info: h : LinearIndependent K fun (b : ↑s) ↦ (fun b ↦ ↑b) b -/
+#guard_msgs in #check h