feat: Improved API for invariants and postconditions (#9805)

This PR improves the API for invariants and postconditions and as such introduces a few breaking changes to the existing pre-release API around `Std.Do`. It also adds Markus Himmel's `pairsSumToZero` example as a test case.
2025-08-09 16:42:37 +02:00 · 2025-08-09 16:42:37 +02:00 · 8558b2d278
commit 8558b2d278
parent 756f837f82
11 changed files with 333 additions and 142 deletions
--- a/src/Lean/Elab/Tactic/Do/Spec.lean
+++ b/src/Lean/Elab/Tactic/Do/Spec.lean
@ -96,11 +96,11 @@ partial def dischargeFailEntails (u : Level) (ps : Expr) (Q : Expr) (Q' : Expr)
  if ps.isAppOf ``PostShape.pure then
    return mkConst ``True.intro
  if ← isDefEq Q Q' then
-    return mkApp2 (mkConst ``FailConds.entails.refl [u]) ps Q
-  if ← isDefEq Q (mkApp (mkConst ``FailConds.false [u]) ps) then
-    return mkApp2 (mkConst ``FailConds.entails_false [u]) ps Q'
-  if ← isDefEq Q' (mkApp (mkConst ``FailConds.true [u]) ps) then
-    return mkApp2 (mkConst ``FailConds.entails_true [u]) ps Q
+    return mkApp2 (mkConst ``ExceptConds.entails.refl [u]) ps Q
+  if ← isDefEq Q (mkApp (mkConst ``ExceptConds.false [u]) ps) then
+    return mkApp2 (mkConst ``ExceptConds.entails_false [u]) ps Q'
+  if ← isDefEq Q' (mkApp (mkConst ``ExceptConds.true [u]) ps) then
+    return mkApp2 (mkConst ``ExceptConds.entails_true [u]) ps Q
  -- the remaining cases are recursive.
  if let some (_σ, ps) := ps.app2? ``PostShape.arg then
    return ← dischargeFailEntails u ps Q Q' goalTag
@ -117,7 +117,7 @@ partial def dischargeFailEntails (u : Level) (ps : Expr) (Q : Expr) (Q' : Expr)
    let prf₂ ← dischargeFailEntails u ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except)
    return ← mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand
  -- This case happens when decomposing with unknown `ps : PostShape`
-  mkFreshExprSyntheticOpaqueMVar (mkApp3 (mkConst ``FailConds.entails [u]) ps Q Q') goalTag
+  mkFreshExprSyntheticOpaqueMVar (mkApp3 (mkConst ``ExceptConds.entails [u]) ps Q Q') goalTag
 end

 def dischargeMGoal (goal : MGoal) (goalTag : Name) : n Expr := do
--- a/src/Lean/Elab/Tactic/Do/Syntax.lean
+++ b/src/Lean/Elab/Tactic/Do/Syntax.lean
@ -18,13 +18,22 @@ namespace Std.Do
 open Lean Parser Meta Elab Term PrettyPrinter Delaborator

 open Std.Do in
-@[builtin_delab app.Std.Do.PostCond.total]
-private def unexpandPostCondTotal : Delab := do
+@[builtin_delab PostCond.noThrow]
+private def unexpandPostCondNoThrow : Delab := do
  match ← SubExpr.withAppArg <| delab with
  | `(fun $xs:term* => $e) =>
    let t ← `(⇓ $xs* => $(← SPred.Notation.unpack e))
    return ⟨t.raw⟩
-  | t => `($(mkIdent ``PostCond.total):term $t)
+  | t => `($(mkIdent ``PostCond.noThrow):term $t)
+
+open Std.Do in
+@[builtin_delab PostCond.mayThrow]
+private def unexpandPostCondMayThrow : Delab := do
+  match ← SubExpr.withAppArg <| delab with
+  | `(fun $xs:term* => $e) =>
+    let t ← `(⇓? $xs* => $(← SPred.Notation.unpack e))
+    return ⟨t.raw⟩
+  | t => `($(mkIdent ``PostCond.mayThrow):term $t)

@[inherit_doc Triple, builtin_doc, builtin_term_elab triple]
 private def elabTriple : TermElab
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@ -70,15 +70,20 @@ where
      mvar.withContext <| do
      -- trace[Elab.Tactic.Do.vcgen] "assignMVars {← mvar.getTag}, isDelayedAssigned: {← mvar.isDelayedAssigned},\n{mvar}"
      let ty ← mvar.getType
-      if (← isProp ty) || ty.isAppOf ``PostCond || ty.isAppOf ``SPred then
-        -- This code path will re-introduce `mvar` as a synthetic opaque goal upon discharge failure.
-        -- This is the right call for (previously natural) holes such as loop invariants, which
-        -- would otherwise lead to spurious instantiations.
-        -- But it's wrong for, e.g., schematic variables. The latter should never be PostConds or
-        -- SPreds, hence the condition.
+      if ← isProp ty then
+        -- Might contain more `P ⊢ₛ wp⟦prog⟧ Q` apps. Try and prove it!
        mvar.assign (← tryGoal ty (← mvar.getTag))
-      else
-        addSubGoalAsVC mvar
+        return
+
+      if ty.isAppOf ``PostCond || ty.isAppOf ``Invariant || ty.isAppOf ``SPred then
+        -- Here we make `mvar` a synthetic opaque goal upon discharge failure.
+        -- This is the right call for (previously natural) holes such as loop invariants, which
+        -- would otherwise lead to spurious instantiations and unwanted renamings (when leaving the
+        -- scope of a local).
+        -- But it's wrong for, e.g., schematic variables. The latter should never be PostConds,
+        -- Invariants or SPreds, hence the condition.
+        mvar.setKind .syntheticOpaque
+      addSubGoalAsVC mvar

  onGoal goal name : VCGenM Expr := do
    let T := goal.target
--- a/src/Std/Do/PostCond.lean
+++ b/src/Std/Do/PostCond.lean
@ -72,69 +72,69 @@ abbrev Assertion (ps : PostShape.{u}) : Type u :=
 /--
  Encodes one continuation barrel for each `PostShape.except` in the given predicate shape.
  ```
-  example : FailConds (.pure) = Unit := rfl
-  example : FailConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
-  example : FailConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
-  example : FailConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
+  example : ExceptConds (.pure) = Unit := rfl
+  example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
+  example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
+  example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
  ```
 -/
-def FailConds : PostShape.{u} → Type u
+def ExceptConds : PostShape.{u} → Type u
  | .pure => PUnit
-  | .arg _ ps => FailConds ps
-  | .except ε ps => (ε → Assertion ps) × FailConds ps
+  | .arg _ ps => ExceptConds ps
+  | .except ε ps => (ε → Assertion ps) × ExceptConds ps

@[simp]
-def FailConds.const {ps : PostShape.{u}} (p : Prop) : FailConds ps := match ps with
+def ExceptConds.const {ps : PostShape.{u}} (p : Prop) : ExceptConds ps := match ps with
  | .pure => ⟨⟩
-  | .arg _ ps => @FailConds.const ps p
-  | .except _ ps => (fun _ε => spred(⌜p⌝), @FailConds.const ps p)
+  | .arg _ ps => @ExceptConds.const ps p
+  | .except _ ps => (fun _ε => spred(⌜p⌝), @ExceptConds.const ps p)

-def FailConds.true : FailConds ps := FailConds.const True
+def ExceptConds.true : ExceptConds ps := ExceptConds.const True

-def FailConds.false : FailConds ps := FailConds.const False
+def ExceptConds.false : ExceptConds ps := ExceptConds.const False

-instance : Inhabited (FailConds ps) where
-  default := FailConds.true
+instance : Inhabited (ExceptConds ps) where
+  default := ExceptConds.true

-def FailConds.entails {ps : PostShape.{u}} (x y : FailConds ps) : Prop :=
+def ExceptConds.entails {ps : PostShape.{u}} (x y : ExceptConds ps) : Prop :=
  match ps with
  | .pure => True
  | .arg _ ps => @entails ps x y
  | .except _ ps => (∀ e, x.1 e ⊢ₛ y.1 e) ∧ @entails ps x.2 y.2

-scoped infix:25 " ⊢ₑ " => FailConds.entails
+scoped infix:25 " ⊢ₑ " => ExceptConds.entails

@[refl, simp]
-theorem FailConds.entails.refl {ps : PostShape} (x : FailConds ps) : x ⊢ₑ x := by
+theorem ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) : x ⊢ₑ x := by
  induction ps <;> simp [entails, *]

-theorem FailConds.entails.rfl {ps : PostShape} {x : FailConds ps} : x ⊢ₑ x := refl x
+theorem ExceptConds.entails.rfl {ps : PostShape} {x : ExceptConds ps} : x ⊢ₑ x := refl x

-theorem FailConds.entails.trans {ps : PostShape} {x y z : FailConds ps} : (x ⊢ₑ y) → (y ⊢ₑ z) → x ⊢ₑ z := by
+theorem ExceptConds.entails.trans {ps : PostShape} {x y z : ExceptConds ps} : (x ⊢ₑ y) → (y ⊢ₑ z) → x ⊢ₑ z := by
  induction ps
  case pure => intro _ _; trivial
  case arg σ s ih => exact ih
  case except ε s ih => intro h₁ h₂; exact ⟨fun e => (h₁.1 e).trans (h₂.1 e), ih h₁.2 h₂.2⟩

@[simp]
-theorem FailConds.entails_false {x : FailConds ps} : FailConds.false ⊢ₑ x := by
+theorem ExceptConds.entails_false {x : ExceptConds ps} : ExceptConds.false ⊢ₑ x := by
  induction ps <;> simp_all [false, const, entails, SPred.false_elim]

@[simp]
-theorem FailConds.entails_true {x : FailConds ps} : x ⊢ₑ FailConds.true := by
+theorem ExceptConds.entails_true {x : ExceptConds ps} : x ⊢ₑ ExceptConds.true := by
  induction ps <;> simp_all [true, const, entails]

@[simp]
-def FailConds.and {ps : PostShape.{u}} (x : FailConds ps) (y : FailConds ps) : FailConds ps :=
+def ExceptConds.and {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
  match ps with
  | .pure => ⟨⟩
-  | .arg _ ps => @FailConds.and ps x y
-  | .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), FailConds.and x.2 y.2)
+  | .arg _ ps => @ExceptConds.and ps x y
+  | .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), ExceptConds.and x.2 y.2)

-infixr:35 " ∧ₑ " => FailConds.and
+infixr:35 " ∧ₑ " => ExceptConds.and

@[simp]
-theorem FailConds.and_true {x : FailConds ps} : x ∧ₑ FailConds.true ⊢ₑ x := by
+theorem ExceptConds.and_true {x : ExceptConds ps} : x ∧ₑ ExceptConds.true ⊢ₑ x := by
  induction ps
  case pure => trivial
  case arg ih => exact ih
@ -143,7 +143,7 @@ theorem FailConds.and_true {x : FailConds ps} : x ∧ₑ FailConds.true ⊢ₑ x
    constructor <;> simp only [SPred.and_true.mp, implies_true, ih]

@[simp]
-theorem FailConds.true_and {x : FailConds ps} : FailConds.true ∧ₑ x ⊢ₑ x := by
+theorem ExceptConds.true_and {x : ExceptConds ps} : ExceptConds.true ∧ₑ x ⊢ₑ x := by
  induction ps
  case pure => trivial
  case arg ih => exact ih
@ -152,7 +152,7 @@ theorem FailConds.true_and {x : FailConds ps} : FailConds.true ∧ₑ x ⊢ₑ x
    constructor <;> simp only [SPred.true_and.mp, implies_true, ih]

@[simp]
-theorem FailConds.and_false {x : FailConds ps} : x ∧ₑ FailConds.false ⊢ₑ FailConds.false := by
+theorem ExceptConds.and_false {x : ExceptConds ps} : x ∧ₑ ExceptConds.false ⊢ₑ ExceptConds.false := by
  induction ps
  case pure => trivial
  case arg ih => exact ih
@ -161,7 +161,7 @@ theorem FailConds.and_false {x : FailConds ps} : x ∧ₑ FailConds.false ⊢ₑ
    constructor <;> simp only [SPred.and_false.mp, implies_true, ih]

@[simp]
-theorem FailConds.false_and {x : FailConds ps} : FailConds.false ∧ₑ x ⊢ₑ FailConds.false := by
+theorem ExceptConds.false_and {x : ExceptConds ps} : ExceptConds.false ∧ₑ x ⊢ₑ ExceptConds.false := by
  induction ps
  case pure => trivial
  case arg ih => exact ih
@ -169,7 +169,7 @@ theorem FailConds.false_and {x : FailConds ps} : FailConds.false ∧ₑ x ⊢ₑ
    simp_all only [and, false, const]
    constructor <;> simp only [SPred.false_and.mp, implies_true, ih]

-theorem FailConds.and_eq_left {ps : PostShape} {p q : FailConds ps} (h : p ⊢ₑ q) :
+theorem ExceptConds.and_eq_left {ps : PostShape} {p q : ExceptConds ps} (h : p ⊢ₑ q) :
    p = (p ∧ₑ q) := by
  induction ps
  case pure => trivial
@ -188,10 +188,10 @@ example : PostCond α (.arg ρ .pure) = ((α → ρ → Prop) × Unit) := rfl
 example : PostCond α (.except ε .pure) = ((α → Prop) × (ε → Prop) × Unit) := rfl
 example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → Prop) × (ε → Prop) × Unit) := rfl
 example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → Prop) × (ε → σ → Prop) × Unit) := rfl
-  ```
+```
 -/
 abbrev PostCond (α : Type u) (ps : PostShape.{u}) : Type u :=
-  (α → Assertion ps) × FailConds ps
+  (α → Assertion ps) × ExceptConds ps

@[inherit_doc PostCond]
 scoped macro:max "post⟨" handlers:term,+,? "⟩" : term =>
@ -204,12 +204,12 @@ A postcondition expressing total correctness.
 That is, it expresses that the asserted computation finishes without throwing an exception
 *and* the result satisfies the given predicate `p`.
 -/
-abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
-  (p, FailConds.false)
+abbrev PostCond.noThrow (p : α → Assertion ps) : PostCond α ps :=
+  (p, ExceptConds.false)

-@[inherit_doc PostCond.total]
+@[inherit_doc PostCond.noThrow]
 scoped macro:max ppAllowUngrouped "⇓" xs:term:max+ " => " e:term : term =>
-  `(PostCond.total (by exact fun $xs* => spred($e)))
+  `(PostCond.noThrow (by exact fun $xs* => spred($e)))

 /--
 A postcondition expressing partial correctness.
@ -217,35 +217,39 @@ That is, it expresses that *if* the asserted computation finishes without throwi
 *then* the result satisfies the given predicate `p`.
 Nothing is asserted when the computation throws an exception.
 -/
-abbrev PostCond.partial (p : α → Assertion ps) : PostCond α ps :=
-  (p, FailConds.true)
+abbrev PostCond.mayThrow (p : α → Assertion ps) : PostCond α ps :=
+  (p, ExceptConds.true)
+
+@[inherit_doc PostCond.mayThrow]
+scoped macro:max ppAllowUngrouped "⇓?" xs:term:max+ " => " e:term : term =>
+  `(PostCond.mayThrow (by exact fun $xs* => spred($e)))

 instance : Inhabited (PostCond α ps) where
-  default := PostCond.total fun _ => default
+  default := PostCond.noThrow fun _ => default

@[simp]
 def PostCond.entails (p q : PostCond α ps) : Prop :=
-  (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ FailConds.entails p.2 q.2
+  (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ ExceptConds.entails p.2 q.2

 scoped infix:25 " ⊢ₚ " => PostCond.entails

@[refl, simp]
-theorem PostCond.entails.refl (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), FailConds.entails.refl Q.2⟩
+theorem PostCond.entails.refl (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), ExceptConds.entails.refl Q.2⟩
 theorem PostCond.entails.rfl {Q : PostCond α ps} : Q ⊢ₚ Q := refl Q

 theorem PostCond.entails.trans {P Q R : PostCond α ps} (h₁ : P ⊢ₚ Q) (h₂ : Q ⊢ₚ R) : P ⊢ₚ R :=
  ⟨fun a => (h₁.1 a).trans (h₂.1 a), h₁.2.trans h₂.2⟩

@[simp]
-theorem PostCond.entails_total (p : α → Assertion ps) (q : PostCond α ps) : PostCond.total p ⊢ₚ q ↔ ∀ a, p a ⊢ₛ q.1 a := by
-  simp only [entails, FailConds.entails_false, and_true]
+theorem PostCond.entails_noThrow (p : α → Assertion ps) (q : PostCond α ps) : PostCond.noThrow p ⊢ₚ q ↔ ∀ a, p a ⊢ₛ q.1 a := by
+  simp only [entails, ExceptConds.entails_false, and_true]

@[simp]
-theorem PostCond.entails_partial (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.partial q ↔ ∀ a, p.1 a ⊢ₛ q a := by
-  simp only [entails, FailConds.entails_true, and_true]
+theorem PostCond.entails_mayThrow (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.mayThrow q ↔ ∀ a, p.1 a ⊢ₛ q a := by
+  simp only [entails, ExceptConds.entails_true, and_true]

 abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
-  (fun a => SPred.and (p.1 a) (q.1 a), FailConds.and p.2 q.2)
+  (fun a => SPred.and (p.1 a) (q.1 a), ExceptConds.and p.2 q.2)

 scoped infixr:35 " ∧ₚ " => PostCond.and

@ -253,4 +257,4 @@ theorem PostCond.and_eq_left {p q : PostCond α ps} (h : p ⊢ₚ q) :
    p = (p ∧ₚ q) := by
  ext
  · exact (SPred.and_eq_left.mp (h.1 _)).to_eq
-  · exact FailConds.and_eq_left h.2
+  · exact ExceptConds.and_eq_left h.2
--- a/src/Std/Do/Triple/Basic.lean
+++ b/src/Std/Do/Triple/Basic.lean
@ -60,7 +60,7 @@ theorem bind [Monad m] [WPMonad m ps] {α β : Type u} {P : Assertion ps} {Q :
  apply SPred.entails.trans hx
  simp only [WP.bind]
  apply (wp x).mono _ _
-  simp only [PostCond.entails, Assertion, FailConds.entails.refl, and_true]
+  simp only [PostCond.entails, Assertion, ExceptConds.entails.refl, and_true]
  exact hf

 theorem and [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ Q₂) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@ -303,22 +303,68 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q :

 /-! # `ForIn` -/

+/--
+The type of loop invariants used by the specifications of `for ... in ...` loops.
+A loop invariant is a `PostCond` that takes as parameters
+
+* A `List.Zipper xs` representing the iteration state of the loop. It is parameterized by the list
+  of elements `xs` that the `for` loop iterates over.
+* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
+  `let mut` variables and early return.
+
+The loop specification lemmas will use this in the following way:
+Before entering the loop, the zipper's prefix is empty and the suffix is `xs`.
+After leaving the loop, the zipper's suffix is empty and the prefix is `xs`.
+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.
+-/
+abbrev Invariant {α : Type u} (xs : List α) (β : Type u) (ps : PostShape) :=
+  PostCond (List.Zipper xs × β) ps
+
+/--
+Helper definition for specifying loop invariants for loops with early return.
+
+`for ... in ...` loops with early return of type `γ` elaborate to a call like this:
+```lean
+forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody
+```
+Note that the first component of the `MProd` state tuple is the optional early return value.
+It is `none` as long as there was no early return and `some r` if the loop returned early with `r`.
+
+This function allows to specify different invariants for the loop body depending on whether the loop
+terminated early or not. When there was an early return, the loop has effectively finished, which is
+encoded by the additional `⌜xs.suff = []⌝` assertion in the invariant. This assertion is vital for
+successfully proving the induction step, as it contradicts with the assumption that
+`xs.suff = x::rest` of the inductive hypothesis at the start of the loop body, meaning that users
+won't need to prove anything about the bogus case where the loop has returned early yet takes
+another iteration of the loop body.
+-/
+abbrev Invariant.withEarlyReturn
+  (onContinue : List.Zipper xs → β → Assertion ps)
+  (onReturn : γ → β → Assertion ps)
+  (onFail : ExceptConds ps := ExceptConds.false) :
+    Invariant xs (MProd (Option γ) β) ps :=
+  ⟨fun ⟨xs, x, b⟩ => spred(
+        (⌜x = none⌝ ∧ onContinue xs b)
+      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suff = []⌝ ∧ onReturn r b)),
+   onFail⟩
+
@[spec]
 theorem Spec.forIn'_list {α β : Type u}
    [Monad m] [WPMonad m ps]
    {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
-    (inv : PostCond (β × List.Zipper xs) ps)
+    (inv : Invariant xs β ps)
    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f x hx b
        ⦃(fun r => match r with
-                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
-                   | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs, by simp⟩)} forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)} := by
+                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.reverse, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
  suffices h : ∀ rpref suff (h : xs = rpref.reverse ++ suff),
-      ⦃inv.1 (init, ⟨rpref, suff, by simp [h]⟩)}
+      ⦃inv.1 (⟨rpref, suff, by simp [h]⟩, init)}
      forIn' (m:=m) suff init (fun a ha => f a (by simp[h,ha]))
-      ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp [h]⟩), inv.2)}
+      ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp [h]⟩, b), inv.2)}
    from h [] xs rfl
  intro rpref suff h
  induction suff generalizing rpref init
