feat: lhs and rhs conv tactics

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

@@ -11,7 +11,7 @@ import Lean.Elab.Tactic.BuiltinTactic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
-def mkConvGoalFor (lhs : Expr) : TacticM (Expr × Expr) := do
+def mkConvGoalFor (lhs : Expr) : MetaM (Expr × Expr) := do
   let lhsType ← inferType lhs
   let rhs ← mkFreshExprMVar lhsType
   let targetNew ← mkEq lhs rhs
@@ -35,11 +35,14 @@ def convert (lhs : Expr) (conv : TacticM 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"
+def getLhsRhsCore (mvarId : MVarId) : MetaM (Expr × Expr) :=
+  withMVarContext mvarId do
+    let some (_, lhs, rhs) ← matchEq? (← getMVarType mvarId) | throwError "invalid 'conv' goal"
     return (lhs, rhs)
 
+def getLhsRhs : TacticM (Expr × Expr) := do
+  getLhsRhsCore (← getMainGoal)
+
 def getLhs : TacticM Expr :=
   return (← getLhsRhs).1
 

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

@@ -9,9 +9,9 @@ import Lean.Elab.Tactic.Conv.Basic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
-@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
-   withMainContext do
-     let (lhs, rhs) ← getLhsRhs
+def congr (mvarId : MVarId) : MetaM (List MVarId) :=
+  withMVarContext mvarId do
+     let (lhs, rhs) ← getLhsRhsCore mvarId
      unless lhs.isApp do
        throwError "invalid 'congr' conv tactic, application expected{indentD lhs}"
      lhs.withApp fun f args => do
@@ -35,7 +35,21 @@ open Meta
         i := i + 1
       let proof ← r.getProof
       assignExprMVar rhs.mvarId! r.expr
-      assignExprMVar (← getMainGoal) proof
-      replaceMainGoal newGoals.toList
+      assignExprMVar mvarId proof
+      return newGoals.toList
+
+
+@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
+   replaceMainGoal (← congr (← getMainGoal))
+
+@[builtinTactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun stx => do
+   let [mvarId₁, mvarId₂] ← congr (← getMainGoal) | throwError "invalid 'lhs' conv tactic, binary application expected"
+   applyRefl mvarId₂
+   replaceMainGoal [mvarId₁]
+
+@[builtinTactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun stx => do
+   let [mvarId₁, mvarId₂] ← congr (← getMainGoal) | throwError "invalid 'rhs' conv tactic, binary application expected"
+   applyRefl mvarId₁
+   replaceMainGoal [mvarId₂]
 
 end Lean.Elab.Tactic.Conv

tests/lean/conv1.lean

@@ -0,0 +1,33 @@
+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
+    congr
+    . skip
+    . whnf; skip
+  traceState
+  rw [Nat.add_comm]
+  rfl
+
+example (x y : Nat) : p (x + y) (y + x + 0) := by
+  conv =>
+    whnf
+    rhs
+    whnf
+  traceState
+  rw [Nat.add_comm]
+  rfl
+
+example (x y : Nat) : p (x + y) (y + x + 0) := by
+  conv =>
+    whnf
+    lhs
+    whnf
+  conv =>
+    rhs
+    whnf
+  traceState
+  apply Nat.add_comm x y

tests/lean/conv1.lean.expected.out

@@ -0,0 +1,6 @@
+x y : Nat
+⊢ x + y = Nat.add y x
+x y : Nat
+⊢ x + y = Nat.add y x
+x y : Nat
+⊢ Nat.add x y = Nat.add y x

tests/lean/run/conv1.lean

@@ -11,3 +11,23 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
   traceState
   rw [Nat.add_comm]
   rfl
+
+example (x y : Nat) : p (x + y) (y + x + 0) := by
+  conv =>
+    whnf
+    rhs
+    whnf
+  traceState
+  rw [Nat.add_comm]
+  rfl
+
+example (x y : Nat) : p (x + y) (y + x + 0) := by
+  conv =>
+    whnf
+    lhs
+    whnf
+  conv =>
+    rhs
+    whnf
+  traceState
+  apply Nat.add_comm x y