feat: add apply conv macro

src/Init/Conv.lean

@@ -31,7 +31,7 @@ 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. -/
+/-- Focus, 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,8 +52,9 @@ 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 "skip" : conv => `(tactic => rfl)
 macro "done" : conv => `(tactic' => done)
 macro "traceState" : conv => `(tactic' => traceState)
+macro "apply " e:term : conv => `(tactic => apply $e)
 
 end Lean.Parser.Tactic.Conv

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -30,12 +30,14 @@ def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
   try
     setGoals [newGoal.mvarId!]
     conv
-    pruneSolvedGoals
     for mvarId in (← getGoals) do
       try
         applyRefl mvarId
       catch _ =>
-        throwError "convert tactic failed, there are unsolved goal"
+        pure ()
+    pruneSolvedGoals
+    unless (← getGoals).isEmpty do
+      throwError "convert tactic failed, there are unsolved goals\n{goalsToMessageData (← getGoals)}"
     pure ()
   finally
     setGoals savedGoals
@@ -95,7 +97,7 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 
 /-- 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 newGoals ← (← getUnsolvedGoals).mapM fun mvarId => withMVarContext mvarId do
     let target ← getMVarType mvarId
     if let some (_, lhs, rhs) ← matchEq? target then
       if rhs.getAppFn.isMVar then
@@ -108,7 +110,7 @@ def remarkAsConvGoal : TacticM Unit := do
 
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedTacticCore] def evalNestedTacticCore : Tactic := fun stx => do
   let seq := stx[2]
-  focus do evalTactic seq; remarkAsConvGoal
+  evalTactic seq; remarkAsConvGoal
 
 @[builtinTactic Lean.Parser.Tactic.Conv.nestedTactic] def evalNestedTactic : Tactic := fun stx => do
   let seq := stx[2]

tests/lean/conv1.lean

@@ -104,3 +104,14 @@ example : (fun x => 0 + x) = id := by
     tactic => funext x
     traceState
     rw [Nat.zero_add]
+
+example (p : Prop) (x : Nat) : (x = x → p) → p := by
+  conv =>
+    apply implies_congr
+    . apply implies_congr
+      simp
+  traceState
+  conv =>
+    lhs
+    simp
+  intros; assumption

tests/lean/conv1.lean.expected.out

@@ -39,3 +39,6 @@ x : Nat
 case h
 x : Nat
 ⊢ 0 + x
+p : Prop
+x : Nat
+⊢ (True → p) → p