feat: allow conv mode's arg command to access implicit arguments

src/Init/Conv.lean

@@ -26,7 +26,7 @@ syntax (name := whnf) "whnf" : conv
 /-- Put term in normal form, this tactic is ment for debugging purposes only -/
 syntax (name := reduce) "reduce" : conv
 syntax (name := congr) "congr" : conv
-syntax (name := arg) "arg " num : conv
+syntax (name := arg) "arg " "@"? num : conv
 syntax (name := ext) "ext " (colGt ident)* : conv
 syntax (name := change) "change " term : conv
 syntax (name := delta) "delta " ident : conv
@@ -54,10 +54,11 @@ macro "left" : conv => `(lhs)
 macro "right" : conv => `(rhs)
 macro "intro " xs:(colGt ident)* : conv => `(ext $xs*)
 
-syntax enterArg := ident <|> num
+syntax enterArg := ident <|> group("@"? num)
 syntax "enter " "[" (colGt enterArg),+ "]": conv
 macro_rules
   | `(conv| enter [$i:num]) => `(conv| arg $i)
+  | `(conv| enter [@$i:num]) => `(conv| arg @$i)
   | `(conv| enter [$id:ident]) => `(conv| ext $id)
   | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
 

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

@@ -11,7 +11,8 @@ open Meta
 
 /-- Returns a list of new congruence subgoals, which contains `none` for each argument with
 forward dependencies. -/
-private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MVarId)) :=
+private def congrApp (mvarId : MVarId) (lhs rhs : Expr) (addImplicitArgs := false) :
+   MetaM (List (Option MVarId)) :=
   -- TODO: add support for `[congr]` lemmas
   lhs.withApp fun f args => do
     let infos := (← getFunInfoNArgs f args.size).paramInfo
@@ -19,10 +20,11 @@ private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MV
     let mut newGoals : Array (Option MVarId) := #[]
     let mut i := 0
     for arg in args do
-      let addGoal ← if i < infos.size then
-        pure infos[i].binderInfo.isExplicit
-      else
-        pure (← whnfD (← inferType r.expr)).isArrow
+      let addGoal ←
+        if i < infos.size then
+          pure (addImplicitArgs || infos[i].binderInfo.isExplicit)
+        else
+          pure (← whnfD (← inferType r.expr)).isArrow
       let hasFwdDep := i < infos.size && infos[i].hasFwdDeps
       if addGoal then
         if hasFwdDep then
@@ -54,14 +56,14 @@ def isImplies (e : Expr) : MetaM Bool :=
   else
     return false
 
-def congr (mvarId : MVarId) : MetaM (List (Option MVarId)) :=
+def congr (mvarId : MVarId) (addImplicitArgs := false) : MetaM (List (Option MVarId)) :=
   withMVarContext mvarId do
     let (lhs, rhs) ← getLhsRhsCore mvarId
     let lhs := (← instantiateMVars lhs).consumeMData
     if (← isImplies lhs) then
       return (← congrImplies mvarId).map Option.some
     else if lhs.isApp then
-      congrApp mvarId lhs rhs
+      congrApp mvarId lhs rhs addImplicitArgs
     else
       throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
 
@@ -95,12 +97,12 @@ private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i
 
 @[builtinTactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
    match stx with
-   | `(conv| arg $i) =>
+   | `(conv| arg $[@%$tk?]? $i:num) =>
       let i := i.isNatLit?.getD 0
       if i == 0 then
         throwError "invalid 'arg' conv tactic, index must be greater than 0"
       let i := i - 1
-      let mvarIds ← congr (← getMainGoal)
+      let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome)
       selectIdx "arg" mvarIds i
    | _ => throwUnsupportedSyntax
 

tests/lean/conv1.lean

@@ -150,6 +150,18 @@ example (p : (n : Nat) → Fin n → Prop) (i : Fin 5) (hp : p 5 i) (hi : j = i)
     rw [hi]
   exact hp
 
+example (p : {_ : Nat} → Nat → Prop) (x y : Nat) (h1 : y = 0) (h2 : @p x x) : @p (y + x) (y + x) := by
+  conv =>
+    enter [@1, 1]
+    trace_state
+    rw [h1]
+  conv =>
+    enter [@2, 1]
+    trace_state
+    rw [h1]
+  rw [Nat.zero_add]
+  exact h2
+
 example (p : Nat → Prop) (x y : Nat) (h : y = 0) : p (y + x) := by
   conv => lhs
 

tests/lean/conv1.lean.expected.out

@@ -68,8 +68,18 @@ i : Fin 5
 hp : p 5 i
 hi : j = i
 | j
-conv1.lean:154:10-154:13: error: invalid 'lhs' conv tactic, application has only 1 (nondependent) argument(s)
-conv1.lean:157:10-157:15: error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s)
-conv1.lean:160:10-160:13: error: invalid 'congr' conv tactic, application or implication expected
+p : {x : Nat} → Nat → Prop
+x y : Nat
+h1 : y = 0
+h2 : p x
+| y
+p : {x : Nat} → Nat → Prop
+x y : Nat
+h1 : y = 0
+h2 : p x
+| y
+conv1.lean:166:10-166:13: error: invalid 'lhs' conv tactic, application has only 1 (nondependent) argument(s)
+conv1.lean:169:10-169:15: error: invalid 'arg' conv tactic, application has only 1 (nondependent) argument(s)
+conv1.lean:172:10-172:13: error: invalid 'congr' conv tactic, application or implication expected
   p
-conv1.lean:163:10-163:15: error: cannot select argument with forward dependencies
+conv1.lean:175:10-175:15: error: cannot select argument with forward dependencies