chore: rename mvcgen_invariant_type attribute to spec_invariant_type, part 1 (#13153)

This PR registers the new `spec_invariant_type` attribute alongside the
old
`mvcgen_invariant_type`, renames internal identifiers, and replaces the
hardcoded `Invariant` check in `Spec.lean` with `isSpecInvariantType`.

A follow-up PR will switch all usages to `spec_invariant_type` and
remove
the old attribute after stage0 is updated.

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

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

@@ -256,15 +256,20 @@ Marks a type as an invariant type for the `mvcgen` tactic.
 Goals whose type is an application of a tagged type will be classified
 as invariants rather than verification conditions.
 -/
+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 `@[mvcgen_invariant_type]`.
+Returns `true` if `ty` is an application of a type tagged with `@[spec_invariant_type]`.
 -/
-def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
+def isSpecInvariantType (env : Environment) (ty : Expr) : Bool :=
   if let .const name .. := ty.getAppFn then
-    mvcgenInvariantAttr.hasTag env name
+    specInvariantAttr.hasTag env name || mvcgenInvariantAttr.hasTag env name
   else
     false

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

@@ -75,7 +75,7 @@ def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM SpecTheorem :
   | none => findSpec (← getSpecTheorems) wp
   | some stx => elabTermIntoSpecTheorem stx expectedTy
 
-variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n]
+variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] [MonadEnv n]
 
 private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do
   return (← projectCore? Q i).getD (mkProj n i Q)
@@ -181,11 +181,12 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag
   -- Instantiation creates `.natural` MVars, which possibly get instantiated by the def eq checks
   -- below when they occur in `P` or `Q`.
   -- That's good for many such as MVars ("schematic variables"), but problematic for MVars
-  -- corresponding to `Invariant`s, which should end up as user goals.
-  -- To prevent accidental instantiation, we mark all `Invariant` MVars as synthetic opaque.
+  -- corresponding to invariant types, which should end up as user goals.
+  -- To prevent accidental instantiation, we mark all invariant MVars as synthetic opaque.
+  let env ← getEnv
   for mvar in mvars do
     let ty ← mvar.mvarId!.getType
-    if ty.isAppOf ``Invariant then mvar.mvarId!.setKind .syntheticOpaque
+    if isSpecInvariantType env ty then mvar.mvarId!.setKind .syntheticOpaque
 
   -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application
   let T := goal.target.consumeMData

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -104,7 +104,7 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   -- VC to the user as-is, without abstracting any variables in the local context.
   -- This only makes sense for synthetic opaque metavariables.
   goal.setKind .syntheticOpaque
-  if isMVCGenInvariantType (← getEnv) ty then
+  if isSpecInvariantType (← getEnv) ty then
     modify fun s => { s with invariants := s.invariants.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }

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 1/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.