17.4. 为 Monad 启用 `mvcgen`🔗

如果 monad 是根据 Lean 标准库提供的 monad 转换器实现的，例如 ExceptT 和 StateT，那么它不需要额外的实例。其他 monad 将需要 WP、LawfulMonad 和 WPMonad 的实例。策略旨在支持对具有可能被中断状态的单线程控制进行建模的 monad；换句话说，就是普通命令式编程中存在的效果。更多奇特效应尚未得到研究。

提供基本实例后，下一步就是证明充分性引理。这个引理应该表明，运行单子计算和断言所需谓词的最弱前提条件实际上足以证明该谓词。

除了 monad 的定义之外，典型的库还提供一组原始运算符。其中每一个都应提供规范引理。将状态内部设为私有并导出一组精心设计的断言运算符可能也很有用。

理想情况下，库的原始运算符的规范引理应该是作为谓词转换器的运算符的精确规范。虽然通常更容易思考运算符如何将输入状态转换为输出状态，但当后置条件完全自由时，验证条件生成将更可靠地工作。这允许自动化使用下一个语句的精确前提条件来实例化后置条件，而不需要显示蕴涵。换句话说，将前置条件指定为后置条件的函数的规范在实践中比仅关联前置条件和后置条件的规范效果更好。

Schematic Postconditions

函数 double 将自然数状态加倍：

def double : StateM Nat Unit := do
  modify (2 * ·)

按时间顺序思考，一个合理的规范是输出状态的值是输入状态的两倍。这是使用代表初始状态的示意图变量来表达的：

theorem double_spec :
    ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := byn:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ double ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄
  simp [double]n:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ modify fun x => 2 * x ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄
  mvcgen with grindAll goals completed! 🐙

然而，当 double 用于其他函数时，示意性地处理后置条件的等效规范将导致更小的验证条件：

@[spec]
theorem better_double_spec {Q : PostCond Unit (.arg Nat .pure)} :
    ⦃ fun s => Q.1 () (2 * s) ⦄ double ⦃ Q ⦄ := byQ:PostCond Unit (PostShape.arg Nat PostShape.pure)⊢ ⦃fun s => Q.fst () (2 * s)⦄ double ⦃Q⦄
  simp [double]Q:PostCond Unit (PostShape.arg Nat PostShape.pure)⊢ ⦃fun s => Q.fst () (2 * s)⦄ modify fun x => 2 * x ⦃Q⦄
  mvcgen with grindAll goals completed! 🐙

后置条件的第一个投影是它的状态断言。现在，前置条件仅规定后置条件应保持初始状态的两倍。

Live ↪

A Logging Monad

monad LogM 在计算期间维护一个仅附加日志：

structure LogM (β : Type u) (α : Type v) : Type (max u v) where
  log : Array β
  value : α

instance : Monad (LogM β) where
  pure x := ⟨#[], x⟩
  bind x f :=
    let { log, value } := f x.value
    { log := x.log ++ log, value }

它还有一个 LawfulMonad 实例。

可以使用 log 写入日志，并且可以使用 LogM.run 计算值和关联的日志。