@ -347,20 +393,20 @@ theorem Spec.forIn'_list_const_inv {α β : Type u}
        f x hx b
        ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) :
    ⦃inv.1 init} forIn' xs init f ⦃inv} :=
-  Spec.forIn'_list (fun p => inv.1 p.1, inv.2) (fun b _ x hx _ _ => step x hx b)
+  Spec.forIn'_list (fun p => inv.1 p.2, inv.2) (fun b _ x hx _ _ => step x hx b)

@[spec]
 theorem Spec.forIn_list {α β : Type u}
    [Monad m] [WPMonad m ps]
    {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
-    (inv : PostCond (β × List.Zipper xs) ps)
+    (inv : Invariant xs β ps)
    (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f x b
        ⦃(fun r => match r with
-                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
-                   | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs, by simp⟩)} forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)} := by
+                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.reverse, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
  simp only [← forIn'_eq_forIn]
  exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h)

@ -374,18 +420,18 @@ theorem Spec.forIn_list_const_inv {α β : Type u}
        f hd b
        ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) :
    ⦃inv.1 init} forIn xs init f ⦃inv} :=
-  Spec.forIn_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b)
+  Spec.forIn_list (fun p => inv.1 p.2, inv.2) (fun b _ hd _ _ => step hd b)

@[spec]
 theorem Spec.foldlM_list {α β : Type u}
    [Monad m] [WPMonad m ps]
    {xs : List α} {init : β} {f : β → α → m β}
