From 346e3ac845ef5851bc470ae9d38e9fc6274faba8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Sep 2021 17:43:32 -0700
Subject: [PATCH] feat: add helper methods for `conv`

---
 src/Lean/Elab/Tactic/Conv/Basic.lean | 34 ++++++++++++++++++++++++----
 tests/lean/run/conv1.lean            | 10 ++++++++
 2 files changed, 40 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/conv1.lean

diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 1ec0a47bbf..97c79e3635 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -11,10 +11,7 @@ import Lean.Elab.Tactic.BuiltinTactic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
-abbrev ConvM := TacticM
-abbrev Conv  := Tactic
-
-def convert (lhs : Expr) (conv : ConvM Unit) : TacticM (Expr × Expr) := do
+def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
   let lhsType ← inferType lhs
   let rhs ← mkFreshExprMVar lhsType
   let targetNew ← mkEq lhs rhs
@@ -34,11 +31,40 @@ def convert (lhs : Expr) (conv : ConvM Unit) : TacticM (Expr × Expr) := do
     setGoals savedGoals
   return (← instantiateMVars rhs, ← instantiateMVars newGoal)
 
+def getLhsRhs : TacticM (Expr × Expr) :=
+  withMainContext do
+    let some (_, lhs, rhs) ← matchEq? (← getMainTarget) | throwError "invalid 'conv' goal"
+    return (lhs, rhs)
+
+def getLhs : TacticM Expr :=
+  return (← getLhsRhs).1
+
+def getRhs : TacticM Expr :=
+  return (← getLhsRhs).2
+
+/-- `⊢ lhs = rhs` ~~> `⊢ lhs' = rhs` using `h : lhs = lhs'`. -/
+def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do
+  let rhs ← getRhs
+  let newGoal ← mkFreshExprSyntheticOpaqueMVar (← mkEq lhs' rhs)
+  assignExprMVar (← getMainGoal) (← mkEqTrans h newGoal)
+  replaceMainGoal [newGoal.mvarId!]
+
+/-- Replace `lhs` with the definitionally equal `lhs'`. -/
+def changeLhs (lhs' : Expr) : TacticM Unit := do
+  let rhs ← getRhs
+  liftMetaTactic1 fun mvarId => do
+    replaceTargetDefEq mvarId (← mkEq lhs' rhs)
+
 @[builtinTactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun stx => do
    liftMetaTactic1 fun mvarId => do
      applyRefl mvarId
      return none
 
+@[builtinTactic Lean.Parser.Tactic.Conv.whnf] def evalWhnf : Tactic := fun stx =>
+   withMainContext do
+     let lhs ← getLhs
+     changeLhs (← whnf lhs)
+
 @[builtinTactic Lean.Parser.Tactic.Conv.convSeq1Indented] def evalConvSeq1Indented : Tactic := fun stx => do
   evalTacticSeq1Indented stx
 
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
new file mode 100644
index 0000000000..1bfa181fde
--- /dev/null
+++ b/tests/lean/run/conv1.lean
@@ -0,0 +1,10 @@
+set_option pp.analyze false
+
+def p (x y : Nat) := x = y
+
+example (x y : Nat) : p (x + y) (y + x + 0) := by
+  conv =>
+    whnf
+    skip
+  simp
+  rw [Nat.add_comm]