From de455a90100e71fd3aba09f29b6284bd581ee197 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Sep 2021 19:41:39 -0700
Subject: [PATCH] chore: add `tactic' => ...` which preserves the conv goal
 annotation

---
 src/Init/Conv.lean                   | 10 +++++++---
 src/Lean/Elab/Tactic/Conv/Basic.lean | 13 +++----------
 2 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 3831014c30..a8f07a6156 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -18,20 +18,20 @@ syntax convSeq := convSeq1Indented <|> convSeqBracketed
 
 syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
 
-syntax (name := skip) "skip" : conv
-syntax (name := done) "done" : conv
 syntax (name := lhs) "lhs" : conv
 syntax (name := rhs) "rhs" : conv
 syntax (name := whnf) "whnf" : conv
 syntax (name := congr) "congr" : conv
 syntax (name := arg) "arg " num : conv
-syntax (name := traceState) "traceState" : conv
 syntax (name := ext) "ext " (colGt ident)* : conv
 syntax (name := change) "change " term : conv
 syntax (name := pattern) "pattern " term : conv
 syntax (name := rewrite) "rewrite " rwRuleSeq : conv
 syntax (name := erewrite) "erewrite " rwRuleSeq : conv
 syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
+/-- Execute the given tactic block without converting `conv` goal into a regular goal -/
+syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
+/-- Convert the `conv` goal `⊢ lhs` into a regular goal `⊢ lhs = rhs`, and then execute the given tactic block. -/
 syntax (name := nestedTactic) "tactic" " => " tacticSeq : conv
 syntax (name := nestedConv) convSeqBracketed : conv
 syntax (name := paren) "(" convSeq ")" : conv
@@ -52,4 +52,8 @@ macro_rules
   | `(conv| enter [$id:ident]) => `(conv| ext $id)
   | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
 
+macro "skip" : conv => `(tactic' => rfl)
+macro "done" : conv => `(tactic' => done)
+macro "traceState" : conv => `(tactic' => traceState)
+
 end Lean.Parser.Tactic.Conv
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index f4e2a34691..132c7acd15 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -68,11 +68,6 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
   liftMetaTactic1 fun mvarId => do
     replaceTargetDefEq mvarId (mkLHSGoal (← 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
@@ -98,11 +93,9 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 @[builtinTactic Lean.Parser.Tactic.Conv.paren] def evalParen : Tactic := fun stx =>
   evalTactic stx[1]
 
-@[builtinTactic Lean.Parser.Tactic.Conv.done] def evalDone : Tactic := fun _ =>
-  done
-
-@[builtinTactic Lean.Parser.Tactic.Conv.traceState] def evalTraceState : Tactic :=
-  Tactic.evalTraceState
+@[builtinTactic Lean.Parser.Tactic.Conv.nestedTacticCore] def evalNestedTacticCore : Tactic := fun stx => do
+  let seq := stx[2]
+  focus <| evalTactic seq
 
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
   let seq := stx[2]