-    (inv : PostCond (β × List.Zipper xs) ps)
+    (inv : Invariant xs β ps)
    (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f b x
-        ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs, by simp⟩)} List.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)} := by
+        ⦃(fun b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs, by simp⟩, init)} List.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.reverse, [], by simp⟩, b), inv.2)} := by
  have : xs.foldlM f init = forIn xs init (fun a b => .yield <$> f b a) := by
    simp only [List.forIn_yield_eq_foldlM, id_map']
  rw[this]
@ -403,20 +449,20 @@ theorem Spec.foldlM_list_const_inv {α β : Type u}
        f b hd
        ⦃(fun b' => inv.1 b', inv.2)}) :
  ⦃inv.1 init} List.foldlM f init xs ⦃inv} :=
-    Spec.foldlM_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b)
+    Spec.foldlM_list (fun p => inv.1 p.2, inv.2) (fun b _ hd _ _ => step hd b)

@[spec]
 theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape}
    [Monad m] [WPMonad m ps]
    {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
-    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (inv : Invariant xs.toList β ps)
    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f x hx b
        ⦃(fun r => match r with
-                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
-                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by
+                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
  simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1]
  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (Std.Range.mem_of_mem_range' hx) suff h)

@ -424,14 +470,14 @@ theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape}
 theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape}
    [Monad m] [WPMonad m ps]
    {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)}
