feat: add simp conv tactic

src/Lean/Elab/Tactic/Conv.lean

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

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

@@ -0,0 +1,21 @@
+/-
+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
+
+@[builtinTactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => do
+  let { ctx, .. } ← mkSimpContext stx (eraseLocal := false)
+  let lhs ← getLhs
+  let result ← simp lhs ctx
+  if result.proof?.isNone then
+    changeLhs result.expr
+  else
+    updateLhs result.expr (← result.getProof)
+
+end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Simp.lean

@@ -137,7 +137,7 @@ structure MkSimpContextResult where
   fvarIdToLemmaId : FVarIdToLemmaId
 
 --  If `ctx == false`, the argument is assumed to have type `Meta.Simp.Config`, and `Meta.Simp.ConfigCtx` otherwise. -/
-private def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
+def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (ctx := false) (ignoreStarArg : Bool := false) : TacticM MkSimpContextResult := do
   let simpOnly := !stx[2].isNone
   let simpLemmas ←
     if simpOnly then

tests/lean/run/conv1.lean

@@ -68,3 +68,21 @@ example : id (fun x => 0 + x) = id := by
     arg 1
     funext y
     rw [Nat.zero_add]
+
+def f (x : Nat) :=
+  if x > 0 then
+    x + 1
+  else
+    x + 2
+
+example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by
+  conv =>
+    rhs
+    simp [f, h₂]
+  exact h₁
+
+example (h₁ : f x = x + 1) (h₂ : x > 0) : f x = f x := by
+  conv =>
+    rhs
+    simp [f, h₂]
+  exact h₁