chore: add test case from Rob

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,96 @@
+/-
+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 : ∃ (inst : CCPO α), (letI := inst; monotone f) then
+    @fix α h.choose f h.choose_spec
+  else
+    -- Return `opaqueFix f` so that `implemented_by opaqueFix` is sound.
+    -- In effect, `extrinsicFix` is opaque if no CCPO makes `f` monotone.
+    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 CCPO instance and monotonicity of `f`,
+{lean}`extrinsicFix f = f (extrinsicFix f)`.
+-/
+theorem extrinsicFix_eq [inst : CCPO α] {f : α → α}
+    (hf : monotone f) :
+    extrinsicFix f = f (extrinsicFix f) := by
+  have h : ∃ inst' : CCPO α, (letI := inst'; monotone f) := ⟨inst, hf⟩
+  simp only [extrinsicFix, dif_pos h]
+  exact @fix_eq α h.choose f h.choose_spec
+
+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

@@ -1780,6 +1780,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/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
 

tests/elab/repeat_extrinsic.lean

@@ -0,0 +1,126 @@
+module
+
+import Std
+
+set_option mvcgen.warning false
+
+open Std.Do
+
+/-!
+# Tests for `Loop`-based `repeat`/`while` loops with `extrinsicFix`
+
+These tests verify that the `Loop.forIn` implementation using `extrinsicFix` and its
+verification infrastructure work correctly with `MonadTail`.
+-/
+
+/-- `sqrt n` computes the integer square root of `n` using a `while` loop. -/
+def sqrt (n : Nat) : Id Nat := do
+  if n = 0 then
+    return 0
+  let mut i := 0
+  while i * i ≤ n
+  do
+    i := i + 1
+  return i - 1
+
+/-- The `sqrt` function returns the correct integer square root. -/
+theorem sqrt_correct :
+    ⦃⌜True⌝⦄ sqrt n ⦃⇓ res => ⌜res * res ≤ n ∧ n < (res + 1) * (res+1)⌝⦄ := by
+  mvcgen [sqrt]
+  invariants
+  | inv1 => fun i => ULift.up ((n + 2) - i)
+  | inv2 => ⇓ (done, i) => ⌜∀ j, j < i → j * j ≤ n⌝ ∧ ⌜done = true → n < i * i⌝
+  with (try grind)
+  | vc2 r _ hsqr _ _ =>
+    have : r ≤ n := Nat.le_trans (Nat.le_mul_self r) hsqr
+    grind
+  | vc5 res h =>
+    have : res - 1 < res := by grind
+    grind
+
+-- Verify sqrt computes correctly
+#guard Id.run (sqrt 0) == 0
+#guard Id.run (sqrt 1) == 1
+#guard Id.run (sqrt 4) == 2
+#guard Id.run (sqrt 8) == 2
+#guard Id.run (sqrt 9) == 3
+#guard Id.run (sqrt 15) == 3
+#guard Id.run (sqrt 16) == 4
+#guard Id.run (sqrt 100) == 10
+
+/-- `sqrtState n` is the same as `sqrt` but uses `StateT`. -/
+def sqrtState (n : Nat) : StateT Nat Id Nat := do
+  if n = 0 then
+    return 0
+  let mut i := 0
+  while i * i ≤ n
+  do
+    i := i + 1
+  return i - 1
+
+/-- The `sqrtState` function returns the correct integer square root. -/
+theorem sqrtState_correct :
+    ⦃⌜True⌝⦄ sqrtState n ⦃⇓ res => ⌜res * res ≤ n ∧ n < (res + 1) * (res+1)⌝⦄ := by
+  mvcgen [sqrtState]
+  invariants
+  | inv1 => fun i _ => ULift.up ((n + 2) - i)
+  | inv2 => ⇓ (done, i) => ⌜∀ j, j < i → j * j ≤ n⌝ ∧ ⌜done = true → n < i * i⌝
+  with (try grind)
+  | vc2 r _ hsqr _ _ _ =>
+    have : r ≤ n := Nat.le_trans (Nat.le_mul_self r) hsqr
+    grind
+  | vc5 res h _ =>
+    have : res - 1 < res := by grind
+    grind
+
+/-- A loop that only terminates when the initial value satisfies `i ≤ x`. -/
+def loopWithTerminationPrecond (x : Nat) : Id Nat := do
+  let mut i := 0
+  while i ≠ x do
+    i := i + 1
+  return i
+
+example : ⦃⌜True⌝⦄ loopWithTerminationPrecond x ⦃⇓ r => ⌜r = x⌝⦄ := by
+  mvcgen [loopWithTerminationPrecond] invariants
+  | inv1 => fun i => ULift.up (x - i)
+  | inv2 => ⇓ (done, i) => ⌜i ≤ x⌝ ∧ ⌜done = true → i = x⌝
+  with grind
+
+/-- A loop that only terminates when the initial *state* satisfies some invariant. -/
+def loopWithStatefulTerminationPrecond (x : Nat) : StateM Nat Nat := do
+  set 0
+  while (← get) ≠ x do
+    modify fun i => i + 1
+  get
+
+example : ⦃⌜True⌝⦄ loopWithStatefulTerminationPrecond x ⦃⇓ r => ⌜r = x⌝⦄ := by
+  mvcgen [loopWithStatefulTerminationPrecond] invariants
+  | inv1 => fun _ s => ULift.up (x - s)
+  | inv2 => ⇓ (done, _) s => ⌜s ≤ x ∧ (done = true → s = x)⌝
+  with (try grind)
+
+/-- A loop that does not terminate for all inputs. -/
+def possiblyDivergentLoop (x : Nat) : Id Nat := do
+  let mut x := x
+  while x ≠ 20 do
+    x := x + 1
+  return x
+
+example : ⦃⌜x ≤ 20⌝⦄ possiblyDivergentLoop x ⦃⇓ r => ⌜r = 20⌝⦄ := by
+  mvcgen [possiblyDivergentLoop] invariants
+  | inv1 => fun i => ULift.up (20 - i)
+  | inv2 => ⇓ (done, i) => ⌜i ≤ 20⌝ ∧ ⌜done = true → i = 20⌝
+  with grind
+
+def terminatesSometimes (n : Nat) (p : Nat → Bool) :  Option Nat := do
+  let mut n := n
+  while !p n do
+    n := n + 2
+  return n
+
+example (n m : Nat) (h : n ≤ m) (heven : n % 2 = 0) (hmeven : m % 2 = 0) (h : p m) :
+    ⦃⌜True⌝⦄ terminatesSometimes n p ⦃⇓ r => ⌜r % 2 = 0⌝⦄ := by
+  mvcgen [terminatesSometimes] invariants
+  | inv1 => fun i => ULift.up (m + 1 - i)
+  | inv2 => ⇓ (done, i) => ⌜i % 2 = 0 ∧ i ≤ m⌝ ∧ ⌜done = true → p i⌝
+  with grind