-    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (inv : Invariant xs.toList β ps)
    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f x b
        ⦃(fun r => match r with
-                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
-                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by
+                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
  simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
  apply Spec.forIn_list inv step

@ -439,14 +485,14 @@ theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape}
 theorem Spec.forIn'_array {α β : Type u}
    [Monad m] [WPMonad m ps]
    {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
-    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (inv : Invariant xs.toList β ps)
    (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f x hx b
        ⦃(fun r => match r with
-                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
-                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by
+                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
  cases xs
  simp
  apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h)
@ -455,14 +501,14 @@ theorem Spec.forIn'_array {α β : Type u}
 theorem Spec.forIn_array {α β : Type u}
    [Monad m] [WPMonad m ps]
    {xs : Array α} {init : β} {f : α → β → m (ForInStep β)}
-    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (inv : Invariant xs.toList β ps)
    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f x b
        ⦃(fun r => match r with
-                   | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩)
-                   | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by
+                   | .yield b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b')
+                   | .done b' => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
  cases xs
  simp
  apply Spec.forIn_list inv step
@ -471,12 +517,12 @@ theorem Spec.forIn_array {α β : Type u}
 theorem Spec.foldlM_array {α β : Type u}
    [Monad m] [WPMonad m ps]
    {xs : Array α} {init : β} {f : β → α → m β}
-    (inv : PostCond (β × List.Zipper xs.toList) ps)
+    (inv : Invariant xs.toList β ps)
    (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff),
-        ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)}
+        ⦃inv.1 (⟨rpref, x::suff, by simp [h]⟩, b)}
        f b x
