From 3f70bc543fa6b0d3972bfc22763669f7e30efbe8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Sep 2021 12:06:15 -0700
Subject: [PATCH] feat: add `simp` conv tactic

---
 src/Lean/Elab/Tactic/Conv.lean      |  1 +
 src/Lean/Elab/Tactic/Conv/Simp.lean | 21 +++++++++++++++++++++
 src/Lean/Elab/Tactic/Simp.lean      |  2 +-
 tests/lean/run/conv1.lean           | 18 ++++++++++++++++++
 4 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 src/Lean/Elab/Tactic/Conv/Simp.lean

diff --git a/src/Lean/Elab/Tactic/Conv.lean b/src/Lean/Elab/Tactic/Conv.lean
index 3f2db6572f..8772657308 100644
--- a/src/Lean/Elab/Tactic/Conv.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Conv/Simp.lean b/src/Lean/Elab/Tactic/Conv/Simp.lean
new file mode 100644
index 0000000000..b80415786c
--- /dev/null
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index d3b9203262..71f6ce7213 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/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
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
index d8c55d041d..6715843bbc 100644
--- a/tests/lean/run/conv1.lean
+++ b/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₁