feat: improve pattern pretty printer

Delaborator does not support loose bound variables.

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -56,6 +56,8 @@ structure Choice where
   gen        : Nat
   /-- Partial assignment so far. Recall that pattern variables are encoded as de-Bruijn variables. -/
   assignment : Array Expr
+  /-- Higher-order pattern arguments pending `isDefEq` check at instantiation time. -/
+  hoPending  : Array (Expr × Expr) := #[]
   deriving Inhabited
 
 /-- Context for the E-matching monad. -/
@@ -210,6 +212,8 @@ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM C
       return { c with cnstrs := .offset (some genInfo) pArg k eArg :: c.cnstrs }
     else
       return { c with cnstrs := .match (some genInfo) pArg eArg :: c.cnstrs }
+  else if let some pat := hoPattern? pArg then
+    return { c with hoPending := c.hoPending.push (pat, eArg) }
   else
     return { c with cnstrs := .match none pArg eArg :: c.cnstrs }
 
@@ -791,6 +795,12 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
     reportEMatchIssue! "unexpected number of parameters at {thm.origin.pp}"
     return ()
   let (some _, c) ← applyAssignment mvars |>.run c | return ()
+  -- Process higher-order pattern arguments using `isDefEq`
+  for (pat, e) in c.hoPending do
+    let pat := pat.instantiateRev mvars
+    unless (← isDefEq pat e) do
+      reportEMatchIssue! "failed to match higher-order pattern at {thm.origin.pp}"
+      return ()
   let some _ ← synthesizeInsts mvars bis | return ()
   if (← checkConstraints thm c.gen proof mvars) then
     let guards ← collectGuards thm proof mvars

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.TryThis
 import Lean.Meta.Sym.Util
 import Lean.Meta.Sym.Eta
+import Init.Omega
 public section
 namespace Lean.Meta.Grind
 /-!
@@ -399,15 +400,26 @@ def groundPattern? (e : Expr) : Option Expr :=
 private def isGroundPattern (e : Expr) : Bool :=
   groundPattern? e |>.isSome
 
+def mkHOPattern (e : Expr) : Expr :=
+  mkAnnotation `grind.ho_pat e
+
+def hoPattern? (e : Expr) : Option Expr :=
+  annotation? `grind.ho_pat e
+
+def isHOPattern (e : Expr) : Bool :=
+  hoPattern? e |>.isSome
+
 def isPatternDontCare (e : Expr) : Bool :=
   e == dontCare
 
 private def isAtomicPattern (e : Expr) : Bool :=
-  e.isBVar || isPatternDontCare e || isGroundPattern e
+  e.isBVar || isPatternDontCare e || isGroundPattern e || isHOPattern e
 
 partial def ppPattern (pattern : Expr) : MessageData := Id.run do
   if let some e := groundPattern? pattern then
     return m!"`[{e}]"
+  else if let some e := hoPattern? pattern then
+    return m!"ho[{ppHOBody e}]"
   else if isPatternDontCare pattern then
     return m!"_"
   else match pattern with
@@ -428,6 +440,97 @@ where
       ppPattern arg
     else
       .paren (ppPattern arg)
