perf: improve heuristic at isDefEq (#3837)

This is intended to fail at present: it just adds a test case containing
a minimization of a Mathlib slowdown from #3807.

Prior to #3807, the declaration `exists_algHom_adjoin_of_splits'''` at
the end of the file would take around 16,000 heartbeats. Now it takes
around 210,000 heartbeats.

---------

Co-authored-by: Leonardo de Moura <[email protected]>

src/Lean/Meta/ExprDefEq.lean

@@ -1173,6 +1173,35 @@ private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do
   trace[Meta.isDefEq.delta.unfoldLeftRight] fn
   toLBoolM <| Meta.isExprDefEqAux t s
 
+/-- Helper predicate for `tryHeuristic`. -/
+private def isNonTrivialRegular (info : DefinitionVal) : MetaM Bool := do
+  match info.hints with
+  | .regular d =>
+    if (← isProjectionFn info.name) then
+      -- All projections are considered trivial
+      return false
+    if d > 2 then
+      -- If definition depth is greater than 2, we claim it is not a trivial definition
+      return true
+    -- After consuming the lambda expressions, we consider a regular definition non-trivial if it is not "simple".
+    -- Where simple is a bvar/lit/sort/proj or a single application where all arguments are bvar/lit/sort/proj.
+    let val := consumeDefnPreamble info.value
+    return !isSimple val (allowApp := true)
+  | _ => return false
+where
+  consumeDefnPreamble (e : Expr) : Expr :=
+    match e with
+    | .mdata _ e => consumeDefnPreamble e
+    | .lam _ _ b _ => consumeDefnPreamble b
+    | _ => e
+  isSimple (e : Expr) (allowApp : Bool) : Bool :=
+    match e with
+    | .bvar .. | .sort .. | .lit .. | .fvar .. | .mvar .. => true
+    | .app f a => isSimple a false && isSimple f allowApp
+    | .proj _ _ b => isSimple b false
+    | .mdata _ b => isSimple b allowApp
+    | .lam .. | .letE .. | .forallE .. | .const .. => false
+
 /-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`.
 
     Auxiliary method for isDefEqDelta -/
@@ -1181,19 +1210,32 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
   let mut s := s
   let tFn := t.getAppFn
   let sFn := s.getAppFn
-  let info ← getConstInfo tFn.constName!
-  /- We only use the heuristic when `f` is a regular definition or an auxiliary `match` application.
-     That is, it is not marked an abbreviation (e.g., a user-facing projection) or as opaque (e.g., proof).
-     We check whether terms contain metavariables to make sure we can solve constraints such
-     as `S.proj ?x =?= S.proj t` without performing delta-reduction.
-     That is, we are assuming the heuristic implemented by this method is seldom effective
-     when `t` and `s` do not have metavariables, are not structurally equal, and `f` is an abbreviation.
-     On the other hand, by unfolding `f`, we often produce smaller terms.
-
-     Recall that auxiliary `match` definitions are marked as abbreviations, but we must use the heuristic on
-     them since they will not be unfolded when smartUnfolding is turned on. The abbreviation annotation in this
-     case is used to help the kernel type checker. -/
-  unless info.hints.isRegular || isMatcherCore (← getEnv) tFn.constName! do
+  -- If `f` (i.e., `tFn`) is not a definition, we do not apply the heuristic.
+  let .defnInfo info ← getConstInfo tFn.constName! | return false
+  /-
+  We apply the heuristic in the following cases:
+  1- `f` is a non-trivial regular definition (see predicate `isNonTrivialRegular`)
+  2- `f` is `match` application.
+  3- `t` or `s` contain meta-variables.
+
+  The third case is important to make sure we can solve constraints such as
+  `S.proj ?x =?= S.proj t` without performing delta-reduction.
+
+  When the conditions 1&2&3 do not hold, we are assuming the heuristic implemented by this method is seldom effective
+  when `f` is not simple, `t` and `s` do not have metavariables, are not structurally equal.
+
+  Recall that auxiliary `match` definitions are marked as abbreviations, but we must use the heuristic on
+  them since they will not be unfolded when smartUnfolding is turned on. The abbreviation annotation in this
+  case is used to help the kernel type checker.
+
+  The `isNonTrivialRegular` predicate is also useful to avoid applying the heuristic to very simple definitions that
+  have not been marked as abbreviations by the user. Example:
+  ```
+  protected def Mem (a : α) (s : Set α) : Prop := s a
+  ```
+  at test 3807.lean
+  -/
+  unless (← isNonTrivialRegular info) || isMatcherCore (← getEnv) tFn.constName! do
     unless t.hasExprMVar || s.hasExprMVar do
       return false
   withTraceNodeBefore `Meta.isDefEq.delta (return m!"{t} =?= {s}") do