-        ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)}) :
-    ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} Array.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by
+        ⦃(fun b' => inv.1 (⟨x::rpref, suff, by simp [h]⟩, b'), inv.2)}) :
+    ⦃inv.1 (⟨[], xs.toList, by simp⟩, init)} Array.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.toList.reverse, [], by simp⟩, b), inv.2)} := by
  cases xs
  simp
  apply Spec.foldlM_list inv step
--- a/src/Std/Do/WP/Basic.lean
+++ b/src/Std/Do/WP/Basic.lean
@ -98,13 +98,13 @@ instance Except.instWP : WP (Except ε) (.except ε .pure) :=
  inferInstanceAs (WP (ExceptT ε Id) (.except ε .pure))

 theorem Id.by_wp {α : Type u} {x : α} {prog : Id α} (h : Id.run prog = x) (P : α → Prop) :
-  (⊢ₛ wp⟦prog⟧ (PostCond.total (fun a => ⟨P a⟩))) → P x := h ▸ (· True.intro)
+  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow (fun a => ⟨P a⟩))) → P x := h ▸ (· True.intro)

 theorem StateM.by_wp {α} {x : α × σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) :
-  (⊢ₛ wp⟦prog⟧ (PostCond.total (fun a s' => ⟨P (a, s')⟩)) s) → P x := h ▸ (· True.intro)
+  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow (fun a s' => ⟨P (a, s')⟩)) s) → P x := h ▸ (· True.intro)

 theorem ReaderM.by_wp {α} {x : α} {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) :
