Lean 语言参考手册

17.5. 证明模式🔗

有状态目标可使用特殊的证明模式来证明；在该模式下，目标显示两个假设上下文：普通 Lean 上下文包含 Lean 变量，特殊的有状态上下文包含关于单子状态的假设。在证明模式中，目标是 SPred 而非 Prop，且整个目标等价于从所有假设之合取到结论的蕴涵关系（SPred.entails）。

语法证明模式目标

证明模式目标显示为一系列具名假设，每行一个，随后是 Std.Tactic.Do.mgoalStx⊢ₛ 和一个目标。

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

在证明模式中，特殊策略用于操作有状态上下文。这些策略在策略参考的专门一节中介绍。

处理具体单子时，mvcgen 通常不会留下有状态证明目标——它们会被化简掉。然而，关于任意单子的多态定理可能会留下有状态目标。

有状态证明

函数 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, s + i)
    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! 🐙

在线查看 ↪