feat: add pattern conv tactic

src/Lean/Elab/Tactic/Conv.lean

@@ -8,3 +8,4 @@ import Lean.Elab.Tactic.Conv.Congr
 import Lean.Elab.Tactic.Conv.Rewrite
 import Lean.Elab.Tactic.Conv.Change
 import Lean.Elab.Tactic.Conv.Simp
+import Lean.Elab.Tactic.Conv.Pattern

src/Lean/Elab/Tactic/Conv/Pattern.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Tactic.Simp
+import Lean.Elab.Tactic.Conv.Basic
+
+namespace Lean.Elab.Tactic.Conv
+open Meta
+
+private def getContext : MetaM Simp.Context := do
+  return {
+    simpLemmas    := {}
+    congrLemmas   := (← getCongrLemmas)
+    config.zeta   := false
+    config.beta   := false
+    config.eta    := false
+    config.iota   := false
+    config.proj   := false
+    config.decide := false
+  }
+
+private def pre (pattern : Expr) (found? : IO.Ref (Option Expr)) (e : Expr) : SimpM Simp.Step := do
+  if (← withReducible <| isDefEqGuarded pattern e) then
+    let (rhs, newGoal) ← mkConvGoalFor e
+    found?.set newGoal
+    return Simp.Step.done { expr := rhs, proof? := newGoal }
+  else
+    return Simp.Step.visit { expr := e }
+
+private def findPattern? (pattern : Expr) (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
+    return some (newGoal.mvarId!, result)
+  else
+    return none
+
+@[builtinTactic Lean.Parser.Tactic.Conv.pattern] def evalPattern : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| pattern $p) =>
+    let pattern ← Term.withoutPending <| Term.elabTerm p none
+    let lhs ← getLhs
+    match (← findPattern? pattern lhs) with
+    | none => throwError "'pattern' conv tactic failed, pattern was not found{indentExpr pattern}"
+    | some (mvarId', result) =>
+      updateLhs result.expr (← result.getProof)
+      applyRefl (← getMainGoal)
+      replaceMainGoal [mvarId']
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic.Conv

src/Lean/Elab/Term.lean

@@ -1254,6 +1254,17 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPo
   let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
   withRef stx <| ensureHasType expectedType? e errorMsgHeader?
 
+/--
+  Execute `x` and then restore `syntheticMVars`, `levelNames`, `mvarErrorInfos`, and `letRecsToLift`.
+  We use this combinator when we don't want the pending problems created by `x` to persist after its execution. -/
+def withoutPending (x : TermElabM α) : TermElabM α := do
+  let saved ← get
+  try
+    x
+  finally
+    modify fun s => { s with syntheticMVars := saved.syntheticMVars, levelNames := saved.levelNames,
+                             letRecsToLift := saved.letRecsToLift, mvarErrorInfos := saved.mvarErrorInfos }
+
 /-- Execute `x` and return `some` if no new errors were recorded or exceptions was thrown. Otherwise, return `none` -/
 def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do
   let saved ← saveState

tests/lean/conv1.lean

@@ -115,3 +115,14 @@ example (p : Prop) (x : Nat) : (x = x → p) → p := by
     lhs
     simp
   intros; assumption
+
+example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f z z = z) (h₂ : ∀ x y, f (g x) (g y) = y) : f (g (0 + y)) (f (g x) (g (0 + x))) = x := by
+  conv =>
+    pattern _ + _
+    apply Nat.zero_add
+  traceState
+  conv =>
+    pattern 0 + _
+    apply Nat.zero_add
+  traceState
+  simp [h₁, h₂]

tests/lean/conv1.lean.expected.out

@@ -42,3 +42,15 @@ x : Nat
 p : Prop
 x : Nat
 ⊢ (True → p) → p
+x y : Nat
+f : Nat → Nat → Nat
+g : Nat → Nat
+h₁ : ∀ (z : Nat), f z z = z
+h₂ : ∀ (x y : Nat), f (g x) (g y) = y
+⊢ f (g y) (f (g x) (g (0 + x))) = x
+x y : Nat
+f : Nat → Nat → Nat
+g : Nat → Nat
+h₁ : ∀ (z : Nat), f z z = z
+h₂ : ∀ (x y : Nat), f (g x) (g y) = y
+⊢ f (g y) (f (g x) (g x)) = x