+  /- **Note**: This is a workaround because the current delaborator panics if the expression contains loose de Bruijn variables. -/
+  ppHOBody (e : Expr) (names : List Name := []) : MessageData :=
+    match e with
+    | .forallE n _ b _ | .lam n _ b _ =>
+      let name := if n.isAnonymous then `x else if n.hasMacroScopes then `_ else n
+      let body := ppHOBody b (name :: names)
+      if e.isLambda then m!"fun {name} => {body}" else m!"∀ {name}, {body}"
+    | .bvar idx =>
+      match names[idx]? with
+      | some n => m!"{n}"
+      | none   => m!"#{idx - names.length}"
+    | .app .. =>
+      let f := e.getAppFn
+      let args := e.getAppArgs
+      args.foldl (init := ppHOBody f names) fun r arg =>
+        r ++ " " ++ ppHOBodyAtom arg names
+    | .mdata _ b => ppHOBody b names
+    | _ =>
+      -- **Note**: This is a workaround. We use `toString` if there are loose de Bruijn variables to avoid panic in the delaborator.
+      if e.hasLooseBVars then m!"{toString e}" else m!"{e}"
+  ppHOBodyAtom (e : Expr) (names : List Name) : MessageData :=
+    match e with
+    | .bvar _ => ppHOBody e names
+    | .app .. => .paren (ppHOBody e names)
+    | .mdata _ b => ppHOBodyAtom b names
+    | _ => ppHOBody e names
+
+namespace MillerCheck
+/--
+Result of the Miller pattern check. Tracks all pattern variables found in the lambda body
+that are Miller pattens.
+-/
+private structure State where
+  /-- All pattern variable indices (adjusted by offset) found in the body. -/
+  foundVars     : Array Nat := #[]
+
+/--
+Checks whether the arguments are distinct variables `< offset`
+-/
+private def checkMillerArgs (args : Array Expr) (offset : Nat) : Bool := Id.run do
+  for h : i in *...args.size do
+    have : i < args.size := by omega
+    let arg := args[i]
+    let .bvar idx := arg | return false
+    unless idx < offset do return false
+    for h : j in *...i do
+      have : j < i := by omega
+      let prev := args[j]
+      if prev == arg then return false
+  return true
+
+private abbrev MillerM := StateM State
+
+private def addVar (idx : Nat) : MillerM Unit := do
+  unless (← get).foundVars.contains idx do
+    modify fun s => { s with foundVars := s.foundVars.push idx }
+
+private partial def visit (e : Expr) (offset : Nat) : MillerM Unit := do
+  match e with
+  | .app .. => e.withApp fun f args => do
+    if let .bvar idx := f then
+      if idx ≥ offset && checkMillerArgs args offset then
+        addVar (idx - offset)
+      else return ()
+    else
+      args.forM (visit · offset)
+  | .bvar idx => if idx ≥ offset then addVar (idx - offset)
+  | .const .. | .sort .. | .fvar .. | .mvar .. | .lit .. => return ()
+  | .mdata _ b => visit b offset
+  | .forallE _ _ b _ | .lam _ _ b _ => visit b (offset+1)
+  | .proj .. | .letE .. => unreachable!
+
+end MillerCheck
+
+/--
+Checks whether the given lambda expression `e` contains subterms satisfying the Miller's pattern condition for
+higher-order matching.
+
+The function traverses the lambda body and validates:
+For each bvar with `index >= offset` (i.e., a pattern variable) where `offset` is the number of binders.
+- If applied (`#k a₁ ... aₙ`): all `aᵢ` must be distinct bvars with `index < offset`
+- If bare: OK (the metavar can't capture lambda-bound vars anyway)
+- At least one pattern variable must appear in a proper Miller application position
+  (i.e., applied to lambda-bound variables).
+
+Returns adjusted bvar indices `(index - offset)` of the pattern variables found, or `none` on violation.
+-/
+private def checkMillerHOPattern? (e : Expr) : Option (Array Nat) :=
+  let (_, { foundVars }) := MillerCheck.visit e 0 |>.run {}
+  if foundVars.isEmpty then none
+  else some foundVars
 
 namespace NormalizePattern
 
@@ -701,17 +804,61 @@ where
           saveBVar idx
           pure arg
       | _ =>
-        if let some _ ← getPatternFn? arg inSupport (root := false) argKind then
+        if arg.isLambda then
+          if let some bvarIndices := checkMillerHOPattern? arg then
+            -- Ignore if `arg` does not contain any ney bvar
+            if (← bvarIndices.anyM fun idx => return !(← foundBVar idx)) then
+              -- **Note**: see postprocessor `removeRedundantHOPatterns`
+              return mkHOPattern arg
+          return dontCare
+        else if let some _ ← getPatternFn? arg inSupport (root := false) argKind then
           go arg inSupport (root := false)
         else
-          pure dontCare
+          return dontCare
 
-def main (patterns : List Expr) (symPrios : SymbolPriorities) (minPrio : Nat) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat) := do
-  let (patterns, s) ← patterns.mapM (go (inSupport := false) (root := true)) { symPrios, minPrio } |>.run {}
-  return (patterns, s.symbols.toList, s.bvarsFound)
+/-- Collect bvar indices that appear in non-HO positions of a pattern. -/
+private partial def collectNonHOBVars (e : Expr) (s : Array Nat := #[]) : Array Nat :=
+  if isPatternDontCare e || (hoPattern? e).isSome || (groundPattern? e).isSome then s
+  else match e with
+  | .bvar idx => if s.contains idx then s else s.push idx
+  | .app f a => collectNonHOBVars a (collectNonHOBVars f s)
+  | .mdata _ b => collectNonHOBVars b s
+  | _ => s
+
+/-- Replace HO patterns with `dontCare` if all their pattern variables already appear in non-HO positions. -/
+private partial def removeRedundantHOPatterns (e : Expr) (nonHOBVars : Array Nat) : Expr :=
+  go e
+where
+  go (e : Expr) : Expr := Id.run do
+    if isPatternDontCare e || (groundPattern? e).isSome || e.isBVar then return e
+    if let some body := hoPattern? e then
+      let some bvarIndices := checkMillerHOPattern? body | return dontCare
+      if bvarIndices.all nonHOBVars.contains then return dontCare else return e
+    else
+      match e with
+      | .app f a => return mkApp (go f) (go a)
+      | .mdata d b => return mkMData d (go b)
+      | _ => return e
+
+/-- Save bvar indices from remaining HO patterns after redundant ones have been removed. -/
+private partial def saveHOPatternBVars (e : Expr) : M Unit := do
+  if let some body := hoPattern? e then
+    if let some bvarIndices := checkMillerHOPattern? body then
+      bvarIndices.forM saveBVar
+  else
+    let .app f a := e | return ()
+    saveHOPatternBVars f; saveHOPatternBVars a
 
 private def normalizePattern (e : Expr) : M Expr := do
-  go e (inSupport := false) (root := true)
+  let p ← go e (inSupport := false) (root := true)
+  let nonHOBVars := collectNonHOBVars p
+  let p := removeRedundantHOPatterns p nonHOBVars
+  saveHOPatternBVars p
+  return p
+
+def main (patterns : List Expr) (symPrios : SymbolPriorities) (minPrio : Nat) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat) := do
+  let (patterns, s) ← patterns.mapM normalizePattern { symPrios, minPrio } |>.run {}
+  return (patterns, s.symbols.toList, s.bvarsFound)
 
 end NormalizePattern
 

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -190,6 +190,9 @@ where
   go (pattern : Expr) : GoalM Expr := do
     if pattern.isBVar || isPatternDontCare pattern then
       return pattern
