feat: change lhs and rhs conv tactic semantics

They can now be applied to non binary applications.

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

@@ -63,15 +63,24 @@ def congr (mvarId : MVarId) : MetaM (List MVarId) :=
 @[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
    replaceMainGoal (← congr (← getMainGoal))
 
+private def selectIdx (tacticName : String) (mvarIds : List MVarId) (i : Int) : TacticM Unit := do
+  if i >= 0 then
+    let i := i.toNat
+    if h : i < mvarIds.length then
+      for mvarId in mvarIds, j in [:mvarIds.length] do
+        if i != j then
+          applyRefl mvarId
+      replaceMainGoal [mvarIds.get i h]
+      return ()
+  throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"
+
 @[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₁]
+   let mvarIds ← congr (← getMainGoal)
+   selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
 
 @[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₂]
+   let mvarIds ← congr (← getMainGoal)
+   selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
 
 @[builtinTactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
    match stx with
@@ -81,13 +90,7 @@ def congr (mvarId : MVarId) : MetaM (List MVarId) :=
         throwError "invalid 'arg' conv tactic, index must be greater than 0"
       let i := i - 1
       let mvarIds ← congr (← getMainGoal)
-      if h : i < mvarIds.length then
-        for mvarId in mvarIds, j in [:mvarIds.length] do
-          if i != j then
-            applyRefl mvarId
-        replaceMainGoal [mvarIds.get i h]
-      else
-        throwError "invalid 'arg' conv tactic, application has only {mvarIds.length} (nondependent) arguments"
+      selectIdx "arg" mvarIds i
    | _ => throwUnsupportedSyntax
 
 private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :=

tests/lean/conv1.lean

@@ -126,3 +126,28 @@ example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f
     apply Nat.zero_add
   traceState
   simp [h₁, h₂]
+
+example (x y : Nat) (h : y = 0) : x + ((y + x) + x) = x + (x + x) := by
+  conv =>
+    lhs
+    rhs
+    lhs
+    traceState
+    rw [h, Nat.zero_add]
+
+example (p : Nat → Prop) (x y : Nat) (h : y = 0) : p (y + x) := by
+  conv => lhs
+
+example (p : Nat → Prop) (x y : Nat) (h : y = 0) : p (y + x) := by
+  conv => arg 2
+
+example (p : Prop) : p := by
+  conv => rhs
+
+example (p : Nat → Prop) (x y : Nat) (h1 : y = 0) (h2 : p x) : p (y + x) := by
+  conv =>
+    rhs
+    traceState
+    rw [h1]
+    apply Nat.zero_add
+  exact h2

tests/lean/conv1.lean.expected.out

@@ -54,3 +54,15 @@ g : Nat → Nat
 h₁ : ∀ (z : Nat), f z z = z
 h₂ : ∀ (x y : Nat), f (g x) (g y) = y
 ⊢ f (g y) (f (g x) (g x)) = x
+x y : Nat
+h : y = 0
+⊢ y + x
+conv1.lean:139:10-139:13: error: invalid 'lhs' conv tactic, application has only 1 (nondependent) argument(s)
+conv1.lean:142:10-142:15: error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s)
+conv1.lean:145:10-145:13: error: invalid 'congr' conv tactic, application or implication expected
+  p
+p : Nat → Prop
+x y : Nat
+h1 : y = 0
+h2 : p x
+⊢ y + x