From 41040a81decedd4d9daf061d682f4ce2d8d70df7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Dec 2021 16:06:41 -0800
Subject: [PATCH] fix: auxiliary matcher definitions should be treated as
 abbreviations

The motivation is to prevent performance problems such as the one
described at issue #854.

Fixes #854 after a update stage0
---
 src/Lean/Meta/ExprDefEq.lean   | 12 ++++++++----
 src/Lean/Meta/Match/Match.lean | 10 +++++-----
 tests/lean/run/854.lean        | 17 +++++++++++++++++
 3 files changed, 30 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/854.lean

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index bbc8b60685..ba64ea0146 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1035,14 +1035,18 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
   let tFn := t.getAppFn
   let sFn := s.getAppFn
   let info ← getConstInfo tFn.constName!
-  /- We only use the heuristic when `f` is a regular definition. That is, it is marked an abbreviation
-     (e.g., a user-facing projection) or as opaque (e.g., proof).
+  /- 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. -/
-  unless info.hints.isRegular do
+     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
     unless t.hasExprMVar || s.hasExprMVar do
       return false
   traceCtx `Meta.isDefEq.delta do
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 77af4a18c0..0f05037546 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -715,11 +715,11 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   | some nameNew => (mkMatcherConst nameNew, none)
   | none =>
     let decl := Declaration.defnDecl {
-      name        := name,
-      levelParams := result.levelParams.toList,
-      type        := result.type,
-      value       := result.value,
-      hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1),
+      name
+      levelParams := result.levelParams.toList
+      type        := result.type
+      value       := result.value
+      hints       := ReducibilityHints.abbrev
       safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
     }
     trace[Meta.debug] "{name} : {result.type} := {result.value}"
diff --git a/tests/lean/run/854.lean b/tests/lean/run/854.lean
new file mode 100644
index 0000000000..08b8d86eb2
--- /dev/null
+++ b/tests/lean/run/854.lean
@@ -0,0 +1,17 @@
+example (a : Nat) : (a - 8000) + 1 = Nat.succ (a - 8000) := by
+  rfl
+
+theorem mwe (a : Nat) : (a - 100000000) + 1 <= 1 := by
+  apply Nat.succ_le_succ
+  sorry
+
+@[irreducible]
+def someConstant : Nat := 100000000
+
+theorem mwe' (a : Nat) : (a - someConstant) + 1 <= someConstant + 1 := by
+  apply Nat.succ_le_succ
+  sorry
+
+theorem mwe'' (a : Nat) : Nat.add (a - 100000000) 1 <= Nat.zero.succ := by
+  apply Nat.succ_le_succ
+  sorry