+    else if (hoPattern? pattern).isSome then
+      -- HO patterns are matched via `isDefEq` at instantiation time, not via the E-graph
+      return pattern
     else if let some e := groundPattern? pattern then
       let e ← preprocessLight e
       let e ← if e.hasLevelParam && origin matches .decl _ then

tests/lean/run/grind_ematch_ho.lean

@@ -0,0 +1,82 @@
+module
+reset_grind_attrs%
+public section
+set_option trace.grind.ematch.pattern true
+set_option warn.sorry false
+
+/-! # Higher-order E-matching tests
+
+These tests verify the HO pattern matching feature. When a pattern contains a
+lambda whose body applies pattern variables to distinct lambda-bound variables
+(Miller condition), it is wrapped as `ho[...]` and matched via `isDefEq` at
+instantiation time rather than the E-graph.
+
+Lambdas of the form `fun x => f x` are eta-reduced during pattern preprocessing,
+so they never reach the HO handler. These tests use non-eta-reducible lambdas.
+-/
+
+/-! ## Basic: lambda with argument reordering (non-eta-reducible) -/
+
+opaque applyFlip : (Nat → Nat → Nat) → Nat → Nat → Nat
+
+/-- trace: [grind.ematch.pattern] applyFlip_spec: [applyFlip ho[fun x => fun y => #2 y x] #1 #0] -/
+#guard_msgs (trace, warning) in
+@[grind =] theorem applyFlip_spec (f : Nat → Nat → Nat) (a b : Nat)
+    : applyFlip (fun x y => f y x) a b = f b a := sorry
+
+example (h : applyFlip (fun x y => Nat.add y x) 3 4 = 42) : Nat.add 4 3 = 42 := by
+  grind
+
+/-! ## Partial application: lambda uses only some lambda-bound vars -/
+
+opaque applyConst : (Nat → Nat → Nat) → Nat → Nat → Nat
+
+/-- trace: [grind.ematch.pattern] applyConst_spec: [applyConst ho[fun x => fun _ => #2 x] #1 #0] -/
+#guard_msgs (trace, warning) in
+@[grind =] theorem applyConst_spec (f : Nat → Nat) (a b : Nat)
+    : applyConst (fun x _ => f x) a b = f a := sorry
+
+example (h : applyConst (fun x _ => x + 1) 5 10 = 42) : 6 = 42 := by
+  grind
+
+/-! ## Non-Miller rejection: fun x => g (x + 1) fails Miller → dontCare -/
+
+-- `g (x + 1)` means the argument to `g` is not a bare bvar → Miller fails.
+-- With dontCare, `g` is not covered on the LHS nor RHS.
+-- This theorem can still be tagged with `@[grind .]` which finds a multi-pattern.
+opaque applyMod : (Nat → Nat) → Nat → Nat
+
+theorem applyMod_spec (g : Nat → Nat) (a : Nat)
+    : applyMod (fun x => g (x + 1)) a = g (a + 1) := sorry
+
+/-! ## Pattern variable in both HO and FO positions -/
+
+opaque applyWith : (Nat → Nat → Nat) → Nat → Nat → Nat → Nat
+
+/--
+trace: [grind.ematch.pattern] applyWith_spec: [applyWith ho[fun x => fun y => #3 y x] #2 #1 #0]
+-/
+#guard_msgs (trace, warning) in
+@[grind =] theorem applyWith_spec (f : Nat → Nat → Nat) (a b c : Nat)
+    : applyWith (fun x y => f y x) a b c = f b a + c := sorry
+
+example (h : applyWith (fun x y => Nat.add y x) 1 2 3 = 42) : Nat.add 2 1 + 3 = 42 := by
+  grind
+
+/-! ## Realistic example: foldl with flipped cons -/
+
+-- The lambda `fun xs y => y :: xs` doesn't need HO matching (no pattern variable
+-- in Miller position — only `α` appears as a bare bvar). First-order matching with
+-- dontCare suffices since the lambda is alpha-equivalent to the one in the goal.
+/-- trace: [grind.ematch.pattern] foldl_flip_cons_eq_append': [@List.foldl (List #2) _ _ #0 #1] -/
+#guard_msgs (trace, warning) in
+@[grind =] theorem foldl_flip_cons_eq_append' {l l' : List α}
+    : l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := sorry
+
+example (xs ys : List Nat) (h : xs.foldl (fun a b => b :: a) ys = [1, 2, 3])
+    : xs.reverse ++ ys = [1, 2, 3] := by
+  grind
+
+
+
+end