From 1e21815e417dbf7ba4cdb48b6ba5721173de37b1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Jan 2022 14:37:51 -0800
Subject: [PATCH] fix: equality theorem generation when named patterns are used

closed #945
---
 src/Lean/Meta/Match/MatchEqs.lean | 12 ++++++++++++
 tests/lean/run/945.lean           |  5 +++++
 2 files changed, 17 insertions(+)
 create mode 100644 tests/lean/run/945.lean

diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 64baad8643..282a497620 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -126,6 +126,16 @@ where
       | some (_, lhs, rhs) => simpEq lhs rhs
       | _ => throwError "failed to generate equality theorems for 'match', equality expected{indentExpr eq}"
 
+private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := withMVarContext mvarId do
+  for localDecl in (← getLCtx) do
+    if let some (_, lhs, rhs) ← matchEq? localDecl.type then
+      if lhs.isFVar then
+        if !(← dependsOn rhs lhs.fvarId!) then
+          match (← subst? mvarId lhs.fvarId!) with
+          | some mvarId => return #[mvarId]
+          | none => pure ()
+  throwError "substSomeVar failed"
+
 /--
   Helper method for proving a conditional equational theorem associated with an alternative of
   the `match`-eliminator `matchDeclName`. `type` contains the type of the theorem. -/
@@ -158,6 +168,8 @@ where
           else
             throwError "spliIf failed")
       <|>
+      (substSomeVar mvarId)
+      <|>
       (throwError "failed to generate equality theorems for `match` expression\n{MessageData.ofGoal mvarId}")
     subgoals.forM (go . (depth+1))
 
diff --git a/tests/lean/run/945.lean b/tests/lean/run/945.lean
new file mode 100644
index 0000000000..26f055711a
--- /dev/null
+++ b/tests/lean/run/945.lean
@@ -0,0 +1,5 @@
+@[simp] def iota : Nat → List Nat
+  | 0       => []
+  | m@(n+1) => m :: iota n
+
+attribute [simp] List.iota