From 41cfef5bc46b2ea4f7c99ac0e92dc84ae798c2dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 4 Sep 2021 18:02:46 -0700
Subject: [PATCH] feat: add `pattern` conv tactic

---
 src/Lean/Elab/Tactic/Conv.lean         |  1 +
 src/Lean/Elab/Tactic/Conv/Pattern.lean | 53 ++++++++++++++++++++++++++
 src/Lean/Elab/Term.lean                | 11 ++++++
 tests/lean/conv1.lean                  | 11 ++++++
 tests/lean/conv1.lean.expected.out     | 12 ++++++
 5 files changed, 88 insertions(+)
 create mode 100644 src/Lean/Elab/Tactic/Conv/Pattern.lean

diff --git a/src/Lean/Elab/Tactic/Conv.lean b/src/Lean/Elab/Tactic/Conv.lean
index 8772657308..637998311e 100644
--- a/src/Lean/Elab/Tactic/Conv.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean
new file mode 100644
index 0000000000..a2f04da7ec
--- /dev/null
+++ b/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
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index d42a35c62e..624ae3ee98 100644
--- a/src/Lean/Elab/Term.lean
+++ b/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
diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean
index 707f310cf8..62b98f629f 100644
--- a/tests/lean/conv1.lean
+++ b/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₂]
diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out
index 91fb6320e3..72436d2a27 100644
--- a/tests/lean/conv1.lean.expected.out
+++ b/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