From 6c9a3b9fc64b06387af80e4c59d665170e8c4a96 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 30 Mar 2026 10:40:03 +0000 Subject: [PATCH 1/4] feat(Tactic/Linter): add `auxLemma` linter for auto-generated declaration references Add a syntax linter that flags explicit references to auto-generated auxiliary declarations such as `_proof_N`, `match_N`, `_match_N`, and `_sizeOf_N`. These names are internal to the Lean elaborator and are not stable across refactors. Co-Authored-By: Claude Opus 4.6 (1M context) --- Mathlib.lean | 1 + Mathlib/Init.lean | 2 + Mathlib/Tactic.lean | 1 + Mathlib/Tactic/Linter/AuxLemma.lean | 71 +++++++++++++++++++++++++++++ 4 files changed, 75 insertions(+) create mode 100644 Mathlib/Tactic/Linter/AuxLemma.lean diff --git a/Mathlib.lean b/Mathlib.lean index 5bd4bef36f0368..503f734043c67b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7081,6 +7081,7 @@ public import Mathlib.Tactic.LinearCombination public import Mathlib.Tactic.LinearCombination' public import Mathlib.Tactic.LinearCombination.Lemmas public import Mathlib.Tactic.Linter +public import Mathlib.Tactic.Linter.AuxLemma public import Mathlib.Tactic.Linter.CommandRanges public import Mathlib.Tactic.Linter.CommandStart public import Mathlib.Tactic.Linter.DeprecatedModule diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index 939c4d13159223..b62cfcba098b60 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -4,6 +4,7 @@ public import Lean.Linter.Sets -- for the definition of linter sets public import Lean.LibrarySuggestions.Default -- for `+suggestions` modes in tactics public import Mathlib.Lean.Linter -- linter utilities; will be transitively imported in #31134 public import Mathlib.Tactic.Lemma +public import Mathlib.Tactic.Linter.AuxLemma public import Mathlib.Tactic.Linter.DeprecatedSyntaxLinter public import Mathlib.Tactic.Linter.DirectoryDependency public import Mathlib.Tactic.Linter.DocPrime @@ -82,6 +83,7 @@ all these linters, or add the `weak.linter.mathlibStandardSet` option to their l register_linter_set linter.mathlibStandardSet := -- linter.allScriptsDocumented -- disabled, let's not impose this requirement downstream. -- linter.checkInitImports -- disabled, not relevant downstream. + linter.style.auxLemma linter.flexible linter.hashCommand linter.oldObtain diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 3264322c33fed9..3aebf5e7a772b1 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -158,6 +158,7 @@ public import Mathlib.Tactic.LinearCombination public import Mathlib.Tactic.LinearCombination' public import Mathlib.Tactic.LinearCombination.Lemmas public import Mathlib.Tactic.Linter +public import Mathlib.Tactic.Linter.AuxLemma public import Mathlib.Tactic.Linter.CommandRanges public import Mathlib.Tactic.Linter.CommandStart public import Mathlib.Tactic.Linter.DeprecatedModule diff --git a/Mathlib/Tactic/Linter/AuxLemma.lean b/Mathlib/Tactic/Linter/AuxLemma.lean new file mode 100644 index 00000000000000..e063092db0b02b --- /dev/null +++ b/Mathlib/Tactic/Linter/AuxLemma.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Kim Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +module + +public meta import Lean.Elab.Command +public meta import Mathlib.Tactic.Linter.Header -- shake: keep + +/-! +# The `auxLemma` linter + +The `auxLemma` linter flags explicit references to auto-generated "auxiliary" declarations +such as `_proof_1`, `_match_1`, or `_sizeOf_1`. + +## Why is this bad? + +These names are internal implementation details generated by the Lean elaborator. +They are not stable across refactors (e.g. reordering fields in a structure can renumber +`_proof_` indices), so depending on them makes code fragile. +-/ + +meta section + +open Lean Elab Linter + +namespace Mathlib.Linter.Style + +/-- Returns `true` if `s` has the form `pfx ++ digits`, e.g. `"_proof_17"`. -/ +private def matchesAuxPattern (pfx : String) (s : String) : Bool := + s.startsWith pfx && (s.drop pfx.length).all (·.isDigit) && s.length > pfx.length + +/-- Returns `true` if `s` is an auto-generated auxiliary name component, +such as `_proof_1`, `match_2`, or `_sizeOf_3`. -/ +private def isAuxName (s : String) : Bool := + matchesAuxPattern "_proof_" s || + matchesAuxPattern "match_" s || + matchesAuxPattern "_match_" s || + matchesAuxPattern "_sizeOf_" s + +/-- Returns `true` if any component of `nm` is an auto-generated auxiliary name. -/ +private def nameRefersToAuxLemma : Name → Bool + | .str p s => isAuxName s || nameRefersToAuxLemma p + | .num p _ => nameRefersToAuxLemma p + | .anonymous => false + +/-- The `auxLemma` linter emits a warning on any explicit reference to an auto-generated +auxiliary declaration (such as `_proof_1`, `_match_1`, or `_sizeOf_1`). + +These names are internal to the Lean elaborator and are not stable across refactors. +-/ +public register_option linter.style.auxLemma : Bool := { + defValue := true + descr := "enable the `auxLemma` linter" +} + +/-- The `auxLemma` linter: see docstring above -/ +def auxLemmaLinter : Linter where run := withSetOptionIn fun stx => do + unless getLinterValue linter.style.auxLemma (← getLinterOptions) do + return + if (← MonadState.get).messages.hasErrors then + return + if let some id := stx.find? fun s => s.isIdent && nameRefersToAuxLemma s.getId then + Linter.logLint linter.style.auxLemma id + m!"'{id.getId}' refers to an auto-generated auxiliary declaration. \ + These are not stable across refactors; consider using a different approach." + +initialize addLinter auxLemmaLinter + +end Mathlib.Linter.Style From 1e6da49d7cc4ab9d6d4b7fd7e0b657397b9100e3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Apr 2026 05:56:59 +0000 Subject: [PATCH 2/4] chore: suppress auxLemma linter at existing call sites Co-Authored-By: Claude Opus 4.6 (1M context) --- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean | 1 + Mathlib/CategoryTheory/Functor/Category.lean | 1 + Mathlib/Data/List/Sigma.lean | 2 ++ 3 files changed, 4 insertions(+) diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean index 1608c8f3a73275..be1f7b9251fef0 100644 --- a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean +++ b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean @@ -380,6 +380,7 @@ theorem constFormalMultilinearSeries_apply_of_nonzero [NontriviallyNormedField {n : ℕ} (hn : n ≠ 0) : constFormalMultilinearSeries 𝕜 E c n = 0 := Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn +set_option linter.style.auxLemma false in @[simp] lemma constFormalMultilinearSeries_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] : diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean index 217c5ec85576be..a69187ffbc6ca0 100644 --- a/Mathlib/CategoryTheory/Functor/Category.lean +++ b/Mathlib/CategoryTheory/Functor/Category.lean @@ -113,6 +113,7 @@ def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ H ⟶ G ⋙ I wh -- Horizontal composition has two possible definitions that are dual to each other, -- and we need to prove to `to_dual` that these are equivalent. +set_option linter.style.auxLemma false in attribute [to_dual none] hcomp._proof_2 hcomp._proof_3 to_dual_insert_cast hcomp := by ext x; exact β.naturality' (α.app x) diff --git a/Mathlib/Data/List/Sigma.lean b/Mathlib/Data/List/Sigma.lean index a055f158bcc771..6922c177c1fc48 100644 --- a/Mathlib/Data/List/Sigma.lean +++ b/Mathlib/Data/List/Sigma.lean @@ -547,6 +547,7 @@ theorem kerase_comm (a₁ a₂) (l : List (Sigma β)) : else by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂] else by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁] +set_option linter.style.auxLemma false in theorem sizeOf_kerase [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) : SizeOf.sizeOf (List.kerase x xs) ≤ SizeOf.sizeOf xs := by simp only [SizeOf.sizeOf, _sizeOf_1] @@ -646,6 +647,7 @@ theorem dlookup_dedupKeys (a : α) (l : List (Sigma β)) : dlookup a (dedupKeys · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne] exact h +set_option linter.style.auxLemma false in theorem sizeOf_dedupKeys [SizeOf (Sigma β)] (xs : List (Sigma β)) : SizeOf.sizeOf (dedupKeys xs) ≤ SizeOf.sizeOf xs := by simp only [SizeOf.sizeOf, _sizeOf_1] From 8261284f52d2a1c7d89c85915c8889165a5323d1 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Apr 2026 06:28:12 +0000 Subject: [PATCH 3/4] chore: suppress auxLemma linter at existing test call sites Co-Authored-By: Claude Opus 4.6 (1M context) --- MathlibTest/CompileInductive.lean | 1 + MathlibTest/interactiveUnfold.lean | 1 + MathlibTest/toAdditive.lean | 2 ++ 3 files changed, 4 insertions(+) diff --git a/MathlibTest/CompileInductive.lean b/MathlibTest/CompileInductive.lean index 54079959673da0..681094863f46f5 100644 --- a/MathlibTest/CompileInductive.lean +++ b/MathlibTest/CompileInductive.lean @@ -21,6 +21,7 @@ example := @Nat.brecOn example := @List.brecOn example := @Fin2.brecOn +set_option linter.style.auxLemma false in example := @List._sizeOf_1 open Lean Elab Term diff --git a/MathlibTest/interactiveUnfold.lean b/MathlibTest/interactiveUnfold.lean index e1d95e83811d08..03308b774a4355 100644 --- a/MathlibTest/interactiveUnfold.lean +++ b/MathlibTest/interactiveUnfold.lean @@ -122,6 +122,7 @@ variable {α : Type} [Group α] (a : α) in -- The proof `aux._proof_1` is an implementation detail. It should not be a problem if -- that appears in the expression, as long as it appears inside an implicit argument. def aux {α : Type} [Semiring α] := (3 : α) +set_option linter.style.auxLemma false in /-- info: Unfolds for 3 + 3: · Nat.add 3 3 diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean index 38f19c53ae8587..0832d0fbc34775 100644 --- a/MathlibTest/toAdditive.lean +++ b/MathlibTest/toAdditive.lean @@ -769,11 +769,13 @@ def Subtype.mul_inv_iff_mul_inv {α β : Type} [Group α] [MyRing β] (a : α) ( exists a simp +set_option linter.style.auxLemma false in /-- info: Subtype.mul_inv_iff_mul_inv._proof_1 {α β : Type} [Group α] [MyRing β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1 -/ #guard_msgs in #check Subtype.mul_inv_iff_mul_inv._proof_1 +set_option linter.style.auxLemma false in /-- info: Subtype.add_neg_iff_mul_inv._proof_1 {α β : Type} [AddGroup α] [MyRing β] (a : α) (b : β) : a + -a = 0 ↔ b * b⁻¹ = 1 -/ From dc9c15cb06703d581bffb484fed1f530fceff953 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 29 Apr 2026 11:47:23 +1000 Subject: [PATCH 4/4] chore(Tactic/Linter/AuxLemma): address review Apply review suggestions from @thorimur: - move out of `Style` namespace and rename option to `linter.auxLemma` - broaden the matched prefix list (`_sizeOf_`, `grind_`, `_simp_`, `_gcongr_`, `_aux_`) - use `s.rawEndPos > pfx.rawEndPos`, `MonadLog.hasErrors`, `@[inline]` on `matchesAuxPattern`, and `@[inherit_doc]` on the linter - minor wording / docstring fixes Co-Authored-By: Claude Opus 4.7 (1M context) --- .../Calculus/FormalMultilinearSeries.lean | 2 +- Mathlib/CategoryTheory/Functor/Category.lean | 2 +- Mathlib/Data/List/Sigma.lean | 4 +-- Mathlib/Init.lean | 4 +-- Mathlib/Tactic/Linter/AuxLemma.lean | 31 ++++++++++--------- MathlibTest/CompileInductive.lean | 2 +- MathlibTest/interactiveUnfold.lean | 2 +- MathlibTest/toAdditive.lean | 4 +-- 8 files changed, 27 insertions(+), 24 deletions(-) diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean index be1f7b9251fef0..0c0fbf7ddc9c05 100644 --- a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean +++ b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean @@ -380,7 +380,7 @@ theorem constFormalMultilinearSeries_apply_of_nonzero [NontriviallyNormedField {n : ℕ} (hn : n ≠ 0) : constFormalMultilinearSeries 𝕜 E c n = 0 := Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in @[simp] lemma constFormalMultilinearSeries_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] : diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean index a69187ffbc6ca0..bdab664cd5beb1 100644 --- a/Mathlib/CategoryTheory/Functor/Category.lean +++ b/Mathlib/CategoryTheory/Functor/Category.lean @@ -113,7 +113,7 @@ def hcomp {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) : F ⋙ H ⟶ G ⋙ I wh -- Horizontal composition has two possible definitions that are dual to each other, -- and we need to prove to `to_dual` that these are equivalent. -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in attribute [to_dual none] hcomp._proof_2 hcomp._proof_3 to_dual_insert_cast hcomp := by ext x; exact β.naturality' (α.app x) diff --git a/Mathlib/Data/List/Sigma.lean b/Mathlib/Data/List/Sigma.lean index 6922c177c1fc48..9d1475d21aeef3 100644 --- a/Mathlib/Data/List/Sigma.lean +++ b/Mathlib/Data/List/Sigma.lean @@ -547,7 +547,7 @@ theorem kerase_comm (a₁ a₂) (l : List (Sigma β)) : else by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂] else by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁] -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in theorem sizeOf_kerase [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) : SizeOf.sizeOf (List.kerase x xs) ≤ SizeOf.sizeOf xs := by simp only [SizeOf.sizeOf, _sizeOf_1] @@ -647,7 +647,7 @@ theorem dlookup_dedupKeys (a : α) (l : List (Sigma β)) : dlookup a (dedupKeys · rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne] exact h -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in theorem sizeOf_dedupKeys [SizeOf (Sigma β)] (xs : List (Sigma β)) : SizeOf.sizeOf (dedupKeys xs) ≤ SizeOf.sizeOf xs := by simp only [SizeOf.sizeOf, _sizeOf_1] diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index b62cfcba098b60..a6281933189de9 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -83,7 +83,7 @@ all these linters, or add the `weak.linter.mathlibStandardSet` option to their l register_linter_set linter.mathlibStandardSet := -- linter.allScriptsDocumented -- disabled, let's not impose this requirement downstream. -- linter.checkInitImports -- disabled, not relevant downstream. - linter.style.auxLemma + linter.auxLemma linter.flexible linter.hashCommand linter.oldObtain @@ -128,7 +128,7 @@ register_linter_set linter.weeklyLintSet := linter.tacticAnalysis.verifyGrindOnly -- Check that all linter options mentioned in the mathlib standard linter set exist. -open Lean Elab.Command Linter Mathlib.Linter Style UnusedInstancesInType +open Lean Elab.Command Linter Mathlib.Linter Style UnusedInstancesInType AuxLemma run_cmd liftTermElabM do let DefinedInScripts : Array Name := diff --git a/Mathlib/Tactic/Linter/AuxLemma.lean b/Mathlib/Tactic/Linter/AuxLemma.lean index e063092db0b02b..886796d959f8e7 100644 --- a/Mathlib/Tactic/Linter/AuxLemma.lean +++ b/Mathlib/Tactic/Linter/AuxLemma.lean @@ -25,11 +25,11 @@ meta section open Lean Elab Linter -namespace Mathlib.Linter.Style +namespace Mathlib.Linter.AuxLemma /-- Returns `true` if `s` has the form `pfx ++ digits`, e.g. `"_proof_17"`. -/ -private def matchesAuxPattern (pfx : String) (s : String) : Bool := - s.startsWith pfx && (s.drop pfx.length).all (·.isDigit) && s.length > pfx.length +@[inline] private def matchesAuxPattern (pfx : String) (s : String) : Bool := + s.startsWith pfx && (s.drop pfx.length).all (·.isDigit) && s.rawEndPos > pfx.rawEndPos /-- Returns `true` if `s` is an auto-generated auxiliary name component, such as `_proof_1`, `match_2`, or `_sizeOf_3`. -/ @@ -37,9 +37,13 @@ private def isAuxName (s : String) : Bool := matchesAuxPattern "_proof_" s || matchesAuxPattern "match_" s || matchesAuxPattern "_match_" s || - matchesAuxPattern "_sizeOf_" s + matchesAuxPattern "_sizeOf_" s || + matchesAuxPattern "grind_" s || + matchesAuxPattern "_simp_" s || + matchesAuxPattern "_gcongr_" s || + matchesAuxPattern "_aux_" s -/-- Returns `true` if any component of `nm` is an auto-generated auxiliary name. -/ +/-- Returns `true` if any component of the name is an auto-generated auxiliary name. -/ private def nameRefersToAuxLemma : Name → Bool | .str p s => isAuxName s || nameRefersToAuxLemma p | .num p _ => nameRefersToAuxLemma p @@ -48,24 +52,23 @@ private def nameRefersToAuxLemma : Name → Bool /-- The `auxLemma` linter emits a warning on any explicit reference to an auto-generated auxiliary declaration (such as `_proof_1`, `_match_1`, or `_sizeOf_1`). -These names are internal to the Lean elaborator and are not stable across refactors. --/ -public register_option linter.style.auxLemma : Bool := { +These names are internal to the Lean elaborator and are not stable across refactors. -/ +public register_option linter.auxLemma : Bool := { defValue := true descr := "enable the `auxLemma` linter" } -/-- The `auxLemma` linter: see docstring above -/ +@[inherit_doc linter.auxLemma] def auxLemmaLinter : Linter where run := withSetOptionIn fun stx => do - unless getLinterValue linter.style.auxLemma (← getLinterOptions) do + unless getLinterValue linter.auxLemma (← getLinterOptions) do return - if (← MonadState.get).messages.hasErrors then + if ← MonadLog.hasErrors then return if let some id := stx.find? fun s => s.isIdent && nameRefersToAuxLemma s.getId then - Linter.logLint linter.style.auxLemma id - m!"'{id.getId}' refers to an auto-generated auxiliary declaration. \ + logLint linter.auxLemma id + m!"`{id.getId}` refers to an auto-generated auxiliary declaration. \ These are not stable across refactors; consider using a different approach." initialize addLinter auxLemmaLinter -end Mathlib.Linter.Style +end Mathlib.Linter.AuxLemma diff --git a/MathlibTest/CompileInductive.lean b/MathlibTest/CompileInductive.lean index 681094863f46f5..3e3b6c146cded9 100644 --- a/MathlibTest/CompileInductive.lean +++ b/MathlibTest/CompileInductive.lean @@ -21,7 +21,7 @@ example := @Nat.brecOn example := @List.brecOn example := @Fin2.brecOn -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in example := @List._sizeOf_1 open Lean Elab Term diff --git a/MathlibTest/interactiveUnfold.lean b/MathlibTest/interactiveUnfold.lean index 03308b774a4355..8241050da3016c 100644 --- a/MathlibTest/interactiveUnfold.lean +++ b/MathlibTest/interactiveUnfold.lean @@ -122,7 +122,7 @@ variable {α : Type} [Group α] (a : α) in -- The proof `aux._proof_1` is an implementation detail. It should not be a problem if -- that appears in the expression, as long as it appears inside an implicit argument. def aux {α : Type} [Semiring α] := (3 : α) -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in /-- info: Unfolds for 3 + 3: · Nat.add 3 3 diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean index 0832d0fbc34775..061ab19726df92 100644 --- a/MathlibTest/toAdditive.lean +++ b/MathlibTest/toAdditive.lean @@ -769,13 +769,13 @@ def Subtype.mul_inv_iff_mul_inv {α β : Type} [Group α] [MyRing β] (a : α) ( exists a simp -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in /-- info: Subtype.mul_inv_iff_mul_inv._proof_1 {α β : Type} [Group α] [MyRing β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1 -/ #guard_msgs in #check Subtype.mul_inv_iff_mul_inv._proof_1 -set_option linter.style.auxLemma false in +set_option linter.auxLemma false in /-- info: Subtype.add_neg_iff_mul_inv._proof_1 {α β : Type} [AddGroup α] [MyRing β] (a : α) (b : β) : a + -a = 0 ↔ b * b⁻¹ = 1 -/