From b3f8feffd3b3d6bd2ff79d7b2949b51fe5663714 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 15 Jan 2025 08:43:59 -0800
Subject: [PATCH] fix: improve E-matching pattern selection heuristics (#6653)

This PR improves the E-matching pattern selection heuristics in the
`grind` tactic. They now take into account type predicates and
transformers.
---
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 23 ++++++++++++++++---
 tests/lean/run/grind_t1.lean                  |  3 +++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index acf370f11f..1ec2300dfc 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -269,19 +269,36 @@ private def getPatternFn? (pattern : Expr) : Option Expr :=
 
 /--
 Returns a bit-mask `mask` s.t. `mask[i]` is true if the corresponding argument is
-- a type (that is not a proposition) or type former, or
+- a type (that is not a proposition) or type former (which has forward dependencies) or
 - a proof, or
 - an instance implicit argument
 
 When `mask[i]`, we say the corresponding argument is a "support" argument.
 -/
 def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
+  let pinfos := (← getFunInfoNArgs f numArgs).paramInfo
   forallBoundedTelescope (← inferType f) numArgs fun xs _ => do
-    xs.mapM fun x => do
+    xs.mapIdxM fun idx x => do
       if (← isProp x) then
         return false
-      else if (← isTypeFormer x <||> isProof x) then
+      else if (← isProof x) then
         return true
+      else if (← isTypeFormer x) then
+        if h : idx < pinfos.size then
+          /-
+          We originally wanted to ignore types and type formers in `grind` and treat them as supporting elements.
+          Thus, we would always return `true`. However, we changed our heuristic because of the following example:
+          ```
+          example {α} (f : α → Type) (a : α) (h : ∀ x, Nonempty (f x)) : Nonempty (f a) := by
+            grind
+          ```
+          In this example, we are reasoning about types. Therefore, we adjusted the heuristic as follows:
+          a type or type former is considered a supporting element only if it has forward dependencies.
+          Note that this is not the case for `Nonempty`.
+          -/
+          return pinfos[idx].hasFwdDeps
+        else
+          return true
       else
         return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
 
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 4e5ce23fa8..e138b663d3 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -280,3 +280,6 @@ example {a b : Nat} (h : a < b) : ¬ b < a := by
 
 example {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m := by
   grind
+
+example {α} (f : α → Type) (a : α) (h : ∀ x, Nonempty (f x)) : Nonempty (f a) := by
+  grind