-  (⊢ₛ wp⟦prog⟧ (PostCond.total (fun a _ => ⟨P a⟩)) r) → P x := h ▸ (· True.intro)
+  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow (fun a _ => ⟨P a⟩)) r) → P x := h ▸ (· True.intro)

 theorem Except.by_wp {α} {x : Except ε α} (P : Except ε α → Prop) :
  (⊢ₛ wp⟦x⟧ post⟨fun a => ⟨P (.ok a)⟩, fun e => ⟨P (.error e)⟩⟩) → P x := by
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@ -148,9 +148,9 @@ macro (name := mleave) "mleave" : tactic =>
              $(mkIdent ``Std.Do.SVal.uncurry_nil):term,
              $(mkIdent ``Std.Do.SVal.getThe_here):term,
              $(mkIdent ``Std.Do.SVal.getThe_there):term,
-              $(mkIdent ``Std.Do.FailConds.entails.refl):term,
-              $(mkIdent ``Std.Do.FailConds.entails_true):term,
-              $(mkIdent ``Std.Do.FailConds.entails_false):term,
+              $(mkIdent ``Std.Do.ExceptConds.entails.refl):term,
+              $(mkIdent ``Std.Do.ExceptConds.entails_true):term,
+              $(mkIdent ``Std.Do.ExceptConds.entails_false):term,
              $(mkIdent ``ULift.down_ite):term,
              $(mkIdent ``ULift.down_dite):term,
              $(mkIdent ``and_imp):term,
--- a/tests/lean/run/bhaviksSampler.lean
+++ b/tests/lean/run/bhaviksSampler.lean
@ -152,7 +152,7 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] :
  sampler (m:=m) n k h
  ⦃⇓ xs => ⌜xs.toList.Nodup⌝⦄ := by
  mvcgen -leave [sampler]
-  case inv => exact (⇓ (midway, xs) => ⌜Midway.valid midway xs.rpref.length⌝)
+  case inv => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.rpref.length⌝)
  -- case step => simp_all
  case post.success =>
    dsimp
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@ -87,7 +87,7 @@ theorem sum_loop_spec :
  mintro -
  unfold sum_loop
  mspec
-  case inv => exact (⇓ (r, xs) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
+  case inv => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
  all_goals simp_all +decide; try omega
  intros
  mintro _
@ -155,7 +155,7 @@ theorem throwing_loop_spec :
  mspec
  mspec
  mspec
-  case inv => exact post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
+  case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩
  case post.success =>
    mspec
    mspec
@ -181,7 +181,7 @@ theorem beaking_loop_spec :
  dsimp only [breaking_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
  mspec
  mspec
-  case inv => exact (⇓ (r, xs) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
+  case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
  all_goals simp_all
  case post =>
    intro _ h
@ -204,7 +204,7 @@ theorem returning_loop_spec :
  dsimp only [returning_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
  mspec
  mspec
-  case inv => exact (⇓ (r, xs) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
+  case inv => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
  all_goals simp_all
  case post =>
    split
@ -245,7 +245,7 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
  if h : n = 0 then simp [h] else
  simp only [h, reduceIte]
  mspec -- Spec.pure
-  mspec Spec.forIn_range (⇓ (⟨a, b⟩, xs) => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
+  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
  case step => dsimp; intros; mintro _; simp_all
  simp_all [Nat.sub_one_add_one]

@ -256,19 +256,19 @@ theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_sp
  mintro -
  simp only [fib_impl, h, reduceIte]
  mspec
-  mspec Spec.forIn_range (⇓ (⟨a, b⟩, xs) => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
+  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step
  case step => dsimp; intros; mintro _; mspec; mspec; simp_all
  simp_all [Nat.sub_one_add_one]

 theorem fib_impl_vcs
    (Q : Nat → PostCond Nat PostShape.pure)
    (I : (n : Nat) → (_ : ¬n = 0) →
-      PostCond (MProd Nat Nat × Std.List.Zipper [1:n].toList) PostShape.pure)
+      Invariant [1:n].toList (MProd Nat Nat) PostShape.pure)
    (ret : ⊢ₛ (Q 0).1 0)
-    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 (⟨0, 1⟩, Std.List.Zipper.begin _))
-    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 (r, Std.List.Zipper.end _) ⊢ₛ (Q n).1 r.snd)
+    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨Std.List.Zipper.begin _, 0, 1⟩)
+    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨Std.List.Zipper.end _, r⟩ ⊢ₛ (Q n).1 r.2)
    (loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff),
-                  (I n hn).1 (r, ⟨rpref, x::suff, by simp[h]⟩) ⊢ₛ (I n hn).1 (⟨r.2, r.1+r.2⟩, ⟨x::rpref, suff, by simp[h]⟩))
+                  (I n hn).1 ⟨⟨rpref, x::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨x::rpref, suff, by simp[h]⟩, r.2, r.1+r.2⟩)
    : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
  apply fib_impl.fun_cases n _ ?case1 ?case2
  case case1 => intro h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec
@ -289,7 +289,7 @@ theorem fib_impl_vcs

 theorem fib_triple_vcs : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
  apply fib_impl_vcs
-  case I => intro n hn; exact (⇓ (⟨a, b⟩, xs) => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝)
+  case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝)
  case ret => mpure_intro; rfl
  case loop_pre => intros; mpure_intro; trivial
  case loop_post => simp_all [Nat.sub_one_add_one]
@ -407,14 +407,14 @@ open Code
 theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
  unfold fib_impl
  mvcgen
-  case inv => exact ⇓ (⟨a, b⟩, xs) =>
+  case inv => exact ⇓ (xs, ⟨a, b⟩) =>
    ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝
  all_goals simp_all +zetaDelta [Nat.sub_one_add_one]

 theorem fib_triple_step : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
  unfold fib_impl
  mvcgen (stepLimit := some 14) -- 13 still has a wp⟦·⟧
