Lean 语言参考

17.5. 校样模式🔗

有状态目标可以使用特殊的证明模式来证明，其中目标通过两个假设上下文来呈现：普通的 Lean 上下文，其中包含 Lean 变量，以及特殊的有状态上下文，其中包含有关单子状态的假设。在证明模式下，目标是SPred，而不是Prop，整个目标相当于从假设的合取到结论的蕴涵关系（SPred.entails）。

syntaxProof Mode Goals

证明模式目标呈现为一系列命名假设，每行一个，后跟 Std.Tactic.Do.mgoalStx⊢ₛ 和一个目标。

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

在证明模式下，特殊的策略操纵有状态上下文。这些策略在策略参考中其自己的部分中进行了描述。

当使用具体的 monad 时，mvcgen 通常不会产生有状态的证明目标——它们被简化了。然而，单子多态定理可以导致有状态的目标保留。

Stateful Proofs

函数 bump 将其状态增加指定的量并返回结果值。

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

bump 的规范引理以有意的低级方式进行证明，以演示中间证明状态：

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! 🐙

引理也可以仅使用简化器来证明：

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 ↪