From 397774157f8b039204ea2e97d7a74d757bcef4e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Sep 2021 19:12:05 -0700
Subject: [PATCH] feat: nested tactic support in conv mode

---
 src/Init/Conv.lean                   |  2 +-
 src/Lean/Elab/Tactic/Conv/Basic.lean |  8 ++++++++
 src/Lean/Expr.lean                   |  4 ++++
 tests/lean/run/conv1.lean            | 13 +++++++++++++
 4 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 6ac226a601..11f5b47d06 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -31,7 +31,7 @@ syntax (name := change) "change " 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
-syntax (name := nestedTactic) "tactic " tacticSeq : conv
+syntax (name := nestedTactic) "tactic" " => " tacticSeq : conv
 syntax (name := nestedConv) convSeqBracketed : conv
 syntax (name := paren) "(" convSeq ")" : conv
 
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 254f787719..b9fad05188 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -93,6 +93,14 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 @[builtinTactic Lean.Parser.Tactic.Conv.traceState] def evalTraceState : Tactic :=
   Tactic.evalTraceState
 
+@[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
+  let seq := stx[2]
+  let target ← getMainTarget
+  if let some _ := isLHSGoal? target then
+    liftMetaTactic1 fun mvarId =>
+      replaceTargetDefEq mvarId target.mdataExpr!
+  focus <| evalTactic seq
+
 private def convTarget (conv : Syntax) : TacticM Unit := do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (evalTactic conv)
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index f673f9d319..30d003f2b8 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -598,6 +598,10 @@ def consumeMData : Expr → Expr
   | mdata _ e _ => consumeMData e
   | e           => e
 
+def mdataExpr! : Expr → Expr
+  | mdata _ e _ => e
+  | _           => panic! "mdata expression expected"
+
 def hasLooseBVars (e : Expr) : Bool :=
   e.looseBVarRange > 0
 
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
index 6b8d493486..a27780bead 100644
--- a/tests/lean/run/conv1.lean
+++ b/tests/lean/run/conv1.lean
@@ -41,3 +41,16 @@ example (x y : Nat) : p (x + y) (0 + y + x) := by
     skip
     done
   rfl
+
+axiom div_self (x : Nat) : x ≠ 0 → x / x = 1
+
+example (h : x ≠ 0) : x / x + x = x.succ := by
+  conv =>
+    lhs
+    arg 2
+    rw [div_self]
+    skip
+    tactic => assumption
+    done
+  show 1 + x = x.succ
+  rw [Nat.succ_add, Nat.zero_add]