chore: generalize definition of extrinsicFix further to make a point

This reverts commit 2198b357f6.

src/Init/Internal/Order.lean

@@ -7,5 +7,7 @@ module
 
 prelude
 public import Init.Internal.Order.Basic
+public import Init.Internal.Order.ExtrinsicFix
 public import Init.Internal.Order.Lemmas
+public import Init.Internal.Order.MonadTail
 public import Init.Internal.Order.Tactic

src/Init/Internal/Order/ExtrinsicFix.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf, Robin Arnez
+-/
+module
+
+prelude
+public import Init.Internal.Order.Basic
+public import Init.Internal.Order.MonadTail
+import Init.Classical
+
+set_option linter.missingDocs true
+
+/-!
+This module provides a fixpoint combinator that combines advantages of `partial` and
+`partial_fixpoint` recursion.
+
+The combinator is similar to {lean}`CCPO.fix`, but does not require a CCPO instance or
+monotonicity proof at the definition site. Therefore, it can be used in situations in which
+these constraints are unavailable (e.g., when the monad does not have a `MonadTail` instance).
+Given a CCPO and monotonicity proof, there are theorems guaranteeing that it equals
+{lean}`CCPO.fix` and satisfies fixpoint induction.
+-/
+
+public section
+
+namespace Lean.Order
+
+/--
+The function implemented as the loop {lean}`opaqueFix f = f (opaqueFix f)`.
+{lean}`opaqueFix f` is the fixpoint of {name}`f`, as long as `f` is monotone with respect to
+some CCPO on `α`.
+
+The loop might run forever depending on {name}`f`. It is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+@[specialize]
+partial def opaqueFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
+  f (opaqueFix f)
+
+/-
+SAFE assuming that the code generated by iteration over `f` is equivalent to the CCPO
+fixpoint of `f` if there exists a CCPO making `f` monotone.
+-/
+open _root_.Classical in
+/--
+A fixpoint combinator that can be used to construct recursive definitions with an *extrinsic*
+proof of monotonicity.
+
+Given a fixpoint functional {name}`f`, {lean}`extrinsicFix f` is the recursive function obtained
+by having {name}`f` call itself recursively.
+
+If there is no CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` might run forever.
+In this case, nothing interesting can be proved about the result; it is opaque.
+
+If there _is_ a CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` is equivalent to
+{lean}`CCPO.fix f`, logically and regarding its termination behavior.
+-/
+@[cbv_opaque, implemented_by opaqueFix]
+def extrinsicFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
+  if h : ∃ x, x = f x then
+    h.choose
+  else
+    -- Return `opaqueFix f` so that `implemented_by opaqueFix` is sound.
+    -- In effect, `extrinsicFix` is opaque if no fixpoint exists.
+    opaqueFix f
+
+/--
+A fixpoint combinator that allows for deferred proofs of monotonicity.
+
+{lean}`extrinsicFix f` is a function implemented as the loop
+{lean}`extrinsicFix f = f (extrinsicFix f)`.
+
+If there is a CCPO making `f` monotone, {name}`extrinsicFix_eq` proves that it satisfies the
+fixpoint equation, and {name}`extrinsicFix_induct` enables fixpoint induction.
+Otherwise, {lean}`extrinsicFix f` is opaque, i.e., it is impossible to prove nontrivial
+properties about it.
+-/
+add_decl_doc extrinsicFix
+
+/-- Every CCPO has at least one element (the bottom element). -/
+noncomputable local instance CCPO.instNonempty [CCPO α] : Nonempty α := ⟨bot⟩
+
+/--
+The fixpoint equation for `extrinsicFix`: given a proof that the fixpoint exists, unfold
+`extrinsicFix`.
+-/
+theorem extrinsicFix_eq {f : α → α}
+    (x : α) (h : x = f x) :
+    letI : Nonempty α := ⟨x⟩; extrinsicFix f = f (extrinsicFix f) := by
+  letI : Nonempty α := ⟨x⟩
+  have h : ∃ x, x = f x := ⟨x, h⟩
+  simp only [extrinsicFix, dif_pos h]
+  exact h.choose_spec
+
+/--
+The fixpoint equation for `extrinsicFix`: given a CCPO instance and monotonicity of `f`,
+{lean}`extrinsicFix f = f (extrinsicFix f)`.
+-/
+theorem extrinsicFix_eq_mono [inst : CCPO α] {f : α → α}
+    (hf : monotone f) :
+    extrinsicFix f = f (extrinsicFix f) :=
+  extrinsicFix_eq (fix f hf) (fix_eq hf)
+
+abbrev discardR {C : α → Sort _} {R : α → α → Prop}
+    (f : ∀ a, (∀ a', R a' a → C a') → C a) : ((∀ a, C a) → (∀ a, C a)) :=
+  fun rec a => f a (fun a _ => rec a)
+
+theorem extrinsicFix_eq_wf {C : α → Sort _} [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {f : ∀ a, (∀ a', R a' a → C a') → C a} (h : WellFounded R) {a : α} :
+    extrinsicFix (discardR f) a = f a (fun a _ => extrinsicFix (discardR f) a) := by
+  suffices extrinsicFix (discardR f) = fun a => f a (fun a _ => extrinsicFix (discardR f) a) by
+    conv => lhs; rw [this]
+  apply extrinsicFix_eq (fun a => WellFounded.fix h f a) (funext fun a => (WellFounded.fix_eq h f a))
+
+end Lean.Order

src/Init/Internal/Order/MonadTail.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Internal.Order.Basic
+import all Init.System.ST  -- for EST.bind in MonadTail instance
+
+set_option linter.missingDocs true
+
+public section
+
+namespace Lean.Order
+
+/--
+A *tail monad* is a monad whose bind operation preserves any suitable ordering of the continuation.
+Specifically, `MonadTail m` asserts that every `m β` carries a chain-complete partial order (CCPO)
+and that `>>=` is monotone in its second (continuation) argument with respect to that order.
+
+This is a weaker requirement than `MonoBind`, which requires monotonicity in both arguments.
+`MonadTail` is sufficient for `partial_fixpoint`-based recursive definitions where the
+recursive call only appears in the continuation (second argument) of `>>=`.
+-/
+class MonadTail (m : Type u → Type v) [Bind m] where
+  /-- Every `m β` with `Nonempty β` has a chain-complete partial order. -/
+  instCCPO β [Nonempty β] : CCPO (m β)
+  /-- Bind is monotone in the second (continuation) argument. -/
+  bind_mono_right {a : m α} {f₁ f₂ : α → m β} [Nonempty β] (h : ∀ x, f₁ x ⊑ f₂ x) :
+    a >>= f₁ ⊑ a >>= f₂
+
+attribute [implicit_reducible] MonadTail.instCCPO
+attribute [instance] MonadTail.instCCPO
+
+@[scoped partial_fixpoint_monotone]
+theorem MonadTail.monotone_bind_right
+    (m : Type u → Type v) [Monad m] [MonadTail m]
+    {α β : Type u} [Nonempty β]
+    {γ : Sort w} [PartialOrder γ]
+    (f : m α) (g : γ → α → m β)
+    (hmono : monotone g) :
+    monotone (fun (x : γ) => f >>= g x) :=
+  fun _ _ h => MonadTail.bind_mono_right (hmono _ _ h)
+
+instance : MonadTail Id where
+  instCCPO _ := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
+  bind_mono_right h := h _
+
+instance {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] [Nonempty σ] :
+    MonadTail (StateT σ m) where
+  instCCPO α := inferInstanceAs (CCPO (σ → m (α × σ)))
+  bind_mono_right h := by
+    intro s
+    show StateT.bind _ _ s ⊑ StateT.bind _ _ s
+    simp only [StateT.bind]
+    apply MonadTail.bind_mono_right (m := m)
+    intro ⟨x, s'⟩
+    exact h x s'
+
+instance {ε : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (ExceptT ε m) where
+  instCCPO β := MonadTail.instCCPO (Except ε β)
+  bind_mono_right h := by
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    cases x with
+    | error => exact PartialOrder.rel_refl
+    | ok a => exact h a
+
+instance : MonadTail (Except ε) where
+  instCCPO β := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
+  bind_mono_right h := by
+    cases ‹Except _ _› with
+    | error => exact FlatOrder.rel.refl
+    | ok a => exact h a
+
+instance {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (OptionT m) where
+  instCCPO β := MonadTail.instCCPO (Option β)
+  bind_mono_right h := by
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    cases x with
+    | none => exact PartialOrder.rel_refl
+    | some a => exact h a
+
+instance : MonadTail Option where
+  instCCPO _ := inferInstance
+  bind_mono_right h := MonoBind.bind_mono_right h
+
+instance {ρ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (ReaderT ρ m) where
+  instCCPO α := inferInstanceAs (CCPO (ρ → m α))
+  bind_mono_right h := by
+    intro r
+    show ReaderT.bind _ _ r ⊑ ReaderT.bind _ _ r
+    simp only [ReaderT.bind]
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    exact h x r
+
+set_option linter.missingDocs false in
+noncomputable def ST.bot' [Nonempty α] (s : Void σ) : @FlatOrder (ST.Out σ α) (.mk Classical.ofNonempty (Classical.choice ⟨s⟩)) :=
+  .mk Classical.ofNonempty (Classical.choice ⟨s⟩)
+
+instance [Nonempty α] : CCPO (ST σ α) where
+  rel := PartialOrder.rel (α := ∀ s, FlatOrder (ST.bot' s))
+  rel_refl := PartialOrder.rel_refl
+  rel_antisymm := PartialOrder.rel_antisymm
+  rel_trans := PartialOrder.rel_trans
+  has_csup hchain := CCPO.has_csup (α := ∀ s, FlatOrder (ST.bot' s)) hchain
+
+instance : MonadTail (ST σ) where
+  instCCPO _ := inferInstance
+  bind_mono_right {_ _ a f₁ f₂} _ h := by
+    intro w
+    change FlatOrder.rel (ST.bind a f₁ w) (ST.bind a f₂ w)
+    simp only [ST.bind]
+    apply h
+
+instance : MonadTail BaseIO :=
+  inferInstanceAs (MonadTail (ST IO.RealWorld))
+
+instance [Nonempty ε] : MonadTail (EST ε σ) where
+  instCCPO _ := inferInstance
+  bind_mono_right h := MonoBind.bind_mono_right h
+
+instance [Nonempty ε] : MonadTail (EIO ε) :=
+  inferInstanceAs (MonadTail (EST ε IO.RealWorld))
+
+instance : MonadTail IO :=
+  inferInstanceAs (MonadTail (EIO IO.Error))
+
+instance {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [MonadTail m] :
+    MonadTail (StateRefT' ω σ m) :=
+  inferInstanceAs (MonadTail (ReaderT (ST.Ref ω σ) m))
+
+end Lean.Order

src/Init/While.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Core
+public import Init.Internal.Order.ExtrinsicFix
 
 public section
 
@@ -21,18 +22,38 @@ namespace Lean
 inductive Loop where
   | mk
 
+open Lean.Order in
 @[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop (b : β) : m β := do
+def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m]
+    (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  haveI : Nonempty (β → m β) := ⟨fun b => pure b⟩
+  Lean.Order.extrinsicFix (fun (cont : β → m β) (b : β) => do
     match ← f () b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop b
-  loop init
+    | .done val => pure val
+    | .yield val => cont val) init
 
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-syntax "repeat " doSeq : doElem
+open Lean.Order in
+theorem Loop.forIn_eq [Monad m] [MonadTail m]
+    {l : Loop} {b : β} {f : Unit → β → m (ForInStep β)} :
+    Loop.forIn l b f = (do
+      match ← f () b with
+      | .done val => pure val
+      | .yield val => Loop.forIn l val f) := by
+  haveI : Nonempty β := ⟨b⟩
+  simp only [Loop.forIn]
+  apply congrFun
+  apply extrinsicFix_eq
+  intro cont₁ cont₂ h b'
+  apply MonadTail.bind_mono_right
+  intro r
+  cases r with
+  | done => exact PartialOrder.rel_refl
+  | yield val => exact h val
+
+syntax (name := doRepeat) "repeat " doSeq : doElem
 
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)

src/Lean/Elab/Do/Legacy.lean

@@ -1782,6 +1782,10 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
+          else if k == `Lean.doRepeat then
+            let seq := doElem[1]
+            let expanded ← `(doElem| for _ in Loop.mk do $seq)
+            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Parser/Do.lean

@@ -66,6 +66,14 @@ def notFollowedByRedefinedTermToken :=
       "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
+namespace InternalSyntax
+/--
+Internal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
+uses `()` if possible and gives better error messages.
+-/
+scoped syntax (name := doSkip) "skip" : doElem
+end InternalSyntax
+
 @[builtin_doElem_parser] def doLet      := leading_parser
   "let " >> optional "mut " >> letConfig >> letDecl
 @[builtin_doElem_parser] def doLetElse  := leading_parser withPosition <|

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -117,12 +117,13 @@ private partial def isSyntheticTacticCompletion
     (cmdStx   : Syntax)
     : Bool := Id.run do
   let hoverFilePos := fileMap.toPosition hoverPos
-  go hoverFilePos cmdStx 0
+  go hoverFilePos cmdStx 0 none
 where
   go
-      (hoverFilePos : Position)
-      (stx : Syntax)
-      (leadingWs : Nat)
+      (hoverFilePos         : Position)
+      (stx                  : Syntax)
+      (leadingWs            : Nat)
+      (leadingTokenTailPos? : Option String.Pos.Raw)
       : Bool := Id.run do
     match stx.getPos?, stx.getTailPos? with
     | some startPos, some endPos =>
@@ -132,8 +133,9 @@ where
       if ! isCursorInCompletionRange then
         return false
       let mut wsBeforeArg := leadingWs
+      let mut lastArgTailPos? := leadingTokenTailPos?
       for arg in stx.getArgs do
-        if go hoverFilePos arg wsBeforeArg then
+        if go hoverFilePos arg wsBeforeArg lastArgTailPos? then
           return true
         -- We must account for the whitespace before an argument because the syntax nodes we use
         -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
@@ -141,7 +143,12 @@ where
         -- This method of computing whitespace assumes that there are no syntax nodes without tokens
         -- after `by` and before the first proper tactic syntax.
         wsBeforeArg := arg.getTrailingSize
-      return isCompletionInEmptyTacticBlock stx
+        -- Track the tail position of the most recent preceding sibling that has a position so
+        -- that empty tactic blocks (which lack positions) can locate their opening token (e.g.
+        -- the `by` keyword) for indentation checking. The tail position lets us distinguish
+        -- cursors before and after the opener on the opener's line.
+        lastArgTailPos? := arg.getTailPos? <|> lastArgTailPos?
+      return isCompletionInEmptyTacticBlock stx lastArgTailPos?
         || isCompletionAfterSemicolon stx
         || isCompletionOnTacticBlockIndentation hoverFilePos stx
     | _, _ =>
@@ -150,7 +157,7 @@ where
       -- tactic blocks always occur within other syntax with ranges that let us narrow down the
       -- search to the degree that we can be sure that the cursor is indeed in this empty tactic
       -- block.
-      return isCompletionInEmptyTacticBlock stx
+      return isCompletionInEmptyTacticBlock stx leadingTokenTailPos?
 
   isCompletionOnTacticBlockIndentation
       (hoverFilePos : Position)
@@ -190,8 +197,47 @@ where
     else
       none
 
-  isCompletionInEmptyTacticBlock (stx : Syntax) : Bool :=
-    isCursorInProperWhitespace fileMap hoverPos && isEmptyTacticBlock stx
+  isCompletionInEmptyTacticBlock (stx : Syntax) (leadingTokenTailPos? : Option String.Pos.Raw) : Bool := Id.run do
+    if ! isCursorInProperWhitespace fileMap hoverPos then
+      return false
+    if ! isEmptyTacticBlock stx then
+      return false
+    -- Bracketed tactic blocks `{ ... }` are delimited by the braces themselves, so tactics
+    -- inserted in an empty bracketed block can appear at any column between the braces
+    -- (`withoutPosition` disables indentation constraints inside `tacticSeqBracketed`).
+    if stx.getKind == ``Parser.Tactic.tacticSeqBracketed then
+      let some openEndPos := stx[0].getTailPos?
+        | return false
+      let some closeStartPos := stx[2].getPos?
+        | return false
+      return openEndPos.byteIdx <= hoverPos.byteIdx && hoverPos.byteIdx <= closeStartPos.byteIdx
+    return isAtExpectedTacticIndentation leadingTokenTailPos?
+
+  -- After an empty tactic opener like `by`, tactics on a subsequent line must be inserted at an
+  -- increased indentation level (two spaces past the indentation of the line containing the
+  -- opener token). We mirror that here so that tactic completions are not offered in positions
+  -- where a tactic could not actually be inserted. On the same line as the opener, completions
+  -- are allowed only in the trailing whitespace past the opener — cursors earlier on the line
+  -- belong to the surrounding term, not to the tactic block.
+  isAtExpectedTacticIndentation (leadingTokenTailPos? : Option String.Pos.Raw) : Bool := Id.run do
+    let some tokenTailPos := leadingTokenTailPos?
+      | return true
+    let hoverFilePos := fileMap.toPosition hoverPos
+    let tokenTailFilePos := fileMap.toPosition tokenTailPos
+    if hoverFilePos.line == tokenTailFilePos.line then
+      return hoverPos.byteIdx >= tokenTailPos.byteIdx
+    let expectedColumn := countLeadingSpaces (fileMap.lineStart tokenTailFilePos.line) + 2
+    return hoverFilePos.column == expectedColumn
+
+  countLeadingSpaces (pos : String.Pos.Raw) : Nat := Id.run do
+    let mut p := pos
+    let mut n : Nat := 0
+    while ! p.atEnd fileMap.source do
+      if p.get fileMap.source != ' ' then
+        break
+      p := p.next fileMap.source
+      n := n + 1
+    return n
 
   isEmptyTacticBlock (stx : Syntax) : Bool :=
     stx.getKind == ``Parser.Tactic.tacticSeq && isEmpty stx

src/Std/Do/SPred/DerivedLaws.lean

@@ -178,6 +178,48 @@ theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entai
 @[simp] theorem entails_4 {P Q : SPred [σ₁, σ₂, σ₃, σ₄]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄, (P s₁ s₂ s₃ s₄).down → (Q s₁ s₂ s₃ s₄).down) := iff_of_eq rfl
 @[simp] theorem entails_5 {P Q : SPred [σ₁, σ₂, σ₃, σ₄, σ₅]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄ s₅, (P s₁ s₂ s₃ s₄ s₅).down → (Q s₁ s₂ s₃ s₄ s₅).down) := iff_of_eq rfl
 
+/-!
+# `SPred.evalsTo`
+
+Relates a stateful value `SVal σs α` to a pure value `a : α`, lifting equality through the state.
+-/
+
+/-- Relates a stateful value to a pure value, lifting equality through the state layers. -/
+def evalsTo {α : Type u} {σs : List (Type u)} (f : SVal σs α) (a : α) : SPred σs :=
+  match σs with
+  | [] => ⌜a = f⌝
+  | _ :: _ => fun s => evalsTo (f s) a
+
+@[simp, grind =] theorem evalsTo_nil {f : SVal [] α} {a : α} :
+    evalsTo f a = ⌜a = f⌝ := rfl
+
+theorem evalsTo_cons {f : σ → SVal σs α} {a : α} {s : σ} :
+    evalsTo (σs := σ::σs) f a s = evalsTo (f s) a := rfl
+
+@[simp, grind =] theorem evalsTo_1 {f : SVal [σ] α} {a : α} {s : σ} :
+    evalsTo f a s = evalsTo (f s) a := rfl
+
+@[simp, grind =] theorem evalsTo_2 {f : SVal [σ₁, σ₂] α} {a : α} {s₁ : σ₁} {s₂ : σ₂} :
+    evalsTo f a s₁ s₂ = evalsTo (f s₁ s₂) a := rfl
+
+@[simp, grind =] theorem evalsTo_3 {f : SVal [σ₁, σ₂, σ₃] α} {a : α}
+    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} :
+    evalsTo f a s₁ s₂ s₃ = evalsTo (f s₁ s₂ s₃) a := rfl
+
+@[simp, grind =] theorem evalsTo_4 {f : SVal [σ₁, σ₂, σ₃, σ₄] α} {a : α}
+    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} {s₄ : σ₄} :
+    evalsTo f a s₁ s₂ s₃ s₄ = evalsTo (f s₁ s₂ s₃ s₄) a := rfl
+
+@[simp, grind =] theorem evalsTo_5 {f : SVal [σ₁, σ₂, σ₃, σ₄, σ₅] α} {a : α}
+    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} {s₄ : σ₄} {s₅ : σ₅} :
+    evalsTo f a s₁ s₂ s₃ s₄ s₅ = evalsTo (f s₁ s₂ s₃ s₄ s₅) a := rfl
+
+theorem evalsTo_total {P : SPred σs} (f : SVal σs α) :
+    P ⊢ₛ ∃ m, evalsTo f m := by
+  induction σs with
+  | nil => simp
+  | cons _ _ ih => intro s; apply ih
+
 /-! # Tactic support -/
 
 namespace Tactic
@@ -338,3 +380,4 @@ theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ]
     · exact HasFrame.reassoc.mp.trans SPred.and_elim_r
     · intro hp
       exact HasFrame.reassoc.mp.trans (SPred.and_elim_l' (h hp))
+

src/Std/Do/SPred/Laws.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
+import Init.PropLemmas
 
 @[expose] public section
 
@@ -157,3 +158,17 @@ theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t =>
   induction σs
   case nil => rfl
   case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih
+
+/-! # Prop-indexed quantifiers -/
+
+/-- Simplifies an existential over a true proposition. -/
+theorem exists_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∃ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.exists_prop_of_true h
+  | cons σ σs ih => ext; exact ih
+
+/-- Simplifies a universal over a true proposition. -/
+theorem forall_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∀ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.forall_prop_of_true h
+  | cons σ σs ih => ext; exact ih

src/Std/Do/Triple/RepeatSpec.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Std.Do.Triple.SpecLemmas
+import Std.Tactic.Do.Syntax
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+namespace Std.Do
+
+/-!
+# Specification theorem for `Loop`-based `repeat`/`while` loops
+
+This file contains the `@[spec]` theorem for `forIn` over `Lean.Loop`, which enables
+verified reasoning about `repeat`/`while` loops using `mvcgen`.
+-/
+
+set_option mvcgen.warning false
+
+/-- A variant (termination measure) for a `repeat`/`while` loop. -/
+@[spec_invariant_type]
+abbrev RepeatVariant (β : Type u) (ps : PostShape.{u}) := β → SVal ps.args (ULift Nat)
+
+set_option linter.missingDocs false in
+abbrev RepeatVariant.eval {β ps} (variant : RepeatVariant β ps) (b : β) (n : Nat) :=
+  SPred.evalsTo (variant b) ⟨n⟩
+
+/-- An invariant for a `repeat`/`while` loop. -/
+@[spec_invariant_type]
+abbrev RepeatInvariant β ps := PostCond (Bool × β) ps
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+
+private theorem RepeatVariant.eval_total {P : SPred ps.args} (variant : RepeatVariant β ps) (b : β) :
+    P ⊢ₛ ∃ m, RepeatVariant.eval variant b m := by
+  mintro _
+  mhave h2 := SPred.evalsTo_total (variant b)
+  mcases h2 with ⟨m, h2⟩
+  mexists m.down
+
+private theorem RepeatVariant.add_eval {P Q : SPred ps.args} (variant : RepeatVariant β ps) (b : β)
+    (h : spred(∃ m, RepeatVariant.eval variant b m ∧ P) ⊢ₛ Q) : P ⊢ₛ Q := by
+  apply SPred.entails.trans _ h
+  mintro _
+  mhave h2 := RepeatVariant.eval_total variant b
+  mcases h2 with ⟨m, h2⟩
+  mexists m
+  mconstructor <;> massumption
+
+end
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+variable [Monad m] [Lean.Order.MonadTail m] [WPMonad m ps]
+
+@[spec]
+theorem Spec.forIn_loop
+    {l : _root_.Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)}
+    (measure : RepeatVariant β ps)
+    (inv : RepeatInvariant β ps)
+    (step : ∀ b mb,
+      Triple (f () b)
+        spred(RepeatVariant.eval measure b mb ∧ inv.1 (false, b))
+        (fun r => match r with
+          | .yield b' => spred(∃ mb', RepeatVariant.eval measure b' mb' ∧ ⌜mb' < mb⌝ ∧ inv.1 (false, b'))
+          | .done b' => inv.1 (true, b'), inv.2)) :
+    Triple (forIn l init f) spred(inv.1 (false, init)) (fun b => inv.1 (true, b), inv.2) := by
+  haveI : Nonempty β := ⟨init⟩
+  simp only [forIn]
+  apply RepeatVariant.add_eval measure init
+  apply SPred.exists_elim
+  intro minit
+  induction minit using Nat.strongRecOn generalizing init with
+  | _ minit ih =>
+  rw [_root_.Lean.Loop.forIn_eq]
+  mvcgen [step, ih] with
+  | vc2 =>
+    mrename_i h
+    mcases h with ⟨mb', ⟨hmeasure, ⌜hmb'⌝, h⟩⟩
+    mspec Triple.of_entails_wp (ih mb' hmb')
+
+end
+
+end Std.Do

src/Std/Do/Triple/SpecLemmas.lean

@@ -10,6 +10,7 @@ public import Std.Do.Triple.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Range.Polymorphic
 public import Init.Data.Slice.Array
+public import Init.While
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.

src/Std/Tactic/Do.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Tactic.Do.ProofMode
 public import Std.Tactic.Do.Syntax
+public import Std.Do.Triple.RepeatSpec
 
 @[expose] public section