From 5a751d468813d141a1b6be4be96e1a18e6a84c20 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 7 Oct 2025 17:38:34 +0200
Subject: [PATCH] fix: induction: do not allow generalizing variables occurring
 in the `using` clause (#10697)

This PR lets `induction` print a warning if a variable occurring in the
`using` clause is generalized. Fixes #10683.
---
 src/Lean/Elab/Tactic/Induction.lean | 13 ++++++++-----
 tests/lean/run/issue10683.lean      | 20 ++++++++++++++++++++
 2 files changed, 28 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/issue10683.lean

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 8ff28e41d2..688036470c 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -586,14 +586,17 @@ private def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :
       getFVarIds vars
 
 -- process `generalizingVars` subterm of induction Syntax `stx`.
-private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) : TacticM (Array FVarId × MVarId) :=
+private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) (elimExpr : Expr) : TacticM (Array FVarId × MVarId) :=
   mvarId.withContext do
     let userFVarIds ← getUserGeneralizingFVarIds stx
-    let forbidden ← mkGeneralizationForbiddenSet targets
-    let mut s ← getFVarSetToGeneralize targets forbidden
+    let forbidden1 ← mkGeneralizationForbiddenSet targets
+    let forbidden2 ← mkGeneralizationForbiddenSet #[elimExpr]
+    let mut s ← getFVarSetToGeneralize targets (forbidden1.union forbidden2)
     for userFVarId in userFVarIds do
-      if forbidden.contains userFVarId then
+      if forbidden1.contains userFVarId then
         throwError "Variable `{mkFVar userFVarId}` cannot be generalized because the induction target depends on it"
+      if forbidden2.contains userFVarId then
+        throwError "Variable `{mkFVar userFVarId}` cannot be generalized because the induction principle depends on it"
       if s.contains userFVarId then
         throwOrLogError m!"Unnecessary `generalizing` argument: Variable `{mkFVar userFVarId}` is generalized automatically"
       s := s.insert userFVarId
@@ -947,7 +950,7 @@ private def evalInductionCore (stx : Syntax) (elimInfo : ElimInfo) (targets : Ar
   mvarId.withContext do
     checkInductionTargets targets
     let targetFVarIds := targets.map (·.fvarId!)
-    let (generalized, mvarId) ← generalizeVars mvarId stx targets
+    let (generalized, mvarId) ← generalizeVars mvarId stx targets elimInfo.elimExpr
     mvarId.withContext do
       let result ← withRef stx[1] do -- use target position as reference
         ElimApp.mkElimApp elimInfo targets tag
diff --git a/tests/lean/run/issue10683.lean b/tests/lean/run/issue10683.lean
new file mode 100644
index 0000000000..f0eb5d1107
--- /dev/null
+++ b/tests/lean/run/issue10683.lean
@@ -0,0 +1,20 @@
+def orderedInsert (a : Nat) : List Nat → List Nat
+  | [] => [a]
+  | b :: l => if a < b then a :: b :: l else b :: orderedInsert a l
+
+/-- error: Variable `x` cannot be generalized because the induction principle depends on it -/
+#guard_msgs in
+example : orderedInsert  x l = [] := by
+  induction l using orderedInsert.induct_unfolding (a := x) generalizing x
+
+/-- error: Variable `x` cannot be generalized because the induction principle depends on it -/
+#guard_msgs in
+example : orderedInsert  x l = [] := by
+  fun_induction orderedInsert generalizing x
+
+axiom foo_induct (n : Nat) {motive : Nat → Prop} (h : ∀ m, n = m): ∀ m, motive m
+
+/-- error: Variable `n` cannot be generalized because the induction principle depends on it -/
+#guard_msgs in
+example (n m : Nat) : n = m := by
+  induction m using foo_induct (n := n) generalizing n