chore: rename mvcgen_invariant_type attribute to spec_invariant_type, part 2 (#13157)

This PR switches all usages from `@[mvcgen_invariant_type]` to
`@[spec_invariant_type]` and removes the old attribute registration.
Concludes the work of #13153.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -260,16 +260,11 @@ builtin_initialize specInvariantAttr : TagAttribute ←
   registerTagAttribute `spec_invariant_type
     "marks a type as an invariant type for the `mvcgen` tactic"
 
--- Keep old attribute name temporarily for bootstrapping; removed after stage0 update.
-builtin_initialize mvcgenInvariantAttr : TagAttribute ←
-  registerTagAttribute `mvcgen_invariant_type
-    "marks a type as an invariant type for the `mvcgen` tactic"
-
 /--
 Returns `true` if `ty` is an application of a type tagged with `@[spec_invariant_type]`.
 -/
 def isSpecInvariantType (env : Environment) (ty : Expr) : Bool :=
   if let .const name .. := ty.getAppFn then
-    specInvariantAttr.hasTag env name || mvcgenInvariantAttr.hasTag env name
+    specInvariantAttr.hasTag env name
   else
     false

src/Std/Do/Triple/SpecLemmas.lean

@@ -697,7 +697,7 @@ After leaving the loop, the cursor's prefix is `xs` and the suffix is empty.
 During the induction step, the invariant holds for a suffix with head element `x`.
 After running the loop body, the invariant then holds after shifting `x` to the prefix.
 -/
-@[mvcgen_invariant_type]
+@[spec_invariant_type]
 abbrev Invariant {α : Type u₁} (xs : List α) (β : Type u₂) (ps : PostShape.{max u₁ u₂}) :=
   PostCond (List.Cursor xs × β) ps
 
@@ -2027,7 +2027,7 @@ A loop invariant is a `PostCond` that takes as parameters
 * A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
   `let mut` variables and early return.
 -/
-@[mvcgen_invariant_type]
+@[spec_invariant_type]
 abbrev StringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) :=
   PostCond (s.Pos × β) ps
 
@@ -2112,7 +2112,7 @@ A loop invariant is a `PostCond` that takes as parameters
 * A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
   `let mut` variables and early return.
 -/
-@[mvcgen_invariant_type]
+@[spec_invariant_type]
 abbrev StringSliceInvariant (s : String.Slice) (β : Type u) (ps : PostShape.{u}) :=
   PostCond (s.Pos × β) ps
 

stage0/src/stdlib_flags.h

@@ -22,6 +22,7 @@ options get_default_options() {
     opts = opts.update({"quotPrecheck"}, true);
 
     opts = opts.update({"pp", "rawOnError"}, true);
+    // update stage0 for spec_invariant_type attribute rename (step 2/2)
 
     // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced
     // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt.

tests/elab/specInvariantAttr.lean

@@ -7,11 +7,11 @@ open Std Do
 set_option grind.warning false
 set_option mvcgen.warning false
 
--- Test that `@[mvcgen_invariant_type]` works end-to-end with a custom invariant type.
+-- Test that `@[spec_invariant_type]` works end-to-end with a custom invariant type.
 -- We replicate the `StringInvariant` setup locally: define a type, tag it, provide a spec,
 -- and verify that `mvcgen` classifies the invariant goal as `inv1` rather than `vc1`.
 
-@[mvcgen_invariant_type]
+@[spec_invariant_type]
 abbrev MyStringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) :=
   PostCond (s.Pos × β) ps
 
@@ -43,7 +43,7 @@ def stringLoop (s : String) : Id Unit := do
 
 theorem stringLoop_correct (s : String) :
     ⦃⌜True⌝⦄ stringLoop s ⦃⇓ _ => ⌜True⌝⦄ := by
-  -- With `@[mvcgen_invariant_type]` on `MyStringInvariant`, mvcgen classifies the
+  -- With `@[spec_invariant_type]` on `MyStringInvariant`, mvcgen classifies the
   -- loop invariant goal as `inv1` rather than `vc1`, enabling the `invariants` syntax.
   mvcgen [stringLoop] invariants
   · ⇓ _ => ⌜True⌝