From 94bc386fb48e618c918982a35cf17088ea88fc71 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Sep 2021 19:52:51 -0700
Subject: [PATCH] feat: remark goals as conv goals at the end of nested tactic
 block

---
 src/Lean/Elab/Tactic/Conv/Basic.lean | 17 +++++++++++++++--
 tests/lean/conv1.lean                |  7 +++++++
 tests/lean/conv1.lean.expected.out   |  3 +++
 3 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 132c7acd15..04e529c5f9 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -93,9 +93,22 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 @[builtinTactic Lean.Parser.Tactic.Conv.paren] def evalParen : Tactic := fun stx =>
   evalTactic stx[1]
 
+/-- Mark goals of the form `⊢ a = ?m ..` with the conv goal annotation -/
+def remarkAsConvGoal : TacticM Unit := do
+  let newGoals ← (← getGoals).mapM fun mvarId => withMVarContext mvarId do
+    let target ← getMVarType mvarId
+    if let some (_, lhs, rhs) ← matchEq? target then
+      if rhs.getAppFn.isMVar then
+        replaceTargetDefEq mvarId (mkLHSGoal target)
+      else
+        return mvarId
+    else
+      return mvarId
+  setGoals newGoals
+
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedTacticCore] def evalNestedTacticCore : Tactic := fun stx => do
   let seq := stx[2]
-  focus <| evalTactic seq
+  focus do evalTactic seq; remarkAsConvGoal
 
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
   let seq := stx[2]
@@ -103,7 +116,7 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
   if let some _ := isLHSGoal? target then
     liftMetaTactic1 fun mvarId =>
       replaceTargetDefEq mvarId target.mdataExpr!
-  focus <| evalTactic seq
+  focus do evalTactic seq; remarkAsConvGoal
 
 private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do
    let target ← getMainTarget
diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean
index 2360344419..baed1bf7cb 100644
--- a/tests/lean/conv1.lean
+++ b/tests/lean/conv1.lean
@@ -97,3 +97,10 @@ example (p : Prop) (x : Nat) : (x = x → p) → p := by
     simp
   intros
   assumption
+
+example : (fun x => 0 + x) = id := by
+  conv =>
+    lhs
+    tactic => funext x
+    traceState
+    rw [Nat.zero_add]
diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out
index 102b109d33..cbfc126d96 100644
--- a/tests/lean/conv1.lean.expected.out
+++ b/tests/lean/conv1.lean.expected.out
@@ -36,3 +36,6 @@ x : Nat
 p : Prop
 x : Nat
 ⊢ (True → p) → p
+case h
+x : Nat
+⊢ 0 + x