chore: switch Invariant helpers from abbrev to def + @[simp] (#13583)

This PR changes `Invariant`, `StringInvariant`, and
`StringSliceInvariant` from `abbrev` to `@[spec_invariant_type, simp,
grind =] def`, so that they remain visible as applications of a named
constant in proof states (where `SymM` does not unfold `def`s) and can
be detected as invariant types by `isSpecInvariantType`. The `@[simp,
grind =]` annotations ensure they still unfold on demand under `simp`
and `grind`.

src/Std/Do/Triple/SpecLemmas.lean

@@ -698,8 +698,8 @@ 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.
 -/
-@[spec_invariant_type]
-abbrev Invariant {α : Type u₁} (xs : List α) (β : Type u₂) (ps : PostShape.{max u₁ u₂}) :=
+@[spec_invariant_type, simp, grind =]
+def Invariant {α : Type u₁} (xs : List α) (β : Type u₂) (ps : PostShape.{max u₁ u₂}) :=
   PostCond (List.Cursor xs × β) ps
 
 /--
@@ -2028,8 +2028,8 @@ 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.
 -/
-@[spec_invariant_type]
-abbrev StringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) :=
+@[spec_invariant_type, simp, grind =]
+def StringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) :=
   PostCond (s.Pos × β) ps
 
 /--
@@ -2113,8 +2113,8 @@ 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.
 -/
-@[spec_invariant_type]
-abbrev StringSliceInvariant (s : String.Slice) (β : Type u) (ps : PostShape.{u}) :=
+@[spec_invariant_type, simp, grind =]
+def StringSliceInvariant (s : String.Slice) (β : Type u) (ps : PostShape.{u}) :=
   PostCond (s.Pos × β) ps
 
 /--