def log (v : β) : LogM β Unit := { log := #[v], value := () }

def LogM.run (x : LogM β α) : α × Array β := (x.value, x.log)

WP 实例使用 PredTrans.pushArg，而不是从头开始编写。该运算符旨在对状态单子进行建模，但 LogM 可以被视为只能附加到状态的状态单子。此附加在实例的主体中可见，其中附加了初始状态和操作产生的日志：

instance : WP (LogM β) (.arg (Array β) .pure) where
  wp
    | { log, value } =>
      PredTrans.pushArg (fun s => PredTrans.pure (value, s ++ log))

WPMonad 实例也受益于作为状态单子的概念模型，并允许非常简短的证明：

instance : WPMonad (LogM β) (.arg (Array β) .pure) where
  wp_pure x := byα:Type ?u.5σ:List (Type u)ps:PostShapex✝:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20x:α✝⊢ wp (pure x) = pure x
    extα:Type ?u.5σ:List (Type u)ps:PostShapex✝:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20x:α✝Q✝:PostCond α✝ (PostShape.arg (Array β) PostShape.pure)s✝:Array β⊢ (wp⟦pure x⟧ Q✝ s✝).down ↔ ((pure x).apply Q✝ s✝).down
    simp [wp, pure]All goals completed! 🐙

  wp_bind _ _ := byα:Type ?u.5σ:List (Type u)ps:PostShapex:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20β✝:Type ?u.20x✝¹:LogM β α✝x✝:α✝ → LogM β β✝⊢ (wp do
    let a ← x✝¹
    x✝ a) =
  do
  let a ← wp x✝¹
  wp (x✝ a)
    extα:Type ?u.5σ:List (Type u)ps:PostShapex:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20β✝:Type ?u.20x✝¹:LogM β α✝x✝:α✝ → LogM β β✝Q✝:PostCond β✝ (PostShape.arg (Array β) PostShape.pure)s✝:Array β⊢ (wp⟦do
        let a ← x✝¹
        x✝ a⟧
      Q✝ s✝).down ↔
  ((do
          let a ← wp x✝¹
          wp (x✝ a)).apply
      Q✝ s✝).down
    simp [wp, bind]All goals completed! 🐙

充分性引理有一个重要细节：最弱前提条件变换的结果应用于空数组。这是必要的，因为日志记录计算已被建模为仅附加状态，因此必须有一些初始状态。从语义上讲，空数组是正确的选择，以便不将不是来自程序的项目放入日志中；从技术上讲，它还必须是一个可以与数组上的追加运算符进行交换的值。

theorem LogM.of_wp_run_eq {x : α × Array β} {prog : LogM β α}
    (h : LogM.run prog = x) (P : α × Array β → Prop) :
    (⊢ₛ wp⟦prog⟧ (⇓ v l => ⌜P (v, l)⌝) #[]) → P x := byα:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P x
  rw [← hα:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P prog.run]α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P prog.run
  intro h'α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Proph':⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]⊢ P prog.run
  simp [wp] at h'α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Proph':P (prog.value, prog.log)⊢ P prog.run
  exact h'All goals completed! 🐙

接下来，应该为库中的每个运算符提供一个规范引理。只有一个：log。对于新的单子，这些证明必须经常打破 Hoare 三元组的抽象边界和最弱的前提条件；然后，图书馆的客户可以抽象地使用它们提供的规范。

theorem log_spec {x : β} :
    ⦃ fun s => ⌜s = s'⌝ ⦄ log x ⦃ ⇓ () s => ⌜s = s'.push x⌝ ⦄ := byβ:Types':Array βx:β⊢ ⦃fun s => ⌜s = s'⌝⦄ log x ⦃PostCond.noThrow fun x_1 s => ⌜s = s'.push x⌝⦄
  simp [log, Triple, wp]All goals completed! 🐙

log 的更好规范使用示意性后置条件：

variable {Q : PostCond Unit (.arg (Array β) .pure)}

@[spec]
theorem log_spec_better {x : β} :
    ⦃ fun s => Q.1 () (s.push x) ⦄ log x ⦃ Q ⦄ := byβ:TypeQ:PostCond Unit (PostShape.arg (Array β) PostShape.pure)x:β⊢ ⦃fun s => Q.fst () (s.push x)⦄ log x ⦃Q⦄
  simp [log, Triple, wp]All goals completed! 🐙

将所有自然数记录到某个界限的函数 logUntil 将始终生成长度等于其参数的日志：

def logUntil (n : Nat) : LogM Nat Unit := do
  for i in 0...n do
    log i

theorem logUntil_length : (logUntil n).run.2.size = n := byn:Nat⊢ (logUntil n).run.snd.size = n
  generalize h : (logUntil n).run = xn:Natx:Unit × Array Nath:(logUntil n).run = x⊢ x.snd.size = n
  unfold logUntil at hn:Natx:Unit × Array Nath:(do
      forIn (0...n) PUnit.unit fun i r => do
          log i
          pure (ForInStep.yield PUnit.unit)
      pure PUnit.unit).run =
  x⊢ x.snd.size = n
  apply LogM.of_wp_run_eq hn:Natx:Unit × Array Nath:(do
      forIn (0...n) PUnit.unit fun i r => do
          log i
          pure (ForInStep.yield PUnit.unit)
      pure PUnit.unit).run =
  x⊢ ⊢ₛ
  wp⟦do
      forIn (0...n) PUnit.unit fun i r => do
          log i
          pure (ForInStep.yield PUnit.unit)
      pure PUnit.unit⟧
    (PostCond.noThrow fun v l => ⌜(v, l).snd.size = n⌝) #[]
  mvcgen invariants
  · ⇓⟨xs, _⟩ s => ⌜xs.pos = s.size⌝
  with
    simp_all [List.Cursor.pos]All goals completed! 🐙 <;>
    grind [Std.PRange.Nat.size_rco, Std.Rco.length_toList]

Live ↪

17.4. 为 Monad 启用 mvcgen🔗

17.4. 为 Monad 启用 `mvcgen`🔗