-  case inv => exact ⇓ (⟨a, b⟩, xs) =>
+  case inv => exact ⇓ ⟨xs, a, b⟩ =>
    ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝
  all_goals simp_all +zetaDelta [Nat.sub_one_add_one]

@ -431,12 +431,12 @@ theorem fib_triple_erase : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_sp
 theorem fib_impl_vcs
    (Q : Nat → PostCond Nat PostShape.pure)
    (I : (n : Nat) → (_ : ¬n = 0) →
-      PostCond (MProd Nat Nat × Std.List.Zipper [1:n].toList) PostShape.pure)
+      Invariant [1:n].toList (MProd Nat Nat) PostShape.pure)
    (ret : ⊢ₛ (Q 0).1 0)
-    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 (⟨0, 1⟩, Std.List.Zipper.begin _))
-    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 (r, Std.List.Zipper.end _) ⊢ₛ (Q n).1 r.snd)
+    (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 ⟨Std.List.Zipper.begin _, 0, 1⟩)
+    (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 ⟨Std.List.Zipper.end _, r⟩ ⊢ₛ (Q n).1 r.2)
    (loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff),
-                  (I n hn).1 (r, ⟨rpref, x::suff, by simp[h]⟩) ⊢ₛ (I n hn).1 (⟨r.2, r.1+r.2⟩, ⟨x::rpref, suff, by simp[h]⟩))
+                  (I n hn).1 ⟨⟨rpref, x::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨x::rpref, suff, by simp[h]⟩, r.2, r.1+r.2⟩)
    : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
  unfold fib_impl
  mvcgen
@ -484,7 +484,7 @@ theorem sum_loop_spec :
  -- cf. `ByHand.sum_loop_spec`
  mintro -
  mvcgen [sum_loop]
