From ad5a3291dcc02c3dbda9e940fe2e4df82f5ba1ed Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 30 Apr 2026 11:57:44 +0200 Subject: [PATCH] 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 | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index 45785525a0..cdcc0a2705 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/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 /--