feat: Upstream MPL.SPred.* from mpl (#8745)

This PR adds a logic of stateful predicates `SPred` to `Std.Do` in order to support reasoning about monadic programs. It comes with a dedicated proof mode the tactics of which are accessible by importing `Std.Tactic.Do`. Co-authored-by: Sebastian Graf <sg@lean-fro.org>
2025-06-20 17:13:40 +02:00 · 2025-06-20 17:13:40 +02:00 · 61ee83f73b
commit 61ee83f73b
parent 26b7e49c05
35 changed files with 3029 additions and 0 deletions
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@ -1790,6 +1790,307 @@ macro (name := bvNormalizeMacro) (priority:=low) "bv_normalize" optConfig : tact
  Macro.throwError "to use `bv_normalize`, please include `import Std.Tactic.BVDecide`"


+/--
+`massumption` is like `assumption`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q : SPred σs) : Q ⊢ₛ P → Q := by
+  mintro _ _
+  massumption
+```
+-/
+macro (name := massumptionMacro) (priority:=low) "massumption" : tactic =>
+  Macro.throwError "to use `massumption`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mclear` is like `clear`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
+  mintro HP
+  mintro HQ
+  mclear HP
+  mexact HQ
+```
+-/
+macro (name := mclearMacro) (priority:=low) "mclear" : tactic =>
+  Macro.throwError "to use `mclear`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mconstructor` is like `constructor`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
+  mintro HQ
+  mconstructor <;> mexact HQ
+```
+-/
+macro (name := mconstructorMacro) (priority:=low) "mconstructor" : tactic =>
+  Macro.throwError "to use `mconstructor`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mexact` is like `exact`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (Q : SPred σs) : Q ⊢ₛ Q := by
+  mstart
+  mintro HQ
+  mexact HQ
+```
+-/
+macro (name := mexactMacro) (priority:=low) "mexact" : tactic =>
+  Macro.throwError "to use `mexact`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mexfalso` is like `exfalso`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
+  mintro HP
+  mexfalso
+  mexact HP
+```
+-/
+macro (name := mexfalsoMacro) (priority:=low) "mexfalso" : tactic =>
+  Macro.throwError "to use `mexfalso`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mexists` is like `exists`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
+  mintro H
+  mexists 42
+```
+-/
+macro (name := mexistsMacro) (priority:=low) "mexists" : tactic =>
+  Macro.throwError "to use `mexists`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mframe` infers which hypotheses from the stateful context can be moved into the pure context.
+This is useful because pure hypotheses "survive" the next application of modus ponens
+(`Std.Do.SPred.mp`) and transitivity (`Std.Do.SPred.entails.trans`).
+
+It is used as part of the `mspec` tactic.
+
+```lean
+example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
+  mintro _
+  mframe
+  /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/
+  mcases h with hP
+  mexact h
+```
+-/
+macro (name := mframeMacro) (priority:=low) "mframe" : tactic =>
+  Macro.throwError "to use `mframe`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mhave` is like `have`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
+  mexact HQ
+```
+-/
+macro (name := mhaveMacro) (priority:=low) "mhave" : tactic =>
+  Macro.throwError "to use `mhave`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mreplace` is like `replace`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
+  mexact HPQ
+```
+-/
+macro (name := mreplaceMacro) (priority:=low) "mreplace" : tactic =>
+  Macro.throwError "to use `mreplace`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mleft` is like `left`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
+  mintro HP
+  mleft
+  mexact HP
+```
+-/
+macro (name := mleftMacro) (priority:=low) "mleft" : tactic =>
+  Macro.throwError "to use `mleft`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mright` is like `right`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by
+  mintro HP
+  mright
+  mexact HP
+```
+-/
+macro (name := mrightMacro) (priority:=low) "mright" : tactic =>
+  Macro.throwError "to use `mright`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mpure` moves a pure hypothesis from the stateful context into the pure context.
+```lean
+example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
+  mintro Hφ
+  mpure Hφ
+  mexact (ψ Hφ)
+```
+-/
+macro (name := mpureMacro) (priority:=low) "mpure" : tactic =>
+  Macro.throwError "to use `mpure`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mpure_intro` operates on a stateful `Std.Do.SPred` goal of the form `P ⊢ₛ ⌜φ⌝`.
+It leaves the stateful proof mode (thereby discarding `P`), leaving the regular goal `φ`.
+```lean
+theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
+  mpure_intro
+  exact True.intro
+```
+-/
+macro (name := mpureIntroMacro) (priority:=low) "mpure_intro" : tactic =>
+  Macro.throwError "to use `mpure_intro`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mrevert` is like `revert`, but operating on a stateful `Std.Do.SPred` goal.
+```lean
+example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
+  mintro ⟨HP, HQ, HR⟩
+  mrevert HR
+  mrevert HP
+  mintro HP'
+  mintro HR'
+  mexact HR'
+```
+-/
+macro (name := mrevertMacro) (priority:=low) "mrevert" : tactic =>
+  Macro.throwError "to use `mrevert`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mspecialize` is like `specialize`, but operating on a stateful `Std.Do.SPred` goal.
+It specializes a hypothesis from the stateful context with hypotheses from either the pure
+or stateful context or pure terms.
+```lean
+example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mspecialize HPQ HP
+  mexact HPQ
+
+example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
+  mintro HQ HΨ
+  mspecialize HΨ (y + 1) hP HQ
+  mexact HΨ
+```
+-/
+macro (name := mspecializeMacro) (priority:=low) "mspecialize" : tactic =>
+  Macro.throwError "to use `mspecialize`, please include `import Std.Tactic.Do`"
+
+
+/--
+`mspecialize_pure` is like `mspecialize`, but it specializes a hypothesis from the
+*pure* context with hypotheses from either the pure or stateful context or pure terms.
+```lean
+example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
+  mintro HQ
+  mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
+  mexact HΨ
+```
+-/
+macro (name := mspecializePureMacro) (priority:=low) "mspecialize_pure" : tactic =>
+  Macro.throwError "to use `mspecialize_pure`, please include `import Std.Tactic.Do`"
+
+
+/--
+Start the stateful proof mode of `Std.Do.SPred`.
+This will transform a stateful goal of the form `H ⊢ₛ T` into `⊢ₛ H → T`
+upon which `mintro` can be used to re-introduce `H` and give it a name.
+It is often more convenient to use `mintro` directly, which will
+try `mstart` automatically if necessary.
+-/
+macro (name := mstartMacro) (priority:=low) "mstart" : tactic =>
+  Macro.throwError "to use `mstart`, please include `import Std.Tactic.Do`"
+
+
+/--
+Stops the stateful proof mode of `Std.Do.SPred`.
+This will simply forget all the names given to stateful hypotheses and pretty-print
+a bit differently.
+-/
+macro (name := mstopMacro) (priority:=low) "mstop" : tactic =>
+  Macro.throwError "to use `mstop`, please include `import Std.Tactic.Do`"
+
+
+/--
+Like `rcases`, but operating on stateful `Std.Do.SPred` goals.
+Example: Given a goal `h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R`,
+`mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩` will yield two goals:
+`(hq : Q, hqr : Q → R) ⊢ₛ R` and `(hr : R) ⊢ₛ R`.
+
+That is, `mcases h with pat` has the following semantics, based on `pat`:
+* `pat=□h'` renames `h` to `h'` in the stateful context, regardless of whether `h` is pure
+* `pat=⌜h'⌝` introduces `h' : φ`  to the pure local context if `h : ⌜φ⌝`
+  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`)
+* `pat=h'` is like `pat=⌜h'⌝` if `h` is pure
+  (c.f. `Lean.Elab.Tactic.Do.ProofMode.IsPure`), otherwise it is like `pat=□h'`.
+* `pat=_` renames `h` to an inaccessible name
+* `pat=-` discards `h`
+* `⟨pat₁, pat₂⟩` matches on conjunctions and existential quantifiers and recurses via
+  `pat₁` and `pat₂`.
+* `⟨pat₁ | pat₂⟩` matches on disjunctions, matching the left alternative via `pat₁` and the right
+  alternative via `pat₂`.
+-/
+macro (name := mcasesMacro) (priority:=low) "mcases" : tactic =>
+  Macro.throwError "to use `mcases`, please include `import Std.Tactic.Do`"
+
+
+/--
+Like `refine`, but operating on stateful `Std.Do.SPred` goals.
+```lean
+example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
+  mintro ⟨HP, HQ, HR⟩
+  mrefine ⟨HP, HR⟩
+
+example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
+  mintro H
+  mrefine ⟨⌜42⌝, H⟩
+```
+-/
+macro (name := mrefineMacro) (priority:=low) "mrefine" : tactic =>
+  Macro.throwError "to use `mrefine`, please include `import Std.Tactic.Do`"
+
+
+/--
+Like `intro`, but introducing stateful hypotheses into the stateful context of the `Std.Do.SPred`
+proof mode.
+That is, given a stateful goal `(hᵢ : Hᵢ)* ⊢ₛ P → T`, `mintro h` transforms
+into `(hᵢ : Hᵢ)*, (h : P) ⊢ₛ T`.
+
+Furthermore, `mintro ∀s` is like `intro s`, but preserves the stateful goal.
+That is, `mintro ∀s` brings the topmost state variable `s:σ` in scope and transforms
+`(hᵢ : Hᵢ)* ⊢ₛ T` (where the entailment is in `Std.Do.SPred (σ::σs)`) into
+`(hᵢ : Hᵢ s)* ⊢ₛ T s` (where the entailment is in `Std.Do.SPred σs`).
+
+Beyond that, `mintro` supports the full syntax of `mcases` patterns
+(`mintro pat = (mintro h; mcases h with pat`), and can perform multiple
+introductions in sequence.
+-/
+macro (name := mintroMacro) (priority:=low) "mintro" : tactic =>
+  Macro.throwError "to use `mintro`, please include `import Std.Tactic.Do`"
+
 end Tactic

 namespace Attr
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@ -52,3 +52,4 @@ import Lean.Elab.Tactic.ExposeNames
 import Lean.Elab.Tactic.SimpArith
 import Lean.Elab.Tactic.Show
 import Lean.Elab.Tactic.Lets