-  case inv => exact (⇓ (r, xs) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
+  case inv => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
  all_goals simp_all +decide; try grind

 theorem throwing_loop_spec :
@ -493,7 +493,7 @@ theorem throwing_loop_spec :
  ⦃post⟨fun _ _ => ⌜False⌝,
        fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
  mvcgen [throwing_loop]
-  case inv => exact post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝,
+  case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝,
                         fun e s => ⌜e = 42 ∧ s = 4⌝⟩
  case pre1 => simp_all only [SVal.curry_nil]; decide
  case post.success => simp_all only [SVal.curry_nil]; grind
@ -506,7 +506,7 @@ theorem test_loop_break :
  breaking_loop
  ⦃⇓ r => ⌜r > 4 ∧ ‹Nat›ₛ = 1⌝⦄ := by
  mvcgen [breaking_loop]
-  case inv => exact (⇓ (r, xs) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
+  case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
  case pre1 => simp_all
  case isTrue => intro _; mleave; grind
  case isFalse => intro _; simp_all only [SVal.curry_nil]; grind
@ -522,7 +522,7 @@ theorem test_loop_early_return :
  returning_loop
  ⦃⇓ r s => ⌜r = 42 ∧ s = 4⌝⦄ := by
  mvcgen [returning_loop]
-  case inv => exact (⇓ (r, xs) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
+  case inv => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
  case isTrue => intro _; mleave; grind
  case isFalse => intro _; mleave; grind
  case pre1 => simp_all
@ -559,7 +559,7 @@ theorem test_sum :
    pure (f := Id) x
  ⦃⇓r => ⌜r < 30⌝⦄ := by
  mvcgen
-  case inv => exact (⇓ (r, xs) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
+  case inv => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
  case step =>
    simp_all
    omega
@ -606,7 +606,7 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
  · intro h
    apply Id.by_wp (P := (· = true)) rfl
    mvcgen
-    case inv => exact (⇓ (r, xs) => ⌜r.1 = none ∧ ∀ x, x ∈ xs.suff → p x⌝)
+    case inv => exact (⇓ (xs, r) => ⌜r.1 = none ∧ ∀ x, x ∈ xs.suff → p x⌝)
    case pre1 => simp; intro a ha; apply h a ha.upper
    all_goals simp_all
  · intro ht i hin
@ -616,7 +616,7 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
      have hin : i ∈ [0:n] := by simp [Std.instMembershipNatRange, hin]
      apply Id.by_wp (P := (· = false)) rfl
      mvcgen
-      case inv => exact (⇓ (r, xs) =>
+      case inv => exact (⇓ (xs, r) =>
        match r.1 with
        | none => ⌜i ∈ xs.suff⌝
        | some b => ⌜b = false ∧ xs.suff = []⌝)
@ -769,7 +769,7 @@ def max_and_sum (xs : Array Nat) : Id (Nat × Nat) := do
 theorem max_and_sum_spec (xs : Array Nat) :
    ⦃⌜∀ i, (h : i < xs.size) → xs[i] ≥ 0⌝⦄ max_and_sum xs ⦃⇓ (m, s) => ⌜s ≤ m * xs.size⌝⦄ := by
  mvcgen [max_and_sum]
-  case inv => exact (⇓ (⟨m, s⟩, xs) => ⌜s ≤ m * xs.rpref.length⌝)
+  case inv => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.rpref.length⌝)
  all_goals simp_all
  · rw [Nat.left_distrib]
    simp +zetaDelta only [Nat.mul_one, Nat.add_le_add_iff_right]
@ -916,14 +916,14 @@ theorem naive_expo_correct (x n : Nat) : naive_expo x n = x^n := by
  generalize h : naive_expo x n = r
  apply Id.by_wp h
  mvcgen
-  case inv => exact ⇓⟨r, xs⟩ => ⌜r = x^xs.pref.length⌝
+  case inv => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.rpref.length⌝
  all_goals simp_all [Nat.pow_add_one]

 theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
  generalize h : fast_expo x n = r
  apply Id.by_wp h
  mvcgen
-  case inv => exact ⇓⟨⟨e, x', y⟩, xs⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.pref.length⌝
+  case inv => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.rpref.length⌝
  all_goals simp_all
  case isFalse.isFalse b _ _ _ _ _ _ _ _ _ _ ih _ =>
    obtain ⟨e, y, x'⟩ := b
--- a/tests/lean/run/pairsSumToZero.lean
+++ b/tests/lean/run/pairsSumToZero.lean
@ -0,0 +1,127 @@
+/-
+This is from Markus's blog post on monadic reasoning:
+https://markushimmel.de/blog/my-first-verified-imperative-program/
+-/
+
+import Std.Data.HashSet.Lemmas
+import Std.Tactic.Do
+
+open Std Do
+
+/-!
+# Missing standard library material that will be part of a future Lean release
+-/
+
+namespace List
+
+theorem exists_mem_iff_exists_getElem (P : α → Prop) (l : List α) :
+    (∃ x ∈ l, P x) ↔ ∃ (i : Nat), ∃ hi, P (l[i]'hi) := by
+  grind [mem_iff_getElem]
+
+/--
+`l.ExistsPair P` asserts that there are indices `i` and `j` such that `i < j` and `P l[i] l[j]` is true.
+-/
+structure ExistsPair (P : α → α → Prop) (l : List α) where
+  not_pairwise : ¬l.Pairwise (¬P · ·)
+
+theorem existsPair_iff_not_pairwise {P : α → α → Prop} {l : List α} :
+    l.ExistsPair P ↔ ¬l.Pairwise (fun x y => ¬P x y) := by
+  grind [ExistsPair]
+
+@[simp, grind]
+theorem not_existsPair_nil {P : α → α → Prop} : ¬[].ExistsPair P := by
+  simp [existsPair_iff_not_pairwise]
+
+@[simp, grind]
+theorem existsPair_cons {P : α → α → Prop} {x : α} {xs : List α} :
+    (x::xs).ExistsPair P  ↔ (∃ y ∈ xs, P x y) ∨ xs.ExistsPair P := by
+  grind [List.existsPair_iff_not_pairwise, pairwise_iff_forall_sublist]
+
+@[simp, grind]
+theorem existsPair_append {P : α → α → Prop} {xs ys : List α} :
+    (xs ++ ys).ExistsPair P ↔ xs.ExistsPair P ∨ ys.ExistsPair P ∨ (∃ x ∈ xs, ∃ y ∈ ys, P x y) := by
+  grind [List.existsPair_iff_not_pairwise]
+
+end List
+
+-- Tell Lean that it doesn't need to warn us that `mvcgen` is still a pre-release.
+set_option mvcgen.warning false
+
+/-!
+# Imperative implementation
+-/
+
+def pairsSumToZero (l : List Int) : Bool := Id.run do
+  let mut seen : HashSet Int := ∅
+
+  for x in l do
+    if -x ∈ seen then
+      return true
+    seen := seen.insert x
+
+  return false
+
+/-!
+# Verification of imperative implementation
+-/
+
+theorem pairsSumToZero_correct (l : List Int) : pairsSumToZero l ↔ l.ExistsPair (fun a b => a + b = 0) := by
+  generalize h : pairsSumToZero l = r
+  apply Id.by_wp h
+
+  mvcgen
+
+  case inv =>
+    exact Invariant.withEarlyReturn
+      (onReturn := fun r b => ⌜r = true ∧ l.ExistsPair (fun a b => a + b = 0)⌝)
+      (onContinue := fun traversalState seen =>
+        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.rpref) ∧ ¬traversalState.pref.ExistsPair (fun a b => a + b = 0)⌝)
+
+  all_goals simp_all <;> grind
+
+/--
+trace: l : List Int
+⊢ (match
+          (forIn l ⟨none, ∅⟩ fun x r =>
+                if -x ∈ r.snd then pure (ForInStep.done ⟨some true, r.snd⟩)
+                else pure (ForInStep.yield ⟨none, r.snd.insert x⟩)).run.fst with
+        | none => pure false
+        | some a => pure a).run =
+      true ↔
+    List.ExistsPair (fun a b => a + b = 0) l
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+theorem pairsSumToZero_correct_directly (l : List Int) : pairsSumToZero l ↔ l.ExistsPair (fun a b => a + b = 0) := by
+  simp [pairsSumToZero]
+  trace_state
+  -- give up; need lemma about `forIn`
+  admit
+
+namespace Functional
+
+/-!
+# Bonus: functional implementation
+-/
+
+def pairsSumToZero (l : List Int) : Bool :=
+  go l ∅
+where
+  go (m : List Int) (seen : HashSet Int) : Bool :=
+    match m with
+    | [] => false
+    | x::xs => if -x ∈ seen then true else go xs (seen.insert x)
+
+/-!
+# Bonus: verification of functional implementation
+-/
+
+theorem pairsSumToZero_go_iff (l : List Int) (seen : HashSet Int) :
+    pairsSumToZero.go l seen = true ↔
+      l.ExistsPair (fun a b => a + b = 0) ∨ ∃ a ∈ seen, ∃ b ∈ l, a + b = 0 := by
+  fun_induction pairsSumToZero.go <;> simp_all <;> grind
+
+theorem pairsSumToZero_iff (l : List Int) :
+    pairsSumToZero l = true ↔ l.ExistsPair (fun a b => a + b = 0) := by
+  simp [pairsSumToZero, pairsSumToZero_go_iff]