From 7acbbb4fbb264288f2aa91c31e9cae7af9ec10b8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Jan 2022 09:57:41 -0800
Subject: [PATCH] fix: auxiliary `whnfAux` used at `mkEqns`

---
 src/Lean/Elab/PreDefinition/Eqns.lean |  9 +++++----
 tests/lean/run/eqnsAtSimp3.lean       | 19 +++++++++++++++++++
 2 files changed, 24 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/eqnsAtSimp3.lean

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index cad43e8be4..05bdba6ba3 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -132,10 +132,11 @@ def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := wit
   replaceTargetDefEq mvarId (← mkEq lhs rhs)
 
 private partial def whnfAux (e : Expr) : MetaM Expr := do
-  let e ← whnfR e
-  match e with
-  | Expr.proj _ _ s _ => e.updateProj! (← whnfAux s)
-  | _ => e
+  let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
+  let f := e.getAppFn
+  match f with
+  | Expr.proj _ _ s _ => mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
+  | _ => return e
 
 /-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
 def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do
diff --git a/tests/lean/run/eqnsAtSimp3.lean b/tests/lean/run/eqnsAtSimp3.lean
new file mode 100644
index 0000000000..6e30c845eb
--- /dev/null
+++ b/tests/lean/run/eqnsAtSimp3.lean
@@ -0,0 +1,19 @@
+import Lean
+
+open Lean
+open Lean.Meta
+def tst (declName : Name) : MetaM Unit := do
+  IO.println (← getEqnsFor? declName)
+
+def f (x y : Nat) : Nat :=
+  match x, y with
+  | 0,   0 => 1
+  | 0,   y => y
+  | x+1, 5 => 2 * f x 0
+  | x+1, y => 2 * f x y
+
+#eval tst ``f
+#check f._eq_1
+#check f._eq_2
+#check f._eq_3
+#check f._eq_4