From e82cd9b62c96f0276825d694f4539bb9f3376b8d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Apr 2026 16:31:49 +0200 Subject: [PATCH] fix: filter assigned metavariables before computing `apply` subgoal tags (#13476) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR refines how the `apply` tactic (and related tactics like `rewrite`) name and tag the remaining subgoals. Assigned metavariables are now filtered out *before* computing subgoal tags. As a consequence, when only one unassigned subgoal remains, it inherits the tag of the input goal instead of being given a fresh suffixed tag. User-visible effect: proof states that previously displayed tags like `case h`, `case a`, or `case upper.h` for a single remaining goal now display the input goal's tag directly (e.g. no tag at all, or `case upper`). This removes noise from `funext`, `rfl`-style, and `induction`-alternative goals when the applied lemma introduces only one non-assigned metavariable. Multi-goal applications are unaffected — their subgoals continue to receive distinguishing suffixes. This may affect users whose proofs rely on the previous tag names (for example, `case h => ...` after `funext`). Such scripts need to be updated to use the input goal's tag instead. --------- Co-authored-by: Claude Opus 4.7 (1M context) --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 15 +++++++++++---- src/Lean/Meta/Tactic/Apply.lean | 2 +- src/Lean/Meta/Tactic/Rewrite.lean | 1 + tests/elab/1856.lean.out.expected | 1 - tests/elab/2042.lean | 6 ++---- tests/elab/apply_subgoal_name_issue.lean | 18 ++++++++++++++++++ tests/elab/consumePPHint.lean.out.expected | 1 - tests/elab/convInConv.lean.out.expected | 1 - tests/elab/inductionCheckAltNames.lean | 4 ++-- tests/elab/meta.lean | 1 - tests/elab/rflTacticErrors.lean | 4 ---- tests/elab_fail/conv1.lean.out.expected | 9 ++------- .../elab_fail/decreasing_by.lean.out.expected | 1 - .../inductionErrors.lean.out.expected | 4 ++-- tests/elab_fail/mutwf1.lean.out.expected | 2 -- .../server_interactive/6594.lean.out.expected | 7 +++---- 16 files changed, 42 insertions(+), 35 deletions(-) create mode 100644 tests/elab/apply_subgoal_name_issue.lean diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index ebe955d4b9..76f6656345 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -497,14 +497,21 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : /-- Searches for a metavariable `g` s.t. `tag` is its exact name. If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name. - If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/ + If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. + + We erase macro scopes from the metavariable's user name before comparing, so that + user-written tags match even when a previous tactic left hygienic macro scopes at + the end of the tag (e.g. `e_a.yield._@._internal._hyg.0`, where `yield` is not the + literal last component of the name). Case tags written by the user are never + macro-scoped, so erasing scopes on the mvar side is sufficient. +-/ private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do - match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName) with + match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName.eraseMacroScopes) with | some mvarId => return mvarId | none => - match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName) with + match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName.eraseMacroScopes) with | some mvarId => return mvarId - | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName + | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName.eraseMacroScopes private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do let gs ← getUnsolvedGoals diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index ec11dc6aa4..0b1ce93f4b 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -128,7 +128,6 @@ def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures -- TODO: default and auto params - appendParentTag mvarId newMVars binderInfos private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool := otherMVars.anyM fun otherMVar => do @@ -223,6 +222,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := let e ← instantiateMVars e mvarId.assign (mkAppN e newMVars) let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned + appendParentTag mvarId newMVars binderInfos let otherMVarIds ← getMVarsNoDelayed e let newMVarIds ← reorderGoals newMVars cfg.newGoals let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean index 01f7ac8cb9..f616c869ab 100644 --- a/src/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Rewrite.lean @@ -82,6 +82,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) postprocessAppMVars `rewrite mvarId newMVars binderInfos (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions)) let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned + appendParentTag mvarId newMVars binderInfos let otherMVarIds ← getMVarsNoDelayed heqIn let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·) let newMVarIds := newMVarIds ++ otherMVarIds diff --git a/tests/elab/1856.lean.out.expected b/tests/elab/1856.lean.out.expected index ea3e8d8318..767dbb8e55 100644 --- a/tests/elab/1856.lean.out.expected +++ b/tests/elab/1856.lean.out.expected @@ -1,4 +1,3 @@ -case h α : Type ?u inst✝ : DecidableEq α i : α diff --git a/tests/elab/2042.lean b/tests/elab/2042.lean index 849e1eaf3e..d93de4ccc9 100644 --- a/tests/elab/2042.lean +++ b/tests/elab/2042.lean @@ -2,8 +2,7 @@ 2 * a /-- -trace: case h -x : Nat +trace: x : Nat ⊢ 2 * x = x + x -/ #guard_msgs in @@ -19,8 +18,7 @@ by | a => 2 * a /-- -trace: case h -x : Nat +trace: x : Nat ⊢ 2 * x = x + x -/ #guard_msgs in diff --git a/tests/elab/apply_subgoal_name_issue.lean b/tests/elab/apply_subgoal_name_issue.lean new file mode 100644 index 0000000000..e9c430c8d2 --- /dev/null +++ b/tests/elab/apply_subgoal_name_issue.lean @@ -0,0 +1,18 @@ +/-! +Regression test: `case ` must keep working after `congr; ext _; cases _` +even though the subgoal tags produced by `apply`-family tactics now inherit +the parent tag (without appending the binder name) when only one subgoal is +left. The case-tag matcher erases macro scopes so that `case yield` still +matches tags like `e_a.yield._@._internal._hyg.0`. +-/ + +example {δ : Type} {m : Type → Type} [Monad m] [LawfulMonad m] + (x : m (ForInStep δ)) + (f g : ForInStep δ → m (ForInStep δ)) + (h : ∀ a, f a = g a) : + (x >>= f) = (x >>= g) := by + congr + ext step + cases step + case yield => apply h + case done => apply h diff --git a/tests/elab/consumePPHint.lean.out.expected b/tests/elab/consumePPHint.lean.out.expected index 60e65f9b40..256da39cf6 100644 --- a/tests/elab/consumePPHint.lean.out.expected +++ b/tests/elab/consumePPHint.lean.out.expected @@ -1,5 +1,4 @@ consumePPHint.lean:8:8-8:14: warning: declaration uses `sorry` -case a ⊢ q (have x := 0; x + 1) diff --git a/tests/elab/convInConv.lean.out.expected b/tests/elab/convInConv.lean.out.expected index d2a4e26cbc..de68ddc060 100644 --- a/tests/elab/convInConv.lean.out.expected +++ b/tests/elab/convInConv.lean.out.expected @@ -10,7 +10,6 @@ y : Nat | (fun x => x + y = 0) = fun x => False y : Nat | fun x => x + y = 0 -case h y x : Nat | y + x = 0 y : Nat diff --git a/tests/elab/inductionCheckAltNames.lean b/tests/elab/inductionCheckAltNames.lean index e2f743874d..9720c1ef16 100644 --- a/tests/elab/inductionCheckAltNames.lean +++ b/tests/elab/inductionCheckAltNames.lean @@ -10,7 +10,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat) error: Invalid alternative name `lower2`: Expected `lower` --- error: unsolved goals -case upper.h +case upper q d : Nat ⊢ q + d.succ > q --- @@ -62,7 +62,7 @@ theorem invalidWildCard (p: Nat) : p ≤ q ∨ p > q := by error: Invalid alternative name `lower2`: There are no unhandled alternatives --- error: unsolved goals -case lower.h +case lower p delta✝ : Nat ⊢ p > p + delta✝.succ -/ diff --git a/tests/elab/meta.lean b/tests/elab/meta.lean index c67bd4d548..b0f6ccbcef 100644 --- a/tests/elab/meta.lean +++ b/tests/elab/meta.lean @@ -100,7 +100,6 @@ x y : Nat h : x = y ⊢ y = x ----- -case h x y : Nat h : x = y ⊢ x = y diff --git a/tests/elab/rflTacticErrors.lean b/tests/elab/rflTacticErrors.lean index 7e3551c59b..9032605703 100644 --- a/tests/elab/rflTacticErrors.lean +++ b/tests/elab/rflTacticErrors.lean @@ -505,28 +505,24 @@ is not definitionally equal to the right-hand side example : S true false := by with_reducible apply_rfl -- Error /-- error: unsolved goals -case a ⊢ true = true -/ #guard_msgs in example : S true true := by apply_rfl -- Error (left-over goal) /-- error: unsolved goals -case a ⊢ true = true -/ #guard_msgs in example : S true true := by with_reducible apply_rfl -- Error (left-over goal) /-- error: unsolved goals -case a ⊢ false = true -/ #guard_msgs in example : S false false := by apply_rfl -- Error (left-over goal) /-- error: unsolved goals -case a ⊢ false = true -/ #guard_msgs in diff --git a/tests/elab_fail/conv1.lean.out.expected b/tests/elab_fail/conv1.lean.out.expected index d35b5c483e..b4b00e9cd2 100644 --- a/tests/elab_fail/conv1.lean.out.expected +++ b/tests/elab_fail/conv1.lean.out.expected @@ -9,14 +9,13 @@ x y : Nat case x x y : Nat ⊢ x + y = y.add x -case a a b : Nat | foo (0 + a) (b + 0) -case a.x +case x a b : Nat | 0 + a -case a.y +case y a b : Nat | b + 0 a b : Nat @@ -55,13 +54,10 @@ x y : Nat ⊢ f x (x.add y) y = y + x x y : Nat | x + y -case h.h a b : Nat | 0 + a + b -case h.h a b : Nat | a + b -case h.h a b : Nat | 0 + a + b p : Nat → Prop @@ -83,7 +79,6 @@ x : Nat p : Prop x : Nat ⊢ (True → p) → p -case h x : Nat | 0 + x p : Prop diff --git a/tests/elab_fail/decreasing_by.lean.out.expected b/tests/elab_fail/decreasing_by.lean.out.expected index af6287dc37..24ef23fc02 100644 --- a/tests/elab_fail/decreasing_by.lean.out.expected +++ b/tests/elab_fail/decreasing_by.lean.out.expected @@ -19,7 +19,6 @@ n m : Nat n m : Nat ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m) decreasing_by.lean:85:0-85:22: error: unsolved goals -case a n m : Nat ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m) diff --git a/tests/elab_fail/inductionErrors.lean.out.expected b/tests/elab_fail/inductionErrors.lean.out.expected index db63894049..3555d274c2 100644 --- a/tests/elab_fail/inductionErrors.lean.out.expected +++ b/tests/elab_fail/inductionErrors.lean.out.expected @@ -1,9 +1,9 @@ inductionErrors.lean:11:12-11:27: error: unsolved goals -case lower.h +case lower p d : Nat ⊢ p ≤ p + d.succ inductionErrors.lean:12:12-12:27: error: unsolved goals -case upper.h +case upper q d : Nat ⊢ q + d.succ > q inductionErrors.lean:16:19-16:26: error(lean.unknownIdentifier): Unknown identifier `elimEx2` diff --git a/tests/elab_fail/mutwf1.lean.out.expected b/tests/elab_fail/mutwf1.lean.out.expected index 38e10798a9..3622517c62 100644 --- a/tests/elab_fail/mutwf1.lean.out.expected +++ b/tests/elab_fail/mutwf1.lean.out.expected @@ -1,5 +1,4 @@ mutwf1.lean:21:2-21:6: error: unsolved goals -case h.a n : Nat h : n ≠ 0 ⊢ n.sub 0 ≠ 0 @@ -7,6 +6,5 @@ mutwf1.lean:31:22-31:29: error: failed to prove termination, possible solutions: - Use `have`-expressions to prove the remaining goals - Use `termination_by` to specify a different well-founded relation - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -case h n : Nat ⊢ n + 1 < n diff --git a/tests/server_interactive/6594.lean.out.expected b/tests/server_interactive/6594.lean.out.expected index d59ad74054..89ec61f4e9 100644 --- a/tests/server_interactive/6594.lean.out.expected +++ b/tests/server_interactive/6594.lean.out.expected @@ -4,12 +4,11 @@ "goals": ["case right\n⊢ True"]} {"textDocument": {"uri": "file:///6594.lean"}, "position": {"line": 9, "character": 2}} -{"rendered": "```lean\ncase a\n⊢ True ∧ True\n```", - "goals": ["case a\n⊢ True ∧ True"]} +{"rendered": "```lean\n⊢ True ∧ True\n```", "goals": ["⊢ True ∧ True"]} {"textDocument": {"uri": "file:///6594.lean"}, "position": {"line": 13, "character": 2}} -{"rendered": "```lean\ncase a.right\n⊢ True\n```", - "goals": ["case a.right\n⊢ True"]} +{"rendered": "```lean\ncase right\n⊢ True\n```", + "goals": ["case right\n⊢ True"]} {"textDocument": {"uri": "file:///6594.lean"}, "position": {"line": 20, "character": 2}} {"rendered": "```lean\ncase right\n⊢ True\n```",