The Lean Language Reference

18.5. Proof Mode🔗

Stateful goals can be proven using a special proof mode in which goals are rendered with two contexts of hypotheses: the ordinary Lean context, which contains Lean variables, and a special stateful context, which contains assumptions about the monadic state. In the proof mode, the goal is an SPred, rather than a Prop, and the entire goal is equivalent to an entailment relation (SPred.entails) from the conjunction of the hypotheses to the conclusion.

syntaxProof Mode Goals

Proof mode goals are rendered as a series of named hypotheses, one per line, followed by Std.Tactic.Do.mgoalStx⊢ₛ and a goal.

mgoalStx ::= ...
    | (ident : term)*
      ⊢ₛ term

In the proof mode, special tactics manipulate the stateful context. These tactics are described in their own section in the tactic reference.

When working with concrete monads, mvcgen typically does not result in stateful proof goals—they are simplified away. However, monad-polymorphic theorems can lead to stateful goals remaining.

Stateful Proofs

The function bump increments its state by the indicated amount and returns the resulting value.

variable [Monad m] [WPMonad m ps]
def bump (n : Nat) : StateT Nat m Nat := do
  modifyThe Nat (· + n)
  getThe Nat

This specification lemma for bump is proved in an intentionally low-level manner to demonstrate the intermediate proof states:

theorem bump_correct :
      ⦃ fun n => ⌜n = k⌝ ⦄
      bump (m := m) i
      ⦃ ⇓ r n => ⌜r = n ∧ n = k + i⌝ ⦄ := bym:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ ⦃fun n => ⌜n = k⌝⦄ bump i ⦃PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝⦄
  mintro n_eq_km:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ 
n_eq_k : fun n => ⌜n = k⌝
⊢ₛ wp⟦bump i⟧ (PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝)
  unfold bumpm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ 
n_eq_k : fun n => ⌜n = k⌝
⊢ₛ
wp⟦do
    modifyThe Nat fun x => x + i
    getThe Nat⟧
  (PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝)
  unfold modifyThem:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ 
n_eq_k : fun n => ⌜n = k⌝
⊢ₛ
wp⟦do
    MonadStateOf.modifyGet fun s => (PUnit.unit, (fun x => x + i) s)
    getThe Nat⟧
  (PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝)
  mspecm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ 
n_eq_k : fun n => ⌜n = k⌝
⊢ₛ fun s => wp⟦getThe Nat⟧ (PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝) (s + i)
  mspecm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nats✝:Nath✝:s✝ = k⊢ 
⊢ₛ ⌜True ∧ s✝ + i = k + i⌝
  mpure_introm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nats✝:Nath✝:s✝ = k⊢ True ∧ s✝ + i = k + i
  constructorleftm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nats✝:Nath✝:s✝ = k⊢ Truerightm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nats✝:Nath✝:s✝ = k⊢ s✝ + i = k + i
  .leftm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nats✝:Nath✝:s✝ = k⊢ True trivialAll goals completed! 🐙
  .rightm:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nats✝:Nath✝:s✝ = k⊢ s✝ + i = k + i simp_allAll goals completed! 🐙

The lemma can also be proved using only the simplifier:

theorem bump_correct' :
    ⦃ fun n => ⌜n = k⌝ ⦄
    bump (m := m) i
    ⦃ ⇓ r n => ⌜r = n ∧ n = k + i⌝ ⦄ := bym:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ ⦃fun n => ⌜n = k⌝⦄ bump i ⦃PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝⦄
  mintro _m:Type → Type u_1ps:PostShapeinst✝¹:Monad minst✝:WPMonad m psi:Natk:Nat⊢ 
h✝ : fun n => ⌜n = k⌝
⊢ₛ wp⟦bump i⟧ (PostCond.noThrow fun r n => ⌜r = n ∧ n = k + i⌝)
  simp_all [bump]All goals completed! 🐙

Live ↪