From e8bdb66ddaa83f93abced8dfb9ea54db73354371 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 10 Oct 2021 14:52:29 -0700
Subject: [PATCH] fix: make sure we can match pattern inside binders

This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256890867
---
 src/Lean/Elab/Tactic/Conv/Pattern.lean                 | 10 +++++++---
 tests/lean/matchPatternInsideBinders.lean              |  4 ++++
 tests/lean/matchPatternInsideBinders.lean.expected.out |  2 ++
 3 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/matchPatternInsideBinders.lean
 create mode 100644 tests/lean/matchPatternInsideBinders.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean
index a2f04da7ec..35f3e331d0 100644
--- a/src/Lean/Elab/Tactic/Conv/Pattern.lean
+++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean
@@ -21,7 +21,10 @@ private def getContext : MetaM Simp.Context := do
     config.decide := false
   }
 
-private def pre (pattern : Expr) (found? : IO.Ref (Option Expr)) (e : Expr) : SimpM Simp.Step := do
+private def pre (pattern : AbstractMVarsResult) (found? : IO.Ref (Option Expr)) (e : Expr) : SimpM Simp.Step := do
+  /- TODO: check whether the following is a performance bottleneck. If it is, recall that we used `AbstractMVarsResult` to make
+     sure we can match the pattern inside of binders. So, it is not needed in most cases. -/
+  let (_, _, pattern) ← openAbstractMVarsResult pattern
   if (← withReducible <| isDefEqGuarded pattern e) then
     let (rhs, newGoal) ← mkConvGoalFor e
     found?.set newGoal
@@ -29,7 +32,7 @@ private def pre (pattern : Expr) (found? : IO.Ref (Option Expr)) (e : Expr) : Si
   else
     return Simp.Step.visit { expr := e }
 
-private def findPattern? (pattern : Expr) (e : Expr) : MetaM (Option (MVarId × Simp.Result)) := do
+private def findPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (MVarId × Simp.Result)) := do
   let found? ← IO.mkRef none
   let result ← Simp.main e (← getContext) (methods := { pre := pre pattern found? })
   if let some newGoal ← found?.get then
@@ -41,8 +44,9 @@ private def findPattern? (pattern : Expr) (e : Expr) : MetaM (Option (MVarId ×
   match stx with
   | `(conv| pattern $p) =>
     let pattern ← Term.withoutPending <| Term.elabTerm p none
+    let patternA ← abstractMVars pattern
     let lhs ← getLhs
-    match (← findPattern? pattern lhs) with
+    match (← findPattern? patternA lhs) with
     | none => throwError "'pattern' conv tactic failed, pattern was not found{indentExpr pattern}"
     | some (mvarId', result) =>
       updateLhs result.expr (← result.getProof)
diff --git a/tests/lean/matchPatternInsideBinders.lean b/tests/lean/matchPatternInsideBinders.lean
new file mode 100644
index 0000000000..6417ada156
--- /dev/null
+++ b/tests/lean/matchPatternInsideBinders.lean
@@ -0,0 +1,4 @@
+def test : (λ x : Nat => id (id x)) = λ x => x := by
+  conv in (id _) =>
+    trace_state
+    simp
diff --git a/tests/lean/matchPatternInsideBinders.lean.expected.out b/tests/lean/matchPatternInsideBinders.lean.expected.out
new file mode 100644
index 0000000000..e5146554b9
--- /dev/null
+++ b/tests/lean/matchPatternInsideBinders.lean.expected.out
@@ -0,0 +1,2 @@
+x : Nat
+⊢ id (id x)