feat: add auto_attach simp set (no functionality yet) (leanprover#6956

)

this PR helps with bootstrapping leanprover#6744.

src/Init/Tactics.lean

@@ -1662,6 +1662,14 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
+/--
+Theorems tagged with the `auto_attach` attribute are used during the processing of functions defined
+by well-founded recursion. They are applied to the function's body to add additional hypotheses,
+such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with
+`xs.attach.map`. Also see `wfParam`.
+-/
+syntax (name := auto_attach) "auto_attach" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
 

src/Lean/Elab/PreDefinition/WF/AutoAttach.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.Meta.Transform
+import Lean.Meta.Match.MatcherApp.Basic
+import Lean.Elab.Tactic.Simp
+
+open Lean Meta
+
+namespace Lean.Elab.WF
+
+builtin_initialize autoAttachSimpExtension : SimpExtension ←
+  registerSimpAttr `auto_attach
+    "(not yet functional)"
+
+end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -13,6 +13,7 @@ import Lean.Elab.PreDefinition.WF.Rel
 import Lean.Elab.PreDefinition.WF.Fix
 import Lean.Elab.PreDefinition.WF.Unfold
 import Lean.Elab.PreDefinition.WF.Ite
+import Lean.Elab.PreDefinition.WF.AutoAttach
 import Lean.Elab.PreDefinition.WF.GuessLex
 
 namespace Lean.Elab

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;