max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: induction: do not allow generalizing variables occurring in the using clause (#10697)

Browse source 
This PR lets `induction` print a warning if a variable occurring in the
`using` clause is generalized. Fixes #10683.
This commit is contained in:
Joachim Breitner 2025-10-07 17:38:34 +02:00 • committed by GitHub
parent 486d93c5fd
commit 5a751d4688
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 28 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Elab/Tactic/Induction.lean
View file

@ -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

20
tests/lean/run/issue10683.lean Normal file
View file

@ -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