+import Lean.Elab.Tactic.Do
--- a/src/Lean/Elab/Tactic/Do.lean
+++ b/src/Lean/Elab/Tactic/Do.lean
@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Lean.Elab.Tactic.Do.ProofMode
--- a/src/Lean/Elab/Tactic/Do/ProofMode.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode.lean
@ -0,0 +1,23 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Display
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Clear
+import Lean.Elab.Tactic.Do.ProofMode.Intro
+import Lean.Elab.Tactic.Do.ProofMode.Revert
+import Lean.Elab.Tactic.Do.ProofMode.Exact
+import Lean.Elab.Tactic.Do.ProofMode.Assumption
+import Lean.Elab.Tactic.Do.ProofMode.Pure
+import Lean.Elab.Tactic.Do.ProofMode.Frame
+import Lean.Elab.Tactic.Do.ProofMode.LeftRight
+import Lean.Elab.Tactic.Do.ProofMode.Constructor
+import Lean.Elab.Tactic.Do.ProofMode.Specialize
+import Lean.Elab.Tactic.Do.ProofMode.Cases
+import Lean.Elab.Tactic.Do.ProofMode.Exfalso
+import Lean.Elab.Tactic.Do.ProofMode.Have
+import Lean.Elab.Tactic.Do.ProofMode.Refine
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean
@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Exact
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+theorem Assumption.assumption_l {σs : List Type} {P Q R : SPred σs} (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R :=
+  SPred.and_elim_l.trans h
+theorem Assumption.assumption_r {σs : List Type} {P Q R : SPred σs} (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R :=
+  SPred.and_elim_r.trans h
+
+partial def MGoal.assumption (goal : MGoal) : OptionT MetaM Expr := do
+  if let some _ := parseEmptyHyp? goal.hyps then
+    failure
+  if let some hyp := parseHyp? goal.hyps then
+    guard (← isDefEq hyp.p goal.target)
+    return mkApp2 (mkConst ``SPred.entails.refl) goal.σs hyp.p
+  if let some (σs, lhs, rhs) := parseAnd? goal.hyps then
+    -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display).
+    mkApp5 (mkConst ``Assumption.assumption_r) σs lhs rhs goal.target <$> assumption { goal with hyps := rhs }
+    <|>
+    mkApp5 (mkConst ``Assumption.assumption_l) σs lhs rhs goal.target <$> assumption { goal with hyps := lhs }
+  else
+    panic! s!"assumption: hypothesis without proper metadata: {goal.hyps}"
+
+def MGoal.assumptionPure (goal : MGoal) : OptionT MetaM Expr := do
+  let φ := mkApp2 (mkConst ``SPred.tautological) goal.σs goal.target
+  let fvarId ← OptionT.mk (findLocalDeclWithType? φ)
+  let inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ goal.σs goal.target)
+  return mkApp6 (mkConst ``Exact.from_tautology) φ goal.σs goal.hyps goal.target inst (.fvar fvarId)
+
+@[builtin_tactic Lean.Parser.Tactic.massumption]
+def elabMAssumption : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+
+  let some proof ← liftMetaM <|
+    goal.assumption <|> goal.assumptionPure
+    | throwError "hypothesis not found"
+  mvar.assign proof
+  replaceMainGoal []
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean
@ -0,0 +1,60 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Lean.Meta
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab.Tactic Meta
+
+structure MStartResult where
+  goal : MGoal
+  proof? : Option Expr := none
+
+def mStart (goal : Expr) : MetaM MStartResult := do
+  -- check if already in proof mode
+  if let some mgoal := parseMGoal? goal then
+    return { goal := mgoal }
+
+  let listType := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero))
+  let σs ← mkFreshExprMVar listType
+  let P ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs)
+  let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) goal σs P)
+  let prf := mkApp4 (mkConst ``ProofMode.start_entails) σs P goal inst
+  let goal : MGoal := { σs,  hyps := emptyHyp σs, target := ← instantiateMVars P }
+  return { goal, proof? := some prf }
+
+def mStartMVar (mvar : MVarId) : MetaM (MVarId × MGoal) := mvar.withContext do
+  let goal ← instantiateMVars <| ← mvar.getType
+  unless ← isProp goal do
+    throwError "type mismatch\n{← mkHasTypeButIsExpectedMsg (← inferType goal) (mkSort .zero)}"
+
+  let result ← mStart goal
+  if let some proof := result.proof? then
+    let subgoal ←
+      mkFreshExprSyntheticOpaqueMVar result.goal.toExpr (← mvar.getTag)
+    mvar.assign (mkApp proof subgoal)
+    return (subgoal.mvarId!, result.goal)
+  else
+    return (mvar, result.goal)
+
+@[builtin_tactic Lean.Parser.Tactic.mstart]
+def elabMStart : Tactic | _ => do
+  let (mvar, _) ← mStartMVar (← getMainGoal)
+  replaceMainGoal [mvar]
+
+@[builtin_tactic Lean.Parser.Tactic.mstop]
+def elabMStop : Tactic | _ => do
+  -- parse goal
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let goal ← instantiateMVars <| ← mvar.getType
+
+  -- check if already in proof mode
+  let some mgoal := parseMGoal? goal | throwError "not in proof mode"
+  mvar.setType mgoal.strip
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean
@ -0,0 +1,233 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Pure
+import Lean.Elab.Tactic.Do.ProofMode.Intro
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do Lean.Parser.Tactic
+open Lean Elab Tactic Meta
+
+initialize registerTraceClass `Meta.Tactic.Do.cases
+
+theorem SCases.add_goal {σs} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T :=
+  hand.mp.trans hgoal
+
+theorem SCases.clear {σs} {Q H T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ∧ H ⊢ₛ T :=
+  (SPred.and_mono_r SPred.true_intro).trans hgoal
+
+theorem SCases.pure {σs} {Q T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ⊢ₛ T :=
+  (SPred.and_intro .rfl SPred.true_intro).trans hgoal
+
+theorem SCases.and_1 {σs} {Q H₁' H₂' H₁₂' T : SPred σs} (hand : H₁' ∧ H₂' ⊣⊢ₛ H₁₂') (hgoal : Q ∧ H₁₂' ⊢ₛ T) : (Q ∧ H₁') ∧ H₂' ⊢ₛ T :=
+  ((SPred.and_congr_r hand.symm).trans SPred.and_assoc.symm).mpr.trans hgoal
+
+theorem SCases.and_2 {σs} {Q H₁' H₂ T : SPred σs} (hgoal : (Q ∧ H₁') ∧ H₂ ⊢ₛ T) : (Q ∧ H₂) ∧ H₁' ⊢ₛ T :=
+  SPred.and_right_comm.mp.trans hgoal
+
+theorem SCases.and_3 {σs} {Q H₁ H₂ H T : SPred σs} (hand : H ⊣⊢ₛ H₁ ∧ H₂) (hgoal : (Q ∧ H₂) ∧ H₁ ⊢ₛ T) : Q ∧ H ⊢ₛ T :=
+  (SPred.and_congr_r hand).mp.trans (SPred.and_assoc.mpr.trans (SPred.and_right_comm.mp.trans hgoal))
+
+theorem SCases.exists {σs : List Type} {Q : SPred σs} {ψ : α → SPred σs} {T : SPred σs}
+  (h : ∀ a, Q ∧ ψ a ⊢ₛ T) : Q ∧ (∃ a, ψ a) ⊢ₛ T :=
+    SPred.imp_elim' (SPred.exists_elim fun a => SPred.imp_intro (SPred.entails.trans SPred.and_symm (h a)))
+
+class IsAnd {σs : List Type} (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where to_and : P ⊣⊢ₛ Q₁ ∧ Q₂
+instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl
+instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := SPred.pure_and.symm
+instance (σs) (P Q₁ Q₂ : σ → SPred σs) [base : ∀ s, IsAnd (P s) (Q₁ s) (Q₂ s)] : IsAnd (σs:=σ::σs) P Q₁ Q₂ where to_and := fun s => (base s).to_and
+
+-- Given σs and H, produces H₁, H₂ and a proof that H₁ ∧ H₂ ⊣⊢ₛ H.
+def synthIsAnd (σs H : Expr) : OptionT MetaM (Expr × Expr × Expr) := do
+  if let some (_σs, H₁, H₂) := parseAnd? H.consumeMData then
+    return (H₁, H₂, mkApp2 (mkConst ``SPred.bientails.refl) σs H)
+  try
+    let H₁ ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs)
+    let H₂ ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs)
+    let inst ← synthInstance (mkApp4 (mkConst ``IsAnd) σs H H₁ H₂)
+    return (H₁, H₂, mkApp5 (mkConst ``IsAnd.to_and) σs H H₁ H₂ inst)
+  catch _ => failure
+
+-- Produce a proof for Q ∧ H ⊢ₛ T by opening a new goal P ⊢ₛ T, where P ⊣⊢ₛ Q ∧ H.
+def mCasesAddGoal (goals : IO.Ref (Array MVarId)) (σs : Expr) (T : Expr) (Q : Expr) (H : Expr) : MetaM (Unit × MGoal × Expr) := do
+  let (P, hand) := mkAnd σs Q H
+  -- hand : Q ∧ H ⊣⊢ₛ P
+  -- Need to produce a proof that P ⊢ₛ T and return res
+  let goal : MGoal := { σs := σs, hyps := P, target := T }
+  let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr
+  goals.modify (·.push m.mvarId!)
+  let prf := mkApp7 (mkConst ``SCases.add_goal) σs P Q H T hand m
+  let goal := { goal with hyps := mkAnd! σs Q H }
+  return ((), goal, prf)
+
+private def getQH (goal : MGoal) : MetaM (Expr × Expr) := do
+  let some (_, Q, H) := parseAnd? goal.hyps | throwError m!"Internal error: Hypotheses not a conjunction {goal.hyps}"
+  return (Q, H)
+
+-- Pretty much like sPureCore, but for existential quantifiers.
+-- This function receives the hypothesis H=(∃ (x : α), ψ x) to destruct.
+-- It will provide a proof for Q ∧ H ⊢ₛ T
+-- if `k` produces a proof for Q ∧ ψ n ⊢ₛ T that may range over `name : α`.
+-- It calls `k` with name.
+def mCasesExists (H : Expr) (name : TSyntax ``binderIdent)
+  (k : Expr /-name:α-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do
+  let some (α, σs, ψ) := H.consumeMData.app3? ``SPred.exists | throwError "Not an existential quantifier {H}"
+  let (name, ref) ← getFreshHypName name
+  withLocalDeclD name α fun x => do
+    addLocalVarInfo ref (← getLCtx) x α
+    let (r, goal, prf /- : goal.toExpr -/) ← k x
+    let (Q, _) ← getQH goal
+    let u ← getLevel α
+    let prf := mkApp6 (mkConst ``SCases.exists [u]) α σs Q ψ goal.target (← mkLambdaFVars #[x] prf)
+    let goal := { goal with hyps := mkAnd! σs Q H }
+    return (r, goal, prf)
+
+-- goal is P ⊢ₛ T
+-- The caller focuses on hypothesis H, P ⊣⊢ₛ Q ∧ H.
+-- scasesCore on H, pat and k builds H ⊢ₛ H' according to pat, then calls k with H'
+-- k knows context Q and builds goal Q ∧ H' ⊢ₛ T and a proof of the goal.
+-- (k should not also apply H ⊢ₛ H' or unfocus because that does not work with spureCore which needs the see `P'` and not `Q ∧ _`.)
+-- then scasesCore builds a proof for Q ∧ H ⊢ₛ T from P' ⊢ₛ T:
+--   Q ∧ H ⊢ₛ Q ∧ H' ⊢ₛ P' ⊢ₛ T
+-- and finally the caller builds the proof for
+--   P ⊢ₛ Q ∧ H ⊢ₛ T
+-- by unfocussing.
+partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → MetaM (α × MGoal × Expr)): MetaM (α × MGoal × Expr) :=
+  match pat with
+  | .clear => do
+    let H' := emptyHyp σs -- H' = ⌜True⌝
+    let (a, goal, prf) ← k H'
+    let (Q, _H) ← getQH goal
+    -- prf : Q ∧ ⌜True⌝ ⊢ₛ T
+    -- Then Q ∧ H ⊢ₛ Q ∧ ⌜True⌝ ⊢ₛ T
+    let prf := mkApp5 (mkConst ``SCases.clear) σs Q H goal.target prf
+    let goal := { goal with hyps := mkAnd! σs Q H }
+    return (a, goal, prf)
+  | .stateful name => do
+    let (name, ref) ← getFreshHypName name
+    let uniq ← mkFreshId
+    let hyp := Hyp.mk name uniq H.consumeMData
+    addHypInfo ref σs hyp (isBinder := true)
+    k hyp.toExpr
+  | .pure name => do
+    mPureCore σs H name fun _ _hφ => do
+      -- This case is very similar to the clear case, but we need to
+      -- return Q ⊢ₛ T, not Q ∧ H ⊢ₛ T.
+      let H' := emptyHyp σs -- H' = ⌜True⌝
+      let (a, goal, prf) ← k H'
+      let (Q, _H) ← getQH goal
+      -- prf : Q ∧ ⌜True⌝ ⊢ₛ T
+      -- Then Q ⊢ₛ Q ∧ ⌜True⌝ ⊢ₛ T
+      let prf := mkApp4 (mkConst ``SCases.pure) σs Q goal.target prf
+      let goal := { goal with hyps := Q }
+      return (a, goal, prf)
+    -- Now prf : Q ∧ H ⊢ₛ T (where H is ⌜φ⌝). Exactly what is needed.
+  | .one name => do
+    try
+      -- First try to see if H can be introduced as a pure hypothesis
+      let φ ← mkFreshExprMVar (mkSort .zero)
+      let _ ← synthInstance (mkApp3 (mkConst ``IsPure) σs H φ)
+      mCasesCore σs H (.pure name) k
+    catch _ =>
+      -- Otherwise introduce it as a stateful hypothesis.
+      mCasesCore σs H (.stateful name) k
+  | .tuple [] => mCasesCore σs H .clear k
+  | .tuple [p] => mCasesCore σs H p k
+  | .tuple (p :: ps) => do
+    if let some (H₁, H₂, hand) ← synthIsAnd σs H then
+      -- goal is Q ∧ H ⊢ₛ T, where `hand : H ⊣⊢ₛ H₁ ∧ H₂`. Plan:
+      -- 1. Recurse on H₁ and H₂.
+      -- 2. The inner callback sees H₁' and H₂' and calls k on H₁₂', where H₁₂' = mkAnd H₁' H₂'
+      -- 3. The inner callback receives P' ⊢ₛ T, where (P' ⊣⊢ₛ Q ∧ H₁₂').
+      -- 4. The inner callback returns (Q ∧ H₁') ∧ H₂' ⊢ₛ T
+      -- 5. The outer callback receives (Q ∧ H₁') ∧ H₂ ⊢ₛ T
+      -- 6. The outer callback reassociates and returns (Q ∧ H₂) ∧ H₁' ⊢ₛ T
+      -- 7. The top-level receives (Q ∧ H₂) ∧ H₁ ⊢ₛ T
+      -- 8. Reassociate to Q ∧ (H₁ ∧ H₂) ⊢ₛ T, rebuild Q ∧ H ⊢ₛ T and return it.
+      let ((a, Q), goal, prf) ← mCasesCore σs H₁ p fun H₁' => do
+        let ((a, Q), goal, prf) ← mCasesCore σs H₂ (.tuple ps) fun H₂' => do
+          let (H₁₂', hand') := mkAnd σs H₁' H₂'
+          let (a, goal, prf) ← k H₁₂' -- (2)
+          -- (3) prf : Q ∧ H₁₂' ⊢ₛ T
+          -- (4) refocus to (Q ∧ H₁') ∧ H₂'
+          let (Q, _H) ← getQH goal
+          let T := goal.target
+          let prf := mkApp8 (mkConst ``SCases.and_1) σs Q H₁' H₂' H₁₂' T hand' prf
+          -- check prf
+          let QH₁' := mkAnd! σs Q H₁'
+          let goal := { goal with hyps := mkAnd! σs QH₁' H₂' }
+          return ((a, Q), goal, prf)
+        -- (5) prf : (Q ∧ H₁') ∧ H₂ ⊢ₛ T
+        -- (6) refocus to prf : (Q ∧ H₂) ∧ H₁' ⊢ₛ T
+        let prf := mkApp6 (mkConst ``SCases.and_2) σs Q H₁' H₂ goal.target prf
+        let QH₂ := mkAnd! σs Q H₂
+        let goal := { goal with hyps := mkAnd! σs QH₂ H₁' }
+        return ((a, Q), goal, prf)
+      -- (7) prf : (Q ∧ H₂) ∧ H₁ ⊢ₛ T
+      -- (8) rearrange to Q ∧ H ⊢ₛ T
+      let prf := mkApp8 (mkConst ``SCases.and_3) σs Q H₁ H₂ H goal.target hand prf
+      let goal := { goal with hyps := mkAnd! σs Q H }
+      return (a, goal, prf)
+    else if let some (_α, σs, ψ) := H.consumeMData.app3? ``SPred.exists then
+      let .one n := p
+        | throwError "cannot further destruct a term after moving it to the Lean context"
+      -- goal is Q ∧ (∃ x, ψ x) ⊢ₛ T. The plan is pretty similar to sPureCore:
+      -- 1. Recurse on ψ n where (n : α) is named according to the head pattern p.
+      -- 2. Receive a proof for Q ∧ ψ n ⊢ₛ T.
+      -- 3. Build a proof for Q ∧ (∃ x, ψ x) ⊢ₛ T from it (in sCasesExists).
+      mCasesExists H n fun x => mCasesCore σs (ψ.betaRev #[x]) (.alts ps) k
+    else throwError "Neither a conjunction nor an existential quantifier {H}"
+  | .alts [] => throwUnsupportedSyntax
+  | .alts [p] => mCasesCore σs H p k
+  | .alts (p :: ps) => do
+    let some (σs, H₁, H₂) := H.consumeMData.app3? ``SPred.or | throwError "Not a disjunction {H}"
+    -- goal is Q ∧ (H₁ ∨ H₂) ⊢ₛ T. Plan:
+    -- 1. Recurse on H₁ and H₂ with the same k.
+    -- 2. Receive proofs for Q ∧ H₁ ⊢ₛ T and Q ∧ H₂ ⊢ₛ T.
+    -- 3. Build a proof for Q ∧ (H₁ ∨ H₂) ⊢ₛ T from them.
+    let (_a, goal₁,  prf₁) ← mCasesCore σs H₁ p k
+    let (a,  _goal₂, prf₂) ← mCasesCore σs H₂ (.alts ps) k
+    let (Q, _H₁) ← getQH goal₁
+    let goal := { goal₁ with hyps := mkAnd! σs Q (mkApp3 (mkConst ``SPred.or) σs H₁ H₂) }
+    let prf := mkApp7 (mkConst ``SPred.and_or_elim_r) σs Q H₁ H₂ goal.target prf₁ prf₂
+    return (a, goal, prf)
+
+private theorem assembled_proof {σs} {P P' Q H H' T : SPred σs}
+  (hfocus : P ⊣⊢ₛ Q ∧ H) (hcases : H ⊢ₛ H') (hand : Q ∧ H' ⊣⊢ₛ P') (hprf₃ : P' ⊢ₛ T) : P ⊢ₛ T :=
+  hfocus.mp.trans ((SPred.and_mono_r hcases).trans (hand.mp.trans hprf₃))
+
+private theorem blah2 {σs} {P Q H R : SPred σs}
+  (h₁ : P ⊣⊢ₛ Q ∧ H) (h₂ : Q ∧ H ⊢ₛ R) : P ⊢ₛ R :=
+  h₁.mp.trans h₂
+
+private theorem blah3 {σs} {P Q H T : SPred σs}
+  (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T :=
+  hand.mp.trans hgoal
+
+@[builtin_tactic Lean.Parser.Tactic.mcases]
+def elabMCases : Tactic
+  | `(tactic| mcases $hyp:ident with $pat:mcasesPat) => do
+  let pat ← liftMacroM <| MCasesPat.parse pat
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  let focus ← goal.focusHypWithInfo hyp
+  -- goal : P ⊢ₛ T,
+  -- hfocus : P ⊣⊢ₛ Q ∧ H
+  let Q := focus.restHyps
+  let H := focus.focusHyp
+  let goals ← IO.mkRef #[]
+  let (_, _new_goal, prf) ← mCasesCore goal.σs H pat (mCasesAddGoal goals goal.σs goal.target Q)
+
+  -- Now prf : Q ∧ H ⊢ₛ T. Prepend hfocus.mp, done.
+  let prf := focus.rewriteHyps goal prf
+  -- check prf
+  mvar.assign prf
+  replaceMainGoal (← goals.get).toList
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean
@ -0,0 +1,32 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+theorem Clear.clear {σs : List Type} {P P' A Q : SPred σs}
+    (hfocus : P ⊣⊢ₛ P' ∧ A) (h : P' ⊢ₛ Q) : P ⊢ₛ Q :=
+    hfocus.mp.trans <| (SPred.and_mono_l h).trans SPred.and_elim_l
+
+@[builtin_tactic Lean.Parser.Tactic.mclear]
+def elabMClear : Tactic
+  | `(tactic| mclear $hyp:ident) => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+  let res ← goal.focusHypWithInfo hyp
+  let m ← mkFreshExprSyntheticOpaqueMVar (res.restGoal goal).toExpr
+
+  mvar.assign (mkApp7 (mkConst ``Clear.clear) goal.σs goal.hyps
+    res.restHyps res.focusHyp goal.target res.proof m)
+  replaceMainGoal [m.mvarId!]
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean
@ -0,0 +1,30 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+def mConstructorCore (mvar : MVarId) : MetaM (MVarId × MVarId) := do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+
+  let mkApp3 (.const ``SPred.and []) σs L R := goal.target | throwError "target is not SPred.and"
+
+  let leftGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := L}.toExpr
+  let rightGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := R}.toExpr
+  mvar.assign (mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps L R leftGoal rightGoal)
+  return (leftGoal.mvarId!, rightGoal.mvarId!)
+
+@[builtin_tactic Lean.Parser.Tactic.mconstructor]
+def elabMConstructor : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let (leftGoal, rightGoal) ← mConstructorCore mvar
+  replaceMainGoal [leftGoal, rightGoal]
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Display.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Display.lean
@ -0,0 +1,55 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Expr Meta PrettyPrinter Delaborator SubExpr
+
+syntax mgoalHyp := ident " : " term
+
+syntax mgoalStx := ppDedent(ppLine mgoalHyp)* ppDedent(ppLine "⊢ₛ " term)
+
+@[app_delab MGoalEntails]
+partial def delabMGoal : Delab := do
+  let expr ← instantiateMVars <| ← getExpr
+
+  -- extract environment
+  let some goal := parseMGoal? expr | failure
+
+  -- delaborate
+  let (_, hyps) ← withAppFn ∘ withAppArg <| delabHypotheses goal.σs ({}, #[])
+  let target ← SPred.Notation.unpack (← withAppArg <| delab)
+
+  -- build syntax
+  return ⟨← `(mgoalStx| $hyps.reverse* ⊢ₛ $target:term)⟩
+where
+  delabHypotheses (σs : Expr)
+      (acc : NameMap Nat × Array (TSyntax ``mgoalHyp)) :
+      DelabM (NameMap Nat × Array (TSyntax ``mgoalHyp)) := do
+    let hyps ← getExpr
+    if let some _ := parseEmptyHyp? hyps then
+      return acc
+    if let some hyp := parseHyp? hyps then
+      let mut (map, lines) := acc
+      let (idx, name') :=
+        if let some idx := map.find? hyp.name then
+          (idx + 1, hyp.name.appendAfter <| if idx == 0 then "✝" else "✝" ++ idx.toSuperscriptString)
+        else
+          (0, hyp.name)
+      let name' := mkIdent name'
+      let stx ← `(mgoalHyp| $name' : $(← SPred.Notation.unpack (← withMDataExpr <| delab)))
+      return (map.insert hyp.name idx, lines.push stx)
+    if (parseAnd? hyps).isSome then
+      let acc_rhs ← withAppArg <| delabHypotheses σs acc
+      let acc_lhs ← withAppFn ∘ withAppArg <| delabHypotheses σs acc_rhs
+      return acc_lhs
+    else
+      failure
+
+@[app_delab HypMarker]
+def delabHypMarker : Delab := do SPred.Notation.unpack (← withAppArg delab)
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean
@ -0,0 +1,50 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+theorem Exact.assumption {σs : List Type} {P P' A : SPred σs}
+  (h : P ⊣⊢ₛ P' ∧ A) : P ⊢ₛ A := h.mp.trans SPred.and_elim_r
+
+theorem Exact.from_tautology {σs : List Type} {P T : SPred σs} [PropAsSPredTautology φ T] (h : φ) : P ⊢ₛ T :=
+  SPred.true_intro.trans (PropAsSPredTautology.iff.mp h)
+
+def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exact (goal : MGoal) (hyp : Syntax) : OptionT MetaM Expr := do
+  if goal.findHyp? hyp.getId |>.isNone then failure
+  let focusRes ← goal.focusHypWithInfo ⟨hyp⟩
+  OptionT.mk do
+  let proof := mkApp5 (mkConst ``Exact.assumption) goal.σs goal.hyps focusRes.restHyps goal.target focusRes.proof
+  unless ← isDefEq focusRes.focusHyp goal.target do
+    throwError "mexact tactic failed, hypothesis {hyp} is not definitionally equal to {goal.target}"
+  return proof
+
+def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exactPure (goal : MGoal) (hyp : Syntax) : TacticM Expr := do
+  let φ ← mkFreshExprMVar (mkSort .zero)
+  let h ← elabTermEnsuringType hyp φ
+  let P ← mkFreshExprMVar (mkApp (mkConst ``SPred) goal.σs)
+  let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ goal.σs P)
+    | throwError "mexact tactic failed, {hyp} is not an SPred tautology"
+  return mkApp6 (mkConst ``Exact.from_tautology) φ goal.σs goal.hyps goal.target inst h
+
+@[builtin_tactic Lean.Parser.Tactic.mexact]
+def elabMExact : Tactic
+  | `(tactic| mexact $hyp:term) => do
+    let mvar ← getMainGoal
+    mvar.withContext do
+      let g ← instantiateMVars <| ← mvar.getType
+      let some goal := parseMGoal? g | throwError "not in proof mode"
+      if let some prf ← liftMetaM (goal.exact hyp) then
+    mvar.assign prf
+      else
+        mvar.assign (← goal.exactPure hyp)
+      replaceMainGoal []
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean
@ -0,0 +1,31 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+
+-- set_option pp.all true in
+-- #check ⌜False⌝
+private def falseProp (σs : Expr) : Expr := -- ⌜False⌝ standing in for an empty conjunction of hypotheses
+  mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``False)
+
+@[builtin_tactic Lean.Parser.Tactic.mexfalso]
+def elabMExfalso : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+  let newGoal := { goal with target := falseProp goal.σs }
+  let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+  let prf := mkApp4 (mkConst ``SPred.exfalso) goal.σs goal.hyps goal.target m
+  mvar.assign prf
+  replaceMainGoal [m.mvarId!]
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean
@ -0,0 +1,80 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Meta
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do ProofMode
+open Lean Elab.Tactic Meta
+
+/-- The result of focussing the context of a goal `goal : MGoal` on a particular hypothesis.
+The focussed hypothesis is returned as `focusHyp : Expr`, along with the
+residual `restHyps : Expr` and a `proof : Expr` for the property
+`goal.hyps ⊣⊢ₛ restHyps ∧ focusHyp`. -/
+structure FocusResult where
+  focusHyp : Expr
+  restHyps : Expr
+  proof : Expr
+  deriving Inhabited
+
+theorem focus_this {σs : List Type} {P : SPred σs} : P ⊣⊢ₛ ⌜True⌝ ∧ P :=
+  SPred.true_and.symm
+
+theorem focus_l {σs : List Type} {P P' Q C R : SPred σs} (h₁ : P ⊣⊢ₛ P' ∧ R) (h₂ : P' ∧ Q ⊣⊢ₛ C) :
+    P ∧ Q ⊣⊢ₛ C ∧ R :=
+  (SPred.and_congr_l h₁).trans (SPred.and_right_comm.trans (SPred.and_congr_l h₂))
+
+theorem focus_r {σs : List Type} {P Q Q' C R : SPred σs} (h₁ : Q ⊣⊢ₛ Q' ∧ R) (h₂ : P ∧ Q' ⊣⊢ₛ C) :
+    P ∧ Q ⊣⊢ₛ C ∧ R :=
+  (SPred.and_congr_r h₁).trans (SPred.and_assoc.symm.trans (SPred.and_congr_l h₂))
+
+partial def focusHyp (σs : Expr) (e : Expr) (name : Name) : Option FocusResult := do
+  if let some hyp := parseHyp? e then
+    if hyp.name = name then
+      return ⟨e, emptyHyp σs, mkApp2 (mkConst ``focus_this) σs e⟩
+    else
+      none
+  else if let some (σs, lhs, rhs) := parseAnd? e then
+    try
+      -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display).
+      let ⟨focus, rhs', h₁⟩ ← focusHyp σs rhs name
+      let ⟨C, h₂⟩ := mkAnd σs lhs rhs'
+      return ⟨focus, C, mkApp8 (mkConst ``focus_r) σs lhs rhs rhs' C focus h₁ h₂⟩
+    catch _ =>
+      let ⟨focus, lhs', h₁⟩ ← focusHyp σs lhs name
+      let ⟨C, h₂⟩ := mkAnd σs lhs' rhs
+      return ⟨focus, C, mkApp8 (mkConst ``focus_l) σs lhs lhs' rhs C focus h₁ h₂⟩
+  else if let some _ := parseEmptyHyp? e then
+    none
+  else
+    panic! s!"focusHyp: hypothesis without proper metadata: {e}"
+
+def MGoal.focusHyp (goal : MGoal) (name : Name) : Option FocusResult :=
+  Lean.Elab.Tactic.Do.ProofMode.focusHyp goal.σs goal.hyps name
+
+def FocusResult.refl (σs : Expr) (restHyps : Expr) (focusHyp : Expr) : FocusResult :=
+  let proof := mkApp2 (mkConst ``SPred.bientails.refl) σs (mkAnd! σs restHyps focusHyp)
+  { restHyps, focusHyp, proof }
+
+def FocusResult.restGoal (res : FocusResult) (goal : MGoal) : MGoal :=
+  { goal with hyps := res.restHyps }
+
+def FocusResult.recombineGoal (res : FocusResult) (goal : MGoal) : MGoal :=
+  { goal with hyps := mkAnd! goal.σs res.restHyps res.focusHyp }
+
+theorem FocusResult.rewrite_hyps {σs} {P Q R : SPred σs} (hrw : P ⊣⊢ₛ Q) (hgoal : Q ⊢ₛ R) : P ⊢ₛ R :=
+  hrw.mp.trans hgoal
+
+/-- Turn a proof for `(res.recombineGoal goal).toExpr` into one for `goal.toExpr`. -/
+def FocusResult.rewriteHyps (res : FocusResult) (goal : MGoal) : Expr → Expr :=
+  mkApp6 (mkConst ``rewrite_hyps) goal.σs goal.hyps (mkAnd! goal.σs res.restHyps res.focusHyp) goal.target res.proof
+
+def MGoal.focusHypWithInfo (goal : MGoal) (name : Ident) : MetaM FocusResult := do
+  let some res := goal.focusHyp name.getId | throwError "unknown hypothesis '{name}'"
+  let some hyp := parseHyp? res.focusHyp | throwError "impossible; res.focusHyp not a hypothesis"
+  addHypInfo name goal.σs hyp
+  pure res
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean
@ -0,0 +1,129 @@
+/-
+Copyright (c) 2025 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+class SimpAnd {σs : List Type} (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop where
+  simp_and : P ∧ Q ⊣⊢ₛ PQ
+
+instance (σs) (P Q : SPred σs) : SimpAnd P Q (spred(P ∧ Q)) where simp_and := .rfl
+instance (σs) (P : SPred σs) : SimpAnd P ⌜True⌝ P where simp_and := SPred.and_true
+instance (σs) (P : SPred σs) : SimpAnd ⌜True⌝ P P where simp_and := SPred.true_and
+
+class HasFrame {σs : List Type} (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where
+  reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝
+instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := SPred.true_and.symm
+instance (σs) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP]: HasFrame (σs:=σs) spred(P ∧ P') QP φ where
+  reassoc := ((SPred.and_congr_l HasFrame.reassoc).trans SPred.and_right_comm).trans (SPred.and_congr_l SimpAnd.simp_and)
+instance (σs) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ]: HasFrame (σs:=σs) spred(P ∧ P') PQ φ where
+  reassoc := ((SPred.and_congr_r HasFrame.reassoc).trans SPred.and_assoc.symm).trans (SPred.and_congr_l SimpAnd.simp_and)
+instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(⌜φ⌝ ∧ P) P φ where reassoc := SPred.and_comm
+instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(P ∧ ⌜φ⌝) P φ where reassoc := .rfl
+instance (σs) (P P' Q Q' QQ : SPred σs) [HasFrame P Q φ] [HasFrame P' Q' ψ] [SimpAnd Q Q' QQ]: HasFrame (σs:=σs) spred(P ∧ P') QQ (φ ∧ ψ) where
+  reassoc := (SPred.and_congr HasFrame.reassoc HasFrame.reassoc).trans
+             <| SPred.and_assoc.trans
+             <| (SPred.and_congr_r
+                  <| SPred.and_assoc.symm.trans
+                  <| (SPred.and_congr_l SPred.and_comm).trans
+                  <| SPred.and_assoc.trans
+                  <| SPred.and_congr_r SPred.pure_and).trans
+             <| SPred.and_assoc.symm.trans
+             <| SPred.and_congr_l SimpAnd.simp_and
+instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(⌜φ⌝ ∧ P) Q (φ ∧ ψ) where
+  reassoc := SPred.and_comm.trans
+             <| (SPred.and_congr_l HasFrame.reassoc).trans
+             <| SPred.and_right_comm.trans
+             <| SPred.and_assoc.trans
+             <| SPred.and_congr_r SPred.pure_and
+instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(P ∧ ⌜φ⌝) Q (ψ ∧ φ) where
+  reassoc := (SPred.and_congr_l HasFrame.reassoc).trans
+             <| SPred.and_right_comm.trans
+             <| SPred.and_assoc.trans
+             <| SPred.and_congr_r (SPred.and_comm.trans SPred.pure_and)
+-- The following instance comes last so that it gets the highest priority.
+-- It's the most efficient and best solution if valid
+instance {P : Prop} : HasFrame (σs:=[]) P ⌜True⌝ P where reassoc := SPred.true_and.symm
+
+-- #synth ∀ {w x P Q y z}, HasFrame spred(⌜w = 2⌝ ∧ ⌜x = 3⌝ ∧ P ∧ ⌜y = 4⌝ ∧ Q ∧ ⌜z=6⌝) _ _
+
+theorem Frame.frame {σs : List Type} {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ]
+  (h : φ → Q ⊢ₛ T) : P ⊢ₛ T := by
+    apply SPred.pure_elim
+    · exact HasFrame.reassoc.mp.trans SPred.and_elim_r
+    · intro hp
+      exact HasFrame.reassoc.mp.trans (SPred.and_elim_l' (h hp))
+
+/-- If `P'` is a conjunction of unnamed hypotheses that are a subset of the named hypotheses of `P`,
+transfer the names of the hypotheses of `P` to the hypotheses of `P'`. -/
+partial def transferHypNames (P P' : Expr) : MetaM Expr := (·.snd) <$> label (collectHyps P) P'
+  where
+    collectHyps (P : Expr) (acc : List Hyp := []) : List Hyp :=
+      if let some hyp := parseHyp? P then
+        hyp :: acc
+      else if let some (_, L, R) := parseAnd? P then
+        collectHyps L (collectHyps R acc)
+      else
+        acc
+
+    label (Ps : List Hyp) (P' : Expr) : MetaM (List Hyp × Expr) := do
+      let P' ← instantiateMVarsIfMVarApp P'
+      if let some _ := parseEmptyHyp? P' then
+        return (Ps, P')
+      if let some (σs, L, R) := parseAnd? P' then
+        let (Ps, L') ← label Ps L
+        let (Ps, R') ← label Ps R
+        return (Ps, mkAnd! σs L' R')
+      else
+        let mut Ps' := Ps
+        repeat
+          -- If we cannot find the hyp, it might be in a nested conjunction.
+          -- Just pick a default name for it.
+          let uniq ← mkFreshId
+          let P :: Ps'' := Ps' | return (Ps, { name := `h, uniq, p := P' : Hyp }.toExpr)
+          Ps' := Ps''
+          if ← isDefEq P.p P' then
+            return (Ps, { P with p := P' }.toExpr)
+        unreachable!
+
+def mFrameCore [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
+  (goal : MGoal) (kFail : m (α × Expr)) (kSuccess : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MGoal → m (α × Expr)) : m (α × Expr) := do
+  let P := goal.hyps
+  let φ ← mkFreshExprMVar (mkSort .zero)
+  let P' ← mkFreshExprMVar (mkApp (mkConst ``SPred) goal.σs)
+  if let some inst ← synthInstance? (mkApp4 (mkConst ``HasFrame) goal.σs P P' φ) then
+    if ← isDefEq (mkConst ``True) φ then return (← kFail)
+    -- copy the name of P to P' if it is a named hypothesis
+    let P' ← transferHypNames P P'
+    let goal := { goal with hyps := P' }
+    withLocalDeclD `h φ fun hφ => do
+      let (a, prf) ← kSuccess φ hφ goal
+      let prf ← mkLambdaFVars #[hφ] prf
+      let prf := mkApp7 (mkConst ``Frame.frame) goal.σs P P' goal.target φ inst prf
+      return (a, prf)
+  else
+    kFail
+
+def mTryFrame [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
+  (goal : MGoal) (k : MGoal → m (α × Expr)) : m (α × Expr) :=
+  mFrameCore goal (k goal) (fun _ _ goal => k goal)
+
+@[builtin_tactic Lean.Parser.Tactic.mframe]
+def elabMFrame : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+  let (m, prf) ← mFrameCore goal (fun _ => throwError "Could not infer frame") fun _ _ goal => do
+    let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr
+    return (m, m)
+  mvar.assign prf
+  replaceMainGoal [m.mvarId!]
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean
@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Cases
+import Lean.Elab.Tactic.Do.ProofMode.Specialize
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+def Have.dup {σs : List Type} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T :=
+  (SPred.and_intro .rfl (hfoc.mp.trans SPred.and_elim_r)).trans hgoal
+
+def Have.have {σs : List Type} {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T :=
+  (SPred.and_intro .rfl hhave).trans (hand.mp.trans hgoal)
+
+def Have.replace {σs : List Type} {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H ) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T :=
+  (SPred.and_intro (hfoc.mp.trans SPred.and_elim_l) hhave).trans (hand.mp.trans hgoal)
+
+@[builtin_tactic Lean.Parser.Tactic.mdup]
+def elabMDup : Tactic
+  | `(tactic| mdup $h:ident => $h₂:ident) => do
+  let (mvar, goal) ← ensureMGoal
+  mvar.withContext do
+  let some res := goal.focusHyp h.raw.getId | throwError m!"Hypothesis {h} not found"
+  let P := goal.hyps
+  let Q := res.restHyps
+  let H := res.focusHyp
+  let uniq ← mkFreshId
+  let hyp := Hyp.mk h₂.raw.getId uniq H.consumeMData
+  addHypInfo h goal.σs hyp (isBinder := true)
+  let H' := hyp.toExpr
+  let T := goal.target
+  let newGoal := { goal with hyps := mkAnd! goal.σs P H' }
+  let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+  mvar.assign (mkApp7 (mkConst ``Have.dup) goal.σs P Q H T res.proof m)
+  replaceMainGoal [m.mvarId!]
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.mhave]
+def elabMHave : Tactic
+  | `(tactic| mhave $h $[: $ty?]? := $rhs) => do
+  let (mvar, goal) ← ensureMGoal
+  mvar.withContext do
+  -- build goal `P ⊢ₛ T` from `P ⊢ₛ H` and residual goal `P ∧ H ⊢ₛ T`
+  let P := goal.hyps
+  let spred := mkApp (mkConst ``SPred) goal.σs
+  let H ← match ty? with
+    | some ty => elabTerm ty spred
+    | _       => mkFreshExprMVar spred
+  let uniq ← mkFreshId
+  let hyp := Hyp.mk h.raw.getId uniq H
+  addHypInfo h goal.σs hyp (isBinder := true)
+  let H := hyp.toExpr
+  let T := goal.target
+  let (PH, hand) := mkAnd goal.σs P H
+  let haveGoal := { goal with target := H }
+  let hhave ← elabTermEnsuringType rhs haveGoal.toExpr
+  let newGoal := { goal with hyps := PH }
+  let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+  mvar.assign (mkApp8 (mkConst ``Have.have) goal.σs P H PH T hand hhave m)
+  replaceMainGoal [m.mvarId!]
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.mreplace]
+def elabMReplace : Tactic
+  | `(tactic| mreplace $h $[: $ty?]? := $rhs) => do
+  let (mvar, goal) ← ensureMGoal
+  mvar.withContext do
+  -- build goal `P ⊢ₛ T` from `P ⊢ₛ H` and residual goal `P ∧ H ⊢ₛ T`
+  let PH := goal.hyps
+  let some res := goal.focusHyp h.raw.getId | throwError m!"Hypothesis {h} not found"
+  let P := res.restHyps
+  let H := res.focusHyp
+  let spred := mkApp (mkConst ``SPred) goal.σs
+  let H' ← match ty? with
+    | some ty => elabTerm ty spred
+    | _       => mkFreshExprMVar spred
+  let uniq ← mkFreshId
+  let hyp := Hyp.mk h.raw.getId uniq H'
+  addHypInfo h goal.σs hyp (isBinder := true)
+  let H' := hyp.toExpr
+  let haveGoal := { goal with target := H' }
+  let hhave ← elabTermEnsuringType rhs haveGoal.toExpr
+  let T := goal.target
+  let (PH', hand) := mkAnd goal.σs P H'
+  let newGoal := { goal with hyps := PH' }
+  let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+  let prf := mkApp (mkApp10 (mkConst ``Have.replace) goal.σs P H H' PH PH' T res.proof hand hhave) m
+  mvar.assign prf
+  replaceMainGoal [m.mvarId!]
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean
@ -0,0 +1,90 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Display
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+theorem Intro.intro {σs : List Type} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T :=
+  SPred.imp_intro (hand.mp.trans h)
+
+partial def mIntro [Monad m] [MonadControlT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) :=
+  controlAt MetaM fun map => do
+  let some (σs, H, T) := goal.target.app3? ``SPred.imp | throwError "Target not an implication {goal.target}"
+  let (name, ref) ← getFreshHypName ident
+  let uniq ← mkFreshId
+  let hyp := Hyp.mk name uniq H
+  addHypInfo ref σs hyp (isBinder := true)
+  let Q := goal.hyps
+  let H := hyp.toExpr
+  let (P, hand) := mkAnd goal.σs goal.hyps H
+  map do
+    let (a, prf) ← k { goal with hyps := P, target := T }
+    let prf := mkApp7 (mkConst ``Intro.intro) σs P Q H T hand prf
+    return (a, prf)
+
+-- This is regular MVar.intro, but it takes care not to leave the proof mode by preserving metadata
+partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax ``binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr) :=
+  controlAt MetaM fun map => do
+  let some (_type, σ, σs') := (← whnf goal.σs).app3? ``List.cons | liftMetaM <| throwError "Ambient state list not a cons {goal.σs}"
+  let name ← match ident with
+  | `(binderIdent| $name:ident) => pure name.getId
+  | `(binderIdent| $_) => liftMetaM <| mkFreshUserName `s
+  withLocalDeclD name σ fun s => do
+    addLocalVarInfo ident (← getLCtx) s σ (isBinder := true)
+    let H := betaRevPreservingHypNames σs' goal.hyps #[s]
+    let T := goal.target.betaRev #[s]
+    map do
+      let (a, prf) ← k { σs:=σs', hyps:=H, target:=T }
+      let prf ← mkLambdaFVars #[s] prf
+      return (a, mkApp5 (mkConst ``SPred.entails_cons_intro) σ σs' goal.hyps goal.target prf)
+
+def mIntroForallN [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m (α × Expr)) : m (α × Expr) :=
+  match n with
+  | 0 => k goal
+  | n+1 => do mIntroForall goal (← liftM (m := MetaM) `(binderIdent| _)) fun g =>
+              mIntroForallN g n k
+
+macro_rules
+  | `(tactic| mintro $pat₁ $pat₂ $pats:mintroPat*) => `(tactic| mintro $pat₁; mintro $pat₂ $pats*)
+  | `(tactic| mintro $pat:mintroPat) => do
+    match pat with
+    | `(mintroPat| $_:binderIdent) => Macro.throwUnsupported -- handled by an elaborator below
+    | `(mintroPat| ∀$_:binderIdent) => Macro.throwUnsupported -- handled by an elaborator below
+    | `(mintroPat| $pat:mcasesPat) => `(tactic| mintro h; mcases h with $pat)
+    | _ => Macro.throwUnsupported -- presently unreachable
+
+@[builtin_tactic Lean.Parser.Tactic.mintro]
+def elabMIntro : Tactic
+  | `(tactic| mintro $ident:binderIdent) => do
+
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  let goals ← IO.mkRef []
+  mvar.assign (← Prod.snd <$> mIntro goal ident fun newGoal => do
+    let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+    goals.modify (m.mvarId! :: ·)
+    return ((), m))
+  replaceMainGoal (← goals.get)
+
+  | `(tactic| mintro ∀$ident:binderIdent) => do
+
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  let goals ← IO.mkRef []
+  mvar.assign (← Prod.snd <$> mIntroForall goal ident fun newGoal => do
+    let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+    goals.modify (m.mvarId! :: ·)
+    return ((), m))
+  replaceMainGoal (← goals.get)
+
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean
@ -0,0 +1,38 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+def mLeftRightCore (right : Bool) (mvar : MVarId) : MetaM MVarId := do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+
+  let mkApp3 (.const ``SPred.or []) σs L R := goal.target | throwError "target is not SPred.or"
+
+  let (thm, keep) := if right then (``SPred.or_intro_r', R) else (``SPred.or_intro_l', L)
+
+  let newGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := keep}.toExpr
+  mvar.assign (mkApp5 (mkConst thm) σs goal.hyps L R newGoal)
+  return newGoal.mvarId!
+
+@[builtin_tactic Lean.Parser.Tactic.mleft]
+def elabMLeft : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let newGoal ← mLeftRightCore (right := false) mvar
+  replaceMainGoal [newGoal]
+
+@[builtin_tactic Lean.Parser.Tactic.mright]
+def elabMRight : Tactic | _ => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let newGoal ← mLeftRightCore (right := true) mvar
+  replaceMainGoal [newGoal]
--- a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean
@ -0,0 +1,192 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Do.SPred.DerivedLaws
+
+import Lean.Meta
+open Lean Elab Meta
+
+namespace Std.Do
+
+/-- Tautology in `SPred` as a definition. -/
+abbrev SPred.tautological {σs : List Type} (Q : SPred σs) : Prop := ⊢ₛ Q
+
+class PropAsSPredTautology (φ : Prop) {σs : outParam (List Type)} (P : outParam (SPred σs)) : Prop where
+  iff : φ ↔ ⊢ₛ P
+
+instance : PropAsSPredTautology (σs := []) φ φ where
+  iff := true_imp_iff.symm
+
+instance : PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q) where
+  iff := (SPred.entails_true_intro P Q).symm
+
+instance : PropAsSPredTautology (⊢ₛ P) P where
+  iff := Iff.rfl
+
+end Std.Do
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+
+theorem start_entails {φ : Prop} [PropAsSPredTautology φ P] : (⊢ₛ P) → φ :=
+  PropAsSPredTautology.iff.mpr
+
+theorem elim_entails {φ : Prop} [PropAsSPredTautology φ P] : φ → (⊢ₛ P) :=
+  PropAsSPredTautology.iff.mp
+
+@[match_pattern] def nameAnnotation := `name
+@[match_pattern] def uniqAnnotation := `uniq
+
+structure Hyp where
+  name : Name
+  uniq : Name -- for display purposes only
+  p : Expr
+
+def parseHyp? : Expr → Option Hyp
+  | .mdata ⟨[(nameAnnotation, .ofName name), (uniqAnnotation, .ofName uniq)]⟩ p =>
+    some ⟨name, uniq, p⟩ -- NB: mdatas are transparent to SubExpr; hence no pos.push
+  | _ => none
+
+def Hyp.toExpr (hyp : Hyp) : Expr :=
+  .mdata ⟨[(nameAnnotation, .ofName hyp.name), (uniqAnnotation, .ofName hyp.uniq)]⟩ hyp.p
+
+/-- An elaborator to create a new named hypothesis for an `MGoal` context. -/
+elab "mk_hyp " name:ident " := " e:term : term <= ty? => do
+  let e ← Lean.Elab.Term.elabTerm e ty?
+  let uniq ← mkFreshId
+  return (Hyp.mk name.getId uniq e).toExpr
+
+-- set_option pp.all true in
+-- #check ⌜True⌝
+def emptyHyp (σs : Expr) : Expr := -- ⌜True⌝ standing in for an empty conjunction of hypotheses
+  mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``True)
+def parseEmptyHyp? : Expr → Option Expr
+  | mkApp3 (.const ``SVal.curry _) (.sort .zero) σs (.lam _ _ (.const ``True _) _) => some σs
+  | _ => none
+
+def pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos :=
+  pos.pushNaryArg 3 1
+
+def pushRightConjunct (pos : SubExpr.Pos) : SubExpr.Pos :=
+  pos.pushNaryArg 3 2
+
+/-- Combine two hypotheses into a conjunction.
+Precondition: Neither `lhs` nor `rhs` is empty (`parseEmptyHyp?`). -/
+def mkAnd! (σs lhs rhs : Expr) : Expr :=
+  mkApp3 (mkConst ``SPred.and) σs lhs rhs
+
+/-- Smart constructor that cancels away empty hypotheses,
+along with a proof that `lhs ∧ rhs ⊣⊢ₛ result`. -/
+def mkAnd (σs lhs rhs : Expr) : Expr × Expr :=
+  if let some _ := parseEmptyHyp? lhs then
+    (rhs, mkApp2 (mkConst ``SPred.true_and) σs rhs)
+  else if let some _ := parseEmptyHyp? rhs then
+    (lhs, mkApp2 (mkConst ``SPred.and_true) σs lhs)
+  else
+    let result := mkAnd! σs lhs rhs
+    (result, mkApp2 (mkConst ``SPred.bientails.refl) σs result)
+
+def σs.mkType : Expr := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero))
+def σs.mkNil : Expr := mkApp (mkConst ``List.nil [.succ .zero]) (mkSort (.succ .zero))
+
+def parseAnd? (e : Expr) : Option (Expr × Expr × Expr) :=
+  e.app3? ``SPred.and <|> (σs.mkNil, ·) <$> e.app2? ``And
+
+structure MGoal where
+  σs : Expr -- Q(List Type)
+  hyps : Expr -- A conjunction of hypotheses in `SPred σs`, each carrying a name and uniq as metadata (`parseHyp?`)
+  target : Expr -- Q(SPred $σs)
+  deriving Inhabited
+
+/-- This is the same as `SPred.entails`.
+This constant is used to detect `SPred` proof mode goals. -/
+abbrev MGoalEntails := @SPred.entails
+
+def parseMGoal? (expr : Expr) : Option MGoal := do
+  let some (σs, hyps, target) := expr.consumeMData.app3? ``MGoalEntails | none
+  some { σs, hyps, target }
+
+open Tactic in
+def ensureMGoal : TacticM (MVarId × MGoal) := do
+  let mvar ← getMainGoal
+  let goal ← instantiateMVars <| (← mvar.getType)
+  if let some goal := parseMGoal? goal then
+    return (mvar, goal)
+  else
+    throwError "Not in proof mode"
+
+def MGoal.strip (goal : MGoal) : Expr := -- omits the .mdata wrapper
+  mkApp3 (mkConst ``SPred.entails) goal.σs goal.hyps goal.target
+
+/-- Roundtrips with `parseMGoal?`. -/
+def MGoal.toExpr (goal : MGoal) : Expr :=
+  mkApp3 (mkConst ``MGoalEntails) goal.σs goal.hyps goal.target
+
+partial def MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × Hyp) := go goal.hyps SubExpr.Pos.root
+  where
+    go (e : Expr) (p : SubExpr.Pos) : Option (SubExpr.Pos × Hyp) := do
+      if let some hyp := parseHyp? e then
+        if hyp.name = name then
+          return (p, hyp)
+        else
+          none
+      else if let some (_, lhs, rhs) := parseAnd? e then
+        -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display).
+        go rhs (pushLeftConjunct p) <|> go lhs (pushRightConjunct p)
+      else if let some _ := parseEmptyHyp? e then
+        none
+      else
+        panic! "MGoal.findHyp?: hypothesis without proper metadata: {e}"
+
+def MGoal.checkProof (goal : MGoal) (prf : Expr) (suppressWarning : Bool := false) : MetaM Unit := do
+  check prf
+  let prf_type ← inferType prf
+  unless ← isDefEq goal.toExpr prf_type do
+    throwError "MGoal.checkProof: the proof and its supposed type did not match.\ngoal:  {goal.toExpr}\nproof: {prf_type}"
+  unless suppressWarning do
+    logWarning m!"stray MGoal.checkProof {prf_type} {goal.toExpr}"
+
+def getFreshHypName : TSyntax ``binderIdent → CoreM (Name × Syntax)
+  | `(binderIdent| $name:ident) => pure (name.getId, name)
+  | stx => return (← mkFreshUserName `h, stx)
+
+partial def betaRevPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr :=
+  if let some _σs := parseEmptyHyp? e then
+    emptyHyp σs'
+  else if let some hyp := parseHyp? e then
+    { hyp with p := hyp.p.betaRev args }.toExpr
+  else if let some (_σs, lhs, rhs) := parseAnd? e then
+    -- _σs = σ :: σs'
+    mkAnd! σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args)
+  else
+    e.betaRev args
+
+def betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr :=
+  betaRevPreservingHypNames σs' e args.reverse
+
+def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do
+  let mut σs := σs
+  for _ in [:n] do
+    let some (_type, _σ, σs') := (← whnfR σs).app3? ``List.cons | throwError "Ambient state list not a cons {σs}"
+    σs := σs'
+  return σs
+
+/-- This is only used for display purposes, so that we can render context variables that appear
+to have type `A : PROP` even though `PROP` is not a type. -/
+def HypMarker {σs : List Type} (_A : SPred σs) : Prop := True
+
+def addLocalVarInfo (stx : Syntax) (lctx : LocalContext)
+    (expr : Expr) (expectedType? : Option Expr) (isBinder := false) : MetaM Unit := do
+  Elab.withInfoContext' (pure ())
+    (fun _ =>
+      return .inl <| .ofTermInfo
+        { elaborator := .anonymous, lctx, expr, stx, expectedType?, isBinder })
+    (return .ofPartialTermInfo { elaborator := .anonymous, lctx, stx, expectedType? })
+
+def addHypInfo (stx : Syntax) (σs : Expr) (hyp : Hyp) (isBinder := false) : MetaM Unit := do
+  let lctx ← getLCtx
+  let ty := mkApp2 (mkConst ``HypMarker) σs hyp.p
+  addLocalVarInfo stx (lctx.mkLocalDecl ⟨hyp.uniq⟩ hyp.name ty) (.fvar ⟨hyp.uniq⟩) ty isBinder
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
@ -0,0 +1,71 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+class IsPure {σs : List Type} (P : SPred σs) (φ : outParam Prop) where to_pure : P ⊣⊢ₛ ⌜φ⌝
+instance (σs) : IsPure (σs:=σs) ⌜φ⌝ φ where to_pure := .rfl
+instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ) where to_pure := SPred.pure_imp
+instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ) where to_pure := SPred.pure_and
+instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∨ ⌜ψ⌝) (φ ∨ ψ) where to_pure := SPred.pure_or
+instance (σs) (P : α → Prop) : IsPure (σs:=σs) spred(∃ x, ⌜P x⌝) (∃ x, P x) where to_pure := SPred.pure_exists
+instance (σs) (P : α → Prop) : IsPure (σs:=σs) spred(∀ x, ⌜P x⌝) (∀ x, P x) where to_pure := SPred.pure_forall
+instance (σs) (P : SPred (σ::σs)) [inst : IsPure P φ] : IsPure (σs:=σs) spred(P s) φ where to_pure := (iff_of_eq SPred.bientails_cons).mp inst.to_pure s
+instance (P : Prop) : IsPure (σs:=[]) P P where to_pure := Iff.rfl
+
+theorem Pure.thm {σs : List Type} {P Q T : SPred σs} {φ : Prop} [IsPure Q φ]
+  (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T := by
+    apply SPred.pure_elim
+    · exact SPred.and_elim_r.trans IsPure.to_pure.mp
+    · intro hp
+      exact SPred.and_elim_l.trans (h hp)
+
+-- NB: We do not use MVarId.intro because that would mean we require all callers to supply an MVarId.
+-- This function only knows about the hypothesis H=⌜φ⌝ to destruct.
+-- It will provide a proof for Q ∧ H ⊢ₛ T
+-- if `k` produces a proof for Q ⊢ₛ T that may range over a pure proof h : φ.
+-- It calls `k` with the φ in H = ⌜φ⌝ and a proof `h : φ` thereof.
+def mPureCore (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent)
+  (k : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do
+  let φ ← mkFreshExprMVar (mkSort .zero)
+  let inst ← synthInstance (mkApp3 (mkConst ``IsPure) σs hyp φ)
+  let (name, ref) ← getFreshHypName name
+  withLocalDeclD name φ fun h => do
+    addLocalVarInfo ref (← getLCtx) h φ
+    let (a, goal, prf /- : goal.toExpr -/) ← k φ h
+    let prf ← mkLambdaFVars #[h] prf
+    let prf := mkApp7 (mkConst ``Pure.thm) σs goal.hyps hyp goal.target φ inst prf
+    let goal := { goal with hyps := mkAnd! σs goal.hyps hyp }
+    return (a, goal, prf)
+
+@[builtin_tactic Lean.Parser.Tactic.mpure]
+def elabMPure : Tactic
+  | `(tactic| mpure $hyp) => do
+  let mvar ← getMainGoal
+  mvar.withContext do
+  let g ← instantiateMVars <| ← mvar.getType
+  let some goal := parseMGoal? g | throwError "not in proof mode"
+  let res ← goal.focusHypWithInfo hyp
+  let (m, _new_goal, prf) ← mPureCore goal.σs res.focusHyp (← `(binderIdent| $hyp:ident)) fun _ _ => do
+    let goal := res.restGoal goal
+    let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr
+    return (m, goal, m)
+  let prf := res.rewriteHyps goal prf
+  mvar.assign prf
+  replaceMainGoal [m.mvarId!]
+  | _ => throwUnsupportedSyntax
+
+/-- A generalization of `SPred.pure_intro` exploiting `IsPure`. -/
+private theorem Pure.intro {σs : List Type} {P Q : SPred σs} {φ : Prop} [IsPure Q φ] (hp : φ) : P ⊢ₛ Q :=
+  (SPred.pure_intro hp).trans IsPure.to_pure.mpr
+
+macro "mpure_intro" : tactic => `(tactic| apply Pure.intro)
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean
@ -0,0 +1,78 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Assumption
+import Lean.Elab.Tactic.Do.ProofMode.Exact
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do Lean.Parser.Tactic
+open Lean Elab Tactic Meta
+
+def patAsTerm (pat : MRefinePat) (expected : Option Expr := none) : OptionT TacticM Expr := do
+  match pat with
+  | .pure t => elabTerm t expected
+  | .one name =>
+    if let `(binderIdent| $name:ident) := name then
+      elabTerm (← `($name)) expected
+    else failure
+  | _ => failure
+
+partial def mRefineCore (goal : MGoal) (pat : MRefinePat) (k : MGoal → TSyntax ``binderIdent → TacticM Expr) : TacticM Expr := do
+  match pat with
+  | .stateful name => liftMetaM do
+    match name with
+    | `(binderIdent| $name:ident) => do
+      let some prf ← goal.exact name | throwError "unknown hypothesis '{repr name}'"
+      return prf
+    | _ => do
+      let some prf ← goal.assumption | throwError "could not solve {goal.target} by assumption"
+      return prf
+  | .pure t => do
+    goal.exactPure t
+  | .one name =>
+      if let `(binderIdent| $_:ident) := name then
+        mRefineCore goal (.pure ⟨name.raw⟩) k <|> mRefineCore goal (.stateful name) k
+      else
+        mRefineCore goal (.stateful name) k
+  | .hole name => k goal name
+  | .tuple [] => throwUnsupportedSyntax
+  | .tuple [p] => mRefineCore goal p k
+  | .tuple (p::ps) => do
+    let T ← whnfR goal.target
+    if let some (σs, T₁, T₂) := parseAnd? T.consumeMData then
+      let prf₁ ← mRefineCore { goal with target := T₁ } p k
+      let prf₂ ← mRefineCore { goal with target := T₂ } (.tuple ps) k
+      return mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps T₁ T₂ prf₁ prf₂
+    else if let some (α, σs, ψ) := T.app3? ``SPred.exists then
+      let some witness ← patAsTerm p (some α) | throwError "pattern does not elaborate to a term to instantiate ψ"
+      let prf ← mRefineCore { goal with target := ψ.betaRev #[witness] } (.tuple ps) k
+      let u ← getLevel α
+      return mkApp6 (mkConst ``SPred.exists_intro' [u]) α σs goal.hyps ψ witness prf
+    else throwError "Neither a conjunction nor an existential quantifier {goal.target}"
+
+@[builtin_tactic Lean.Parser.Tactic.mrefine]
+def elabMRefine : Tactic
+  | `(tactic| mrefine $pat:mrefinePat) => do
+  let pat ← liftMacroM <| MRefinePat.parse pat
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  let goals ← IO.mkRef #[]
+  let prf ← mRefineCore goal pat fun goal name => do
+    let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr name.raw.getId
+    goals.modify (·.push m.mvarId!)
+    return m
+  mvar.assign prf
+  replaceMainGoal (← goals.get).toList
+  | _ => throwUnsupportedSyntax
+
+macro_rules
+  | `(tactic| mexists $args,*) => do
+  let pats ← args.getElems.mapM fun t => `(mrefinePat| ⌜$t⌝)
+  let pat ← pats.foldrM (fun pat acc => `(mrefinePat| ⟨$pat, $acc⟩)) (← `(mrefinePat| ?_))
+  `(tactic| (mrefine $pat; try massumption))
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean
@ -0,0 +1,40 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+theorem Revert.revert {σs : List Type} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (h : Q ⊢ₛ H → T) : P ⊢ₛ T :=
+  hfoc.mp.trans (SPred.imp_elim h)
+
+partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → MetaM Expr) : MetaM Expr := do
+  let res ← goal.focusHypWithInfo ref
+  let P := goal.hyps
+  let Q := res.restHyps
+  let H := res.focusHyp
+  let T := goal.target
+  let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp) goal.σs H T }
+  let prf := mkApp7 (mkConst ``Revert.revert) goal.σs P Q H T res.proof prf
+  return prf
+
+@[builtin_tactic Lean.Parser.Tactic.mrevert]
+def elabMRevert : Tactic
+  | `(tactic| mrevert $h) => do
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  let goals ← IO.mkRef []
+  mvar.assign (← mRevertStep goal h fun newGoal => do
+    let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr
+    goals.modify (m.mvarId! :: ·)
+    return m)
+  replaceMainGoal (← goals.get)
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean
@ -0,0 +1,203 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.Do.ProofMode.Basic
+import Lean.Elab.Tactic.Do.ProofMode.Pure
+
+namespace Lean.Elab.Tactic.Do.ProofMode
+open Std.Do
+open Lean Elab Tactic Meta
+
+initialize registerTraceClass `Meta.Tactic.Do.specialize
+
+theorem Specialize.imp_stateful {P P' Q R : SPred σs}
+  (hrefocus : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q) : P ∧ (Q → R) ⊢ₛ P ∧ R := by
+  calc spred(P ∧ (Q → R))
+    _ ⊢ₛ (P' ∧ Q) ∧ (Q → R) := SPred.and_intro hrefocus.mp SPred.and_elim_r
+    _ ⊢ₛ P' ∧ Q ∧ (Q → R) := SPred.and_assoc.mp
+    _ ⊢ₛ P' ∧ Q ∧ R := SPred.and_mono_r (SPred.and_intro SPred.and_elim_l SPred.imp_elim_r)
+    _ ⊢ₛ (P' ∧ Q) ∧ R := SPred.and_assoc.mpr
+    _ ⊢ₛ P ∧ R := SPred.and_mono_l (hrefocus.mpr.trans SPred.and_elim_l)
+
+theorem Specialize.imp_pure {P Q R : SPred σs} [PropAsSPredTautology φ Q]
+  (h : φ) : P ∧ (Q → R) ⊢ₛ P ∧ R := by
+  calc spred(P ∧ (Q → R))
+    _ ⊢ₛ P ∧ (Q ∧ (Q → R)) := SPred.and_mono_r (SPred.and_intro (SPred.true_intro.trans (PropAsSPredTautology.iff.mp h)) .rfl)
+    _ ⊢ₛ P ∧ R := SPred.and_mono_r (SPred.mp SPred.and_elim_r SPred.and_elim_l)
+
+theorem Specialize.forall {P : SPred σs} {ψ : α → SPred σs}
+  (a : α) : P ∧ (∀ x, ψ x) ⊢ₛ P ∧ ψ a := SPred.and_mono_r (SPred.forall_elim a)
+
+theorem Specialize.pure_start {φ : Prop} {H P T : SPred σs} [PropAsSPredTautology φ H] (hpure : φ) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T :=
+  (SPred.and_intro .rfl (SPred.true_intro.trans (PropAsSPredTautology.iff.mp hpure))).trans hgoal
+
+theorem Specialize.pure_taut {σs} {φ} {P : SPred σs} [IsPure P φ] (h : φ) : ⊢ₛ P :=
+  (SPred.pure_intro h).trans IsPure.to_pure.mpr
+
+def mSpecializeImpStateful (σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do
+  guard (arg.raw.isIdent)
+  let some argRes := focusHyp σs (mkAnd! σs P QR) arg.raw.getId | failure
+  let some hyp := parseHyp? argRes.focusHyp | failure
+  addHypInfo arg σs hyp
+  OptionT.mk do -- no OptionT failure after this point
+  -- The goal is P ∧ (Q → R)
+  -- argRes.proof : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q
+  -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R))
+  let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpStateful violated"
+  let P' := argRes.restHyps
+  let Q := argRes.focusHyp
+  let hrefocus := argRes.proof -- P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q
+  let mkApp3 (.const ``SPred.imp []) σs Q' R := specHyp.p | throwError "Expected implication {QR}"
+  let proof := mkApp6 (mkConst ``Specialize.imp_stateful) σs P P' Q R hrefocus
+  -- check proof
+  trace[Meta.Tactic.Do.specialize] "Statefully specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}"
+  unless ← isDefEq Q Q' do
+    throwError "failed to specialize {specHyp.p} with {Q}"
+
+  return ({ specHyp with p := R }.toExpr, proof)
+
+def mSpecializeImpPure (_σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do
+  let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpPure violated"
+  let mkApp3 (.const ``SPred.imp []) σs Q R := specHyp.p | failure
+  let mut φ ← mkFreshExprMVar (mkSort .zero)
+  let mut (hφ, mvarIds) ← try
+    elabTermWithHoles arg.raw φ `specialize (allowNaturalHoles := true)
+    catch _ => failure
+  -- We might have hφ : φ and Q = ⌜φ⌝. In this case, convert hφ to a proof of ⊢ₛ ⌜φ⌝,
+  -- so that we can infer an instance of `PropAsSPredTautology`.
+  -- NB: PropAsSPredTautology φ ⌜φ⌝ is unfortunately impossible because ⊢ₛ ⌜φ⌝ does not imply φ.
+  -- Hence this additional (lossy) conversion.
+  if let some inst ← synthInstance? (mkApp3 (mkConst ``IsPure) σs Q φ) then
+    hφ := mkApp5 (mkConst ``Specialize.pure_taut) σs φ Q inst hφ
+    φ := mkApp2 (mkConst ``SPred.tautological) σs Q
+
+  let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ σs Q)
+    | failure
+
+  OptionT.mk do -- no OptionT failure after this point
+  -- The goal is P ∧ (Q → R)
+  -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R))
+  pushGoals mvarIds
+  let proof := mkApp7 (mkConst ``Specialize.imp_pure) σs φ P Q R inst hφ
+  -- check proof
+  trace[Meta.Tactic.Do.specialize] "Purely specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}"
+  -- logInfo m!"proof: {← inferType proof}"
+  return ({ specHyp with p := R }.toExpr, proof)
+
+def mSpecializeForall (_σs : Expr) (P : Expr) (Ψ : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do
+  let some specHyp := parseHyp? Ψ | panic! "Precondition of specializeForall violated"
+  let mkApp3 (.const ``SPred.forall [u]) α σs αR := specHyp.p | failure
+  let (a, mvarIds) ← try
+    elabTermWithHoles arg.raw α `specialize (allowNaturalHoles := true)
+    catch _ => failure
+  OptionT.mk do -- no OptionT failure after this point
+  pushGoals mvarIds
+  let proof := mkApp5 (mkConst ``Specialize.forall [u]) σs α P αR a
+  let R := αR.beta #[a]
+  -- check proof
+  trace[Meta.Tactic.Do.specialize] "Instantiate {specHyp.p} with {a}. New Goal: {mkAnd! σs P R}"
+  return ({ specHyp with p := R }.toExpr, proof)
+
+theorem focus {P P' Q R : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ Q) (hnew : P' ∧ Q ⊢ₛ R) : P ⊢ₛ R :=
+  hfocus.mp.trans hnew
+
+@[builtin_tactic Lean.Parser.Tactic.mspecialize]
+def elabMSpecialize : Tactic
+  | `(tactic| mspecialize $hyp $args*) => do
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  -- Want to prove goal P ⊢ T, where hyp occurs in P.
+  -- So we
+  -- 1. focus on hyp (referred to as H):  P ⊣⊢ₛ P' ∧ H. Prove P' ∧ H ⊢ₛ T
+  -- 2. Produce a (transitive chain of) proofs
+  --      P' ∧ H ⊢ P' ∧ H₁ ⊢ₛ P' ∧ H₂ ⊢ₛ ...
+  --    One for each arg; end up with goal P' ∧ H' ⊢ₛ T
+  -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'.
+  -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain.
+  let some specFocus := goal.focusHyp hyp.getId | throwError "unknown identifier '{hyp}'"
+  let σs := goal.σs
+  let P := specFocus.restHyps
+  let mut H := specFocus.focusHyp
+  let some hyp' := parseHyp? H | panic! "Invariant of specialize violated"
+  addHypInfo hyp σs hyp'
+  -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar
+  let mut proof : Expr → Expr :=
+    mkApp7 (mkConst ``focus) σs goal.hyps P H goal.target specFocus.proof
+
+  for arg in args do
+    let res? ← OptionT.run
+      (mSpecializeImpStateful σs P H arg
+        <|> mSpecializeImpPure σs P H arg
+        <|> mSpecializeForall σs P H arg)
+    match res? with
+    | some (H', H2H') =>
+      -- logInfo m!"H: {H}, proof: {← inferType H2H'}"
+      proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal)
+      H := H'
+    | none =>
+      throwError "Could not specialize {H} with {arg}"
+
+  let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr
+  mvar.assign (proof newMVar)
+  replaceMainGoal [newMVar.mvarId!]
+
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.mspecializePure]
+def elabMspecializePure : Tactic
+  | `(tactic| mspecialize_pure $head $args* => $hyp) => do
+  -- "mspecialize_pure" >> term >> many (ppSpace >> checkColGt "irrelevant" >> termParser (eval_prec max)) >> "as" >> ident
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  mvar.withContext do
+
+  -- Want to prove goal P ⊢ₛ T. `head` is a pure proof of type `φ` that turns into `⊢ₛ H` via `start_entails`.
+  -- So we
+  -- 1. Introduce `head` via `PropAsEntails` as stateful hypothesis named `hyp`, P ∧ (hyp : H) ⊢ₛ T
+  -- 2. (from here on it's the same as `mspecialize`.)
+  --    Produce a (transitive chain of) proofs
+  --      P ∧ H ⊢ P ∧ H₁ ⊢ₛ P ∧ H₂ ⊢ₛ ...
+  --    One for each arg; end up with goal P ∧ H' ⊢ₛ T
+  -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'.
+  -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain.
+  let σs := goal.σs
+  let P := goal.hyps
+  let T := goal.target
+  let hφ ← elabTerm head none
+  let φ ← inferType hφ
+  let H ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs)
+  let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) φ σs H)
+  let uniq ← mkFreshId
+  let mut H := (Hyp.mk hyp.getId uniq (← instantiateMVars H)).toExpr
+
+  let goal : MGoal := { goal with hyps := mkAnd! σs P H }
+  -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar
+  let mut proof : Expr → Expr :=
+    mkApp8 (mkConst ``Specialize.pure_start) σs φ H P T inst hφ
+
+  for arg in args do
+    let res? ← OptionT.run
+      (mSpecializeImpStateful σs P H ⟨arg⟩
+        <|> mSpecializeImpPure σs P H ⟨arg⟩
+        <|> mSpecializeForall σs P H ⟨arg⟩)
+    match res? with
+    | some (H', H2H') =>
+      -- logInfo m!"H: {H}, proof: {← inferType H2H'}"
+      proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal)
+      H := H'
+    | none =>
+      throwError "Could not specialize {H} with {arg}"
+
+  let some hyp' := parseHyp? H | panic! "Invariant of specialize_pure violated"
+  addHypInfo hyp σs hyp'
+
+  let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr
+  mvar.assign (proof newMVar)
+  replaceMainGoal [newMVar.mvarId!]
+  | _ => throwUnsupportedSyntax
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Lean.Parser.Term
 import Lean.Parser.Tactic.Doc
+import Std.Tactic.Do.Syntax

 namespace Lean
 namespace Parser
--- a/src/Std.lean
+++ b/src/Std.lean
@ -6,6 +6,7 @@ Authors: Sebastian Ullrich
 prelude
 import Std.Classes
 import Std.Data
+import Std.Do
 import Std.Sat
 import Std.Sync
 import Std.Time
--- a/src/Std/Do.lean
+++ b/src/Std/Do.lean
@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.SPred
--- a/src/Std/Do/SPred.lean
+++ b/src/Std/Do/SPred.lean
@ -0,0 +1,11 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Do.SPred.SVal
+import Std.Do.SPred.SPred
+import Std.Do.SPred.Notation
+import Std.Do.SPred.Laws
+import Std.Do.SPred.DerivedLaws
--- a/src/Std/Do/SPred/DerivedLaws.lean
+++ b/src/Std/Do/SPred/DerivedLaws.lean
@ -0,0 +1,162 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Init.ByCases
+import Std.Do.SPred.Laws
+
+/-!
+# Derived laws of `SPred`
+
+This module contains some laws about `SPred` that are derived from
+the laws in `Std.Do.SPred.Laws`.
+-/
+
+namespace Std.Do.SPred
+
+variable {σs : List Type} {P P' Q Q' R R' : SPred σs} {φ φ₁ φ₂ : Prop}
+
+theorem entails.rfl {σs : List Type} {P : SPred σs} : P ⊢ₛ P := entails.refl P
+
+theorem bientails.rfl {σs : List Type} {P : SPred σs} : P ⊣⊢ₛ P := bientails.refl P
+theorem bientails.of_eq {σs : List Type} {P Q : SPred σs} (h : P = Q) : P ⊣⊢ₛ Q := h ▸ .rfl
+
+theorem bientails.mp {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (P ⊢ₛ Q) := fun h => (bientails.iff.mp h).1
+theorem bientails.mpr {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊢ₛ P) := fun h => (bientails.iff.mp h).2
+
+/-! # Connectives -/
+
+theorem and_elim_l' (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_l.trans h
+theorem and_elim_r' (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_r.trans h
+theorem or_intro_l' (h : P ⊢ₛ Q) : P ⊢ₛ Q ∨ R := h.trans or_intro_l
+theorem or_intro_r' (h : P ⊢ₛ R) : P ⊢ₛ Q ∨ R := h.trans or_intro_r
+theorem and_symm : P ∧ Q ⊢ₛ Q ∧ P := and_intro and_elim_r and_elim_l
+theorem or_symm : P ∨ Q ⊢ₛ Q ∨ P := or_elim or_intro_r or_intro_l
+theorem imp_intro' (h : Q ∧ P ⊢ₛ R) : P ⊢ₛ Q → R := imp_intro <| and_symm.trans h
+theorem entails.trans' (h₁ : P ⊢ₛ Q) (h₂ : P ∧ Q ⊢ₛ R) : P ⊢ₛ R := (and_intro .rfl h₁).trans h₂
+theorem mp (h₁ : P ⊢ₛ Q → R) (h₂ : P ⊢ₛ Q) : P ⊢ₛ R := entails.trans' h₂ (imp_elim h₁)
+theorem imp_elim' (h : Q ⊢ₛ P → R) : P ∧ Q ⊢ₛ R := and_symm.trans <| imp_elim h
+theorem imp_elim_l : (P → Q) ∧ P ⊢ₛ Q := imp_elim .rfl
+theorem imp_elim_r : P ∧ (P → Q) ⊢ₛ Q := imp_elim' .rfl
+theorem false_elim : ⌜False⌝ ⊢ₛ P := pure_elim' False.elim
+theorem true_intro : P ⊢ₛ ⌜True⌝ := pure_intro trivial
+theorem exists_intro' {σs} {P} {Ψ : α → SPred σs} (a : α) (h : P ⊢ₛ Ψ a) : P ⊢ₛ ∃ a, Ψ a := h.trans (exists_intro a)
+theorem and_or_elim_l (hleft : P ∧ R ⊢ₛ T) (hright : Q ∧ R ⊢ₛ T) : (P ∨ Q) ∧ R ⊢ₛ T := imp_elim (or_elim (imp_intro hleft) (imp_intro hright))
+theorem and_or_elim_r (hleft : P ∧ Q ⊢ₛ T) (hright : P ∧ R ⊢ₛ T) : P ∧ (Q ∨ R) ⊢ₛ T := imp_elim' (or_elim (imp_intro (and_symm.trans hleft)) (imp_intro (and_symm.trans hright)))
+theorem exfalso (h : P ⊢ₛ ⌜False⌝) : P ⊢ₛ Q := h.trans false_elim
+
+/-! # Monotonicity and congruence -/
+
+theorem and_mono (hp : P ⊢ₛ P') (hq : Q ⊢ₛ Q') : P ∧ Q ⊢ₛ P' ∧ Q' := and_intro (and_elim_l' hp) (and_elim_r' hq)
+theorem and_mono_l (h : P ⊢ₛ P') : P ∧ Q ⊢ₛ P' ∧ Q := and_mono h .rfl
+theorem and_mono_r (h : Q ⊢ₛ Q') : P ∧ Q ⊢ₛ P ∧ Q' := and_mono .rfl h
+theorem and_congr (hp : P ⊣⊢ₛ P') (hq : Q ⊣⊢ₛ Q') : P ∧ Q ⊣⊢ₛ P' ∧ Q' := bientails.iff.mpr ⟨and_mono (bientails.mp hp) (bientails.mp hq), and_mono (bientails.mpr hp) (bientails.mpr hq)⟩
+theorem and_congr_l (hp : P ⊣⊢ₛ P') : P ∧ Q ⊣⊢ₛ P' ∧ Q := and_congr hp .rfl
+theorem and_congr_r (hq : Q ⊣⊢ₛ Q') : P ∧ Q ⊣⊢ₛ P ∧ Q' := and_congr .rfl hq
+theorem or_mono (hp : P ⊢ₛ P') (hq : Q ⊢ₛ Q') : P ∨ Q ⊢ₛ P' ∨ Q' := or_elim (or_intro_l' hp) (or_intro_r' hq)
+theorem or_mono_l (h : P ⊢ₛ P') : P ∨ Q ⊢ₛ P' ∨ Q := or_mono h .rfl
+theorem or_mono_r (h : Q ⊢ₛ Q') : P ∨ Q ⊢ₛ P ∨ Q' := or_mono .rfl h
+theorem or_congr (hp : P ⊣⊢ₛ P') (hq : Q ⊣⊢ₛ Q') : P ∨ Q ⊣⊢ₛ P' ∨ Q' := bientails.iff.mpr ⟨or_mono (bientails.mp hp) (bientails.mp hq), or_mono (bientails.mpr hp) (bientails.mpr hq)⟩
+theorem or_congr_l (hp : P ⊣⊢ₛ P') : P ∨ Q ⊣⊢ₛ P' ∨ Q := or_congr hp .rfl
+theorem or_congr_r (hq : Q ⊣⊢ₛ Q') : P ∨ Q ⊣⊢ₛ P ∨ Q' := or_congr .rfl hq
+theorem imp_mono (h1 : Q ⊢ₛ P) (h2 : P' ⊢ₛ Q') : (P → P') ⊢ₛ Q → Q' := imp_intro <| (and_mono_r h1).trans <| (imp_elim .rfl).trans h2
+theorem imp_mono_l (h : P' ⊢ₛ P) : (P → Q) ⊢ₛ (P' → Q) := imp_mono h .rfl
+theorem imp_mono_r (h : Q ⊢ₛ Q') : (P → Q) ⊢ₛ (P → Q') := imp_mono .rfl h
+theorem imp_congr (h1 : P ⊣⊢ₛ Q) (h2 : P' ⊣⊢ₛ Q') : (P → P') ⊣⊢ₛ (Q → Q') := bientails.iff.mpr ⟨imp_mono h1.mpr h2.mp, imp_mono h1.mp h2.mpr⟩
+theorem imp_congr_l (h : P ⊣⊢ₛ P') : (P → Q) ⊣⊢ₛ (P' → Q) := imp_congr h .rfl
+theorem imp_congr_r (h : Q ⊣⊢ₛ Q') : (P → Q) ⊣⊢ₛ (P → Q') := imp_congr .rfl h
+theorem forall_mono {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊢ₛ Ψ a) : (∀ a, Φ a) ⊢ₛ ∀ a, Ψ a := forall_intro fun a => (forall_elim a).trans (h a)
+theorem forall_congr {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊣⊢ₛ Ψ a) : (∀ a, Φ a) ⊣⊢ₛ ∀ a, Ψ a := bientails.iff.mpr ⟨forall_mono fun a => (h a).mp, forall_mono fun a => (h a).mpr⟩
+theorem exists_mono {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊢ₛ Ψ a) : (∃ a, Φ a) ⊢ₛ ∃ a, Ψ a := exists_elim fun a => (h a).trans (exists_intro a)
+theorem exists_congr {Φ Ψ : α → SPred σs} (h : ∀ a, Φ a ⊣⊢ₛ Ψ a) : (∃ a, Φ a) ⊣⊢ₛ ∃ a, Ψ a := bientails.iff.mpr ⟨exists_mono fun a => (h a).mp, exists_mono fun a => (h a).mpr⟩
+
+theorem and_imp (hp : P₁ ⊢ₛ P₂) (hq : Q₁ ⊢ₛ Q₂) : (P₁ ∧ Q₁) ⊢ₛ (P₂ ∧ Q₂) := and_intro (and_elim_l' hp) (and_elim_r' hq)
+theorem or_imp_left (hleft : P₁ ⊢ₛ P₂) : (P₁ ∨ Q) ⊢ₛ (P₂ ∨ Q) := or_elim (or_intro_l' hleft) or_intro_r
+theorem or_imp_right (hright : Q₁ ⊢ₛ Q₂) : (P ∨ Q₁) ⊢ₛ (P ∨ Q₂) := or_elim or_intro_l (or_intro_r' hright)
+
+/-! # Boolean algebra -/
+
+theorem and_self : P ∧ P ⊣⊢ₛ P := bientails.iff.mpr ⟨and_elim_l, and_intro .rfl .rfl⟩
+theorem or_self : P ∨ P ⊣⊢ₛ P := bientails.iff.mpr ⟨or_elim .rfl .rfl, or_intro_l⟩
+theorem and_comm : P ∧ Q ⊣⊢ₛ Q ∧ P := bientails.iff.mpr ⟨and_symm, and_symm⟩
+theorem or_comm : P ∨ Q ⊣⊢ₛ Q ∨ P := bientails.iff.mpr ⟨or_symm, or_symm⟩
+theorem and_assoc : (P ∧ Q) ∧ R ⊣⊢ₛ P ∧ Q ∧ R := bientails.iff.mpr ⟨and_intro (and_elim_l' and_elim_l) (and_mono_l and_elim_r), and_intro (and_mono_r and_elim_l) (and_elim_r' and_elim_r)⟩
+theorem or_assoc : (P ∨ Q) ∨ R ⊣⊢ₛ P ∨ Q ∨ R := bientails.iff.mpr ⟨or_elim (or_mono_r or_intro_l) (or_intro_r' or_intro_r), or_elim (or_intro_l' or_intro_l) (or_mono_l or_intro_r)⟩
+theorem and_eq_right : (P ⊢ₛ Q) ↔ P ⊣⊢ₛ Q ∧ P := Iff.intro (fun h => bientails.iff.mpr ⟨and_intro h .rfl, and_elim_r⟩) (fun h => h.mp.trans and_elim_l)
+theorem and_eq_left : (P ⊢ₛ Q) ↔ P ⊣⊢ₛ P ∧ Q := Iff.intro (fun h => bientails.iff.mpr ⟨and_intro .rfl h, and_elim_l⟩) (fun h => h.mp.trans and_elim_r)
+theorem or_eq_left : (P ⊢ₛ Q) ↔ Q ⊣⊢ₛ Q ∨ P := Iff.intro (fun h => bientails.iff.mpr ⟨or_intro_l' .rfl, or_elim .rfl h⟩) (fun h => or_intro_r.trans h.mpr)
+theorem or_eq_right : (P ⊢ₛ Q) ↔ Q ⊣⊢ₛ P ∨ Q := Iff.intro (fun h => bientails.iff.mpr ⟨or_intro_r' .rfl, or_elim h .rfl⟩) (fun h => or_intro_l.trans h.mpr)
+
+theorem and_or_left : P ∧ (Q ∨ R) ⊣⊢ₛ (P ∧ Q) ∨ (P ∧ R) :=
+  bientails.iff.mpr ⟨and_or_elim_r or_intro_l or_intro_r,
+                     or_elim (and_intro and_elim_l (or_intro_l' and_elim_r)) (and_intro and_elim_l (or_intro_r' and_elim_r))⟩
+theorem or_and_left : P ∨ (Q ∧ R) ⊣⊢ₛ (P ∨ Q) ∧ (P ∨ R) :=
+  bientails.iff.mpr ⟨or_elim (and_intro or_intro_l or_intro_l) (and_imp or_intro_r or_intro_r),
+                     and_or_elim_l (or_intro_l' and_elim_l) (and_or_elim_r (or_intro_l' and_elim_r) or_intro_r)⟩
+theorem or_and_right : (P ∨ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∨ (Q ∧ R) := and_comm.trans (and_or_left.trans (or_congr and_comm and_comm))
+theorem and_or_right : (P ∧ Q) ∨ R ⊣⊢ₛ (P ∨ R) ∧ (Q ∨ R) := or_comm.trans (or_and_left.trans (and_congr or_comm or_comm))
+
+theorem true_and : ⌜True⌝ ∧ P ⊣⊢ₛ P := bientails.iff.mpr ⟨and_elim_r, and_intro (pure_intro trivial) .rfl⟩
+theorem and_true : P ∧ ⌜True⌝ ⊣⊢ₛ P := and_comm.trans true_and
+theorem false_and : ⌜False⌝ ∧ P ⊣⊢ₛ ⌜False⌝ := bientails.iff.mpr ⟨and_elim_l, false_elim⟩
+theorem and_false : P ∧ ⌜False⌝ ⊣⊢ₛ ⌜False⌝ := and_comm.trans false_and
+theorem true_or : ⌜True⌝ ∨ P ⊣⊢ₛ ⌜True⌝ := bientails.iff.mpr ⟨true_intro, or_intro_l⟩
+theorem or_true : P ∨ ⌜True⌝ ⊣⊢ₛ ⌜True⌝ := or_comm.trans true_or
+theorem false_or : ⌜False⌝ ∨ P ⊣⊢ₛ P := bientails.iff.mpr ⟨or_elim false_elim .rfl, or_intro_r⟩
+theorem or_false : P ∨ ⌜False⌝ ⊣⊢ₛ P := or_comm.trans false_or
+
+theorem true_imp : (⌜True⌝ → P) ⊣⊢ₛ P := bientails.iff.mpr ⟨and_true.mpr.trans imp_elim_l, imp_intro and_elim_l⟩
+theorem imp_self : Q ⊢ₛ P → P := imp_intro and_elim_r
+theorem imp_self_simp : (Q ⊢ₛ P → P) ↔ True := iff_true_intro SPred.imp_self
+theorem imp_trans : (P → Q) ∧ (Q → R) ⊢ₛ P → R := imp_intro' <| and_assoc.mpr.trans <| (and_mono_l imp_elim_r).trans imp_elim_r
+theorem false_imp : (⌜False⌝ → P) ⊣⊢ₛ ⌜True⌝ := bientails.iff.mpr ⟨true_intro, imp_intro <| and_elim_r.trans false_elim⟩
+
+/-! # Pure -/
+
+theorem pure_elim {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R) : Q ⊢ₛ R :=
+  and_self.mpr.trans <| imp_elim <| h1.trans <| pure_elim' fun h =>
+    imp_intro' <| and_elim_l.trans (h2 h)
+
+theorem pure_mono {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : ⌜φ₁⌝ ⊢ₛ (⌜φ₂⌝ : SPred σs) := pure_elim' <| pure_intro ∘ h
+theorem pure_congr {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : ⌜φ₁⌝ ⊣⊢ₛ (⌜φ₂⌝ : SPred σs) := bientails.iff.mpr ⟨pure_mono h.1, pure_mono h.2⟩
+
+theorem pure_elim_l {φ : Prop} (h : φ → Q ⊢ₛ R) : ⌜φ⌝ ∧ Q ⊢ₛ R := pure_elim and_elim_l <| and_elim_r' ∘ h
+theorem pure_elim_r {φ : Prop} (h : φ → Q ⊢ₛ R) : Q ∧ ⌜φ⌝ ⊢ₛ R := and_comm.mp.trans (pure_elim_l h)
+theorem pure_true {φ : Prop} (h : φ) : ⌜φ⌝ ⊣⊢ₛ (⌜True⌝ : SPred σs) := eq_true h ▸ .rfl
+theorem pure_and {φ₁ φ₂ : Prop} : ⌜φ₁⌝ ∧ (⌜φ₂⌝ : SPred σs) ⊣⊢ₛ ⌜φ₁ ∧ φ₂⌝ := bientails.iff.mpr ⟨pure_elim and_elim_l fun h => and_elim_r' <| pure_mono <| And.intro h, and_intro (pure_mono And.left) (pure_mono And.right)⟩
+theorem pure_or {φ₁ φ₂ : Prop} : ⌜φ₁⌝ ∨ (⌜φ₂⌝ : SPred σs) ⊣⊢ₛ ⌜φ₁ ∨ φ₂⌝ := bientails.iff.mpr ⟨or_elim (pure_mono Or.inl) (pure_mono Or.inr), pure_elim' (·.elim (or_intro_l' ∘ pure_intro) (or_intro_r' ∘ pure_intro))⟩
+theorem pure_imp_2 {φ₁ φ₂ : Prop} : ⌜φ₁ → φ₂⌝ ⊢ₛ (⌜φ₁⌝ → ⌜φ₂⌝ : SPred σs) := imp_intro <| pure_and.mp.trans <| pure_mono (And.elim id)
+theorem pure_imp {φ₁ φ₂ : Prop} : (⌜φ₁⌝ → ⌜φ₂⌝ : SPred σs) ⊣⊢ₛ ⌜φ₁ → φ₂⌝ := by
+  refine bientails.iff.mpr ⟨?_, pure_imp_2⟩
+  if h : φ₁
+  then exact (mp .rfl (pure_intro h)).trans (pure_mono fun h _ => h)
+  else exact pure_intro h.elim
+
+theorem pure_forall_2 {φ : α → Prop} : ⌜∀ x, φ x⌝ ⊢ₛ ∀ x, (⌜φ x⌝ : SPred σs) := forall_intro fun _ => pure_mono (· _)
+theorem pure_forall {φ : α → Prop} : (∀ x, (⌜φ x⌝ : SPred σs)) ⊣⊢ₛ ⌜∀ x, φ x⌝ := by
+  refine bientails.iff.mpr ⟨?_, pure_forall_2⟩
+  if h : ∃ x, ¬φ x
+  then let ⟨x, h⟩ := h
+       exact (forall_elim x).trans (pure_mono h.elim)
+  else exact pure_intro fun x => Classical.not_not.1 <| mt (⟨x, ·⟩) h
+
+theorem pure_exists {φ : α → Prop} : (∃ x, ⌜φ x⌝ : SPred σs) ⊣⊢ₛ ⌜∃ x, φ x⌝ := bientails.iff.mpr ⟨exists_elim fun a => pure_mono (⟨a, ·⟩), pure_elim' fun ⟨x, h⟩ => (pure_intro h).trans (exists_intro' x .rfl)⟩
+
+@[simp] theorem true_intro_simp : (Q ⊢ₛ ⌜True⌝) ↔ True := iff_true_intro SPred.true_intro
+@[simp] theorem true_intro_simp_nil {Q : SPred []} : (Q ⊢ₛ True) ↔ True := SPred.true_intro_simp
+
+/-! # Miscellaneous -/
+
+theorem and_left_comm : P ∧ Q ∧ R ⊣⊢ₛ Q ∧ P ∧ R := and_assoc.symm.trans <| (and_congr_l and_comm).trans and_assoc
+theorem and_right_comm : (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q := and_assoc.trans <| (and_congr_r and_comm).trans and_assoc.symm
+
+/-! # Working with entailment -/
+
+theorem entails_pure_intro {σs : List Type} (P Q : Prop) (h : P → Q) : SPred.entails ⌜P⌝ (σs := σs) ⌜Q⌝ := pure_elim' fun hp => pure_intro (h hp)
+
+@[simp] theorem entails_elim_nil (P Q : SPred []) : SPred.entails P Q ↔ P → Q := iff_of_eq rfl
+theorem entails_elim_cons {σ : Type} {σs : List Type} (P Q : SPred (σ::σs)) : P ⊢ₛ Q ↔ ∀ s, (P s ⊢ₛ Q s) := by simp only [entails]
+@[simp] theorem entails_pure_elim_cons {σ : Type} {σs : List Type} [Inhabited σ] (P Q : Prop) : SPred.entails ⌜P⌝ (σs := σ::σs) ⌜Q⌝ ↔ SPred.entails ⌜P⌝ (σs := σs) ⌜Q⌝:= by simp [entails]
+@[simp] theorem entails_true_intro {σs : List Type} (P Q : SPred σs) : ⊢ₛ P → Q ↔ P ⊢ₛ Q := Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h))
--- a/src/Std/Do/SPred/Laws.lean
+++ b/src/Std/Do/SPred/Laws.lean
@ -0,0 +1,130 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König, Mario Carneiro, Sebastian Graf
+-/
+prelude
+import Std.Do.SPred.Notation
+
+namespace Std.Do.SPred
+
+/-!
+# Laws of `SPred`
+
+This module contains lemmas about `SPred` that need to be proved by induction on σs.
+That is, they need to proved by appealing to the model of `SPred` and cannot
+be derived without doing so.
+
+`Std.Do.SPred.DerivedLaws` has some more laws that are derivative of what follows.
+-/
+
+/-! # Entailment -/
+
+@[refl,simp]
+theorem entails.refl {σs : List Type} (P : SPred σs) : P ⊢ₛ P := by
+  match σs with
+  | [] => simp [entails]
+  | σ :: _ => intro s; exact entails.refl (P s)
+
+theorem entails.trans {σs : List Type} {P Q R : SPred σs} : (P ⊢ₛ Q) → (Q ⊢ₛ R) → (P ⊢ₛ R) := by
+  match σs with
+  | [] => intro h₁ h₂; exact h₂ ∘ h₁
+  | σ :: _ => intro h₁ h₂; intro s; exact entails.trans (h₁ s) (h₂ s)
+
+instance {σs : List Type} : Trans (@entails σs) entails entails where
+  trans := entails.trans
+
+/-! # Bientailment -/
+
+theorem bientails.iff {σs : List Type} {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P) := by
+  induction σs with
+  | nil => exact Iff.intro (fun h => ⟨h.mp, h.mpr⟩) (fun h => ⟨h.1, h.2⟩)
+  | cons σ σs ih =>
+  apply Iff.intro
+  · exact fun h => ⟨fun s => (ih.mp (h s)).1, fun s => (ih.mp (h s)).2⟩
+  · intro h s; exact ih.mpr ⟨h.1 s, h.2 s⟩
+
+@[refl,simp]
+theorem bientails.refl {σs : List Type} (P : SPred σs) : P ⊣⊢ₛ P := by
+  induction σs <;> simp [bientails, *]
+
+theorem bientails.trans {σs : List Type} {P Q R : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → (P ⊣⊢ₛ R) := by
+  induction σs
+  case nil => simp +contextual only [bientails, implies_true]
+  case cons σ σs ih => intro hpq hqr s; exact ih (hpq s) (hqr s)
+
+instance {σs : List Type} : Trans (@bientails σs) bientails bientails where
+  trans := bientails.trans
+
+theorem bientails.symm {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ P) := by
+  induction σs
+  case nil => exact Iff.symm
+  case cons σ σs ih => intro h s; exact ih (h s)
+
+theorem bientails.to_eq {σs : List Type} {P Q : SPred σs} (h : P ⊣⊢ₛ Q) : P = Q := by
+  induction σs
+  case nil => rw[iff_iff_eq.mp h]
+  case cons σ σs ih =>
+    ext s; rw[ih (h s)]
+
+/-! # Pure -/
+
+theorem pure_intro {σs : List Type} {φ : Prop} {P : SPred σs} : φ → P ⊢ₛ ⌜φ⌝ := by
+  induction σs <;> simp_all [entails]
+
+theorem pure_elim' {σs : List Type} {φ : Prop} {P : SPred σs} : (φ → ⌜True⌝ ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P := by
+  induction σs <;> simp_all [entails]
+
+-- Ideally, we'd like to prove the following theorem:
+-- theorem pure_elim' {σs : List Type} {φ : Prop} : SPred.entails (σs:=σs) ⌜True⌝ ⌜φ⌝ → φ
+-- Unfortunately, this is only true if all `σs` are Inhabited.
+
+/-! # Conjunction -/
+
+theorem and_intro {σs : List Type} {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R := by
+  induction σs <;> simp_all [entails]
+
+theorem and_elim_l {P Q : SPred σs} : P ∧ Q ⊢ₛ P := by
+  induction σs <;> simp_all [entails]
+
+theorem and_elim_r {P Q : SPred σs} : P ∧ Q ⊢ₛ Q := by
+  induction σs <;> simp_all [entails]
+
+/-! # Disjunction -/
+
+theorem or_intro_l {σs : List Type} {P Q : SPred σs} : P ⊢ₛ P ∨ Q := by
+  induction σs <;> simp_all [entails]
+
+theorem or_intro_r {σs : List Type} {P Q : SPred σs} : Q ⊢ₛ P ∨ Q := by
+  induction σs <;> simp_all [entails]
+
+theorem or_elim {σs : List Type} {P Q R : SPred σs} (h1 : P ⊢ₛ R) (h2 : Q ⊢ₛ R) : P ∨ Q ⊢ₛ R := by
+  induction σs
+  case nil => exact (Or.elim · h1 h2)
+  case cons => simp_all [entails]
+
+/-! # Implication -/
+
+theorem imp_intro {σs : List Type} {P Q R : SPred σs} (h : P ∧ Q ⊢ₛ R) : P ⊢ₛ Q → R := by
+  induction σs <;> simp_all [entails]
+
+theorem imp_elim {σs : List Type} {P Q R : SPred σs} (h : P ⊢ₛ Q → R) : P ∧ Q ⊢ₛ R := by
+  induction σs <;> simp_all [entails]
+
+/-! # Quantifiers -/
+
+theorem forall_intro {σs : List Type} {P : SPred σs} {Ψ : α → SPred σs} (h : ∀ a, P ⊢ₛ Ψ a) : P ⊢ₛ ∀ a, Ψ a := by
+  induction σs <;> simp_all [entails]
+
+theorem forall_elim {σs : List Type} {Ψ : α → SPred σs} (a : α) : (∀ a, Ψ a) ⊢ₛ Ψ a := by
+  induction σs <;> simp_all [entails]
+
+theorem exists_intro {σs : List Type} {Ψ : α → SPred σs} (a : α) : Ψ a ⊢ₛ ∃ a, Ψ a := by
+  induction σs
+  case nil => intro _; exists a
+  case cons σ σs ih => intro s; exact @ih (fun a => Ψ a s)
+
+theorem exists_elim {σs : List Type} {Φ : α → SPred σs} {Q : SPred σs} (h : ∀ a, Φ a ⊢ₛ Q) : (∃ a, Φ a) ⊢ₛ Q := by
+  induction σs
+  case nil => intro ⟨a, ha⟩; exact h a ha
+  case cons σ σs ih => intro s; exact ih (fun a => h a s)
--- a/src/Std/Do/SPred/Notation.lean
+++ b/src/Std/Do/SPred/Notation.lean
@ -0,0 +1,175 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Lars König, Sebastian Graf
+-/
+prelude
+import Std.Do.SPred.SPred
+
+namespace Std.Do.SPred.Notation
+
+open Lean Macro Parser PrettyPrinter
+
+-- define `spred` embedding in `term`.
+-- An explicit `spred` marker avoids exponential blowup in terms
+-- that do not opt into the extended syntax.
+syntax:max "spred(" term ")" : term
+syntax:max "term(" term ")" : term
+
+-- allow fallback to `term`
+macro_rules
+  | `(spred(term($t))) => pure t
+  | `(spred($t))       => pure t
+
+-- push `spred` inside some `term` constructs
+macro_rules
+  | `(spred(($P)))                  => ``((spred($P)))
+  | `(spred(fun $xs* => $b))        => ``(fun $xs* => spred($b))
+  | `(spred(if $c then $t else $e)) => ``(if $c then spred($t) else spred($e))
+  | `(spred(($P : $t)))             => ``((spred($P) : $t))
+
+/-- Remove an `spred` layer from a `term` syntax object. -/
+-- inverts the rules above.
+partial def unpack [Monad m] [MonadRef m] [MonadQuotation m] : Term → m Term
+  | `(spred($P))             => do `($P)
+  | `(($P))                  => do `(($(← unpack P)))
+  | `(if $c then $t else $e) => do
+    let t ← unpack t
+    let e ← unpack e
+    `(if $c then $t else $e)
+  | `(fun $xs* => $b)        => do
+    let b ← unpack b
+    `(fun $xs* => $b)
+  | `(($P : $t))             => do ``(($(← unpack P) : $t))
+  | `($t)                    => `($t)
+
+/-! # Idiom notation -/
+
+/-- Embedding of pure Lean values into `SVal`. -/
+syntax "⌜" term "⌝" : term
+/-- ‹t› in `SVal` idiom notation. Accesses the state of type `t`. -/
+syntax "‹" term "›ₛ" : term
+/--
+  Use getter `t : SVal σs σ` in `SVal` idiom notation; sugar for `SVal.uncurry t (by assumption)`.
+-/
+syntax:max "#" term:max : term
+
+/-! # Sugar for `SPred` -/
+
+/-- Entailment in `SPred`; sugar for `SPred.entails`. -/
+syntax:25 term:26 " ⊢ₛ " term:25 : term
+/-- Tautology in `SPred`; sugar for `SPred.entails ⌜True⌝`. -/
+syntax:25 "⊢ₛ " term:25 : term
+/-- Bi-entailment in `SPred`; sugar for `SPred.bientails`. -/
+syntax:25 term:25 " ⊣⊢ₛ " term:25 : term
+
+macro_rules
+  | `(⌜$t⌝) => ``(SVal.curry (fun tuple => $t))
+  | `(#$t) => `(SVal.uncurry $t (by assumption))
+  | `(‹$t›ₛ) => `(#(SVal.getThe $t))
+  | `($P ⊢ₛ $Q) => ``(SPred.entails spred($P) spred($Q))
+  | `(spred($P ∧ $Q)) => ``(SPred.and spred($P) spred($Q))
+  | `(spred($P ∨ $Q)) => ``(SPred.or spred($P) spred($Q))
+  | `(spred(¬ $P)) => ``(SPred.not spred($P))
+  | `(spred($P → $Q)) => ``(SPred.imp spred($P) spred($Q))
+  | `(spred($P ↔ $Q)) => ``(SPred.iff spred($P) spred($Q))
+  | `(spred(∃ $xs:explicitBinders, $P)) => do expandExplicitBinders ``SPred.exists xs (← `(spred($P)))
+  | `(⊢ₛ $P) => ``(SPred.entails ⌜True⌝ spred($P))
+  | `($P ⊣⊢ₛ $Q) => ``(SPred.bientails spred($P) spred($Q))
+  -- Sadly, ∀ does not resently use expandExplicitBinders...
+  | `(spred(∀ _%$tk, $P)) => ``(SPred.forall (fun _%$tk => spred($P)))
+  | `(spred(∀ _%$tk : $ty, $P)) => ``(SPred.forall (fun _%$tk : $ty => spred($P)))
+  | `(spred(∀ (_%$tk $xs* : $ty), $P)) => ``(SPred.forall (fun _%$tk : $ty => spred(∀ ($xs* : $ty), $P)))
+  | `(spred(∀ $x:ident, $P)) => ``(SPred.forall (fun $x => spred($P)))
+  | `(spred(∀ ($x:ident : $ty), $P)) => ``(SPred.forall (fun $x : $ty => spred($P)))
+  | `(spred(∀ ($x:ident $xs* : $ty), $P)) => ``(SPred.forall (fun $x : $ty => spred(∀ ($xs* : $ty), $P)))
+  | `(spred(∀ $x:ident $xs*, $P)) => ``(SPred.forall (fun $x => spred(∀ $xs*, $P)))
+  | `(spred(∀ ($x:ident : $ty) $xs*, $P)) => ``(SPred.forall (fun $x : $ty => spred(∀ $xs*, $P)))
+  | `(spred(∀ ($x:ident $xs* : $ty) $ys*, $P)) => ``(SPred.forall (fun $x : $ty => spred(∀ ($xs* : $ty) $ys*, $P)))
+
+@[app_unexpander SVal.curry]
+private def unexpandCurry : Unexpander
+  | `($_ $t $ts*) => do
+    match t with
+    | `(fun $_ => $e) => if ts.isEmpty then ``(⌜$e⌝) else ``(⌜$e⌝ $ts*)
+    | _ => throw ()
+  | _ => throw ()
+
+@[app_unexpander SVal.uncurry]
+private def unexpandUncurry : Unexpander
+  | `($_ $f $ts*) => do
+    match f with
+    | `(SVal.getThe $t) => if ts.isEmpty then ``(‹$t›ₛ) else ``(‹$t›ₛ $ts*)
+    | `($t) => if ts.isEmpty then ``(#$t) else ``(#$t $ts*)
+  | _ => throw ()
+
+@[app_unexpander SPred.entails]
+private def unexpandEntails : Unexpander
+  | `($_ $P $Q)  => do
+    let P ← unpack P; let Q ← unpack Q;
+    match P with
+    | `(⌜True⌝) => ``(⊢ₛ $Q)
+    | _ => ``($P ⊢ₛ $Q)
+  | _ => throw ()
+
+@[app_unexpander SPred.bientails]
+private def unexpandBientails : Unexpander
+  | `($_ $P $Q)  => do
+    let P ← unpack P; let Q ← unpack Q;
+    ``($P ⊣⊢ₛ $Q)
+  | _ => throw ()
+
+@[app_unexpander SPred.and]
+private def unexpandAnd : Unexpander
+  | `($_ $P $Q) => do
+    let P ← unpack P; let Q ← unpack Q;
+    ``(spred($P ∧ $Q))
+  | _ => throw ()
+
+@[app_unexpander SPred.or]
+private def unexpandOr : Unexpander
+  | `($_ $P $Q) => do
+    let P ← unpack P; let Q ← unpack Q;
+    ``(spred($P ∨ $Q))
+  | _ => throw ()
+
+@[app_unexpander SPred.not]
+private def unexpandNot : Unexpander
+  | `($_ $P) => do
+    let P ← unpack P;
+    ``(spred(¬ $P))
+  | _ => throw ()
+
+@[app_unexpander SPred.imp]
+private def unexpandImp : Unexpander
+  | `($_ $P $Q) => do
+    let P ← unpack P; let Q ← unpack Q;
+    ``(spred($P → $Q))
+  | _ => throw ()
+
+@[app_unexpander SPred.forall]
+private def unexpandForall : Unexpander
+  | `($_ fun $x:ident => ∀ $y:ident $[$z:ident]*, $Ψ) => do
+    let Ψ ← unpack Ψ
+    ``(spred(∀ $x:ident $y:ident $[$z:ident]*, $Ψ))
+  | `($_ fun $x:ident => $Ψ) => do
+    let Ψ ← unpack Ψ
+    ``(spred(∀ $x:ident, $Ψ))
+  | _ => throw ()
+
+@[app_unexpander SPred.exists]
+private def unexpandExists : Unexpander
+  | `($_ fun $x:ident => ∃ $y:ident $[$z:ident]*, $Ψ) => do
+    let Ψ ← unpack Ψ
+    ``(spred(∃ $x:ident $y:ident $[$z:ident]*, $Ψ))
+  | `($_ fun $x:ident => $Ψ) => do
+    let Ψ ← unpack Ψ
+    ``(spred(∃ $x:ident, $Ψ))
+  | _ => throw ()
+
+@[app_unexpander SPred.iff]
+private def unexpandIff : Unexpander
+  | `($_ $P $Q) => do
+    let P ← unpack P; let Q ← unpack Q;
+    ``(spred($P ↔ $Q))
+  | _ => throw ()
--- a/src/Std/Do/SPred/SPred.lean
+++ b/src/Std/Do/SPred/SPred.lean
@ -0,0 +1,109 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Init.Ext
+import Std.Do.SPred.SVal
+
+/-!
+# State-indexed predicates
+
+This module provides a type `SPred σs` of predicates indexed by a list of states.
+This type forms the basis for the notion of assertion in `Std.Do`; see `Std.Do.Assertion`.
+-/
+
+namespace Std.Do
+
+/--
+  A predicate indexed by a list of states.
+  ```
+  example : SPred [Nat, Bool] = (Nat → Bool → Prop) := rfl
+  ```
+-/
+abbrev SPred (σs : List Type) : Type := SVal σs Prop
+
+namespace SPred
+
+/-- A pure proposition `P : Prop` embedded into `SPred`. For internal use in this module only; prefer to use idiom bracket notation `⌜P⌝. -/
+private abbrev pure {σs : List Type} (P : Prop) : SPred σs := SVal.curry (fun _ => P)
+
+@[ext]
+theorem ext {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funext
+
+/-- Entailment in `SPred`. -/
+def entails {σs : List Type} (P Q : SPred σs) : Prop := match σs with
+| [] => P → Q
+| σ :: _ => ∀ (s : σ), entails (P s) (Q s)
+@[simp] theorem entails_nil {P Q : SPred []} : entails P Q = (P → Q) := rfl
+theorem entails_cons {σs : List Type} {P Q : SPred (σ::σs)} : entails P Q = (∀ s, entails (P s) (Q s)) := rfl
+theorem entails_cons_intro {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, entails (P s) (Q s)) → entails P Q := by simp only [entails, imp_self]
+
+-- Reducibility of entails must be semi-reducible so that entails_refl is useful for rfl
+
+/-- Equivalence relation on `SPred`. Convert to `Eq` via `bientails.to_eq`. -/
+def bientails {σs : List Type} (P Q : SPred σs) : Prop := match σs with
+| [] => P ↔ Q
+| σ :: _ => ∀ (s : σ), bientails (P s) (Q s)
+@[simp] theorem bientails_nil {P Q : SPred []} : bientails P Q = (P ↔ Q) := rfl
+theorem bientails_cons {σs : List Type} {P Q : SPred (σ::σs)} : bientails P Q = (∀ s, bientails (P s) (Q s)) := rfl
+theorem bientails_cons_intro {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, bientails (P s) (Q s)) → bientails P Q := by simp only [bientails, imp_self]
+
+/-- Conjunction in `SPred`. -/
+def and {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with
+| [] => P ∧ Q
+| σ :: _ => fun (s : σ) => and (P s) (Q s)
+@[simp] theorem and_nil {P Q : SPred []} : and P Q = (P ∧ Q) := rfl
+@[simp] theorem and_cons {σs : List Type} {P Q : SPred (σ::σs)} : and P Q s = and (P s) (Q s) := rfl
+
+/-- Disjunction in `SPred`. -/
+def or {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with
+| [] => P ∨ Q
+| σ :: _ => fun (s : σ) => or (P s) (Q s)
+@[simp] theorem or_nil {P Q : SPred []} : or P Q = (P ∨ Q) := rfl
+@[simp] theorem or_cons {σs : List Type} {P Q : SPred (σ::σs)} : or P Q s = or (P s) (Q s) := rfl
+
+/-- Negation in `SPred`. -/
+def not {σs : List Type} (P : SPred σs) : SPred σs := match σs with
+| [] => ¬ P
+| σ :: _ => fun (s : σ) => not (P s)
+@[simp] theorem not_nil {P : SPred []} : not P = (¬ P) := rfl
+@[simp] theorem not_cons {σs : List Type} {P : SPred (σ::σs)} : not P s = not (P s) := rfl
+
+/-- Implication in `SPred`. -/
+def imp {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with
+| [] => P → Q
+| σ :: _ => fun (s : σ) => imp (P s) (Q s)
+@[simp] theorem imp_nil {P Q : SPred []} : imp P Q = (P → Q) := rfl
+@[simp] theorem imp_cons {σs : List Type} {P Q : SPred (σ::σs)} : imp P Q s = imp (P s) (Q s) := rfl
+
+/-- Biconditional in `SPred`. -/
+def iff {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with
+| [] => P ↔ Q
+| σ :: _ => fun (s : σ) => iff (P s) (Q s)
+@[simp] theorem iff_nil {P Q : SPred []} : iff P Q = (P ↔ Q) := rfl
+@[simp] theorem iff_cons {σs : List Type} {P Q : SPred (σ::σs)} : iff P Q s = iff (P s) (Q s) := rfl
+
+/-- Existential quantifier in `SPred`. -/
+def «exists» {α} {σs : List Type} (P : α → SPred σs) : SPred σs := match σs with
+| [] => ∃ a, P a
+| σ :: _ => fun (s : σ) => «exists» (fun a => P a s)
+@[simp] theorem exists_nil {α} {P : α → SPred []} : «exists» P = (∃ a, P a) := rfl
+@[simp] theorem exists_cons {σs : List Type} {α} {P : α → SPred (σ::σs)} : «exists» P s = «exists» (fun a => P a s) := rfl
+
+/-- Universal quantifier in `SPred`. -/
+def «forall» {α} {σs : List Type} (P : α → SPred σs) : SPred σs := match σs with
+| [] => ∀ a, P a
+| σ :: _ => fun (s : σ) => «forall» (fun a => P a s)
+@[simp] theorem forall_nil {α} {P : α → SPred []} : «forall» P = (∀ a, P a) := rfl
+@[simp] theorem forall_cons {σs : List Type} {α} {P : α → SPred (σ::σs)} : «forall» P s = «forall» (fun a => P a s) := rfl
+
+/-- Conjunction of a list of `SPred`. -/
+def conjunction {σs : List Type} (env : List (SPred σs)) : SPred σs := match env with
+| [] => pure True
+| P::env => P.and (conjunction env)
+@[simp] theorem conjunction_nil {σs : List Type} : conjunction ([] : List (SPred σs)) = pure True := rfl
+@[simp] theorem conjunction_cons {σs : List Type} {P : SPred σs} {env : List (SPred σs)} : conjunction (P::env) = P.and (conjunction env) := rfl
+@[simp] theorem conjunction_apply {σs : List Type} {env : List (SPred (σ::σs))} : conjunction env s = conjunction (env.map (· s)) := by
+  induction env <;> simp [conjunction, *]
--- a/src/Std/Do/SPred/SVal.lean
+++ b/src/Std/Do/SPred/SVal.lean
@ -0,0 +1,75 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Init.Data.List.Notation
+
+/-! # State-indexed values -/
+
+namespace Std.Do
+
+/--
+  A value indexed by a curried tuple of states.
+  ```
+  example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl
+  ```
+-/
+abbrev SVal (σs : List Type) (α : Type) := match σs with
+| [] => α
+| σ :: σs => σ → SVal σs α
+/- Note about the reducibility of SVal:
+We need SVal to be reducible, otherwise type inference fails for `Triple`.
+(Begs for investigation.)
+-/
+
+namespace SVal
+
+/-- A tuple capturing the whole state of an `SVal`. -/
+def StateTuple (σs : List Type) := match σs with
+| [] => Unit
+| σ :: σs => σ × StateTuple σs
+
+instance : Inhabited (StateTuple []) where
+  default := ()
+
+instance [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ :: σs)) where
+  default := (default, default)
+
+/-- Curry a function taking a `StateTuple` into an `SVal`. -/
+def curry {σs : List Type} (f : StateTuple σs → α) : SVal σs α := match σs with
+| [] => f ()
+| _ :: _ => fun s => curry (fun s' => f (s, s'))
+@[simp] theorem curry_nil {f : StateTuple [] → α} : curry f = f () := rfl
+@[simp] theorem curry_cons {σ : Type} {σs : List Type} {f : StateTuple (σ::σs) → α} {s : σ} : curry f s = curry (fun s' => f (s, s')) := rfl
+
+/-- Uncurry an `SVal` into a function taking a `StateTuple`. -/
+def uncurry {σs : List Type} (f : SVal σs α) : StateTuple σs → α := match σs with
+| [] => fun _ => f
+| _ :: _ => fun (s, t) => uncurry (f s) t
+@[simp] theorem uncurry_nil {σ : Type} {s : σ} : uncurry (σs:=[]) s = fun _ => s := rfl
+@[simp] theorem uncurry_cons {σ : Type} {σs : List Type} {f : SVal (σ::σs) α} {s : σ} {t : StateTuple σs} : uncurry f (s, t) = uncurry (f s) t := rfl
+
+@[simp] theorem uncurry_curry {σs : List Type} {f : StateTuple σs → α} : uncurry (σs:=σs) (curry f) = f := by induction σs <;> (simp[uncurry, curry, *]; rfl)
+@[simp] theorem curry_uncurry {σs : List Type} {f : SVal σs α} : curry (σs:=σs) (uncurry f) = f := by induction σs <;> simp[uncurry, curry, *]
+
+/-- Embed a pure value into an `SVal`. -/
+abbrev pure {σs : List Type} (a : α) : SVal σs α := curry (fun _ => a)
+
+instance [Inhabited α] : Inhabited (SVal σs α) where
+  default := pure default
+
+class GetTy (σ : Type) (σs : List Type) where
+  get : SVal σs σ
+
+instance : GetTy σ (σ :: σs) where
+  get := fun s => pure s
+
+instance [GetTy σ₁ σs] : GetTy σ₁ (σ₂ :: σs) where
+  get := fun _ => GetTy.get
+
+/-- Get the top-most state of type `σ` from an `SVal`. -/
+def getThe {σs : List Type} (σ : Type) [GetTy σ σs] : SVal σs σ := GetTy.get
+@[simp] theorem getThe_here {σs : List Type} (σ : Type) (s : σ) : getThe (σs := σ::σs) σ s = pure s := rfl
+@[simp] theorem getThe_there {σs : List Type} [GetTy σ σs] (σ' : Type) (s : σ') : getThe (σs := σ'::σs) σ s = getThe (σs := σs) σ := rfl
--- a/src/Std/Tactic.lean
+++ b/src/Std/Tactic.lean
@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Std.Tactic.BVDecide
+import Std.Tactic.Do

 /-!
 This directory is mainly used for bootstrapping reasons. Suppose a tactic generates a proof term
--- a/src/Std/Tactic/Do.lean
+++ b/src/Std/Tactic/Do.lean
@ -0,0 +1,13 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Std.Tactic.Do.Syntax
+
+/-!
+This directory contains the syntax definition for tactics related to the proof mode of `Std.Do.SPred`.
+Their builtin implementation lives in `Lean.Elab.Tactic.Do` to enable using the tactics without
+importing `Lean`.
+-/
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@ -0,0 +1,154 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean.Parser.Tactic
+
+@[inherit_doc Lean.Parser.Tactic.massumptionMacro]
+syntax (name := massumption) "massumption" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mclearMacro]
+syntax (name := mclear) "mclear" colGt ident : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mconstructorMacro]
+syntax (name := mconstructor) "mconstructor" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mexactMacro]
+syntax (name := mexact) "mexact" colGt term : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mexfalsoMacro]
+syntax (name := mexfalso) "mexfalso" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mexistsMacro]
+syntax (name := mexists) "mexists" term,+ : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mframeMacro]
+syntax (name := mframe) "mframe" : tactic
+
+/-- Duplicate a stateful `Std.Do.SPred` hypothesis. -/
+syntax (name := mdup) "mdup" ident " => " ident : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mhaveMacro]
+syntax (name := mhave) "mhave" ident optional(":" term) " := " term : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mreplaceMacro]
+syntax (name := mreplace) "mreplace" ident optional(":" term) " := " term : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mrightMacro]
+syntax (name := mright) "mright" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mleftMacro]
+syntax (name := mleft) "mleft" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mpureMacro]
+syntax (name := mpure) "mpure" colGt ident : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mpureIntroMacro]
+syntax (name := mpureIntro) "mpure_intro" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mrevertMacro]
+syntax (name := mrevert) "mrevert" colGt ident : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mspecializeMacro]
+syntax (name := mspecialize) "mspecialize" ident (colGt term:max)* : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mspecializePureMacro]
+syntax (name := mspecializePure) "mspecialize_pure" term (colGt term:max)* " => " ident : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mstartMacro]
+syntax (name := mstart) "mstart" : tactic
+
+@[inherit_doc Lean.Parser.Tactic.mstopMacro]
+syntax (name := mstop) "mstop" : tactic
+
+declare_syntax_cat mcasesPat
+syntax mcasesPatAlts := sepBy1(mcasesPat, " | ")
+syntax binderIdent : mcasesPat
+syntax "-" : mcasesPat
+syntax "⟨" mcasesPatAlts,* "⟩" : mcasesPat
+syntax "(" mcasesPatAlts ")" : mcasesPat
+syntax "⌜" binderIdent "⌝" : mcasesPat
+syntax "□" binderIdent : mcasesPat
+
+macro "%" h:binderIdent : mcasesPat => `(mcasesPat| ⌜$h⌝)
+macro "#" h:binderIdent : mcasesPat => `(mcasesPat| □ $h)
+
+inductive MCasesPat
+  | one (name : TSyntax ``binderIdent)
+  | clear
+  | tuple (args : List MCasesPat)
+  | alts (args : List MCasesPat)
+  | pure       (h : TSyntax ``binderIdent)
+  | stateful (h : TSyntax ``binderIdent)
+  deriving Repr, Inhabited
+
+partial def MCasesPat.parse (pat : TSyntax `mcasesPat) : MacroM MCasesPat := do
+  match go ⟨← expandMacros pat⟩ with
+  | none => Macro.throwUnsupported
+  | some pat => return pat
+where
+  go : TSyntax `mcasesPat → Option MCasesPat
+  | `(mcasesPat| $name:binderIdent) => some <| .one name
+  | `(mcasesPat| -) => some <| .clear
+  | `(mcasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.tuple ·.toList)
+  | `(mcasesPat| ⌜$h⌝) => some (.pure h)
+  | `(mcasesPat| □$h) => some (.stateful h)
+  | `(mcasesPat| ($pat)) => goAlts pat
+  | _ => none
+  goAlts : TSyntax ``mcasesPatAlts → Option MCasesPat
+  | `(mcasesPatAlts| $args|*) =>
+    match args.getElems with
+    | #[arg] => go arg
+    | args   => args.mapM go |>.map (.alts ·.toList)
+  | _ => none
+
+@[inherit_doc Lean.Parser.Tactic.mcasesMacro]
+syntax (name := mcases) "mcases" ident " with " mcasesPat : tactic
+
+declare_syntax_cat mrefinePat
+syntax binderIdent : mrefinePat
+syntax mrefinePats := sepBy1(mrefinePat, ", ")
+syntax "⟨" mrefinePats "⟩" : mrefinePat
+syntax "(" mrefinePat ")" : mrefinePat
+syntax "⌜" term "⌝" : mrefinePat
+syntax "□" binderIdent : mrefinePat
+syntax "?" binderIdent : mrefinePat
+
+macro "%" h:term : mrefinePat => `(mrefinePat| ⌜$h⌝)
+macro "#" h:binderIdent : mrefinePat => `(mrefinePat| □ $h)
+
+inductive MRefinePat
+  | one (name : TSyntax ``binderIdent)
+  | tuple (args : List MRefinePat)
+  | pure       (h : TSyntax `term)
+  | stateful (h : TSyntax ``binderIdent)
+  | hole (name : TSyntax ``binderIdent)
+  deriving Repr, Inhabited
+
+partial def MRefinePat.parse (pat : TSyntax `mrefinePat) : MacroM MRefinePat := do
+  match go ⟨← expandMacros pat⟩ with
+  | none => Macro.throwUnsupported
+  | some pat => return pat
+where
+  go : TSyntax `mrefinePat → Option MRefinePat
+  | `(mrefinePat| $name:binderIdent) => some <| .one name
+  | `(mrefinePat| ?$name) => some (.hole name)
+  | `(mrefinePat| ⟨$[$args],*⟩) => args.mapM go |>.map (.tuple ·.toList)
+  | `(mrefinePat| ⌜$h⌝) => some (.pure h)
+  | `(mrefinePat| □$h) => some (.stateful h)
+  | `(mrefinePat| ($pat)) => go pat
+  | _ => none
+
+@[inherit_doc Lean.Parser.Tactic.mrefineMacro]
+syntax (name := mrefine) "mrefine" mrefinePat : tactic
+
+declare_syntax_cat mintroPat
+syntax mcasesPat : mintroPat
+syntax "∀" binderIdent : mintroPat
+
+@[inherit_doc Lean.Parser.Tactic.mintroMacro]
+syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic
--- a/tests/lean/run/spredProofMode.lean
+++ b/tests/lean/run/spredProofMode.lean
@ -0,0 +1,298 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+import Lean.Elab.Tactic.Do
+import Std.Do
+
+open Std.Do
+
+variable (σs : List Type)
+
+theorem start_stop (Q : SPred σs) (H : Q ⊢ₛ Q) : Q ⊢ₛ Q := by
+  mstart
+  mintro HQ
+  mstop
+  exact H
+
+theorem exact (Q : SPred σs) : Q ⊢ₛ Q := by
+  mstart
+  mintro HQ
+  mexact HQ
+
+theorem exact_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by
+  mintro _
+  mexact hP
+
+theorem clear (P Q : SPred σs) : P ⊢ₛ Q → Q := by
+  mintro HP
+  mintro HQ
+  mclear HP
+  mexact HQ
+
+theorem assumption (P Q : SPred σs) : Q ⊢ₛ P → Q := by
+  mintro _ _
+  massumption
+
+theorem assumption_pure (P Q : SPred σs) (hP : ⊢ₛ P): Q ⊢ₛ P := by
+  mintro _
+  massumption
+
+namespace pure
+
+theorem move (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
+  mintro Hφ
+  mpure Hφ
+  mexact (ψ Hφ)
+
+theorem move_multiple (Q : SPred σs) : ⌜φ₁⌝ ⊢ₛ ⌜φ₂⌝ → Q → Q := by
+  mintro Hφ1
+  mintro Hφ2
+  mintro HQ
+  mpure Hφ1
+  mpure Hφ2
+  mexact HQ
+
+theorem move_conjunction (Q : SPred σs) : (⌜φ₁⌝ ∧ ⌜φ₂⌝) ⊢ₛ Q → Q := by
+  mintro Hφ
+  mintro HQ
+  mpure Hφ
+  mexact HQ
+
+end pure
+
+namespace pureintro
+
+theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
+  mpure_intro
+  exact True.intro
+
+theorem or : ⊢ₛ ⌜True⌝ ∨ (⌜False⌝ : SPred σs) := by
+  mpure_intro
+  left
+  exact True.intro
+
+theorem with_proof (H : A → B) (P Q : SPred σs) : P ⊢ₛ Q → ⌜A⌝ → ⌜B⌝ := by
+  mintro _HP _HQ
+  mpure_intro
+  exact H
+
+end pureintro
+
+namespace frame
+
+theorem move (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
+  mintro _
+  mframe
+  mcases h with hP
+  mexact h
+
+theorem move_multiple (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
+  mintro h
+  mcases h with ⟨hp, hQ, hq, rest⟩
+  mframe
+  mexact hQ
+
+end frame
+
+theorem revert (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ R := by
+  mintro ⟨HP, HQ, HR⟩
+  mrevert HR
+  mrevert HP
+  mintro HP'
+  mintro HR'
+  mexact HR'
+
+namespace constructor
+
+theorem and (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
+  mintro HQ
+  mconstructor <;> mexact HQ
+
+end constructor
+
+theorem exfalso (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
+  mintro HP
+  mexfalso
+  mexact HP
+
+namespace leftright
+
+theorem left (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
+  mintro HP
+  mleft
+  mexact HP
+
+theorem right (P Q : SPred σs) : Q ⊢ₛ P ∨ Q := by
+  mintro HQ
+  mright
+  mexact HQ
+
+theorem complex (P Q R : SPred σs) : ⊢ₛ P → Q → P ∧ (R ∨ Q ∨ R) := by
+  mintro HP HQ
+  mconstructor
+  · massumption
+  mright
+  mleft
+  mexact HQ
+
+end leftright
+
+namespace specialize
+
+theorem simple (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mspecialize HPQ HP
+  mexact HPQ
+
+theorem multiple (P Q R : SPred σs) : ⊢ₛ P → Q → (P → Q → R) → R := by
+  mintro HP HQ HPQR
+  mspecialize HPQR HP HQ
+  mexact HPQR
+
+theorem pure_imp (P Q R : SPred σs) : (⊢ₛ P) → ⊢ₛ Q → (P → Q → R) → R := by
+  intro HP
+  mintro HQ HPQR
+  mspecialize HPQR HP HQ
+  mexact HPQR
+
+theorem forall' (y : Nat) (Q : Nat → SPred σs) : ⊢ₛ (∀ x, Q x) → Q (y + 1) := by
+  mintro HQ
+  mspecialize HQ (y + 1)
+  mexact HQ
+
+theorem mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
+  mintro HQ HΨ
+  mspecialize HΨ (y + 1) hP HQ
+  mexact HΨ
+
+theorem pure_mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
+  mintro HQ
+  mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
+  mexact HΨ
+
+theorem pure_with_local (P : SPred σs) (hc : c) : (⌜c⌝ → P) ⊢ₛ P := by
+  mintro HP
+  mspecialize HP hc
+  mexact HP
+
+end specialize
+
+namespace havereplace
+
+theorem mrepl (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
+  mexact HPQ
+
+theorem mhave (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
+  mintro HP HPQ
+  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
+  mhave HQ := by mspecialize HPQ HP; mexact HPQ
+  mexact HQ
+
+theorem mixed (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
+  mintro HQ HΨ
+  mhave H := by mspecialize HΨ (y + 1) hP HQ; mexact HΨ
+  mexact H
+
+end havereplace
+
+namespace cases
+
+theorem rename (P : SPred σs) : P ⊢ₛ P := by
+  mintro HP
+  mcases HP with HP'
+  mexact HP'
+
+theorem clear (P Q : SPred σs) : ⊢ₛ P → Q → P := by
+  mintro HP HQ
+  mcases HQ with -
+  mexact HP
+
+theorem pure (P : SPred σs) (Q : Prop) : φ → (⊢ₛ P → ⌜Q⌝ → P) := by
+  intro hφ
+  mintro HP HQ
+  mcases HQ with ⌜hQ⌝
+  mexact HP
+
+theorem pure_exact (P : SPred σs) (Q : Prop) (hqr : Q → ⊢ₛ R) : ⊢ₛ P → ⌜Q⌝ → R := by
+  mintro HP HQ
+  mcases HQ with ⌜hQ⌝
+  mexact hqr hQ
+
+theorem and (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ R := by
+  mintro HPQR
+  mcases HPQR with ⟨HP, HQ, HR⟩
+  mexact HR
+
+theorem and_clear_pure (P Q R : SPred σs) (φ : Prop) : (P ∧ Q ∧ ⌜φ⌝ ∧ R) ⊢ₛ R := by
+  mintro HPQR
+  mcases HPQR with ⟨_, -, ⌜hφ⌝, HR⟩
+  mexact HR
+
+theorem or (P Q R : SPred σs) : P ∧ (Q ∨ R) ∧ (Q → R) ⊢ₛ R := by
+  mintro H
+  mcases H with ⟨-, ⟨HQ | HR⟩, HQR⟩
+  · mspecialize HQR HQ
+    mexact HQR
+  · mexact HR
+
+theorem and_persistent (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ R := by
+  mintro HPQR
+  mcases HPQR with ⟨#HP, HQ, □HR⟩
+  mexact HR
+
+theorem and_pure (P Q R : Prop) : (⌜P⌝ ∧ ⌜Q⌝ ∧ ⌜R⌝) ⊢ₛ (⌜R⌝ : SPred σs) := by
+  mintro HPQR
+  mcases HPQR with ⟨%HP, ⌜HQ⌝, HR⟩
+  mpure_intro
+  exact HR
+
+end cases
+
+namespace introforall
+
+theorem beta_conj (P Q R : SPred (Nat::σs)) (H : ∀ n, P n ∧ Q n ⊢ₛ R n) : P ∧ Q ⊢ₛ R := by
+  mintro ⟨HP, HQ⟩ ∀s
+  mstop
+  exact H s
+
+end introforall
+
+namespace refine
+
+theorem and (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
+  mintro ⟨HP, HQ, HR⟩
+  mrefine ⟨HP, HR⟩
+
+theorem exists_1 (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
+  mintro H
+  mrefine ⟨⌜42⌝, H⟩
+
+theorem exists_2 (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
+  mintro H
+  mexists 42
+
+end refine
+
+theorem mosel1 {α : Type} (P : SPred σs) (Φ Ψ : α → SPred σs) :
+  P ∧ (∃ a, Φ a ∨ Ψ a) ⊢ₛ ∃ a, (P ∧ Φ a) ∨ (P ∧ Ψ a) := by
+  mintro ⟨HP, ⟨a, ⟨HΦ | HΨ⟩⟩⟩
+  · mexists a
+    mleft
+    mrefine ⟨HP, HΦ⟩
+  · mexists a
+    mright
+    mrefine ⟨HP, HΨ⟩
+
+theorem mosel3 {α : Type} (P : SPred σs) (Φ Ψ : α → SPred σs) :
+  P ∧ (∃ a, Φ a ∨ Ψ a) ⊢ₛ ∃ a, Φ a ∨ (P ∧ P ∧ Ψ a) := by
+  mintro ⟨HP, ⟨a, ⟨HΦ | HΨ⟩⟩⟩
+  · mexists a
+    mleft
+    mexact HΦ
+  · mexists a
+    mright
+    mrefine ⟨HP, HP, HΨ⟩